Log files for model bluetooth.1 and tool configuration prism_from-prism_check_ex
Log file: prism_from-prism_check_ex_bluetooth.1_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 17.158 seconds
Return code: -9
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:32:04 GMT+02:00 2026
Hostname: n23m0047.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4962482/tmp0n7_l9c5prism_from-prism_check_ex_bluetooth.1_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4962482/tmp0n7_l9c5prism_from-prism_check_ex_bluetooth.1_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4962482/tmp0n7_l9c5prism_from-prism_check_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"
Parsing properties file "/w0/tmp/slurm_tq429871.4962482/tmp0n7_l9c5prism_from-prism_check_ex_bluetooth.1_tmp_indir_/property.props"...
1 property:
(1) "time": filter(max, R=? [ F "target" ], "init")
---------------------------------------------------------------------
Model checking: "time": filter(max, R=? [ F "target" ], "init")
Building model (engine:explicit)...
Computing reachable states...
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_bluetooth.1_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 16.090 seconds
Return code: -9
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 08:58:09 GMT+02:00 2026
Hostname: n23m0254.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4964325/tmp1mh4hsy0prism_from-prism_check_ex_bluetooth.1_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4964325/tmp1mh4hsy0prism_from-prism_check_ex_bluetooth.1_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4964325/tmp1mh4hsy0prism_from-prism_check_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"
Parsing properties file "/w0/tmp/slurm_tq429871.4964325/tmp1mh4hsy0prism_from-prism_check_ex_bluetooth.1_tmp_indir_/property.props"...
1 property:
(1) "time": filter(max, R=? [ F "target" ], "init")
---------------------------------------------------------------------
Model checking: "time": filter(max, R=? [ F "target" ], "init")
Building model (engine:explicit)...
Computing reachable states...
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_bluetooth.1_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 16.193 seconds
Return code: -9
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:20:49 GMT+02:00 2026
Hostname: n23m0107.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4961996/tmpbruww134prism_from-prism_check_ex_bluetooth.1_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4961996/tmpbruww134prism_from-prism_check_ex_bluetooth.1_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4961996/tmpbruww134prism_from-prism_check_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"
Parsing properties file "/w0/tmp/slurm_tq429871.4961996/tmpbruww134prism_from-prism_check_ex_bluetooth.1_tmp_indir_/property.props"...
1 property:
(1) "time": filter(max, R=? [ F "target" ], "init")
---------------------------------------------------------------------
Model checking: "time": filter(max, R=? [ F "target" ], "init")
Building model (engine:explicit)...
Computing reachable states...
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_bluetooth.1_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 14.870 seconds
Return code: -9
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:53:59 GMT+02:00 2026
Hostname: r23m0204.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4967076/tmps50woubnprism_from-prism_check_ex_bluetooth.1_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4967076/tmps50woubnprism_from-prism_check_ex_bluetooth.1_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4967076/tmps50woubnprism_from-prism_check_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"
Parsing properties file "/w0/tmp/slurm_tq429871.4967076/tmps50woubnprism_from-prism_check_ex_bluetooth.1_tmp_indir_/property.props"...
1 property:
(1) "time": filter(max, R=? [ F "target" ], "init")
---------------------------------------------------------------------
Model checking: "time": filter(max, R=? [ F "target" ], "init")
Building model (engine:explicit)...
Computing reachable states...
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_bluetooth.1_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 15.195 seconds
Return code: -9
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:36:28 GMT+02:00 2026
Hostname: n23m0135.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4966267/tmpx7r5gaa8prism_from-prism_check_ex_bluetooth.1_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4966267/tmpx7r5gaa8prism_from-prism_check_ex_bluetooth.1_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4966267/tmpx7r5gaa8prism_from-prism_check_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"
Parsing properties file "/w0/tmp/slurm_tq429871.4966267/tmpx7r5gaa8prism_from-prism_check_ex_bluetooth.1_tmp_indir_/property.props"...
1 property:
(1) "time": filter(max, R=? [ F "target" ], "init")
---------------------------------------------------------------------
Model checking: "time": filter(max, R=? [ F "target" ], "init")
Building model (engine:explicit)...
Computing reachable states...
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g