Log files for model cluster.128-2000-20 and tool configuration storm_from-umb_check_sparse
[50.832, 51.768, 46.096, 41.066, 48.821]
Log file: storm_from-umb_check_sparse_cluster.128-2000-20_rep1.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 50.832 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:29:18 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4962362/tmpnv2zxh7_storm_from-umb_check_sparse_cluster.128-2000-20_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4962362/tmpnv2zxh7_storm_from-umb_check_sparse_cluster.128-2000-20_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.085s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 597012
Transitions: 2908192
Reward Models: none
State Labels: 3 labels
* minimum -> 141117 item(s)
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "qos1": P=? [true U<=2000 (!"minimum")] ...
Result (for initial states): 0.001072402534
Time for model checking: 50.712s.
Performance statistics:
* peak memory usage: 175MB
* CPU time: 50.530s
* wallclock time: 50.799s
Log file: storm_from-umb_check_sparse_cluster.128-2000-20_rep2.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 51.768 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:42:00 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4962927/tmpui8cplpsstorm_from-umb_check_sparse_cluster.128-2000-20_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4962927/tmpui8cplpsstorm_from-umb_check_sparse_cluster.128-2000-20_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.064s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 597012
Transitions: 2908192
Reward Models: none
State Labels: 3 labels
* minimum -> 141117 item(s)
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "qos1": P=? [true U<=2000 (!"minimum")] ...
Result (for initial states): 0.001072402534
Time for model checking: 51.675s.
Performance statistics:
* peak memory usage: 175MB
* CPU time: 51.493s
* wallclock time: 51.741s
Log file: storm_from-umb_check_sparse_cluster.128-2000-20_rep3.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 46.096 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:10:15 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4964934/tmpn8evrpevstorm_from-umb_check_sparse_cluster.128-2000-20_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4964934/tmpn8evrpevstorm_from-umb_check_sparse_cluster.128-2000-20_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.063s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 597012
Transitions: 2908192
Reward Models: none
State Labels: 3 labels
* minimum -> 141117 item(s)
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "qos1": P=? [true U<=2000 (!"minimum")] ...
Result (for initial states): 0.001072402534
Time for model checking: 46.003s.
Performance statistics:
* peak memory usage: 175MB
* CPU time: 45.818s
* wallclock time: 46.068s
Log file: storm_from-umb_check_sparse_cluster.128-2000-20_rep4.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 41.066 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:44:22 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4966648/tmp7ob2xtbzstorm_from-umb_check_sparse_cluster.128-2000-20_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4966648/tmp7ob2xtbzstorm_from-umb_check_sparse_cluster.128-2000-20_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.064s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 597012
Transitions: 2908192
Reward Models: none
State Labels: 3 labels
* minimum -> 141117 item(s)
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "qos1": P=? [true U<=2000 (!"minimum")] ...
Result (for initial states): 0.001072402534
Time for model checking: 40.348s.
Performance statistics:
* peak memory usage: 174MB
* CPU time: 40.236s
* wallclock time: 40.470s
Log file: storm_from-umb_check_sparse_cluster.128-2000-20_rep5.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 48.821 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:01:07 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4961193/tmpkd1in3jpstorm_from-umb_check_sparse_cluster.128-2000-20_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4961193/tmpkd1in3jpstorm_from-umb_check_sparse_cluster.128-2000-20_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.062s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 597012
Transitions: 2908192
Reward Models: none
State Labels: 3 labels
* minimum -> 141117 item(s)
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "qos1": P=? [true U<=2000 (!"minimum")] ...
Result (for initial states): 0.001072402534
Time for model checking: 48.731s.
Performance statistics:
* peak memory usage: 175MB
* CPU time: 48.580s
* wallclock time: 48.796s