Log files for model wlan.5-0 and tool configuration storm_from-umb_check_sparse
[0.239, 0.242, 0.27, 0.259, 0.267]
Log file: storm_from-umb_check_sparse_wlan.5-0_rep1.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 0.239 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:10:25 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4961571/tmpwi0nkmkvstorm_from-umb_check_sparse_wlan.5-0_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4961571/tmpwi0nkmkvstorm_from-umb_check_sparse_wlan.5-0_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.060s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 1295218
Transitions: 2929960
Choices: 1646074
Reward Models: none
State Labels: 3 labels
* target -> 1 item(s)
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "sent": P>=1 [F "target"] ...
Result (for initial states): true
Time for model checking: 0.156s.
Performance statistics:
* peak memory usage: 177MB
* CPU time: 0.188s
* wallclock time: 0.218s
Log file: storm_from-umb_check_sparse_wlan.5-0_rep2.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 0.242 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:23:18 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4965555/tmpmgykbqw0storm_from-umb_check_sparse_wlan.5-0_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4965555/tmpmgykbqw0storm_from-umb_check_sparse_wlan.5-0_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.065s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 1295218
Transitions: 2929960
Choices: 1646074
Reward Models: none
State Labels: 3 labels
* target -> 1 item(s)
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "sent": P>=1 [F "target"] ...
Result (for initial states): true
Time for model checking: 0.154s.
Performance statistics:
* peak memory usage: 177MB
* CPU time: 0.185s
* wallclock time: 0.222s
Log file: storm_from-umb_check_sparse_wlan.5-0_rep3.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 0.270 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:19:39 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4965363/tmpbwghqnjbstorm_from-umb_check_sparse_wlan.5-0_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4965363/tmpbwghqnjbstorm_from-umb_check_sparse_wlan.5-0_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.068s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 1295218
Transitions: 2929960
Choices: 1646074
Reward Models: none
State Labels: 3 labels
* target -> 1 item(s)
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "sent": P>=1 [F "target"] ...
Result (for initial states): true
Time for model checking: 0.176s.
Performance statistics:
* peak memory usage: 177MB
* CPU time: 0.208s
* wallclock time: 0.247s
Log file: storm_from-umb_check_sparse_wlan.5-0_rep4.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 0.259 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:02:46 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4961257/tmp3rvy3dcjstorm_from-umb_check_sparse_wlan.5-0_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4961257/tmp3rvy3dcjstorm_from-umb_check_sparse_wlan.5-0_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.067s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 1295218
Transitions: 2929960
Choices: 1646074
Reward Models: none
State Labels: 3 labels
* target -> 1 item(s)
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "sent": P>=1 [F "target"] ...
Result (for initial states): true
Time for model checking: 0.166s.
Performance statistics:
* peak memory usage: 177MB
* CPU time: 0.197s
* wallclock time: 0.236s
Log file: storm_from-umb_check_sparse_wlan.5-0_rep5.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 0.267 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:32:37 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4962503/tmp65fnlqewstorm_from-umb_check_sparse_wlan.5-0_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4962503/tmp65fnlqewstorm_from-umb_check_sparse_wlan.5-0_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.070s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 1295218
Transitions: 2929960
Choices: 1646074
Reward Models: none
State Labels: 3 labels
* target -> 1 item(s)
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "sent": P>=1 [F "target"] ...
Result (for initial states): true
Time for model checking: 0.170s.
Performance statistics:
* peak memory usage: 177MB
* CPU time: 0.204s
* wallclock time: 0.242s