Log files for model crowds.6-20 and tool configuration prism_from-umb_check_ex
[14.412, 14.028, 13.129, 20.42, 12.657]
Log file: prism_from-umb_check_ex_crowds.6-20_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 14.412 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:25:57 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.4965754/tmp2hzv0draprism_from-umb_check_ex_crowds.6-20_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4965754/tmp2hzv0draprism_from-umb_check_ex_crowds.6-20_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: DTMC
Actions: []
Variables: x
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4965754/tmp2hzv0draprism_from-umb_check_ex_crowds.6-20_tmp_indir_/property.props"...
1 property:
(1) "positive": P=? [ F "target" ]
---------------------------------------------------------------------
Model checking: "positive": P=? [ F "target" ]
Building model (engine:explicit)...
Time for model construction: 1.671 seconds.
Warning: Deadlocks detected and fixed in 230230 states
Type: DTMC
States: 10633591 (1 initial)
Transitions: 38261191
Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain... done (2.29 seconds)
Starting Prob0...
Prob0 took 0.603 seconds.
Starting Prob1...
Prob1 took 4.627 seconds.
target=352935, yes=363561, no=8587502, maybe=1682528
Starting value iteration (with Jacobi)...
Value iteration (with Jacobi) took 206 iterations, 2185323808 multiplications and 4.222 seconds.
Probabilistic reachability took 11.781 seconds.
Value in the initial state: 0.12047517459031508
Time for model checking: 12.049 seconds.
Result: 0.12047517459031508 (+/- 1.1352691080806785E-6 estimated; rel err 9.423261779376928E-6)
---------------------------------------------------------------------
Note: There was 1 warning during computation.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_crowds.6-20_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 14.028 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:07:43 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.4961468/tmpti_gi4ifprism_from-umb_check_ex_crowds.6-20_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4961468/tmpti_gi4ifprism_from-umb_check_ex_crowds.6-20_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: DTMC
Actions: []
Variables: x
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4961468/tmpti_gi4ifprism_from-umb_check_ex_crowds.6-20_tmp_indir_/property.props"...
1 property:
(1) "positive": P=? [ F "target" ]
---------------------------------------------------------------------
Model checking: "positive": P=? [ F "target" ]
Building model (engine:explicit)...
Time for model construction: 1.44 seconds.
Warning: Deadlocks detected and fixed in 230230 states
Type: DTMC
States: 10633591 (1 initial)
Transitions: 38261191
Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain... done (2.229 seconds)
Starting Prob0...
Prob0 took 0.729 seconds.
Starting Prob1...
Prob1 took 4.201 seconds.
target=352935, yes=363561, no=8587502, maybe=1682528
Starting value iteration (with Jacobi)...
Value iteration (with Jacobi) took 206 iterations, 2185323808 multiplications and 4.342 seconds.
Probabilistic reachability took 11.571 seconds.
Value in the initial state: 0.12047517459031508
Time for model checking: 11.908 seconds.
Result: 0.12047517459031508 (+/- 1.1352691080806785E-6 estimated; rel err 9.423261779376928E-6)
---------------------------------------------------------------------
Note: There was 1 warning during computation.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_crowds.6-20_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 13.129 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:31:15 GMT+02:00 2026
Hostname: n23m0293.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4965996/tmpflnkro_4prism_from-umb_check_ex_crowds.6-20_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4965996/tmpflnkro_4prism_from-umb_check_ex_crowds.6-20_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: DTMC
Actions: []
Variables: x
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4965996/tmpflnkro_4prism_from-umb_check_ex_crowds.6-20_tmp_indir_/property.props"...
1 property:
(1) "positive": P=? [ F "target" ]
---------------------------------------------------------------------
Model checking: "positive": P=? [ F "target" ]
Building model (engine:explicit)...
Time for model construction: 1.526 seconds.
Warning: Deadlocks detected and fixed in 230230 states
Type: DTMC
States: 10633591 (1 initial)
Transitions: 38261191
Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain... done (2.285 seconds)
Starting Prob0...
Prob0 took 0.847 seconds.
Starting Prob1...
Prob1 took 2.824 seconds.
target=352935, yes=363561, no=8587502, maybe=1682528
Starting value iteration (with Jacobi)...
Value iteration (with Jacobi) took 206 iterations, 2185323808 multiplications and 4.484 seconds.
Probabilistic reachability took 10.506 seconds.
Value in the initial state: 0.12047517459031508
Time for model checking: 10.82 seconds.
Result: 0.12047517459031508 (+/- 1.1352691080806785E-6 estimated; rel err 9.423261779376928E-6)
---------------------------------------------------------------------
Note: There was 1 warning during computation.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_crowds.6-20_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 20.420 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:02:16 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 -importmodel /w0/tmp/slurm_tq429871.4961224/tmpd73vdr9uprism_from-umb_check_ex_crowds.6-20_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4961224/tmpd73vdr9uprism_from-umb_check_ex_crowds.6-20_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: DTMC
Actions: []
Variables: x
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4961224/tmpd73vdr9uprism_from-umb_check_ex_crowds.6-20_tmp_indir_/property.props"...
1 property:
(1) "positive": P=? [ F "target" ]
---------------------------------------------------------------------
Model checking: "positive": P=? [ F "target" ]
Building model (engine:explicit)...
Time for model construction: 3.153 seconds.
Warning: Deadlocks detected and fixed in 230230 states
Type: DTMC
States: 10633591 (1 initial)
Transitions: 38261191
Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain... done (3.314 seconds)
Starting Prob0...
Prob0 took 0.846 seconds.
Starting Prob1...
Prob1 took 3.665 seconds.
target=352935, yes=363561, no=8587502, maybe=1682528
Starting value iteration (with Jacobi)...
Iteration 196: 5.02 sec so far
Value iteration (with Jacobi) took 206 iterations, 2185323808 multiplications and 5.477 seconds.
Probabilistic reachability took 13.352 seconds.
Value in the initial state: 0.12047517459031508
Time for model checking: 13.691 seconds.
Result: 0.12047517459031508 (+/- 1.1352691080806785E-6 estimated; rel err 9.423261779376928E-6)
---------------------------------------------------------------------
Note: There was 1 warning during computation.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_crowds.6-20_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 12.657 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:04:29 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.4964687/tmpj7xm5rwjprism_from-umb_check_ex_crowds.6-20_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4964687/tmpj7xm5rwjprism_from-umb_check_ex_crowds.6-20_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: DTMC
Actions: []
Variables: x
Labels: "target"
Parsing properties file "/w0/tmp/slurm_tq429871.4964687/tmpj7xm5rwjprism_from-umb_check_ex_crowds.6-20_tmp_indir_/property.props"...
1 property:
(1) "positive": P=? [ F "target" ]
---------------------------------------------------------------------
Model checking: "positive": P=? [ F "target" ]
Building model (engine:explicit)...
Time for model construction: 1.289 seconds.
Warning: Deadlocks detected and fixed in 230230 states
Type: DTMC
States: 10633591 (1 initial)
Transitions: 38261191
Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain... done (2.057 seconds)
Starting Prob0...
Prob0 took 0.757 seconds.
Starting Prob1...
Prob1 took 3.793 seconds.
target=352935, yes=363561, no=8587502, maybe=1682528
Starting value iteration (with Jacobi)...
Value iteration (with Jacobi) took 206 iterations, 2185323808 multiplications and 3.844 seconds.
Probabilistic reachability took 10.483 seconds.
Value in the initial state: 0.12047517459031508
Time for model checking: 10.779 seconds.
Result: 0.12047517459031508 (+/- 1.1352691080806785E-6 estimated; rel err 9.423261779376928E-6)
---------------------------------------------------------------------
Note: There was 1 warning during computation.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g