Log files for model kanban.5 and tool configuration storm_from-umb_check_sparse
[0.417, 0.448, 0.473, 0.45, 0.46]
Log file: storm_from-umb_check_sparse_kanban.5_rep1.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 8.953 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 08:59:12 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4964396/tmpzjycss_4storm_from-umb_check_sparse_kanban.5_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4964396/tmpzjycss_4storm_from-umb_check_sparse_kanban.5_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.417s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 2546432
Transitions: 24460016
Reward Models: throughput
State Labels: 2 labels
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "throughput": R{"throughput"}=? [LRA] ...
Result (for initial states): 0.307124777
Time for model checking: 8.505s.
Performance statistics:
* peak memory usage: 2910MB
* CPU time: 8.375s
* wallclock time: 8.929s
Log file: storm_from-umb_check_sparse_kanban.5_rep2.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 9.422 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:01:40 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4961219/tmpjgbatqthstorm_from-umb_check_sparse_kanban.5_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4961219/tmpjgbatqthstorm_from-umb_check_sparse_kanban.5_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.448s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 2546432
Transitions: 24460016
Reward Models: throughput
State Labels: 2 labels
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "throughput": R{"throughput"}=? [LRA] ...
Result (for initial states): 0.307124777
Time for model checking: 8.939s.
Performance statistics:
* peak memory usage: 2910MB
* CPU time: 8.793s
* wallclock time: 9.394s
Log file: storm_from-umb_check_sparse_kanban.5_rep3.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 11.604 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:03:27 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4964633/tmpyomxmtshstorm_from-umb_check_sparse_kanban.5_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4964633/tmpyomxmtshstorm_from-umb_check_sparse_kanban.5_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.473s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 2546432
Transitions: 24460016
Reward Models: throughput
State Labels: 2 labels
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "throughput": R{"throughput"}=? [LRA] ...
Result (for initial states): 0.307124777
Time for model checking: 11.097s.
Performance statistics:
* peak memory usage: 2910MB
* CPU time: 10.805s
* wallclock time: 11.578s
Log file: storm_from-umb_check_sparse_kanban.5_rep4.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 9.454 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:48:01 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4963214/tmpfet7pj15storm_from-umb_check_sparse_kanban.5_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4963214/tmpfet7pj15storm_from-umb_check_sparse_kanban.5_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.450s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 2546432
Transitions: 24460016
Reward Models: throughput
State Labels: 2 labels
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "throughput": R{"throughput"}=? [LRA] ...
Result (for initial states): 0.307124777
Time for model checking: 8.972s.
Performance statistics:
* peak memory usage: 2910MB
* CPU time: 8.858s
* wallclock time: 9.429s
Log file: storm_from-umb_check_sparse_kanban.5_rep5.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 10.927 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:21:15 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4965434/tmptcmfx0ywstorm_from-umb_check_sparse_kanban.5_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4965434/tmptcmfx0ywstorm_from-umb_check_sparse_kanban.5_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.460s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 2546432
Transitions: 24460016
Reward Models: throughput
State Labels: 2 labels
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "throughput": R{"throughput"}=? [LRA] ...
Result (for initial states): 0.307124777
Time for model checking: 10.428s.
Performance statistics:
* peak memory usage: 2910MB
* CPU time: 10.195s
* wallclock time: 10.896s