Log files for model herman.15 and tool configuration prism_from-umb_check_ex
[0.517, 0.379, 0.383, 0.38, 0.381]
Log file: prism_from-umb_check_ex_herman.15_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 6.836 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 08:57:38 GMT+02:00 2026
Hostname: n23m0252.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4964299/tmpmclrl82hprism_from-umb_check_ex_herman.15_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4964299/tmpmclrl82hprism_from-umb_check_ex_herman.15_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: DTMC
Actions: [step]
Variables: x
Labels: "stable"
Rewards: "steps"
Parsing properties file "/w0/tmp/slurm_tq429871.4964299/tmpmclrl82hprism_from-umb_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)...
Time for model construction: 0.517 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.756 seconds)
Starting Prob1...
Prob1 took 0.251 seconds.
target=30, inf=0, rest=32738
Starting value iteration (with Jacobi) ...
Value iteration (with Jacobi) took 246 iterations, 3529816608 multiplications and 4.096 seconds.
Expected reachability took 5.135 seconds.
Maximum value over states satisfying filter: 33.332616661835104
There are 10 states with (approximately) this value:
5285:(5285)
9513:(9513)
10570:(10570)
11627:(11627)
13741:(13741)
19026:(19026)
21140:(21140)
22197:(22197)
23254:(23254)
27482:(27482)
Time for model checking: 5.484 seconds.
Result: 33.332616661835104
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_herman.15_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 6.122 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:38:04 GMT+02:00 2026
Hostname: n23m0314.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4966339/tmp57avn0rjprism_from-umb_check_ex_herman.15_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4966339/tmp57avn0rjprism_from-umb_check_ex_herman.15_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: DTMC
Actions: [step]
Variables: x
Labels: "stable"
Rewards: "steps"
Parsing properties file "/w0/tmp/slurm_tq429871.4966339/tmp57avn0rjprism_from-umb_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)...
Time for model construction: 0.379 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.816 seconds)
Starting Prob1...
Prob1 took 0.22 seconds.
target=30, inf=0, rest=32738
Starting value iteration (with Jacobi) ...
Value iteration (with Jacobi) took 246 iterations, 3529816608 multiplications and 3.484 seconds.
Expected reachability took 4.541 seconds.
Maximum value over states satisfying filter: 33.332616661835104
There are 10 states with (approximately) this value:
5285:(5285)
9513:(9513)
10570:(10570)
11627:(11627)
13741:(13741)
19026:(19026)
21140:(21140)
22197:(22197)
23254:(23254)
27482:(27482)
Time for model checking: 4.903 seconds.
Result: 33.332616661835104
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_herman.15_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 5.890 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 08:56:35 GMT+02:00 2026
Hostname: n23m0261.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4964252/tmpu_h5rcznprism_from-umb_check_ex_herman.15_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4964252/tmpu_h5rcznprism_from-umb_check_ex_herman.15_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: DTMC
Actions: [step]
Variables: x
Labels: "stable"
Rewards: "steps"
Parsing properties file "/w0/tmp/slurm_tq429871.4964252/tmpu_h5rcznprism_from-umb_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)...
Time for model construction: 0.383 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.826 seconds)
Starting Prob1...
Prob1 took 0.186 seconds.
target=30, inf=0, rest=32738
Starting value iteration (with Jacobi) ...
Value iteration (with Jacobi) took 246 iterations, 3529816608 multiplications and 3.452 seconds.
Expected reachability took 4.492 seconds.
Maximum value over states satisfying filter: 33.332616661835104
There are 10 states with (approximately) this value:
5285:(5285)
9513:(9513)
10570:(10570)
11627:(11627)
13741:(13741)
19026:(19026)
21140:(21140)
22197:(22197)
23254:(23254)
27482:(27482)
Time for model checking: 4.861 seconds.
Result: 33.332616661835104
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_herman.15_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 5.892 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:44:47 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.4963057/tmp97eczfstprism_from-umb_check_ex_herman.15_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4963057/tmp97eczfstprism_from-umb_check_ex_herman.15_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: DTMC
Actions: [step]
Variables: x
Labels: "stable"
Rewards: "steps"
Parsing properties file "/w0/tmp/slurm_tq429871.4963057/tmp97eczfstprism_from-umb_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)...
Time for model construction: 0.38 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.759 seconds)
Starting Prob1...
Prob1 took 0.198 seconds.
target=30, inf=0, rest=32738
Starting value iteration (with Jacobi) ...
Value iteration (with Jacobi) took 246 iterations, 3529816608 multiplications and 3.69 seconds.
Expected reachability took 4.655 seconds.
Maximum value over states satisfying filter: 33.332616661835104
There are 10 states with (approximately) this value:
5285:(5285)
9513:(9513)
10570:(10570)
11627:(11627)
13741:(13741)
19026:(19026)
21140:(21140)
22197:(22197)
23254:(23254)
27482:(27482)
Time for model checking: 4.933 seconds.
Result: 33.332616661835104
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_herman.15_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 5.846 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 10:01:31 GMT+02:00 2026
Hostname: n23m0252.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4967413/tmpi_rvlfx6prism_from-umb_check_ex_herman.15_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4967413/tmpi_rvlfx6prism_from-umb_check_ex_herman.15_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: DTMC
Actions: [step]
Variables: x
Labels: "stable"
Rewards: "steps"
Parsing properties file "/w0/tmp/slurm_tq429871.4967413/tmpi_rvlfx6prism_from-umb_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)...
Time for model construction: 0.381 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.732 seconds)
Starting Prob1...
Prob1 took 0.223 seconds.
target=30, inf=0, rest=32738
Starting value iteration (with Jacobi) ...
Value iteration (with Jacobi) took 246 iterations, 3529816608 multiplications and 3.478 seconds.
Expected reachability took 4.441 seconds.
Maximum value over states satisfying filter: 33.332616661835104
There are 10 states with (approximately) this value:
5285:(5285)
9513:(9513)
10570:(10570)
11627:(11627)
13741:(13741)
19026:(19026)
21140:(21140)
22197:(22197)
23254:(23254)
27482:(27482)
Time for model checking: 4.785 seconds.
Result: 33.332616661835104
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g