[47.899, 43.544, 52.304, 50.03, 56.027]

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

Version: 4.11
Date: Tue Oct 13 09:04:28 GMT+02:00 2026
Hostname: r23m0197.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4964692/tmp11x4n6hwprism_from-prism_check_ex_nand.40-4_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4964692/tmp11x4n6hwprism_from-prism_check_ex_nand.40-4_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4964692/tmp11x4n6hwprism_from-prism_check_ex_nand.40-4_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     multiplex
Actions:     []
Variables:   u c s z zx zy x y
Labels:      "target"

Parsing properties file "/w0/tmp/slurm_tq429871.4964692/tmp11x4n6hwprism_from-prism_check_ex_nand.40-4_tmp_indir_/property.props"...

1 property:
(1) "reliable": P=? [ F "target" ]

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

Model checking: "reliable": P=? [ F "target" ]

Building model (engine:explicit)...

Computing reachable states... 2005089 3999522 states
Reachable states exploration and model construction done in 5.9 secs.
Sorting reachable states list...

Time for model construction: 7.05 seconds.

Type:        DTMC
States:      3999522 (1 initial)
Transitions: 6288542

Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain...  done (0.312 seconds)
Starting Prob0...
Prob0 took 0.58 seconds.
Starting Prob1...
Prob1 took 1.313 seconds.
target=4, yes=141, no=375263, maybe=3624118
Starting value iteration (with Jacobi)...
Iteration 147: 5.02 sec so far
Iteration 299: 10.04 sec so far
Iteration 463: 15.05 sec so far
Iteration 640: 20.08 sec so far
Iteration 826: 25.09 sec so far
Iteration 1043: 30.10 sec so far
Iteration 1303: 35.11 sec so far
Value iteration (with Jacobi) took 1441 iterations, 8212786406 multiplications and 37.643 seconds.
Probabilistic reachability took 39.889 seconds.

Value in the initial state: 0.6186822208151964

Time for model checking: 40.215 seconds.

Result: 0.6186822208151964 (exact floating point)


##############################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: 43.544 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 07:07:42 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.4961454/tmp6brkq1hqprism_from-prism_check_ex_nand.40-4_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4961454/tmp6brkq1hqprism_from-prism_check_ex_nand.40-4_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4961454/tmp6brkq1hqprism_from-prism_check_ex_nand.40-4_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     multiplex
Actions:     []
Variables:   u c s z zx zy x y
Labels:      "target"

Parsing properties file "/w0/tmp/slurm_tq429871.4961454/tmp6brkq1hqprism_from-prism_check_ex_nand.40-4_tmp_indir_/property.props"...

1 property:
(1) "reliable": P=? [ F "target" ]

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

Model checking: "reliable": P=? [ F "target" ]

Building model (engine:explicit)...

Computing reachable states... 2174029 3999522 states
Reachable states exploration and model construction done in 5.478 secs.
Sorting reachable states list...

Time for model construction: 6.575 seconds.

Type:        DTMC
States:      3999522 (1 initial)
Transitions: 6288542

Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain...  done (0.478 seconds)
Starting Prob0...
Prob0 took 0.587 seconds.
Starting Prob1...
Prob1 took 1.189 seconds.
target=4, yes=141, no=375263, maybe=3624118
Starting value iteration (with Jacobi)...
Iteration 159: 5.03 sec so far
Iteration 326: 10.05 sec so far
Iteration 507: 15.07 sec so far
Iteration 708: 20.09 sec so far
Iteration 933: 25.11 sec so far
Iteration 1200: 30.11 sec so far
Value iteration (with Jacobi) took 1441 iterations, 8212786406 multiplications and 34.051 seconds.
Probabilistic reachability took 36.328 seconds.

Value in the initial state: 0.6186822208151964

Time for model checking: 36.415 seconds.

Result: 0.6186822208151964 (exact floating point)


##############################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: 52.304 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 07:45:20 GMT+02:00 2026
Hostname: n23m0056.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4963086/tmp8uldpx3vprism_from-prism_check_ex_nand.40-4_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4963086/tmp8uldpx3vprism_from-prism_check_ex_nand.40-4_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4963086/tmp8uldpx3vprism_from-prism_check_ex_nand.40-4_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     multiplex
Actions:     []
Variables:   u c s z zx zy x y
Labels:      "target"

Parsing properties file "/w0/tmp/slurm_tq429871.4963086/tmp8uldpx3vprism_from-prism_check_ex_nand.40-4_tmp_indir_/property.props"...

1 property:
(1) "reliable": P=? [ F "target" ]

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

Model checking: "reliable": P=? [ F "target" ]

Building model (engine:explicit)...

Computing reachable states... 1752977 3690403 3999522 states
Reachable states exploration and model construction done in 6.561 secs.
Sorting reachable states list...

