Log files for model wlan.5-0 and tool configuration modest_from-jani_check_default
[3.0, 2.8, 2.4000000000000004, 2.8, 3.0]
Log file: modest_from-jani_check_default_wlan.5-0_rep1.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 5.660 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4966384/tmp2ttn1iuumodest_from-jani_check_default_wlan.5-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 1295218 states.
Peak memory usage: 237 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 1295218
Choices: 1646074
Branches: 2929960
Rate: 489685 states/s
Peak memory: 82.61 MB
Final size: 57.27 MB
Size on disk: 10.42 MB
Time (exploration): 2.7 s
Time (merging): 0.3 s
+ Property sent
Result: True
Bounds: [1, 1]
Time: 2.4 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 2.4 s
Min. prob. 1 states: 1295218
Time for min. prob. 1 states: 0.0 s
Log file: modest_from-jani_check_default_wlan.5-0_rep2.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 4.896 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4966844/tmpr0soly71modest_from-jani_check_default_wlan.5-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 1295218 states.
Peak memory usage: 237 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 1295218
Choices: 1646074
Branches: 2929960
Rate: 513161 states/s
Peak memory: 82.94 MB
Final size: 57.27 MB
Size on disk: 10.42 MB
Time (exploration): 2.5 s
Time (merging): 0.3 s
+ Property sent
Result: True
Bounds: [1, 1]
Time: 1.8 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 1.8 s
Min. prob. 1 states: 1295218
Time for min. prob. 1 states: 0.0 s
Log file: modest_from-jani_check_default_wlan.5-0_rep3.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 4.279 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4965989/tmply1xxs0umodest_from-jani_check_default_wlan.5-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 1295218 states.
Peak memory usage: 237 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 1295218
Choices: 1646074
Branches: 2929960
Rate: 594137 states/s
Peak memory: 83.01 MB
Final size: 57.27 MB
Size on disk: 10.42 MB
Time (exploration): 2.2 s
Time (merging): 0.2 s
+ Property sent
Result: True
Bounds: [1, 1]
Time: 1.6 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 1.6 s
Min. prob. 1 states: 1295218
Time for min. prob. 1 states: 0.0 s
Log file: modest_from-jani_check_default_wlan.5-0_rep4.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 4.850 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4961961/tmpepbk568mmodest_from-jani_check_default_wlan.5-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 1295218 states.
Peak memory usage: 237 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 1295218
Choices: 1646074
Branches: 2929960
Rate: 518295 states/s
Peak memory: 83.51 MB
Final size: 57.27 MB
Size on disk: 10.42 MB
Time (exploration): 2.5 s
Time (merging): 0.3 s
+ Property sent
Result: True
Bounds: [1, 1]
Time: 1.7 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 1.7 s
Min. prob. 1 states: 1295218
Time for min. prob. 1 states: 0.0 s
Log file: modest_from-jani_check_default_wlan.5-0_rep5.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 5.310 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4964305/tmpvw6ekbpxmodest_from-jani_check_default_wlan.5-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 1295218 states.
Peak memory usage: 237 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 1295218
Choices: 1646074
Branches: 2929960
Rate: 483832 states/s
Peak memory: 83.09 MB
Final size: 57.27 MB
Size on disk: 10.42 MB
Time (exploration): 2.7 s
Time (merging): 0.3 s
+ Property sent
Result: True
Bounds: [1, 1]
Time: 2.0 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 2.0 s
Min. prob. 1 states: 1295218
Time for min. prob. 1 states: 0.0 s