Log files for model resource-gathering.1300-100-100 and tool configuration prism_from-prism_check_ex
[33.67, 33.406, 33.762, 33.682, 30.68]
Log file: prism_from-prism_check_ex_resource-gathering.1300-100-100_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 33.670 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:27:38 GMT+02:00 2026
Hostname: n23m0045.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4962292/tmpg0mfmj7cprism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4962292/tmpg0mfmj7cprism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4962292/tmpg0mfmj7cprism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/model.prism"...
Type: MDP
Modules: robot goldcounter gemcounter
Actions: [right] [left] [top] [down]
Variables: gold gem attacked x y required_gold required_gem
Labels: "success"
Parsing properties file "/w0/tmp/slurm_tq429871.4962292/tmpg0mfmj7cprism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/property.props"...
1 property:
(1) "prgoldgem": Pmax=? [ F<=1300 "success" ]
---------------------------------------------------------------------
Model checking: "prgoldgem": Pmax=? [ F<=1300 "success" ]
Building model (engine:explicit)...
Computing reachable states... 404276 782032 958894 states
Reachable states exploration and model construction done in 7.402 secs.
Sorting reachable states list...
Time for model construction: 8.906 seconds.
Type: MDP
States: 958894 (1 initial)
Transitions: 3325526
Choices: 3080702
Max/avg: 4/3.21
Starting bounded probabilistic reachability (max)...
Bounded probabilistic reachability (max) took 1300 iterations and 24.056 seconds.
Value in the initial state: 0.6630608525241822
Time for model checking: 24.089 seconds.
Result: 0.6630608525241822 (exact floating point)
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_resource-gathering.1300-100-100_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 33.406 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:32:49 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 /w0/tmp/slurm_tq429871.4966092/tmpotzbnr22prism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4966092/tmpotzbnr22prism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4966092/tmpotzbnr22prism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/model.prism"...
Type: MDP
Modules: robot goldcounter gemcounter
Actions: [right] [left] [top] [down]
Variables: gold gem attacked x y required_gold required_gem
Labels: "success"
Parsing properties file "/w0/tmp/slurm_tq429871.4966092/tmpotzbnr22prism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/property.props"...
1 property:
(1) "prgoldgem": Pmax=? [ F<=1300 "success" ]
---------------------------------------------------------------------
Model checking: "prgoldgem": Pmax=? [ F<=1300 "success" ]
Building model (engine:explicit)...
Computing reachable states... 397012 760769 958894 states
Reachable states exploration and model construction done in 7.936 secs.
Sorting reachable states list...
Time for model construction: 9.538 seconds.
Type: MDP
States: 958894 (1 initial)
Transitions: 3325526
Choices: 3080702
Max/avg: 4/3.21
Starting bounded probabilistic reachability (max)...
Bounded probabilistic reachability (max) took 1300 iterations and 23.2 seconds.
Value in the initial state: 0.6630608525241822
Time for model checking: 23.233 seconds.
Result: 0.6630608525241822 (exact floating point)
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_resource-gathering.1300-100-100_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 33.762 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 09:24:22 GMT+02:00 2026
Hostname: r23m0206.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4965658/tmp7f79a44lprism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4965658/tmp7f79a44lprism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4965658/tmp7f79a44lprism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/model.prism"...
Type: MDP
Modules: robot goldcounter gemcounter
Actions: [right] [left] [top] [down]
Variables: gold gem attacked x y required_gold required_gem
Labels: "success"
Parsing properties file "/w0/tmp/slurm_tq429871.4965658/tmp7f79a44lprism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/property.props"...
1 property:
(1) "prgoldgem": Pmax=? [ F<=1300 "success" ]
---------------------------------------------------------------------
Model checking: "prgoldgem": Pmax=? [ F<=1300 "success" ]
Building model (engine:explicit)...
Computing reachable states... 404575 768581 958894 states
Reachable states exploration and model construction done in 7.491 secs.
Sorting reachable states list...
Time for model construction: 9.035 seconds.
Type: MDP
States: 958894 (1 initial)
Transitions: 3325526
Choices: 3080702
Max/avg: 4/3.21
Starting bounded probabilistic reachability (max)...
Bounded probabilistic reachability (max) took 1300 iterations and 24.066 seconds.
Value in the initial state: 0.6630608525241822
Time for model checking: 24.1 seconds.
Result: 0.6630608525241822 (exact floating point)
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_resource-gathering.1300-100-100_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 33.682 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 07:04:24 GMT+02:00 2026
Hostname: n23m0047.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4961329/tmpbd9cw1kcprism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4961329/tmpbd9cw1kcprism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4961329/tmpbd9cw1kcprism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/model.prism"...
Type: MDP
Modules: robot goldcounter gemcounter
Actions: [right] [left] [top] [down]
Variables: gold gem attacked x y required_gold required_gem
Labels: "success"
Parsing properties file "/w0/tmp/slurm_tq429871.4961329/tmpbd9cw1kcprism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/property.props"...
1 property:
(1) "prgoldgem": Pmax=? [ F<=1300 "success" ]
---------------------------------------------------------------------
Model checking: "prgoldgem": Pmax=? [ F<=1300 "success" ]
Building model (engine:explicit)...
Computing reachable states... 409941 780034 958894 states
Reachable states exploration and model construction done in 7.386 secs.
Sorting reachable states list...
Time for model construction: 8.885 seconds.
Type: MDP
States: 958894 (1 initial)
Transitions: 3325526
Choices: 3080702
Max/avg: 4/3.21
Starting bounded probabilistic reachability (max)...
Bounded probabilistic reachability (max) took 1300 iterations and 24.063 seconds.
Value in the initial state: 0.6630608525241822
Time for model checking: 24.119 seconds.
Result: 0.6630608525241822 (exact floating point)
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
Log file: prism_from-prism_check_ex_resource-gathering.1300-100-100_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 30.680 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Tue Oct 13 08:55:32 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.4964196/tmprp8efu_uprism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4964196/tmprp8efu_uprism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/property.props
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4964196/tmprp8efu_uprism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/model.prism"...
Type: MDP
Modules: robot goldcounter gemcounter
Actions: [right] [left] [top] [down]
Variables: gold gem attacked x y required_gold required_gem
Labels: "success"
Parsing properties file "/w0/tmp/slurm_tq429871.4964196/tmprp8efu_uprism_from-prism_check_ex_resource-gathering.1300-100-100_tmp_indir_/property.props"...
1 property:
(1) "prgoldgem": Pmax=? [ F<=1300 "success" ]
---------------------------------------------------------------------
Model checking: "prgoldgem": Pmax=? [ F<=1300 "success" ]
Building model (engine:explicit)...
Computing reachable states... 433667 836153 958894 states
Reachable states exploration and model construction done in 6.922 secs.
Sorting reachable states list...
Time for model construction: 8.378 seconds.
Type: MDP
States: 958894 (1 initial)
Transitions: 3325526
Choices: 3080702
Max/avg: 4/3.21
Starting bounded probabilistic reachability (max)...
Bounded probabilistic reachability (max) took 1300 iterations and 21.667 seconds.
Value in the initial state: 0.6630608525241822
Time for model checking: 21.697 seconds.
Result: 0.6630608525241822 (exact floating point)
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g