Time for model construction: 7.721 seconds.

Type:        DTMC
States:      3999522 (1 initial)
Transitions: 6288542

Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain...  done (0.595 seconds)
Starting Prob0...
Prob0 took 0.627 seconds.
Starting Prob1...
Prob1 took 1.333 seconds.
target=4, yes=141, no=375263, maybe=3624118
Starting value iteration (with Jacobi)...
Iteration 134: 5.01 sec so far
Iteration 269: 10.01 sec so far
Iteration 414: 15.04 sec so far
Iteration 570: 20.06 sec so far
Iteration 739: 25.06 sec so far
Iteration 926: 30.08 sec so far
Iteration 1137: 35.09 sec so far
Iteration 1384: 40.10 sec so far
Value iteration (with Jacobi) took 1441 iterations, 8212786406 multiplications and 41.266 seconds.
Probabilistic reachability took 43.846 seconds.

Value in the initial state: 0.6186822208151964

Time for model checking: 43.951 seconds.

Result: 0.6186822208151964 (exact floating point)


##############################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: 50.030 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 08:52:05 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.4964112/tmpervekxd0prism_from-prism_check_ex_nand.40-4_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4964112/tmpervekxd0prism_from-prism_check_ex_nand.40-4_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4964112/tmpervekxd0prism_from-prism_check_ex_nand.40-4_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     multiplex
Actions:     []
Variables:   u c s z zx zy x y
Labels:      "target"

Parsing properties file "/w0/tmp/slurm_tq429871.4964112/tmpervekxd0prism_from-prism_check_ex_nand.40-4_tmp_indir_/property.props"...

1 property:
(1) "reliable": P=? [ F "target" ]

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

Model checking: "reliable": P=? [ F "target" ]

Building model (engine:explicit)...

Computing reachable states... 1841170 3738671 3999522 states
Reachable states exploration and model construction done in 6.521 secs.
Sorting reachable states list...

Time for model construction: 7.53 seconds.

Type:        DTMC
States:      3999522 (1 initial)
Transitions: 6288542

Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain...  done (0.303 seconds)
Starting Prob0...
Prob0 took 0.625 seconds.
Starting Prob1...
Prob1 took 1.412 seconds.
target=4, yes=141, no=375263, maybe=3624118
Starting value iteration (with Jacobi)...
Iteration 137: 5.02 sec so far
Iteration 279: 10.03 sec so far
Iteration 432: 15.05 sec so far
Iteration 597: 20.07 sec so far
Iteration 779: 25.08 sec so far
Iteration 983: 30.09 sec so far
Iteration 1221: 35.09 sec so far
Value iteration (with Jacobi) took 1441 iterations, 8212786406 multiplications and 39.225 seconds.
Probabilistic reachability took 41.657 seconds.

Value in the initial state: 0.6186822208151964

Time for model checking: 41.772 seconds.

Result: 0.6186822208151964 (exact floating point)


##############################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: 56.027 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 07:48:01 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.4963211/tmpbrudys5aprism_from-prism_check_ex_nand.40-4_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4963211/tmpbrudys5aprism_from-prism_check_ex_nand.40-4_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4963211/tmpbrudys5aprism_from-prism_check_ex_nand.40-4_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     multiplex
Actions:     []
Variables:   u c s z zx zy x y
Labels:      "target"

Parsing properties file "/w0/tmp/slurm_tq429871.4963211/tmpbrudys5aprism_from-prism_check_ex_nand.40-4_tmp_indir_/property.props"...

1 property:
(1) "reliable": P=? [ F "target" ]

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

Model checking: "reliable": P=? [ F "target" ]

Building model (engine:explicit)...

Computing reachable states... 1680138 3601413 3999522 states
Reachable states exploration and model construction done in 6.799 secs.
Sorting reachable states list...

Time for model construction: 8.26 seconds.

Type:        DTMC
States:      3999522 (1 initial)
Transitions: 6288542

Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain...  done (0.418 seconds)
Starting Prob0...
Prob0 took 0.631 seconds.
Starting Prob1...
Prob1 took 1.495 seconds.
target=4, yes=141, no=375263, maybe=3624118
Starting value iteration (with Jacobi)...
Iteration 123: 5.04 sec so far
Iteration 248: 10.04 sec so far
Iteration 381: 15.06 sec so far
Iteration 524: 20.09 sec so far
Iteration 677: 25.11 sec so far
Iteration 846: 30.14 sec so far
Iteration 1033: 35.16 sec so far
Iteration 1247: 40.17 sec so far
Value iteration (with Jacobi) took 1441 iterations, 8212786406 multiplications and 44.447 seconds.
Probabilistic reachability took 47.035 seconds.

Value in the initial state: 0.6186822208151964

Time for model checking: 47.139 seconds.

Result: 0.6186822208151964 (exact floating point)


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