Log files for model eajs.6-300-13 and tool configuration storm_from-umb_check_sparse
[5.754, 4.936, 5.668, 5.819, 6.061]
Log file: storm_from-umb_check_sparse_eajs.6-300-13_rep1.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 5.754 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:20:13 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4965392/tmpbbux1rv7storm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4965392/tmpbbux1rv7storm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.524s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 7901694
Transitions: 19722777
Choices: 11897412
Reward Models: utilityLocal
State Labels: 3 labels
* emptyBattery -> 28620 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): 12.05111082
Time for model checking: 4.370s.
Performance statistics:
* peak memory usage: 2134MB
* CPU time: 4.423s
* wallclock time: 4.920s
Log file: storm_from-umb_check_sparse_eajs.6-300-13_rep2.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 4.936 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:54:32 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4967094/tmpdoicpze3storm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4967094/tmpdoicpze3storm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.506s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 7901694
Transitions: 19722777
Choices: 11897412
Reward Models: utilityLocal
State Labels: 3 labels
* emptyBattery -> 28620 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): 12.05111082
Time for model checking: 4.376s.
Performance statistics:
* peak memory usage: 2134MB
* CPU time: 4.402s
* wallclock time: 4.906s
Log file: storm_from-umb_check_sparse_eajs.6-300-13_rep3.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 5.668 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:39:38 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4966407/tmp1uh16ob4storm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4966407/tmp1uh16ob4storm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.514s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 7901694
Transitions: 19722777
Choices: 11897412
Reward Models: utilityLocal
State Labels: 3 labels
* emptyBattery -> 28620 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): 12.05111082
Time for model checking: 5.096s.
Performance statistics:
* peak memory usage: 2134MB
* CPU time: 5.137s
* wallclock time: 5.637s
Log file: storm_from-umb_check_sparse_eajs.6-300-13_rep4.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 5.819 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:49:37 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4966843/tmpe3a5s43mstorm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4966843/tmpe3a5s43mstorm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.530s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 7901694
Transitions: 19722777
Choices: 11897412
Reward Models: utilityLocal
State Labels: 3 labels
* emptyBattery -> 28620 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): 12.05111082
Time for model checking: 5.227s.
Performance statistics:
* peak memory usage: 2135MB
* CPU time: 5.283s
* wallclock time: 5.784s
Log file: storm_from-umb_check_sparse_eajs.6-300-13_rep5.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 6.061 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:32:18 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4966069/tmpgvhu1n1hstorm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4966069/tmpgvhu1n1hstorm_from-umb_check_sparse_eajs.6-300-13_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.646s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 7901694
Transitions: 19722777
Choices: 11897412
Reward Models: utilityLocal
State Labels: 3 labels
* emptyBattery -> 28620 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): 12.05111082
Time for model checking: 5.223s.
Performance statistics:
* peak memory usage: 2135MB
* CPU time: 5.271s
* wallclock time: 5.903s