Log files for model eajs.5-250-11 and tool configuration storm_from-umb_check_sparse
[1.928, 1.818, 1.805, 1.737, 1.79]
Log file: storm_from-umb_check_sparse_eajs.5-250-11_rep1.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 1.928 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:27:04 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4962269/tmpbt7j046_storm_from-umb_check_sparse_eajs.5-250-11_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4962269/tmpbt7j046_storm_from-umb_check_sparse_eajs.5-250-11_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.192s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 3049471
Transitions: 6977654
Choices: 4256193
Reward Models: utilityLocal
State Labels: 3 labels
* emptyBattery -> 13476 item(s)
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "ExpUtil": R{"utilityLocal"}max=? [F "emptyBattery"] ...
Result (for initial states): 10.03294069
Time for model checking: 1.703s.
Performance statistics:
* peak memory usage: 796MB
* CPU time: 1.711s
* wallclock time: 1.905s
Log file: storm_from-umb_check_sparse_eajs.5-250-11_rep2.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 1.818 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:12:20 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4965035/tmphpk01_v6storm_from-umb_check_sparse_eajs.5-250-11_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4965035/tmphpk01_v6storm_from-umb_check_sparse_eajs.5-250-11_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.189s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 3049471
Transitions: 6977654
Choices: 4256193
Reward Models: utilityLocal
State Labels: 3 labels
* emptyBattery -> 13476 item(s)
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "ExpUtil": R{"utilityLocal"}max=? [F "emptyBattery"] ...
Result (for initial states): 10.03294069
Time for model checking: 1.592s.
Performance statistics:
* peak memory usage: 796MB
* CPU time: 1.619s
* wallclock time: 1.791s
Log file: storm_from-umb_check_sparse_eajs.5-250-11_rep3.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 1.805 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:36:29 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4966277/tmpmpl39m2bstorm_from-umb_check_sparse_eajs.5-250-11_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4966277/tmpmpl39m2bstorm_from-umb_check_sparse_eajs.5-250-11_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.187s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 3049471
Transitions: 6977654
Choices: 4256193
Reward Models: utilityLocal
State Labels: 3 labels
* emptyBattery -> 13476 item(s)
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "ExpUtil": R{"utilityLocal"}max=? [F "emptyBattery"] ...
Result (for initial states): 10.03294069
Time for model checking: 1.578s.
Performance statistics:
* peak memory usage: 796MB
* CPU time: 1.595s
* wallclock time: 1.774s
Log file: storm_from-umb_check_sparse_eajs.5-250-11_rep4.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 1.737 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:15:24 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4961798/tmp9ec2i6pzstorm_from-umb_check_sparse_eajs.5-250-11_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4961798/tmp9ec2i6pzstorm_from-umb_check_sparse_eajs.5-250-11_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.185s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 3049471
Transitions: 6977654
Choices: 4256193
Reward Models: utilityLocal
State Labels: 3 labels
* emptyBattery -> 13476 item(s)
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "ExpUtil": R{"utilityLocal"}max=? [F "emptyBattery"] ...
Result (for initial states): 10.03294069
Time for model checking: 1.513s.
Performance statistics:
* peak memory usage: 796MB
* CPU time: 1.555s
* wallclock time: 1.707s
Log file: storm_from-umb_check_sparse_eajs.5-250-11_rep5.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 1.790 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:15:29 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4965170/tmphynmfhbtstorm_from-umb_check_sparse_eajs.5-250-11_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4965170/tmphynmfhbtstorm_from-umb_check_sparse_eajs.5-250-11_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.192s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 3049471
Transitions: 6977654
Choices: 4256193
Reward Models: utilityLocal
State Labels: 3 labels
* emptyBattery -> 13476 item(s)
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "ExpUtil": R{"utilityLocal"}max=? [F "emptyBattery"] ...
Result (for initial states): 10.03294069
Time for model checking: 1.560s.
Performance statistics:
* peak memory usage: 796MB
* CPU time: 1.596s
* wallclock time: 1.762s