Log files for model crowds.5-20 and tool configuration prism_from-umb_check_ex
[0.373, 0.348, 0.326, 0.301, 0.355]
Log file: prism_from-umb_check_ex_crowds.5-20_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 3.687 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:46:29 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.4966769/tmpf0qtm0iuprism_from-umb_check_ex_crowds.5-20_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4966769/tmpf0qtm0iuprism_from-umb_check_ex_crowds.5-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.4966769/tmpf0qtm0iuprism_from-umb_check_ex_crowds.5-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: 0.373 seconds.
Warning: Deadlocks detected and fixed in 53130 states
Type: DTMC
States: 2061951 (1 initial)
Transitions: 7374951
Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain... done (0.716 seconds)
Starting Prob0...
Prob0 took 0.15 seconds.
Starting Prob1...
Prob1 took 0.664 seconds.
target=45628, yes=47399, no=1745849, maybe=268703
Starting value iteration (with Jacobi)...
Value iteration (with Jacobi) took 187 iterations, 328436141 multiplications and 0.905 seconds.
Probabilistic reachability took 2.46 seconds.
Value in the initial state: 0.08606841127862014
Time for model checking: 2.543 seconds.
Result: 0.08606841127862014 (+/- 7.183522320847802E-7 estimated; rel err 8.346293621702098E-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.5-20_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 2.824 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:22:30 GMT+02:00 2026
Hostname: n23m0058.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4962073/tmp5fvq84fnprism_from-umb_check_ex_crowds.5-20_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4962073/tmp5fvq84fnprism_from-umb_check_ex_crowds.5-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.4962073/tmp5fvq84fnprism_from-umb_check_ex_crowds.5-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: 0.348 seconds.
Warning: Deadlocks detected and fixed in 53130 states
Type: DTMC
States: 2061951 (1 initial)
Transitions: 7374951
Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain... done (0.485 seconds)
Starting Prob0...
Prob0 took 0.112 seconds.
Starting Prob1...
Prob1 took 0.526 seconds.
target=45628, yes=47399, no=1745849, maybe=268703
Starting value iteration (with Jacobi)...
Value iteration (with Jacobi) took 187 iterations, 328436141 multiplications and 0.588 seconds.
Probabilistic reachability took 1.746 seconds.
Value in the initial state: 0.08606841127862014
Time for model checking: 1.813 seconds.
Result: 0.08606841127862014 (+/- 7.183522320847802E-7 estimated; rel err 8.346293621702098E-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.5-20_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 2.969 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:16:33 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 -importmodel /w0/tmp/slurm_tq429871.4965210/tmpjr6qxsxcprism_from-umb_check_ex_crowds.5-20_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4965210/tmpjr6qxsxcprism_from-umb_check_ex_crowds.5-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.4965210/tmpjr6qxsxcprism_from-umb_check_ex_crowds.5-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: 0.326 seconds.
Warning: Deadlocks detected and fixed in 53130 states
Type: DTMC
States: 2061951 (1 initial)
Transitions: 7374951
Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain... done (0.481 seconds)
Starting Prob0...
Prob0 took 0.106 seconds.
Starting Prob1...
Prob1 took 0.761 seconds.
target=45628, yes=47399, no=1745849, maybe=268703
Starting value iteration (with Jacobi)...
Value iteration (with Jacobi) took 187 iterations, 328436141 multiplications and 0.554 seconds.
Probabilistic reachability took 1.925 seconds.
Value in the initial state: 0.08606841127862014
Time for model checking: 1.989 seconds.
Result: 0.08606841127862014 (+/- 7.183522320847802E-7 estimated; rel err 8.346293621702098E-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.5-20_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 2.549 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:27:37 GMT+02:00 2026
Hostname: n23m0044.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4962290/tmplnnv8lmwprism_from-umb_check_ex_crowds.5-20_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4962290/tmplnnv8lmwprism_from-umb_check_ex_crowds.5-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.4962290/tmplnnv8lmwprism_from-umb_check_ex_crowds.5-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: 0.301 seconds.
Warning: Deadlocks detected and fixed in 53130 states
Type: DTMC
States: 2061951 (1 initial)
Transitions: 7374951
Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain... done (0.456 seconds)
Starting Prob0...
Prob0 took 0.109 seconds.
Starting Prob1...
Prob1 took 0.508 seconds.
target=45628, yes=47399, no=1745849, maybe=268703
Starting value iteration (with Jacobi)...
Value iteration (with Jacobi) took 187 iterations, 328436141 multiplications and 0.521 seconds.
Probabilistic reachability took 1.614 seconds.
Value in the initial state: 0.08606841127862014
Time for model checking: 1.672 seconds.
Result: 0.08606841127862014 (+/- 7.183522320847802E-7 estimated; rel err 8.346293621702098E-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.5-20_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 2.943 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:49:37 GMT+02:00 2026
Hostname: n23m0294.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4966841/tmp_c_pggkcprism_from-umb_check_ex_crowds.5-20_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4966841/tmp_c_pggkcprism_from-umb_check_ex_crowds.5-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.4966841/tmp_c_pggkcprism_from-umb_check_ex_crowds.5-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: 0.355 seconds.
Warning: Deadlocks detected and fixed in 53130 states
Type: DTMC
States: 2061951 (1 initial)
Transitions: 7374951
Starting probabilistic reachability...
Calculating predecessor relation for discrete-time Markov chain... done (0.508 seconds)
Starting Prob0...
Prob0 took 0.125 seconds.
Starting Prob1...
Prob1 took 0.537 seconds.
target=45628, yes=47399, no=1745849, maybe=268703
Starting value iteration (with Jacobi)...
Value iteration (with Jacobi) took 187 iterations, 328436141 multiplications and 0.607 seconds.
Probabilistic reachability took 1.8 seconds.
Value in the initial state: 0.08606841127862014
Time for model checking: 1.872 seconds.
Result: 0.08606841127862014 (+/- 7.183522320847802E-7 estimated; rel err 8.346293621702098E-6)
---------------------------------------------------------------------
Note: There was 1 warning during computation.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g