Log files for model cluster.64-2000-20 and tool configuration storm_from-umb_check_sparse
[0.018, 0.018, 0.018, 0.016, 0.018]
Log file: storm_from-umb_check_sparse_cluster.64-2000-20_rep1.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 9.859 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:10:45 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4964956/tmphv4ecza6storm_from-umb_check_sparse_cluster.64-2000-20_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4964956/tmphv4ecza6storm_from-umb_check_sparse_cluster.64-2000-20_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.018s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 151060
Transitions: 733216
Reward Models: none
State Labels: 3 labels
* minimum -> 36133 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.001044539673
Time for model checking: 9.812s.
Performance statistics:
* peak memory usage: 59MB
* CPU time: 9.791s
* wallclock time: 9.832s
Log file: storm_from-umb_check_sparse_cluster.64-2000-20_rep2.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 9.874 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:27:32 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4965835/tmp_p8wofjcstorm_from-umb_check_sparse_cluster.64-2000-20_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4965835/tmp_p8wofjcstorm_from-umb_check_sparse_cluster.64-2000-20_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.018s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 151060
Transitions: 733216
Reward Models: none
State Labels: 3 labels
* minimum -> 36133 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.001044539673
Time for model checking: 9.833s.
Performance statistics:
* peak memory usage: 59MB
* CPU time: 9.825s
* wallclock time: 9.852s
Log file: storm_from-umb_check_sparse_cluster.64-2000-20_rep3.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 10.402 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:41:11 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4966471/tmprf67nup7storm_from-umb_check_sparse_cluster.64-2000-20_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4966471/tmprf67nup7storm_from-umb_check_sparse_cluster.64-2000-20_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.018s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 151060
Transitions: 733216
Reward Models: none
State Labels: 3 labels
* minimum -> 36133 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.001044539673
Time for model checking: 10.356s.
Performance statistics:
* peak memory usage: 59MB
* CPU time: 10.333s
* wallclock time: 10.376s
Log file: storm_from-umb_check_sparse_cluster.64-2000-20_rep4.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 8.973 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:30:23 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4962399/tmpxi4nmbagstorm_from-umb_check_sparse_cluster.64-2000-20_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4962399/tmpxi4nmbagstorm_from-umb_check_sparse_cluster.64-2000-20_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.016s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 151060
Transitions: 733216
Reward Models: none
State Labels: 3 labels
* minimum -> 36133 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.001044539673
Time for model checking: 8.934s.
Performance statistics:
* peak memory usage: 59MB
* CPU time: 8.927s
* wallclock time: 8.951s
Log file: storm_from-umb_check_sparse_cluster.64-2000-20_rep5.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 10.672 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:23:11 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4962094/tmp8ipam1olstorm_from-umb_check_sparse_cluster.64-2000-20_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4962094/tmp8ipam1olstorm_from-umb_check_sparse_cluster.64-2000-20_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.018s.
--------------------------------------------------------------
Model type: CTMC (sparse)
States: 151060
Transitions: 733216
Reward Models: none
State Labels: 3 labels
* minimum -> 36133 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.001044539673
Time for model checking: 10.626s.
Performance statistics:
* peak memory usage: 59MB
* CPU time: 10.592s
* wallclock time: 10.645s