Log files for model speed-ind.2100 and tool configuration prism_from-umb_check_ex

Parsed values
[1646.358, 1647.363, 1468.509, 1567.909, 1510.944]
Log file: prism_from-umb_check_ex_speed-ind.2100_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 1646.358 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 07:08:17 GMT+02:00 2026
Hostname: n23m0054.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4961490/tmp1a_m0oxjprism_from-umb_check_ex_speed-ind.2100_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4961490/tmp1a_m0oxjprism_from-umb_check_ex_speed-ind.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.4961490/tmp1a_m0oxjprism_from-umb_check_ex_speed-ind.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.741 seconds.

Type:        CTMC
States:      743424 (1 initial)
Transitions: 9518080

Starting backwards transient probability computation...

Uniformisation: q.t = 2.7979107707826114 x 2100.0 = 5875.612618643484
Fox-Glynn (1.25E-7): left = 5336, right = 6527
Backwards transient probability computation took 6528 iters and 1644.094 seconds.

Value in the initial state: 0.04229449797846379

Time for model checking: 1644.145 seconds.

Result: 0.04229449797846379


##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_speed-ind.2100_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 1647.363 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 09:11:48 GMT+02:00 2026
Hostname: n23m0111.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4965001/tmpborffwljprism_from-umb_check_ex_speed-ind.2100_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4965001/tmpborffwljprism_from-umb_check_ex_speed-ind.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.4965001/tmpborffwljprism_from-umb_check_ex_speed-ind.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.782 seconds.

Type:        CTMC
States:      743424 (1 initial)
Transitions: 9518080

Starting backwards transient probability computation...

Uniformisation: q.t = 2.7979107707826114 x 2100.0 = 5875.612618643484
Fox-Glynn (1.25E-7): left = 5336, right = 6527
Backwards transient probability computation took 6528 iters and 1645.825 seconds.

Value in the initial state: 0.04229449797846379

Time for model checking: 1645.862 seconds.

Result: 0.04229449797846379


##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_speed-ind.2100_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 1468.509 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 08:59:43 GMT+02:00 2026
Hostname: n23m0248.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4964417/tmpetr613zfprism_from-umb_check_ex_speed-ind.2100_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4964417/tmpetr613zfprism_from-umb_check_ex_speed-ind.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.4964417/tmpetr613zfprism_from-umb_check_ex_speed-ind.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.631 seconds.

Type:        CTMC
States:      743424 (1 initial)
Transitions: 9518080

Starting backwards transient probability computation...

Uniformisation: q.t = 2.7979107707826114 x 2100.0 = 5875.612618643484
Fox-Glynn (1.25E-7): left = 5336, right = 6527
Backwards transient probability computation took 6528 iters and 1467.182 seconds.

Value in the initial state: 0.04229449797846379

Time for model checking: 1467.269 seconds.

Result: 0.04229449797846379


##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_speed-ind.2100_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 1567.909 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 09:53:59 GMT+02:00 2026
Hostname: r23m0214.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4967080/tmp6b53k87kprism_from-umb_check_ex_speed-ind.2100_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4967080/tmp6b53k87kprism_from-umb_check_ex_speed-ind.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.4967080/tmp6b53k87kprism_from-umb_check_ex_speed-ind.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.644 seconds.

Type:        CTMC
States:      743424 (1 initial)
Transitions: 9518080

Starting backwards transient probability computation...

Uniformisation: q.t = 2.7979107707826114 x 2100.0 = 5875.612618643484
Fox-Glynn (1.25E-7): left = 5336, right = 6527
Backwards transient probability computation took 6528 iters and 1566.586 seconds.

Value in the initial state: 0.04229449797846379

Time for model checking: 1566.626 seconds.

Result: 0.04229449797846379


##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_speed-ind.2100_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 1510.944 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 09:49:37 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.4966856/tmpg08kkzkpprism_from-umb_check_ex_speed-ind.2100_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4966856/tmpg08kkzkpprism_from-umb_check_ex_speed-ind.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.4966856/tmpg08kkzkpprism_from-umb_check_ex_speed-ind.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.653 seconds.

Type:        CTMC
States:      743424 (1 initial)
Transitions: 9518080

Starting backwards transient probability computation...

Uniformisation: q.t = 2.7979107707826114 x 2100.0 = 5875.612618643484
Fox-Glynn (1.25E-7): left = 5336, right = 6527
Backwards transient probability computation took 6528 iters and 1509.577 seconds.

Value in the initial state: 0.04229449797846379

Time for model checking: 1509.669 seconds.

Result: 0.04229449797846379


##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g