Log files for model herman.15 and tool configuration prism_from-prism_check_ex
[23.134, 20.603, 23.58, 21.18, 20.323]
Log file: prism_from-prism_check_ex_herman.15_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 28.313 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:11:29 GMT+02:00 2026
Hostname: n23m0107.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4961623/tmpy6or0n2gprism_from-prism_check_ex_herman.15_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4961623/tmpy6or0n2gprism_from-prism_check_ex_herman.15_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4961623/tmpy6or0n2gprism_from-prism_check_ex_herman.15_tmp_indir_/model.prism"...
Type: DTMC
Modules: process1 process2 process3 process4 process5 process6 process7 process8 process9 process10 process11 process12 process13 process14 process15
Actions: [step]
Variables: x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15
Labels: "stable"
Rewards: "steps"
Parsing properties file "/w0/tmp/slurm_tq429871.4961623/tmpy6or0n2gprism_from-prism_check_ex_herman.15_tmp_indir_/property.props"...
1 property:
(1) "steps": filter(max, R=? [ F "stable" ], "init")
---------------------------------------------------------------------
Model checking: "steps": filter(max, R=? [ F "stable" ], "init")
Building model (engine:explicit)...
Computing reachable states... 973 4321 12815 17154 25600 30751 32697 32768 states
Reachable states exploration and model construction done in 22.524 secs.
Sorting reachable states list...
Time for model construction: 23.134 seconds.
Type: DTMC
States: 32768 (32768 initial)
Transitions: 14348908
Building reward structure...
Starting expected reachability...
Calculating predecessor relation for discrete-time Markov chain... done (0.368 seconds)
Starting Prob1...
Prob1 took 0.487 seconds.
target=30, inf=0, rest=32738
Starting value iteration (with Jacobi) ...
Value iteration (with Jacobi) took 246 iterations, 3529816608 multiplications and 3.275 seconds.
Expected reachability took 4.14 seconds.
Maximum value over states satisfying filter: 33.332616661835104
There are 10 states with (approximately) this value:
5285:(0,0,1,0,1,0,0,1,0,1,0,0,1,0,1)
9513:(0,1,0,0,1,0,1,0,0,1,0,1,0,0,1)
10570:(0,1,0,1,0,0,1,0,1,0,0,1,0,1,0)
11627:(0,1,0,1,1,0,1,0,1,1,0,1,0,1,1)
13741:(0,1,1,0,1,0,1,1,0,1,0,1,1,0,1)
19026:(1,0,0,1,0,1,0,0,1,0,1,0,0,1,0)
21140:(1,0,1,0,0,1,0,1,0,0,1,0,1,0,0)
22197:(1,0,1,0,1,1,0,1,0,1,1,0,1,0,1)
23254:(1,0,1,1,0,1,0,1,1,0,1,0,1,1,0)
27482:(1,1,0,1,0,1,1,0,1,0,1,1,0,1,0)
Time for model checking: 4.471 seconds.
Result: 33.332616661835104
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_herman.15_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 25.455 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:28:44 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 /w0/tmp/slurm_tq429871.4962332/tmpeiambhz2prism_from-prism_check_ex_herman.15_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4962332/tmpeiambhz2prism_from-prism_check_ex_herman.15_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4962332/tmpeiambhz2prism_from-prism_check_ex_herman.15_tmp_indir_/model.prism"...
Type: DTMC
Modules: process1 process2 process3 process4 process5 process6 process7 process8 process9 process10 process11 process12 process13 process14 process15
Actions: [step]
Variables: x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15
Labels: "stable"
Rewards: "steps"
Parsing properties file "/w0/tmp/slurm_tq429871.4962332/tmpeiambhz2prism_from-prism_check_ex_herman.15_tmp_indir_/property.props"...
1 property:
(1) "steps": filter(max, R=? [ F "stable" ], "init")
---------------------------------------------------------------------
Model checking: "steps": filter(max, R=? [ F "stable" ], "init")
Building model (engine:explicit)...
Computing reachable states... 999 5715 14625 20474 28734 32290 32768 states
Reachable states exploration and model construction done in 20.142 secs.
Sorting reachable states list...
Time for model construction: 20.603 seconds.
Type: DTMC
States: 32768 (32768 initial)
Transitions: 14348908
Building reward structure...
Starting expected reachability...
Calculating predecessor relation for discrete-time Markov chain... done (0.286 seconds)
Starting Prob1...
Prob1 took 0.453 seconds.
target=30, inf=0, rest=32738
Starting value iteration (with Jacobi) ...
Value iteration (with Jacobi) took 246 iterations, 3529816608 multiplications and 3.241 seconds.
Expected reachability took 3.986 seconds.
Maximum value over states satisfying filter: 33.332616661835104
There are 10 states with (approximately) this value:
5285:(0,0,1,0,1,0,0,1,0,1,0,0,1,0,1)
9513:(0,1,0,0,1,0,1,0,0,1,0,1,0,0,1)
10570:(0,1,0,1,0,0,1,0,1,0,0,1,0,1,0)
11627:(0,1,0,1,1,0,1,0,1,1,0,1,0,1,1)
13741:(0,1,1,0,1,0,1,1,0,1,0,1,1,0,1)
19026:(1,0,0,1,0,1,0,0,1,0,1,0,0,1,0)
21140:(1,0,1,0,0,1,0,1,0,0,1,0,1,0,0)
22197:(1,0,1,0,1,1,0,1,0,1,1,0,1,0,1)
23254:(1,0,1,1,0,1,0,1,1,0,1,0,1,1,0)
27482:(1,1,0,1,0,1,1,0,1,0,1,1,0,1,0)
Time for model checking: 4.317 seconds.
Result: 33.332616661835104
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_herman.15_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 28.802 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:16:28 GMT+02:00 2026
Hostname: n23m0042.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4961831/tmpwmv_f1mcprism_from-prism_check_ex_herman.15_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4961831/tmpwmv_f1mcprism_from-prism_check_ex_herman.15_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4961831/tmpwmv_f1mcprism_from-prism_check_ex_herman.15_tmp_indir_/model.prism"...
Type: DTMC
Modules: process1 process2 process3 process4 process5 process6 process7 process8 process9 process10 process11 process12 process13 process14 process15
Actions: [step]
Variables: x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15
Labels: "stable"
Rewards: "steps"
Parsing properties file "/w0/tmp/slurm_tq429871.4961831/tmpwmv_f1mcprism_from-prism_check_ex_herman.15_tmp_indir_/property.props"...
1 property:
(1) "steps": filter(max, R=? [ F "stable" ], "init")
---------------------------------------------------------------------
Model checking: "steps": filter(max, R=? [ F "stable" ], "init")
Building model (engine:explicit)...
Computing reachable states... 649 3969 8734 16400 24608 29694 32512 32768 states
Reachable states exploration and model construction done in 23.013 secs.
Sorting reachable states list...
Time for model construction: 23.58 seconds.
Type: DTMC
States: 32768 (32768 initial)
Transitions: 14348908
Building reward structure...
Starting expected reachability...
Calculating predecessor relation for discrete-time Markov chain... done (0.299 seconds)
Starting Prob1...
Prob1 took 0.436 seconds.
target=30, inf=0, rest=32738
Starting value iteration (with Jacobi) ...
Value iteration (with Jacobi) took 246 iterations, 3529816608 multiplications and 3.45 seconds.
Expected reachability took 4.195 seconds.
Maximum value over states satisfying filter: 33.332616661835104
There are 10 states with (approximately) this value:
5285:(0,0,1,0,1,0,0,1,0,1,0,0,1,0,1)
9513:(0,1,0,0,1,0,1,0,0,1,0,1,0,0,1)
10570:(0,1,0,1,0,0,1,0,1,0,0,1,0,1,0)
11627:(0,1,0,1,1,0,1,0,1,1,0,1,0,1,1)
13741:(0,1,1,0,1,0,1,1,0,1,0,1,1,0,1)
19026:(1,0,0,1,0,1,0,0,1,0,1,0,0,1,0)
21140:(1,0,1,0,0,1,0,1,0,0,1,0,1,0,0)
22197:(1,0,1,0,1,1,0,1,0,1,1,0,1,0,1)
23254:(1,0,1,1,0,1,0,1,1,0,1,0,1,1,0)
27482:(1,1,0,1,0,1,1,0,1,0,1,1,0,1,0)
Time for model checking: 4.585 seconds.
Result: 33.332616661835104
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_herman.15_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 26.124 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:01:17 GMT+02:00 2026
Hostname: n23m0110.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4964492/tmp091d_yxzprism_from-prism_check_ex_herman.15_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4964492/tmp091d_yxzprism_from-prism_check_ex_herman.15_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4964492/tmp091d_yxzprism_from-prism_check_ex_herman.15_tmp_indir_/model.prism"...
Type: DTMC
Modules: process1 process2 process3 process4 process5 process6 process7 process8 process9 process10 process11 process12 process13 process14 process15
Actions: [step]
Variables: x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15
Labels: "stable"
Rewards: "steps"
Parsing properties file "/w0/tmp/slurm_tq429871.4964492/tmp091d_yxzprism_from-prism_check_ex_herman.15_tmp_indir_/property.props"...
1 property:
(1) "steps": filter(max, R=? [ F "stable" ], "init")
---------------------------------------------------------------------
Model checking: "steps": filter(max, R=? [ F "stable" ], "init")
Building model (engine:explicit)...
Computing reachable states... 969 4895 14204 18496 28546 31872 32768 states
Reachable states exploration and model construction done in 20.714 secs.
Sorting reachable states list...
Time for model construction: 21.18 seconds.
Type: DTMC
States: 32768 (32768 initial)
Transitions: 14348908
Building reward structure...
Starting expected reachability...
Calculating predecessor relation for discrete-time Markov chain... done (0.279 seconds)
Starting Prob1...
Prob1 took 0.439 seconds.
target=30, inf=0, rest=32738
Starting value iteration (with Jacobi) ...
Value iteration (with Jacobi) took 246 iterations, 3529816608 multiplications and 3.282 seconds.
Expected reachability took 4.024 seconds.
Maximum value over states satisfying filter: 33.332616661835104
There are 10 states with (approximately) this value:
5285:(0,0,1,0,1,0,0,1,0,1,0,0,1,0,1)
9513:(0,1,0,0,1,0,1,0,0,1,0,1,0,0,1)
10570:(0,1,0,1,0,0,1,0,1,0,0,1,0,1,0)
11627:(0,1,0,1,1,0,1,0,1,1,0,1,0,1,1)
13741:(0,1,1,0,1,0,1,1,0,1,0,1,1,0,1)
19026:(1,0,0,1,0,1,0,0,1,0,1,0,0,1,0)
21140:(1,0,1,0,0,1,0,1,0,0,1,0,1,0,0)
22197:(1,0,1,0,1,1,0,1,0,1,1,0,1,0,1)
23254:(1,0,1,1,0,1,0,1,1,0,1,0,1,1,0)
27482:(1,1,0,1,0,1,1,0,1,0,1,1,0,1,0)
Time for model checking: 4.364 seconds.
Result: 33.332616661835104
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_herman.15_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 25.201 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:13:07 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.4961690/tmph4li4vhgprism_from-prism_check_ex_herman.15_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4961690/tmph4li4vhgprism_from-prism_check_ex_herman.15_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4961690/tmph4li4vhgprism_from-prism_check_ex_herman.15_tmp_indir_/model.prism"...
Type: DTMC
Modules: process1 process2 process3 process4 process5 process6 process7 process8 process9 process10 process11 process12 process13 process14 process15
Actions: [step]
Variables: x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15
Labels: "stable"
Rewards: "steps"
Parsing properties file "/w0/tmp/slurm_tq429871.4961690/tmph4li4vhgprism_from-prism_check_ex_herman.15_tmp_indir_/property.props"...
1 property:
(1) "steps": filter(max, R=? [ F "stable" ], "init")
---------------------------------------------------------------------
Model checking: "steps": filter(max, R=? [ F "stable" ], "init")
Building model (engine:explicit)...
Computing reachable states... 1017 6145 15231 21120 28897 32512 32768 states
Reachable states exploration and model construction done in 19.821 secs.
Sorting reachable states list...
Time for model construction: 20.323 seconds.
Type: DTMC
States: 32768 (32768 initial)
Transitions: 14348908
Building reward structure...
Starting expected reachability...
Calculating predecessor relation for discrete-time Markov chain... done (0.283 seconds)
Starting Prob1...
Prob1 took 0.428 seconds.
target=30, inf=0, rest=32738
Starting value iteration (with Jacobi) ...
Value iteration (with Jacobi) took 246 iterations, 3529816608 multiplications and 3.276 seconds.
Expected reachability took 3.994 seconds.
Maximum value over states satisfying filter: 33.332616661835104
There are 10 states with (approximately) this value:
5285:(0,0,1,0,1,0,0,1,0,1,0,0,1,0,1)
9513:(0,1,0,0,1,0,1,0,0,1,0,1,0,0,1)
10570:(0,1,0,1,0,0,1,0,1,0,0,1,0,1,0)
11627:(0,1,0,1,1,0,1,0,1,1,0,1,0,1,1)
13741:(0,1,1,0,1,0,1,1,0,1,0,1,1,0,1)
19026:(1,0,0,1,0,1,0,0,1,0,1,0,0,1,0)
21140:(1,0,1,0,0,1,0,1,0,0,1,0,1,0,0)
22197:(1,0,1,0,1,1,0,1,0,1,1,0,1,0,1)
23254:(1,0,1,1,0,1,0,1,1,0,1,0,1,1,0)
27482:(1,1,0,1,0,1,1,0,1,0,1,1,0,1,0)
Time for model checking: 4.322 seconds.
Result: 33.332616661835104
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g