[0.196, 0.184, 0.17, 0.141, 0.204]

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 1.450 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 09:10:16 GMT+02:00 2026
Hostname: r23m0219.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4964953/tmpfxo85ugrprism_from-prism_check_ex_embedded.8-12_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4964953/tmpfxo85ugrprism_from-prism_check_ex_embedded.8-12_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4964953/tmpfxo85ugrprism_from-prism_check_ex_embedded.8-12_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     sensors proci actuators proco procm bus
Actions:     [] [input_reboot] [output_reboot] [timeout]
Variables:   s i a o m count comp reqi reqo
Labels:      "fail_actuators" "l_down"

Parsing properties file "/w0/tmp/slurm_tq429871.4964953/tmpfxo85ugrprism_from-prism_check_ex_embedded.8-12_tmp_indir_/property.props"...

1 property:
(1) "actuators": P=? [ !"l_down" U "fail_actuators" ]

---------------------------------------------------------------------

Model checking: "actuators": P=? [ !"l_down" U "fail_actuators" ]

Building model (engine:explicit)...

Computing reachable states... 8548 states
Reachable states exploration and model construction done in 0.108 secs.
Sorting reachable states list...

Time for model construction: 0.196 seconds.

Type:        CTMC
States:      8548 (1 initial)
Transitions: 36041
Building embedded DTMC...

Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain...  done (0.024 seconds)
Starting Prob0...
Prob0 took 0.003 seconds.
Starting Prob1...
Prob1 took 0.005 seconds.
target=1064, yes=1064, no=6356, maybe=1128
Starting value iteration (with Jacobi)...
Value iteration (with Jacobi) took 687 iterations, 5072808 multiplications and 0.284 seconds.
Probabilistic reachability took 0.345 seconds.

Value in the initial state: 0.10529804738524096

Time for model checking: 0.413 seconds.

Result: 0.10529804738524096 (+/- 1.0374360534628648E-6 estimated; rel err 9.85237693598748E-6)


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

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 1.506 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 09:07:07 GMT+02:00 2026
Hostname: r23m0213.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4964812/tmpjy_vzoh8prism_from-prism_check_ex_embedded.8-12_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4964812/tmpjy_vzoh8prism_from-prism_check_ex_embedded.8-12_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4964812/tmpjy_vzoh8prism_from-prism_check_ex_embedded.8-12_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     sensors proci actuators proco procm bus
Actions:     [] [input_reboot] [output_reboot] [timeout]
Variables:   s i a o m count comp reqi reqo
Labels:      "fail_actuators" "l_down"

Parsing properties file "/w0/tmp/slurm_tq429871.4964812/tmpjy_vzoh8prism_from-prism_check_ex_embedded.8-12_tmp_indir_/property.props"...

1 property:
(1) "actuators": P=? [ !"l_down" U "fail_actuators" ]

---------------------------------------------------------------------

Model checking: "actuators": P=? [ !"l_down" U "fail_actuators" ]

Building model (engine:explicit)...

Computing reachable states... 8548 states
Reachable states exploration and model construction done in 0.102 secs.
Sorting reachable states list...

Time for model construction: 0.184 seconds.

Type:        CTMC
States:      8548 (1 initial)
Transitions: 36041
Building embedded DTMC...

Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain...  done (0.023 seconds)
Starting Prob0...
Prob0 took 0.004 seconds.
Starting Prob1...
Prob1 took 0.005 seconds.
target=1064, yes=1064, no=6356, maybe=1128
Starting value iteration (with Jacobi)...
Value iteration (with Jacobi) took 687 iterations, 5072808 multiplications and 0.262 seconds.
Probabilistic reachability took 0.321 seconds.

Value in the initial state: 0.10529804738524096

Time for model checking: 0.376 seconds.

Result: 0.10529804738524096 (+/- 1.0374360534628648E-6 estimated; rel err 9.85237693598748E-6)


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

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 1.484 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 07:44:47 GMT+02:00 2026
Hostname: n23m0021.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4963051/tmpn36uaxa4prism_from-prism_check_ex_embedded.8-12_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4963051/tmpn36uaxa4prism_from-prism_check_ex_embedded.8-12_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4963051/tmpn36uaxa4prism_from-prism_check_ex_embedded.8-12_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     sensors proci actuators proco procm bus
Actions:     [] [input_reboot] [output_reboot] [timeout]
Variables:   s i a o m count comp reqi reqo
Labels:      "fail_actuators" "l_down"

Parsing properties file "/w0/tmp/slurm_tq429871.4963051/tmpn36uaxa4prism_from-prism_check_ex_embedded.8-12_tmp_indir_/property.props"...

1 property:
(1) "actuators": P=? [ !"l_down" U "fail_actuators" ]

---------------------------------------------------------------------

