Log files for model csma.3-4 and tool configuration storm_from-umb_check_sparse
[0.423, 1.445, 0.456, 0.543, 0.454]
Log file: storm_from-umb_check_sparse_csma.3-4_rep1.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 0.423 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:25:58 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4962221/tmpj1qhh1ptstorm_from-umb_check_sparse_csma.3-4_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4962221/tmpj1qhh1ptstorm_from-umb_check_sparse_csma.3-4_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.058s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 1460287
Transitions: 2396727
Choices: 1471059
Reward Models: none
State Labels: 4 labels
* deadlock -> 0 item(s)
* collision_max_backoff -> 1427 item(s)
* all_delivered -> 13 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "all_before_max": Pmax=? [(!"collision_max_backoff") U "all_delivered"] ...
Result (for initial states): 0.9324469288
Time for model checking: 0.343s.
Performance statistics:
* peak memory usage: 229MB
* CPU time: 0.359s
* wallclock time: 0.402s
Log file: storm_from-umb_check_sparse_csma.3-4_rep2.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 1.445 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:24:21 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4962141/tmpdu5ekb1astorm_from-umb_check_sparse_csma.3-4_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4962141/tmpdu5ekb1astorm_from-umb_check_sparse_csma.3-4_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.057s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 1460287
Transitions: 2396727
Choices: 1471059
Reward Models: none
State Labels: 4 labels
* deadlock -> 0 item(s)
* collision_max_backoff -> 1427 item(s)
* all_delivered -> 13 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "all_before_max": Pmax=? [(!"collision_max_backoff") U "all_delivered"] ...
Result (for initial states): 0.9324469288
Time for model checking: 0.350s.
Performance statistics:
* peak memory usage: 229MB
* CPU time: 0.357s
* wallclock time: 0.410s
Log file: storm_from-umb_check_sparse_csma.3-4_rep3.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 0.456 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.4961184/tmpc83du4rcstorm_from-umb_check_sparse_csma.3-4_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4961184/tmpc83du4rcstorm_from-umb_check_sparse_csma.3-4_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.061s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 1460287
Transitions: 2396727
Choices: 1471059
Reward Models: none
State Labels: 4 labels
* deadlock -> 0 item(s)
* collision_max_backoff -> 1427 item(s)
* all_delivered -> 13 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "all_before_max": Pmax=? [(!"collision_max_backoff") U "all_delivered"] ...
Result (for initial states): 0.9324469288
Time for model checking: 0.369s.
Performance statistics:
* peak memory usage: 229MB
* CPU time: 0.377s
* wallclock time: 0.432s
Log file: storm_from-umb_check_sparse_csma.3-4_rep4.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 0.543 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 09:06:33 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4964774/tmpq170ega0storm_from-umb_check_sparse_csma.3-4_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4964774/tmpq170ega0storm_from-umb_check_sparse_csma.3-4_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.066s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 1460287
Transitions: 2396727
Choices: 1471059
Reward Models: none
State Labels: 4 labels
* deadlock -> 0 item(s)
* collision_max_backoff -> 1427 item(s)
* all_delivered -> 13 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "all_before_max": Pmax=? [(!"collision_max_backoff") U "all_delivered"] ...
Result (for initial states): 0.9324469288
Time for model checking: 0.444s.
Performance statistics:
* peak memory usage: 229MB
* CPU time: 0.454s
* wallclock time: 0.513s
Log file: storm_from-umb_check_sparse_csma.3-4_rep5.log
Command(s):
../bin/storm --timemem --buildfull --explicit-umb %indir/storm.model.umb --prop %indir/property.props
Wallclock time: 0.454 seconds
Return code: 0
##############################
Storm 1.14.0 (dev)
Date: Tue Oct 13 07:24:51 2026
Command line arguments: --timemem --buildfull --explicit-umb /w0/tmp/slurm_tq429871.4962159/tmpq0bky8k9storm_from-umb_check_sparse_csma.3-4_tmp_indir_/storm.model.umb --prop /w0/tmp/slurm_tq429871.4962159/tmpq0bky8k9storm_from-umb_check_sparse_csma.3-4_tmp_indir_/property.props
Current working directory: /rwthfs/rz/cluster/hpcwork/rwth1632/umb-benchmarking/experiments
Time for model construction: 0.056s.
--------------------------------------------------------------
Model type: MDP (sparse)
States: 1460287
Transitions: 2396727
Choices: 1471059
Reward Models: none
State Labels: 4 labels
* deadlock -> 0 item(s)
* collision_max_backoff -> 1427 item(s)
* all_delivered -> 13 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "all_before_max": Pmax=? [(!"collision_max_backoff") U "all_delivered"] ...
Result (for initial states): 0.9324469288
Time for model checking: 0.375s.
Performance statistics:
* peak memory usage: 230MB
* CPU time: 0.392s
* wallclock time: 0.433s