Log files for model wlan.6-0 and tool configuration storm_from-umb_check_sparse
[0.989, 1.056, 1.222, 0.95, 1.757]
Log file: storm_from-umb_check_sparse_wlan.6-0_rep1.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 0.989 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:36:28 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4966275/tmpzt_ucjaqstorm_from-umb_check_sparse_wlan.6-0_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4966275/tmpzt_ucjaqstorm_from-umb_check_sparse_wlan.6-0_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.239s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 5007548
Transitions: 11475748
Choices: 6350470
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.722s.
Performance statistics:
* peak memory usage: 634MB
* CPU time: 0.830s
* wallclock time: 0.965s
Log file: storm_from-umb_check_sparse_wlan.6-0_rep2.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 1.056 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:21:44 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4965444/tmpzb6x0vl_storm_from-umb_check_sparse_wlan.6-0_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4965444/tmpzb6x0vl_storm_from-umb_check_sparse_wlan.6-0_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.253s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 5007548
Transitions: 11475748
Choices: 6350470
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.774s.
Performance statistics:
* peak memory usage: 634MB
* CPU time: 0.872s
* wallclock time: 1.030s
Log file: storm_from-umb_check_sparse_wlan.6-0_rep3.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 1.222 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:05:30 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4961379/tmpr9zl1o6istorm_from-umb_check_sparse_wlan.6-0_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4961379/tmpr9zl1o6istorm_from-umb_check_sparse_wlan.6-0_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.237s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 5007548
Transitions: 11475748
Choices: 6350470
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.791s.
Performance statistics:
* peak memory usage: 634MB
* CPU time: 0.821s
* wallclock time: 1.035s
Log file: storm_from-umb_check_sparse_wlan.6-0_rep4.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 0.950 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:26:31 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4962234/tmpsb6ad8k6storm_from-umb_check_sparse_wlan.6-0_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4962234/tmpsb6ad8k6storm_from-umb_check_sparse_wlan.6-0_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.224s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 5007548
Transitions: 11475748
Choices: 6350470
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.698s.
Performance statistics:
* peak memory usage: 634MB
* CPU time: 0.799s
* wallclock time: 0.925s
Log file: storm_from-umb_check_sparse_wlan.6-0_rep5.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 1.757 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.4961220/tmp231g289vstorm_from-umb_check_sparse_wlan.6-0_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4961220/tmp231g289vstorm_from-umb_check_sparse_wlan.6-0_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.335s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 5007548
Transitions: 11475748
Choices: 6350470
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: 1.029s.
Performance statistics:
* peak memory usage: 634MB
* CPU time: 1.138s
* wallclock time: 1.369s