Model checking: "actuators": P=? [ !"l_down" U "fail_actuators" ]

Building model (engine:explicit)...

Computing reachable states... 8548 states
Reachable states exploration and model construction done in 0.119 secs.
Sorting reachable states list...

Time for model construction: 0.17 seconds.

Type:        CTMC
States:      8548 (1 initial)
Transitions: 36041
Building embedded DTMC...

Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain...  done (0.027 seconds)
Starting Prob0...
Prob0 took 0.004 seconds.
Starting Prob1...
Prob1 took 0.007 seconds.
target=1064, yes=1064, no=6356, maybe=1128
Starting value iteration (with Jacobi)...
Value iteration (with Jacobi) took 687 iterations, 5072808 multiplications and 0.375 seconds.
Probabilistic reachability took 0.421 seconds.

Value in the initial state: 0.10529804738524096

Time for model checking: 0.494 seconds.

Result: 0.10529804738524096 (+/- 1.0374360534628648E-6 estimated; rel err 9.85237693598748E-6)


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

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 1.307 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 07:04:56 GMT+02:00 2026
Hostname: n23m0097.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4961336/tmpwbfmm535prism_from-prism_check_ex_embedded.8-12_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4961336/tmpwbfmm535prism_from-prism_check_ex_embedded.8-12_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4961336/tmpwbfmm535prism_from-prism_check_ex_embedded.8-12_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     sensors proci actuators proco procm bus
Actions:     [] [input_reboot] [output_reboot] [timeout]
Variables:   s i a o m count comp reqi reqo
Labels:      "fail_actuators" "l_down"

Parsing properties file "/w0/tmp/slurm_tq429871.4961336/tmpwbfmm535prism_from-prism_check_ex_embedded.8-12_tmp_indir_/property.props"...

1 property:
(1) "actuators": P=? [ !"l_down" U "fail_actuators" ]

---------------------------------------------------------------------

Model checking: "actuators": P=? [ !"l_down" U "fail_actuators" ]

Building model (engine:explicit)...

Computing reachable states... 8548 states
Reachable states exploration and model construction done in 0.097 secs.
Sorting reachable states list...

Time for model construction: 0.141 seconds.

Type:        CTMC
States:      8548 (1 initial)
Transitions: 36041
Building embedded DTMC...

Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain...  done (0.02 seconds)
Starting Prob0...
Prob0 took 0.004 seconds.
Starting Prob1...
Prob1 took 0.005 seconds.
target=1064, yes=1064, no=6356, maybe=1128
Starting value iteration (with Jacobi)...
Value iteration (with Jacobi) took 687 iterations, 5072808 multiplications and 0.234 seconds.
Probabilistic reachability took 0.289 seconds.

Value in the initial state: 0.10529804738524096

Time for model checking: 0.361 seconds.

Result: 0.10529804738524096 (+/- 1.0374360534628648E-6 estimated; rel err 9.85237693598748E-6)


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

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 1.396 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 07:02:14 GMT+02:00 2026
Hostname: n23m0049.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4961238/tmpba675_zdprism_from-prism_check_ex_embedded.8-12_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4961238/tmpba675_zdprism_from-prism_check_ex_embedded.8-12_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4961238/tmpba675_zdprism_from-prism_check_ex_embedded.8-12_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     sensors proci actuators proco procm bus
Actions:     [] [input_reboot] [output_reboot] [timeout]
Variables:   s i a o m count comp reqi reqo
Labels:      "fail_actuators" "l_down"

Parsing properties file "/w0/tmp/slurm_tq429871.4961238/tmpba675_zdprism_from-prism_check_ex_embedded.8-12_tmp_indir_/property.props"...

1 property:
(1) "actuators": P=? [ !"l_down" U "fail_actuators" ]

---------------------------------------------------------------------

Model checking: "actuators": P=? [ !"l_down" U "fail_actuators" ]

Building model (engine:explicit)...

Computing reachable states... 8548 states
Reachable states exploration and model construction done in 0.113 secs.
Sorting reachable states list...

Time for model construction: 0.204 seconds.

Type:        CTMC
States:      8548 (1 initial)
Transitions: 36041
Building embedded DTMC...

Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain...  done (0.02 seconds)
Starting Prob0...
Prob0 took 0.005 seconds.
Starting Prob1...
Prob1 took 0.005 seconds.
target=1064, yes=1064, no=6356, maybe=1128
Starting value iteration (with Jacobi)...
Value iteration (with Jacobi) took 687 iterations, 5072808 multiplications and 0.27 seconds.
Probabilistic reachability took 0.323 seconds.

Value in the initial state: 0.10529804738524096

Time for model checking: 0.406 seconds.

Result: 0.10529804738524096 (+/- 1.0374360534628648E-6 estimated; rel err 9.85237693598748E-6)


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