Log files for model wlan.6-0 and tool configuration modest_from-jani_check_default
[28.471, 26.963, 25.939, 25.894, 25.659]
Log file: modest_from-jani_check_default_wlan.6-0_rep1.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 28.471 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4962697/tmprhxxkei2modest_from-jani_check_default_wlan.6-0_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[3]: info: Expanding variable "s1" into 12 locations in automaton "station1".
model.jani:variables[4]: info: Expanding variable "s2" into 12 locations in automaton "station2".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 5007548 states.
Peak memory usage: 590 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 5007548
Choices: 6350470
Branches: 11475748
Rate: 413710 states/s
Peak memory: 255.83 MB
Final size: 223.56 MB
Size on disk: 41.24 MB
Time (exploration): 12.1 s
Time (merging): 0.8 s
+ Property sent
Result: True
Bounds: [1, 1]
Time: 15.2 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 15.2 s
Min. prob. 1 states: 5007548
Time for min. prob. 1 states: 0.0 s
Log file: modest_from-jani_check_default_wlan.6-0_rep2.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 26.963 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4967333/tmpaiib5h9kmodest_from-jani_check_default_wlan.6-0_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[3]: info: Expanding variable "s1" into 12 locations in automaton "station1".
model.jani:variables[4]: info: Expanding variable "s2" into 12 locations in automaton "station2".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 5007548 states.
Peak memory usage: 591 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 5007548
Choices: 6350470
Branches: 11475748
Rate: 453377 states/s
Peak memory: 255.71 MB
Final size: 223.56 MB
Size on disk: 41.24 MB
Time (exploration): 11.1 s
Time (merging): 0.7 s
+ Property sent
Result: True
Bounds: [1, 1]
Time: 14.8 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 14.7 s
Min. prob. 1 states: 5007548
Time for min. prob. 1 states: 0.0 s
Log file: modest_from-jani_check_default_wlan.6-0_rep3.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 25.939 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4967354/tmpb0ro4jhxmodest_from-jani_check_default_wlan.6-0_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[3]: info: Expanding variable "s1" into 12 locations in automaton "station1".
model.jani:variables[4]: info: Expanding variable "s2" into 12 locations in automaton "station2".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 5007548 states.
Peak memory usage: 590 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 5007548
Choices: 6350470
Branches: 11475748
Rate: 449914 states/s
Peak memory: 256.31 MB
Final size: 223.56 MB
Size on disk: 41.24 MB
Time (exploration): 11.2 s
Time (merging): 0.7 s
+ Property sent
Result: True
Bounds: [1, 1]
Time: 13.8 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 13.7 s
Min. prob. 1 states: 5007548
Time for min. prob. 1 states: 0.0 s
Log file: modest_from-jani_check_default_wlan.6-0_rep4.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 25.894 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4962604/tmppp295zclmodest_from-jani_check_default_wlan.6-0_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[3]: info: Expanding variable "s1" into 12 locations in automaton "station1".
model.jani:variables[4]: info: Expanding variable "s2" into 12 locations in automaton "station2".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 5007548 states.
Peak memory usage: 589 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 5007548
Choices: 6350470
Branches: 11475748
Rate: 458609 states/s
Peak memory: 256.38 MB
Final size: 223.56 MB
Size on disk: 41.24 MB
Time (exploration): 10.9 s
Time (merging): 0.7 s
+ Property sent
Result: True
Bounds: [1, 1]
Time: 13.9 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 13.9 s
Min. prob. 1 states: 5007548
Time for min. prob. 1 states: 0.0 s
Log file: modest_from-jani_check_default_wlan.6-0_rep5.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 25.659 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4965926/tmpkr0744ymmodest_from-jani_check_default_wlan.6-0_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[3]: info: Expanding variable "s1" into 12 locations in automaton "station1".
model.jani:variables[4]: info: Expanding variable "s2" into 12 locations in automaton "station2".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 5007548 states.
Peak memory usage: 590 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 5007548
Choices: 6350470
Branches: 11475748
Rate: 471387 states/s
Peak memory: 256.62 MB
Final size: 223.56 MB
Size on disk: 41.24 MB
Time (exploration): 10.6 s
Time (merging): 0.7 s
+ Property sent
Result: True
Bounds: [1, 1]
Time: 13.9 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 13.9 s
Min. prob. 1 states: 5007548
Time for min. prob. 1 states: 0.0 s