Log files for model cluster.128-2000-20 and tool configuration prism_from-prism_check_ex
[3580.063, 3536.355, 3099.817, 3630.536, 3119.676]
Log file: prism_from-prism_check_ex_cluster.128-2000-20_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 3580.063 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:03:19 GMT+02:00 2026
Hostname: n23m0038.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4961276/tmpsrp5ush0prism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4961276/tmpsrp5ush0prism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4961276/tmpsrp5ush0prism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/model.prism"...
Type: CTMC
Modules: Left Right Repairman Line ToLeft ToRight
Actions: [] [startLeft] [repairLeft] [startRight] [repairRight] [startToLeft] [startToRight] [startLine] [repairToLeft] [repairToRight] [repairLine]
Variables: left_n left right_n right r line line_n toleft toleft_n toright toright_n
Labels: "minimum"
Parsing properties file "/w0/tmp/slurm_tq429871.4961276/tmpsrp5ush0prism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/property.props"...
1 property:
(1) "qos1": P=? [ F<=2000 !"minimum" ]
---------------------------------------------------------------------
Model checking: "qos1": P=? [ F<=2000 !"minimum" ]
Building model (engine:explicit)...
Computing reachable states... 582683 597012 states
Reachable states exploration and model construction done in 3.057 secs.
Sorting reachable states list...
Time for model construction: 3.374 seconds.
Type: CTMC
States: 597012 (1 initial)
Transitions: 2908192
Starting backwards transient probability computation...
Uniformisation: q.t = 41.318415 x 2000.0 = 82636.83
Fox-Glynn (1.25E-7): left = 80621, right = 85077
Backwards transient probability computation took 85078 iters and 3575.81 seconds.
Value in the initial state: 0.0010724025337697357
Time for model checking: 3575.877 seconds.
Result: 0.0010724025337697357
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_cluster.128-2000-20_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 3536.355 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:05:31 GMT+02:00 2026
Hostname: n23m0255.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4964732/tmpa76w5tcvprism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4964732/tmpa76w5tcvprism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4964732/tmpa76w5tcvprism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/model.prism"...
Type: CTMC
Modules: Left Right Repairman Line ToLeft ToRight
Actions: [] [startLeft] [repairLeft] [startRight] [repairRight] [startToLeft] [startToRight] [startLine] [repairToLeft] [repairToRight] [repairLine]
Variables: left_n left right_n right r line line_n toleft toleft_n toright toright_n
Labels: "minimum"
Parsing properties file "/w0/tmp/slurm_tq429871.4964732/tmpa76w5tcvprism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/property.props"...
1 property:
(1) "qos1": P=? [ F<=2000 !"minimum" ]
---------------------------------------------------------------------
Model checking: "qos1": P=? [ F<=2000 !"minimum" ]
Building model (engine:explicit)...
Computing reachable states... 597012 states
Reachable states exploration and model construction done in 2.868 secs.
Sorting reachable states list...
Time for model construction: 3.288 seconds.
Type: CTMC
States: 597012 (1 initial)
Transitions: 2908192
Starting backwards transient probability computation...
Uniformisation: q.t = 41.318415 x 2000.0 = 82636.83
Fox-Glynn (1.25E-7): left = 80621, right = 85077
Backwards transient probability computation took 85078 iters and 3532.359 seconds.
Value in the initial state: 0.0010724025337697357
Time for model checking: 3532.408 seconds.
Result: 0.0010724025337697357
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_cluster.128-2000-20_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 3099.817 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:59:20 GMT+02:00 2026
Hostname: n23m0276.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4967306/tmpf7rj4d8wprism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4967306/tmpf7rj4d8wprism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4967306/tmpf7rj4d8wprism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/model.prism"...
Type: CTMC
Modules: Left Right Repairman Line ToLeft ToRight
Actions: [] [startLeft] [repairLeft] [startRight] [repairRight] [startToLeft] [startToRight] [startLine] [repairToLeft] [repairToRight] [repairLine]
Variables: left_n left right_n right r line line_n toleft toleft_n toright toright_n
Labels: "minimum"
Parsing properties file "/w0/tmp/slurm_tq429871.4967306/tmpf7rj4d8wprism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/property.props"...
1 property:
(1) "qos1": P=? [ F<=2000 !"minimum" ]
---------------------------------------------------------------------
Model checking: "qos1": P=? [ F<=2000 !"minimum" ]
Building model (engine:explicit)...
Computing reachable states... 597012 states
Reachable states exploration and model construction done in 2.761 secs.
Sorting reachable states list...
Time for model construction: 3.116 seconds.
Type: CTMC
States: 597012 (1 initial)
Transitions: 2908192
Starting backwards transient probability computation...
Uniformisation: q.t = 41.318415 x 2000.0 = 82636.83
Fox-Glynn (1.25E-7): left = 80621, right = 85077
Backwards transient probability computation took 85078 iters and 3095.918 seconds.
Value in the initial state: 0.0010724025337697357
Time for model checking: 3096.098 seconds.
Result: 0.0010724025337697357
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_cluster.128-2000-20_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 3630.536 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:51:16 GMT+02:00 2026
Hostname: n23m0301.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4966939/tmpd6qjkbulprism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4966939/tmpd6qjkbulprism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4966939/tmpd6qjkbulprism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/model.prism"...
Type: CTMC
Modules: Left Right Repairman Line ToLeft ToRight
Actions: [] [startLeft] [repairLeft] [startRight] [repairRight] [startToLeft] [startToRight] [startLine] [repairToLeft] [repairToRight] [repairLine]
Variables: left_n left right_n right r line line_n toleft toleft_n toright toright_n
Labels: "minimum"
Parsing properties file "/w0/tmp/slurm_tq429871.4966939/tmpd6qjkbulprism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/property.props"...
1 property:
(1) "qos1": P=? [ F<=2000 !"minimum" ]
---------------------------------------------------------------------
Model checking: "qos1": P=? [ F<=2000 !"minimum" ]
Building model (engine:explicit)...
Computing reachable states... 597012 states
Reachable states exploration and model construction done in 2.99 secs.
Sorting reachable states list...
Time for model construction: 3.421 seconds.
Type: CTMC
States: 597012 (1 initial)
Transitions: 2908192
Starting backwards transient probability computation...
Uniformisation: q.t = 41.318415 x 2000.0 = 82636.83
Fox-Glynn (1.25E-7): left = 80621, right = 85077
Backwards transient probability computation took 85078 iters and 3626.38 seconds.
Value in the initial state: 0.0010724025337697357
Time for model checking: 3626.429 seconds.
Result: 0.0010724025337697357
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_cluster.128-2000-20_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 3119.676 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 08:52:36 GMT+02:00 2026
Hostname: n23m0110.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4964119/tmpjjx_2h92prism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4964119/tmpjjx_2h92prism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4964119/tmpjjx_2h92prism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/model.prism"...
Type: CTMC
Modules: Left Right Repairman Line ToLeft ToRight
Actions: [] [startLeft] [repairLeft] [startRight] [repairRight] [startToLeft] [startToRight] [startLine] [repairToLeft] [repairToRight] [repairLine]
Variables: left_n left right_n right r line line_n toleft toleft_n toright toright_n
Labels: "minimum"
Parsing properties file "/w0/tmp/slurm_tq429871.4964119/tmpjjx_2h92prism_from-prism_check_ex_cluster.128-2000-20_tmp_indir_/property.props"...
1 property:
(1) "qos1": P=? [ F<=2000 !"minimum" ]
---------------------------------------------------------------------
Model checking: "qos1": P=? [ F<=2000 !"minimum" ]
Building model (engine:explicit)...
Computing reachable states... 597012 states
Reachable states exploration and model construction done in 2.557 secs.
Sorting reachable states list...
Time for model construction: 2.969 seconds.
Type: CTMC
States: 597012 (1 initial)
Transitions: 2908192
Starting backwards transient probability computation...
Uniformisation: q.t = 41.318415 x 2000.0 = 82636.83
Fox-Glynn (1.25E-7): left = 80621, right = 85077
Backwards transient probability computation took 85078 iters and 3116.04 seconds.
Value in the initial state: 0.0010724025337697357
Time for model checking: 3116.082 seconds.
Result: 0.0010724025337697357
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g