Log files for model bluetooth.1 and tool configuration prism_from-prism_to-umb_ex

Parsed values
[MO, MO, MO, MO, MO]
Log file: prism_from-prism_to-umb_ex_bluetooth.1_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 16.723 seconds
Return code: -9
##############################
PRISM
=====

Version: 4.11
Date: Mon Oct 12 22:28:58 GMT+02:00 2026
Hostname: n23m0261.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4954908/tmpliakizkwprism_from-prism_to-umb_ex_bluetooth.1_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4954908/tmp8xnlos__prism_from-prism_to-umb_ex_bluetooth.1_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4954908/tmpliakizkwprism_from-prism_to-umb_ex_bluetooth.1_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     receiver1 frequency1 sender_frequency replies
Actions:     [] [time] [reply]
Variables:   y1 receiver freq1 train1 z1 f1 t1 send freq train c rep rec
Labels:      "target"
Rewards:     "time"

Building model (engine:explicit)...

Computing reachable states...
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

############################## Output files ##############################
model.umb:	File does not exist.
Log file: prism_from-prism_to-umb_ex_bluetooth.1_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 16.565 seconds
Return code: -9
##############################
PRISM
=====

Version: 4.11
Date: Mon Oct 12 23:08:51 GMT+02:00 2026
Hostname: n23m0071.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956524/tmpkug3c1f3prism_from-prism_to-umb_ex_bluetooth.1_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956524/tmp9l_rjtt4prism_from-prism_to-umb_ex_bluetooth.1_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956524/tmpkug3c1f3prism_from-prism_to-umb_ex_bluetooth.1_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     receiver1 frequency1 sender_frequency replies
Actions:     [] [time] [reply]
Variables:   y1 receiver freq1 train1 z1 f1 t1 send freq train c rep rec
Labels:      "target"
Rewards:     "time"

Building model (engine:explicit)...

Computing reachable states...
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

############################## Output files ##############################
model.umb:	File does not exist.
Log file: prism_from-prism_to-umb_ex_bluetooth.1_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 15.731 seconds
Return code: -9
##############################
PRISM
=====

Version: 4.11
Date: Mon Oct 12 23:28:39 GMT+02:00 2026
Hostname: n23m0303.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957320/tmpopbe6wpuprism_from-prism_to-umb_ex_bluetooth.1_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957320/tmpi0xxqp_eprism_from-prism_to-umb_ex_bluetooth.1_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957320/tmpopbe6wpuprism_from-prism_to-umb_ex_bluetooth.1_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     receiver1 frequency1 sender_frequency replies
Actions:     [] [time] [reply]
Variables:   y1 receiver freq1 train1 z1 f1 t1 send freq train c rep rec
Labels:      "target"
Rewards:     "time"

Building model (engine:explicit)...

Computing reachable states...
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

############################## Output files ##############################
model.umb:	File does not exist.
Log file: prism_from-prism_to-umb_ex_bluetooth.1_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 18.256 seconds
Return code: -9
##############################
PRISM
=====

Version: 4.11
Date: Mon Oct 12 22:47:16 GMT+02:00 2026
Hostname: n23m0269.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955657/tmpkn7k29khprism_from-prism_to-umb_ex_bluetooth.1_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955657/tmp4ewtla7oprism_from-prism_to-umb_ex_bluetooth.1_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955657/tmpkn7k29khprism_from-prism_to-umb_ex_bluetooth.1_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     receiver1 frequency1 sender_frequency replies
Actions:     [] [time] [reply]
Variables:   y1 receiver freq1 train1 z1 f1 t1 send freq train c rep rec
Labels:      "target"
Rewards:     "time"

Building model (engine:explicit)...

Computing reachable states...
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

############################## Output files ##############################
model.umb:	File does not exist.
Log file: prism_from-prism_to-umb_ex_bluetooth.1_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 18.247 seconds
Return code: -9
##############################
PRISM
=====

Version: 4.11
Date: Mon Oct 12 23:41:28 GMT+02:00 2026
Hostname: n23m0259.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957721/tmp89is13w_prism_from-prism_to-umb_ex_bluetooth.1_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957721/tmp6au6akymprism_from-prism_to-umb_ex_bluetooth.1_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957721/tmp89is13w_prism_from-prism_to-umb_ex_bluetooth.1_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     receiver1 frequency1 sender_frequency replies
Actions:     [] [time] [reply]
Variables:   y1 receiver freq1 train1 z1 f1 t1 send freq train c rep rec
Labels:      "target"
Rewards:     "time"

Building model (engine:explicit)...

Computing reachable states...
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

############################## Output files ##############################
model.umb:	File does not exist.