Log files for model firewire.false-36-800 and tool configuration modest_from-jani_check_default
[1.0, 0.9, 1.0, 1.0, 1.0]
Log file: modest_from-jani_check_default_firewire.false-36-800_rep1.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 7.741 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4964235/tmpa6wlri4zmodest_from-jani_check_default_firewire.false-36-800_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:automata[0].variables[0]: info: Expanding variable "w12" into 10 locations in automaton "wire12".
model.jani:variables[2]: info: Expanding variable "s1" into 9 locations in automaton "node1".
model.jani:automata[2].variables[0]: info: Expanding variable "w21" into 10 locations in automaton "wire21".
model.jani:variables[3]: info: Expanding variable "s2" into 9 locations in automaton "node2".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 212268 states.
Peak memory usage: 135 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 212268
Choices: 478756
Branches: 481792
Rate: 236642 states/s
Peak memory: 79.17 MB
Final size: 14.68 MB
Size on disk: 1.68 MB
Time (exploration): 0.9 s
Time (merging): 0.1 s
+ Property deadline
Probability: 0.939453125
Bounds: [0.939453125, 1]
CDF: { (0, 0), ..., (202, 0), (203, 0.5), ..., (323, 0.5), (324, 0.625), ..., (405, 0.625), (406, 0.75), ..., (444, 0.75), (445, 0.78125), ..., (526, 0.78125), (527, 0.84375), ..., (565, 0.84375), (566, 0.8515625), ..., (608, 0.8515625), (609, 0.8828125), ..., (647, 0.8828125), (648, 0.90625), ..., (686, 0.90625), (687, 0.908203125), ..., (729, 0.908203125), (730, 0.931640625), ..., (768, 0.931640625), (769, 0.939453125), ..., (800, 0.939453125) }
Time: 6.5 s
+ Value iteration
Final error: 0
Iterations: 2374
Time: 6.5 s
Log file: modest_from-jani_check_default_firewire.false-36-800_rep2.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 6.048 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4962063/tmprl_4bxcmmodest_from-jani_check_default_firewire.false-36-800_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:automata[0].variables[0]: info: Expanding variable "w12" into 10 locations in automaton "wire12".
model.jani:variables[2]: info: Expanding variable "s1" into 9 locations in automaton "node1".
model.jani:automata[2].variables[0]: info: Expanding variable "w21" into 10 locations in automaton "wire21".
model.jani:variables[3]: info: Expanding variable "s2" into 9 locations in automaton "node2".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 212268 states.
Peak memory usage: 135 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 212268
Choices: 478756
Branches: 481792
Rate: 259496 states/s
Peak memory: 80.03 MB
Final size: 14.68 MB
Size on disk: 1.68 MB
Time (exploration): 0.8 s
Time (merging): 0.1 s
+ Property deadline
Probability: 0.939453125
Bounds: [0.939453125, 1]
CDF: { (0, 0), ..., (202, 0), (203, 0.5), ..., (323, 0.5), (324, 0.625), ..., (405, 0.625), (406, 0.75), ..., (444, 0.75), (445, 0.78125), ..., (526, 0.78125), (527, 0.84375), ..., (565, 0.84375), (566, 0.8515625), ..., (608, 0.8515625), (609, 0.8828125), ..., (647, 0.8828125), (648, 0.90625), ..., (686, 0.90625), (687, 0.908203125), ..., (729, 0.908203125), (730, 0.931640625), ..., (768, 0.931640625), (769, 0.939453125), ..., (800, 0.939453125) }
Time: 5.0 s
+ Value iteration
Final error: 0
Iterations: 2374
Time: 4.9 s
Log file: modest_from-jani_check_default_firewire.false-36-800_rep3.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 7.028 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4966366/tmpeb14hbfbmodest_from-jani_check_default_firewire.false-36-800_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:automata[0].variables[0]: info: Expanding variable "w12" into 10 locations in automaton "wire12".
model.jani:variables[2]: info: Expanding variable "s1" into 9 locations in automaton "node1".
model.jani:automata[2].variables[0]: info: Expanding variable "w21" into 10 locations in automaton "wire21".
model.jani:variables[3]: info: Expanding variable "s2" into 9 locations in automaton "node2".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 212268 states.
Peak memory usage: 135 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 212268
Choices: 478756
Branches: 481792
Rate: 245397 states/s
Peak memory: 79.17 MB
Final size: 14.68 MB
Size on disk: 1.68 MB
Time (exploration): 0.9 s
Time (merging): 0.1 s
+ Property deadline
Probability: 0.939453125
Bounds: [0.939453125, 1]
CDF: { (0, 0), ..., (202, 0), (203, 0.5), ..., (323, 0.5), (324, 0.625), ..., (405, 0.625), (406, 0.75), ..., (444, 0.75), (445, 0.78125), ..., (526, 0.78125), (527, 0.84375), ..., (565, 0.84375), (566, 0.8515625), ..., (608, 0.8515625), (609, 0.8828125), ..., (647, 0.8828125), (648, 0.90625), ..., (686, 0.90625), (687, 0.908203125), ..., (729, 0.908203125), (730, 0.931640625), ..., (768, 0.931640625), (769, 0.939453125), ..., (800, 0.939453125) }
Time: 5.9 s
+ Value iteration
Final error: 0
Iterations: 2374
Time: 5.9 s
Log file: modest_from-jani_check_default_firewire.false-36-800_rep4.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 7.163 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4965318/tmpzv0gy7cbmodest_from-jani_check_default_firewire.false-36-800_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:automata[0].variables[0]: info: Expanding variable "w12" into 10 locations in automaton "wire12".
model.jani:variables[2]: info: Expanding variable "s1" into 9 locations in automaton "node1".
model.jani:automata[2].variables[0]: info: Expanding variable "w21" into 10 locations in automaton "wire21".
model.jani:variables[3]: info: Expanding variable "s2" into 9 locations in automaton "node2".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 212268 states.
Peak memory usage: 135 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 212268
Choices: 478756
Branches: 481792
Rate: 239851 states/s
Peak memory: 79.20 MB
Final size: 14.68 MB
Size on disk: 1.68 MB
Time (exploration): 0.9 s
Time (merging): 0.1 s
+ Property deadline
Probability: 0.939453125
Bounds: [0.939453125, 1]
CDF: { (0, 0), ..., (202, 0), (203, 0.5), ..., (323, 0.5), (324, 0.625), ..., (405, 0.625), (406, 0.75), ..., (444, 0.75), (445, 0.78125), ..., (526, 0.78125), (527, 0.84375), ..., (565, 0.84375), (566, 0.8515625), ..., (608, 0.8515625), (609, 0.8828125), ..., (647, 0.8828125), (648, 0.90625), ..., (686, 0.90625), (687, 0.908203125), ..., (729, 0.908203125), (730, 0.931640625), ..., (768, 0.931640625), (769, 0.939453125), ..., (800, 0.939453125) }
Time: 6.0 s
+ Value iteration
Final error: 0
Iterations: 2374
Time: 6.0 s
Log file: modest_from-jani_check_default_firewire.false-36-800_rep5.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 7.258 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4966362/tmp0se173iomodest_from-jani_check_default_firewire.false-36-800_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:automata[0].variables[0]: info: Expanding variable "w12" into 10 locations in automaton "wire12".
model.jani:variables[2]: info: Expanding variable "s1" into 9 locations in automaton "node1".
model.jani:automata[2].variables[0]: info: Expanding variable "w21" into 10 locations in automaton "wire21".
model.jani:variables[3]: info: Expanding variable "s2" into 9 locations in automaton "node2".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 212268 states.
Peak memory usage: 135 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 212268
Choices: 478756
Branches: 481792
Rate: 236642 states/s
Peak memory: 79.14 MB
Final size: 14.68 MB
Size on disk: 1.68 MB
Time (exploration): 0.9 s
Time (merging): 0.1 s
+ Property deadline
Probability: 0.939453125
Bounds: [0.939453125, 1]
CDF: { (0, 0), ..., (202, 0), (203, 0.5), ..., (323, 0.5), (324, 0.625), ..., (405, 0.625), (406, 0.75), ..., (444, 0.75), (445, 0.78125), ..., (526, 0.78125), (527, 0.84375), ..., (565, 0.84375), (566, 0.8515625), ..., (608, 0.8515625), (609, 0.8828125), ..., (647, 0.8828125), (648, 0.90625), ..., (686, 0.90625), (687, 0.908203125), ..., (729, 0.908203125), (730, 0.931640625), ..., (768, 0.931640625), (769, 0.939453125), ..., (800, 0.939453125) }
Time: 6.1 s
+ Value iteration
Final error: 0
Iterations: 2374
Time: 6.1 s