Log files for model wlan.6-0 and tool configuration modest_from-jani_import_default
[13.3, 11.5, 12.0, 13.3, 11.6]
Log file: modest_from-jani_import_default_wlan.6-0_rep1.log
Command(s):
../bin/modest mcsta %indir/model.jani --stop-after Exploration -D -Y --exhaustive
Wallclock time: 13.695 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4964206/tmpy4izeki6modest_from-jani_import_default_wlan.6-0_tmp_indir_/model.jani --stop-after Exploration -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: 401729 states/s
Peak memory: 254.77 MB
Final size: 223.56 MB
Size on disk: 41.24 MB
Time (exploration): 12.5 s
Time (merging): 0.8 s
Log file: modest_from-jani_import_default_wlan.6-0_rep2.log
Command(s):
../bin/modest mcsta %indir/model.jani --stop-after Exploration -D -Y --exhaustive
Wallclock time: 11.894 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4961367/tmpgfxdynxdmodest_from-jani_import_default_wlan.6-0_tmp_indir_/model.jani --stop-after Exploration -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: 464049 states/s
Peak memory: 256.15 MB
Final size: 223.56 MB
Size on disk: 41.24 MB
Time (exploration): 10.8 s
Time (merging): 0.7 s
Log file: modest_from-jani_import_default_wlan.6-0_rep3.log
Command(s):
../bin/modest mcsta %indir/model.jani --stop-after Exploration -D -Y --exhaustive
Wallclock time: 12.392 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4966858/tmp2ajwx998modest_from-jani_import_default_wlan.6-0_tmp_indir_/model.jani --stop-after Exploration -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: 444562 states/s
Peak memory: 256.01 MB
Final size: 223.56 MB
Size on disk: 41.24 MB
Time (exploration): 11.3 s
Time (merging): 0.7 s
Log file: modest_from-jani_import_default_wlan.6-0_rep4.log
Command(s):
../bin/modest mcsta %indir/model.jani --stop-after Exploration -D -Y --exhaustive
Wallclock time: 13.725 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4962853/tmpv63bp9wdmodest_from-jani_import_default_wlan.6-0_tmp_indir_/model.jani --stop-after Exploration -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: 401310 states/s
Peak memory: 255.92 MB
Final size: 223.56 MB
Size on disk: 41.24 MB
Time (exploration): 12.5 s
Time (merging): 0.8 s
Log file: modest_from-jani_import_default_wlan.6-0_rep5.log
Command(s):
../bin/modest mcsta %indir/model.jani --stop-after Exploration -D -Y --exhaustive
Wallclock time: 12.041 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4964676/tmp4z2r2rfhmodest_from-jani_import_default_wlan.6-0_tmp_indir_/model.jani --stop-after Exploration -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: 458777 states/s
Peak memory: 255.71 MB
Final size: 223.56 MB
Size on disk: 41.24 MB
Time (exploration): 10.9 s
Time (merging): 0.7 s