Log files for model cluster.64-2000-20 and tool configuration prism_from-umb_check_ex
[0.194, 0.182, 0.215, 0.211, 0.252]
Log file: prism_from-umb_check_ex_cluster.64-2000-20_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 594.965 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:56:40 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 -importmodel /w0/tmp/slurm_tq429871.4967212/tmp7mf91di7prism_from-umb_check_ex_cluster.64-2000-20_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4967212/tmp7mf91di7prism_from-umb_check_ex_cluster.64-2000-20_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: CTMC
Actions: [] [startLeft] [repairLeft] [startRight] [repairRight] [startToLeft] [startToRight] [startLine] [repairToLeft] [repairToRight] [repairLine]
Variables: x
Labels: "minimum"
Parsing properties file "/w0/tmp/slurm_tq429871.4967212/tmp7mf91di7prism_from-umb_check_ex_cluster.64-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)...
Time for model construction: 0.194 seconds.
Type: CTMC
States: 151060 (1 initial)
Transitions: 733216
Starting backwards transient probability computation...
Uniformisation: q.t = 41.057295 x 2000.0 = 82114.59000000001
Fox-Glynn (1.25E-7): left = 80105, right = 84548
Backwards transient probability computation took 84549 iters and 594.116 seconds.
Value in the initial state: 0.0010445396729789366
Time for model checking: 594.142 seconds.
Result: 0.0010445396729789366
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_cluster.64-2000-20_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 549.208 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:38:39 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 -importmodel /w0/tmp/slurm_tq429871.4962775/tmp_dulbzzjprism_from-umb_check_ex_cluster.64-2000-20_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4962775/tmp_dulbzzjprism_from-umb_check_ex_cluster.64-2000-20_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: CTMC
Actions: [] [startLeft] [repairLeft] [startRight] [repairRight] [startToLeft] [startToRight] [startLine] [repairToLeft] [repairToRight] [repairLine]
Variables: x
Labels: "minimum"
Parsing properties file "/w0/tmp/slurm_tq429871.4962775/tmp_dulbzzjprism_from-umb_check_ex_cluster.64-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)...
Time for model construction: 0.182 seconds.
Type: CTMC
States: 151060 (1 initial)
Transitions: 733216
Starting backwards transient probability computation...
Uniformisation: q.t = 41.057295 x 2000.0 = 82114.59000000001
Fox-Glynn (1.25E-7): left = 80105, right = 84548
Backwards transient probability computation took 84549 iters and 548.402 seconds.
Value in the initial state: 0.0010445396729789366
Time for model checking: 548.427 seconds.
Result: 0.0010445396729789366
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_cluster.64-2000-20_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 592.825 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 08:56:03 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.4964223/tmpyf77pb2tprism_from-umb_check_ex_cluster.64-2000-20_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4964223/tmpyf77pb2tprism_from-umb_check_ex_cluster.64-2000-20_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: CTMC
Actions: [] [startLeft] [repairLeft] [startRight] [repairRight] [startToLeft] [startToRight] [startLine] [repairToLeft] [repairToRight] [repairLine]
Variables: x
Labels: "minimum"
Parsing properties file "/w0/tmp/slurm_tq429871.4964223/tmpyf77pb2tprism_from-umb_check_ex_cluster.64-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)...
Time for model construction: 0.215 seconds.
Type: CTMC
States: 151060 (1 initial)
Transitions: 733216
Starting backwards transient probability computation...
Uniformisation: q.t = 41.057295 x 2000.0 = 82114.59000000001
Fox-Glynn (1.25E-7): left = 80105, right = 84548
Backwards transient probability computation took 84549 iters and 591.958 seconds.
Value in the initial state: 0.0010445396729789366
Time for model checking: 591.985 seconds.
Result: 0.0010445396729789366
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_cluster.64-2000-20_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 609.729 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:53:59 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 -importmodel /w0/tmp/slurm_tq429871.4967073/tmpsodbnjzaprism_from-umb_check_ex_cluster.64-2000-20_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4967073/tmpsodbnjzaprism_from-umb_check_ex_cluster.64-2000-20_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: CTMC
Actions: [] [startLeft] [repairLeft] [startRight] [repairRight] [startToLeft] [startToRight] [startLine] [repairToLeft] [repairToRight] [repairLine]
Variables: x
Labels: "minimum"
Parsing properties file "/w0/tmp/slurm_tq429871.4967073/tmpsodbnjzaprism_from-umb_check_ex_cluster.64-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)...
Time for model construction: 0.211 seconds.
Type: CTMC
States: 151060 (1 initial)
Transitions: 733216
Starting backwards transient probability computation...
Uniformisation: q.t = 41.057295 x 2000.0 = 82114.59000000001
Fox-Glynn (1.25E-7): left = 80105, right = 84548
Backwards transient probability computation took 84549 iters and 608.775 seconds.
Value in the initial state: 0.0010445396729789366
Time for model checking: 608.802 seconds.
Result: 0.0010445396729789366
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_cluster.64-2000-20_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 721.003 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:43:41 GMT+02:00 2026
Hostname: n23m0287.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4963007/tmplyzzgpseprism_from-umb_check_ex_cluster.64-2000-20_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4963007/tmplyzzgpseprism_from-umb_check_ex_cluster.64-2000-20_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: CTMC
Actions: [] [startLeft] [repairLeft] [startRight] [repairRight] [startToLeft] [startToRight] [startLine] [repairToLeft] [repairToRight] [repairLine]
Variables: x
Labels: "minimum"
Parsing properties file "/w0/tmp/slurm_tq429871.4963007/tmplyzzgpseprism_from-umb_check_ex_cluster.64-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)...
Time for model construction: 0.252 seconds.
Type: CTMC
States: 151060 (1 initial)
Transitions: 733216
Starting backwards transient probability computation...
Uniformisation: q.t = 41.057295 x 2000.0 = 82114.59000000001
Fox-Glynn (1.25E-7): left = 80105, right = 84548
Backwards transient probability computation took 84549 iters and 719.756 seconds.
Value in the initial state: 0.0010445396729789366
Time for model checking: 719.811 seconds.
Result: 0.0010445396729789366
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g