Log files for model eajs.5-250-11 and tool configuration prism_from-umb_check_ex
[0.682, 0.636, 0.617, 0.63, 0.723]
Log file: prism_from-umb_check_ex_eajs.5-250-11_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 16.561 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:00:02 GMT+02:00 2026
Hostname: n23m0120.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4961123/tmpxxj5vgonprism_from-umb_check_ex_eajs.5-250-11_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4961123/tmpxxj5vgonprism_from-umb_check_ex_eajs.5-250-11_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: MDP
Actions: [tick]
Variables: x
Labels: "emptyBattery"
Rewards: "utilityLocal"
Parsing properties file "/w0/tmp/slurm_tq429871.4961123/tmpxxj5vgonprism_from-umb_check_ex_eajs.5-250-11_tmp_indir_/property.props"...
1 property:
(1) "ExpUtil": R{"utilityLocal"}max=? [ F "emptyBattery" ]
---------------------------------------------------------------------
Model checking: "ExpUtil": R{"utilityLocal"}max=? [ F "emptyBattery" ]
Building model (engine:explicit)...
Time for model construction: 0.682 seconds.
Type: MDP
States: 3049471 (1 initial)
Transitions: 6977654
Choices: 4256193
Max/avg: 10/1.40
Building reward structure...
Starting expected reachability (max)...
Starting Prob1 (min)...
Prob1 (min) took 250 iterations and 7.866 seconds.
target=13476, inf=0, rest=3035995
Starting value iteration (max, with Power method)...
Iteration 96: 5.05 sec so far
Value iteration (max, with Power method) took 128 iterations, 889190656 multiplications and 7.034 seconds.
Expected reachability took 14.929 seconds.
Value in the initial state: 10.03294060879421
Time for model checking: 15.105 seconds.
Result: 10.03294060879421 (+/- 7.366891075164757E-5 estimated; rel err 7.342703761953329E-6)
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_eajs.5-250-11_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 16.166 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:11: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.4961636/tmprt9jamrkprism_from-umb_check_ex_eajs.5-250-11_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4961636/tmprt9jamrkprism_from-umb_check_ex_eajs.5-250-11_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: MDP
Actions: [tick]
Variables: x
Labels: "emptyBattery"
Rewards: "utilityLocal"
Parsing properties file "/w0/tmp/slurm_tq429871.4961636/tmprt9jamrkprism_from-umb_check_ex_eajs.5-250-11_tmp_indir_/property.props"...
1 property:
(1) "ExpUtil": R{"utilityLocal"}max=? [ F "emptyBattery" ]
---------------------------------------------------------------------
Model checking: "ExpUtil": R{"utilityLocal"}max=? [ F "emptyBattery" ]
Building model (engine:explicit)...
Time for model construction: 0.636 seconds.
Type: MDP
States: 3049471 (1 initial)
Transitions: 6977654
Choices: 4256193
Max/avg: 10/1.40
Building reward structure...
Starting expected reachability (max)...
Starting Prob1 (min)...
Prob1 (min) took 250 iterations and 7.755 seconds.
target=13476, inf=0, rest=3035995
Starting value iteration (max, with Power method)...
Iteration 98: 5.04 sec so far
Value iteration (max, with Power method) took 128 iterations, 889190656 multiplications and 6.871 seconds.
Expected reachability took 14.652 seconds.
Value in the initial state: 10.03294060879421
Time for model checking: 14.853 seconds.
Result: 10.03294060879421 (+/- 7.366891075164757E-5 estimated; rel err 7.342703761953329E-6)
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_eajs.5-250-11_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 14.555 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:53:59 GMT+02:00 2026
Hostname: n23m0102.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4967067/tmphwgogyn7prism_from-umb_check_ex_eajs.5-250-11_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4967067/tmphwgogyn7prism_from-umb_check_ex_eajs.5-250-11_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: MDP
Actions: [tick]
Variables: x
Labels: "emptyBattery"
Rewards: "utilityLocal"
Parsing properties file "/w0/tmp/slurm_tq429871.4967067/tmphwgogyn7prism_from-umb_check_ex_eajs.5-250-11_tmp_indir_/property.props"...
1 property:
(1) "ExpUtil": R{"utilityLocal"}max=? [ F "emptyBattery" ]
---------------------------------------------------------------------
Model checking: "ExpUtil": R{"utilityLocal"}max=? [ F "emptyBattery" ]
Building model (engine:explicit)...
Time for model construction: 0.617 seconds.
Type: MDP
States: 3049471 (1 initial)
Transitions: 6977654
Choices: 4256193
Max/avg: 10/1.40
Building reward structure...
Starting expected reachability (max)...
Starting Prob1 (min)...
Prob1 (min) took 250 iterations and 6.887 seconds.
target=13476, inf=0, rest=3035995
Starting value iteration (max, with Power method)...
Iteration 108: 5.05 sec so far
Value iteration (max, with Power method) took 128 iterations, 889190656 multiplications and 6.167 seconds.
Expected reachability took 13.089 seconds.
Value in the initial state: 10.03294060879421
Time for model checking: 13.28 seconds.
Result: 10.03294060879421 (+/- 7.366891075164757E-5 estimated; rel err 7.342703761953329E-6)
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_eajs.5-250-11_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 14.880 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:52:54 GMT+02:00 2026
Hostname: r23m0204.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4967020/tmpfqrf_ejgprism_from-umb_check_ex_eajs.5-250-11_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4967020/tmpfqrf_ejgprism_from-umb_check_ex_eajs.5-250-11_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: MDP
Actions: [tick]
Variables: x
Labels: "emptyBattery"
Rewards: "utilityLocal"
Parsing properties file "/w0/tmp/slurm_tq429871.4967020/tmpfqrf_ejgprism_from-umb_check_ex_eajs.5-250-11_tmp_indir_/property.props"...
1 property:
(1) "ExpUtil": R{"utilityLocal"}max=? [ F "emptyBattery" ]
---------------------------------------------------------------------
Model checking: "ExpUtil": R{"utilityLocal"}max=? [ F "emptyBattery" ]
Building model (engine:explicit)...
Time for model construction: 0.63 seconds.
Type: MDP
States: 3049471 (1 initial)
Transitions: 6977654
Choices: 4256193
Max/avg: 10/1.40
Building reward structure...
Starting expected reachability (max)...
Starting Prob1 (min)...
Prob1 (min) took 250 iterations and 7.137 seconds.
target=13476, inf=0, rest=3035995
Starting value iteration (max, with Power method)...
Iteration 106: 5.02 sec so far
Value iteration (max, with Power method) took 128 iterations, 889190656 multiplications and 6.248 seconds.
Expected reachability took 13.411 seconds.
Value in the initial state: 10.03294060879421
Time for model checking: 13.593 seconds.
Result: 10.03294060879421 (+/- 7.366891075164757E-5 estimated; rel err 7.342703761953329E-6)
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-umb_check_ex_eajs.5-250-11_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex -importmodel %indir/prism.model.umb %indir/property.props
Wallclock time: 17.502 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:34:50 GMT+02:00 2026
Hostname: n23m0135.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex -importmodel /w0/tmp/slurm_tq429871.4962606/tmphu32fvzmprism_from-umb_check_ex_eajs.5-250-11_tmp_indir_/prism.model.umb /w0/tmp/slurm_tq429871.4962606/tmphu32fvzmprism_from-umb_check_ex_eajs.5-250-11_tmp_indir_/property.props
Importing model from "prism.model.umb"...
Type: MDP
Actions: [tick]
Variables: x
Labels: "emptyBattery"
Rewards: "utilityLocal"
Parsing properties file "/w0/tmp/slurm_tq429871.4962606/tmphu32fvzmprism_from-umb_check_ex_eajs.5-250-11_tmp_indir_/property.props"...
1 property:
(1) "ExpUtil": R{"utilityLocal"}max=? [ F "emptyBattery" ]
---------------------------------------------------------------------
Model checking: "ExpUtil": R{"utilityLocal"}max=? [ F "emptyBattery" ]
Building model (engine:explicit)...
Time for model construction: 0.723 seconds.
Type: MDP
States: 3049471 (1 initial)
Transitions: 6977654
Choices: 4256193
Max/avg: 10/1.40
Building reward structure...
Starting expected reachability (max)...
Starting Prob1 (min)...
Prob1 (min) took 250 iterations and 8.111 seconds.
target=13476, inf=0, rest=3035995
Starting value iteration (max, with Power method)...
Iteration 89: 5.06 sec so far
Value iteration (max, with Power method) took 128 iterations, 889190656 multiplications and 7.673 seconds.
Expected reachability took 15.819 seconds.
Value in the initial state: 10.03294060879421
Time for model checking: 16.027 seconds.
Result: 10.03294060879421 (+/- 7.366891075164757E-5 estimated; rel err 7.342703761953329E-6)
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g