Log files for model fms.8 and tool configuration storm_from-umb_check_sparse
[10.896, 12.237, 13.054, 10.508, 9.407]
Log file: storm_from-umb_check_sparse_fms.8_rep1.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 10.896 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:50:42 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4966909/tmp7xefqrd3storm_from-umb_check_sparse_fms.8_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4966909/tmp7xefqrd3storm_from-umb_check_sparse_fms.8_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.703s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 4459455
Transitions: 38533968
Reward Models: productivity
State Labels: 2 labels
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "productivity": R{"productivity"}=? [LRA] ...
Result (for initial states): 116.6583013
Time for model checking: 10.157s.
Performance statistics:
* peak memory usage: 4856MB
* CPU time: 9.403s
* wallclock time: 10.872s
Log file: storm_from-umb_check_sparse_fms.8_rep2.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 12.237 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:27:33 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4965828/tmpsuti3zh2storm_from-umb_check_sparse_fms.8_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4965828/tmpsuti3zh2storm_from-umb_check_sparse_fms.8_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.749s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 4459455
Transitions: 38533968
Reward Models: productivity
State Labels: 2 labels
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "productivity": R{"productivity"}=? [LRA] ...
Result (for initial states): 116.6583013
Time for model checking: 11.444s.
Performance statistics:
* peak memory usage: 4857MB
* CPU time: 11.057s
* wallclock time: 12.205s
Log file: storm_from-umb_check_sparse_fms.8_rep3.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 13.054 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:12:54 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4965067/tmpfqjd3mg8storm_from-umb_check_sparse_fms.8_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4965067/tmpfqjd3mg8storm_from-umb_check_sparse_fms.8_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.834s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 4459455
Transitions: 38533968
Reward Models: productivity
State Labels: 2 labels
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "productivity": R{"productivity"}=? [LRA] ...
Result (for initial states): 116.6583013
Time for model checking: 12.175s.
Performance statistics:
* peak memory usage: 4857MB
* CPU time: 11.579s
* wallclock time: 13.021s
Log file: storm_from-umb_check_sparse_fms.8_rep4.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 10.508 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:00:34 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4961147/tmpjetw7ggvstorm_from-umb_check_sparse_fms.8_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4961147/tmpjetw7ggvstorm_from-umb_check_sparse_fms.8_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.734s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 4459455
Transitions: 38533968
Reward Models: productivity
State Labels: 2 labels
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "productivity": R{"productivity"}=? [LRA] ...
Result (for initial states): 116.6583013
Time for model checking: 9.730s.
Performance statistics:
* peak memory usage: 4857MB
* CPU time: 9.406s
* wallclock time: 10.477s
Log file: storm_from-umb_check_sparse_fms.8_rep5.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 9.407 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:43:39 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4962995/tmp7hn9o22cstorm_from-umb_check_sparse_fms.8_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4962995/tmp7hn9o22cstorm_from-umb_check_sparse_fms.8_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.649s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 4459455
Transitions: 38533968
Reward Models: productivity
State Labels: 2 labels
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "productivity": R{"productivity"}=? [LRA] ...
Result (for initial states): 116.6583013
Time for model checking: 8.722s.
Performance statistics:
* peak memory usage: 4856MB
* CPU time: 8.431s
* wallclock time: 9.381s