Log files for model majority.2100 and tool configuration prism_from-umb_check_ex
[0.247, 0.282, 0.246, 0.249, 0.24]
Log file: prism_from-umb_check_ex_majority.2100_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 439.833 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:07:07 GMT+02:00 2026
Hostname: r23m0202.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4964805/tmpscpazoh7prism_from-umb_check_ex_majority.2100_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4964805/tmpscpazoh7prism_from-umb_check_ex_majority.2100_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: CTMC
Actions: []
Variables: x
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4964805/tmpscpazoh7prism_from-umb_check_ex_majority.2100_tmp_indir_/property.props"...
1 property:
(1) "change_state": P=? [ F<=2100 "target" ]
---------------------------------------------------------------------
Model checking: "change_state": P=? [ F<=2100 "target" ]
Building model (engine:explicit)...
Time for model construction: 0.247 seconds.
Type: CTMC
States: 192000 (1 initial)
Transitions: 1961600
Starting backwards transient probability computation...
Uniformisation: q.t = 3.2872265951801265 x 2100.0 = 6903.175849878266
Fox-Glynn (1.25E-7): left = 6319, right = 7610
Backwards transient probability computation took 7611 iters and 438.836 seconds.
Value in the initial state: 0.054299193162504665
Time for model checking: 438.868 seconds.
Result: 0.054299193162504665
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_majority.2100_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 434.882 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 08:59:12 GMT+02:00 2026
Hostname: n23m0125.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4964382/tmpqxcxeb6gprism_from-umb_check_ex_majority.2100_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4964382/tmpqxcxeb6gprism_from-umb_check_ex_majority.2100_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: CTMC
Actions: []
Variables: x
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4964382/tmpqxcxeb6gprism_from-umb_check_ex_majority.2100_tmp_indir_/property.props"...
1 property:
(1) "change_state": P=? [ F<=2100 "target" ]
---------------------------------------------------------------------
Model checking: "change_state": P=? [ F<=2100 "target" ]
Building model (engine:explicit)...
Time for model construction: 0.282 seconds.
Type: CTMC
States: 192000 (1 initial)
Transitions: 1961600
Starting backwards transient probability computation...
Uniformisation: q.t = 3.2872265951801265 x 2100.0 = 6903.175849878266
Fox-Glynn (1.25E-7): left = 6319, right = 7610
Backwards transient probability computation took 7611 iters and 433.845 seconds.
Value in the initial state: 0.054299193162504665
Time for model checking: 433.865 seconds.
Result: 0.054299193162504665
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_majority.2100_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 439.334 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:14:26 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 -importmodel /w0/tmp/slurm_tq429871.4965119/tmpbwu5zd6fprism_from-umb_check_ex_majority.2100_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4965119/tmpbwu5zd6fprism_from-umb_check_ex_majority.2100_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: CTMC
Actions: []
Variables: x
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4965119/tmpbwu5zd6fprism_from-umb_check_ex_majority.2100_tmp_indir_/property.props"...
1 property:
(1) "change_state": P=? [ F<=2100 "target" ]
---------------------------------------------------------------------
Model checking: "change_state": P=? [ F<=2100 "target" ]
Building model (engine:explicit)...
Time for model construction: 0.246 seconds.
Type: CTMC
States: 192000 (1 initial)
Transitions: 1961600
Starting backwards transient probability computation...
Uniformisation: q.t = 3.2872265951801265 x 2100.0 = 6903.175849878266
Fox-Glynn (1.25E-7): left = 6319, right = 7610
Backwards transient probability computation took 7611 iters and 438.395 seconds.
Value in the initial state: 0.054299193162504665
Time for model checking: 438.416 seconds.
Result: 0.054299193162504665
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_majority.2100_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 441.246 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 06:58:26 GMT+02:00 2026
Hostname: n23m0046.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4961063/tmp803jfy1cprism_from-umb_check_ex_majority.2100_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4961063/tmp803jfy1cprism_from-umb_check_ex_majority.2100_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: CTMC
Actions: []
Variables: x
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4961063/tmp803jfy1cprism_from-umb_check_ex_majority.2100_tmp_indir_/property.props"...
1 property:
(1) "change_state": P=? [ F<=2100 "target" ]
---------------------------------------------------------------------
Model checking: "change_state": P=? [ F<=2100 "target" ]
Building model (engine:explicit)...
Time for model construction: 0.249 seconds.
Type: CTMC
States: 192000 (1 initial)
Transitions: 1961600
Starting backwards transient probability computation...
Uniformisation: q.t = 3.2872265951801265 x 2100.0 = 6903.175849878266
Fox-Glynn (1.25E-7): left = 6319, right = 7610
Backwards transient probability computation took 7611 iters and 440.192 seconds.
Value in the initial state: 0.054299193162504665
Time for model checking: 440.216 seconds.
Result: 0.054299193162504665
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_majority.2100_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 397.900 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:04:28 GMT+02:00 2026
Hostname: n23m0279.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4964684/tmpvcewn8fcprism_from-umb_check_ex_majority.2100_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4964684/tmpvcewn8fcprism_from-umb_check_ex_majority.2100_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: CTMC
Actions: []
Variables: x
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4964684/tmpvcewn8fcprism_from-umb_check_ex_majority.2100_tmp_indir_/property.props"...
1 property:
(1) "change_state": P=? [ F<=2100 "target" ]
---------------------------------------------------------------------
Model checking: "change_state": P=? [ F<=2100 "target" ]
Building model (engine:explicit)...
Time for model construction: 0.24 seconds.
Type: CTMC
States: 192000 (1 initial)
Transitions: 1961600
Starting backwards transient probability computation...
Uniformisation: q.t = 3.2872265951801265 x 2100.0 = 6903.175849878266
Fox-Glynn (1.25E-7): left = 6319, right = 7610
Backwards transient probability computation took 7611 iters and 397.034 seconds.
Value in the initial state: 0.054299193162504665
Time for model checking: 397.052 seconds.
Result: 0.054299193162504665
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g