Log files for model consensus.4-4 and tool configuration modest_from-jani_check_default
[0.4, 0.3, 0.4, 0.3, 0.3]
Log file: modest_from-jani_check_default_consensus.4-4_rep1.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 1.229 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4965837/tmp7e05crvkmodest_from-jani_check_default_consensus.4-4_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[3]: info: Expanding variable "pc1" into 4 locations in automaton "process1".
model.jani:variables[5]: info: Expanding variable "pc2" into 4 locations in automaton "process2".
model.jani:variables[7]: info: Expanding variable "pc3" into 4 locations in automaton "process3".
model.jani:variables[9]: info: Expanding variable "pc4" into 4 locations in automaton "process4".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 43136 states.
Peak memory usage: 92 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 43136
Choices: 115840
Branches: 144352
Rate: 121510 states/s
Peak memory: 64.70 MB
Final size: 3.09 MB
Size on disk: 0.44 MB
Time (exploration): 0.4 s
Time (merging): 0.0 s
+ Property disagree
Probability: 0.15605633046939615
Bounds: [0.15605633046939615, 1]
Time: 0.6 s
+ Value iteration
Final error: 9.981462390211186E-07
Iterations: 1246
Time: 0.6 s
Log file: modest_from-jani_check_default_consensus.4-4_rep2.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 1.015 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4967201/tmpjp2mapx6modest_from-jani_check_default_consensus.4-4_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[3]: info: Expanding variable "pc1" into 4 locations in automaton "process1".
model.jani:variables[5]: info: Expanding variable "pc2" into 4 locations in automaton "process2".
model.jani:variables[7]: info: Expanding variable "pc3" into 4 locations in automaton "process3".
model.jani:variables[9]: info: Expanding variable "pc4" into 4 locations in automaton "process4".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 43136 states.
Peak memory usage: 91 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 43136
Choices: 115840
Branches: 144352
Rate: 149260 states/s
Peak memory: 64.70 MB
Final size: 3.09 MB
Size on disk: 0.44 MB
Time (exploration): 0.3 s
Time (merging): 0.0 s
+ Property disagree
Probability: 0.15605633046939615
Bounds: [0.15605633046939615, 1]
Time: 0.5 s
+ Value iteration
Final error: 9.981462390211186E-07
Iterations: 1246
Time: 0.5 s
Log file: modest_from-jani_check_default_consensus.4-4_rep3.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 1.173 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4964916/tmpm9t2np8ymodest_from-jani_check_default_consensus.4-4_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[3]: info: Expanding variable "pc1" into 4 locations in automaton "process1".
model.jani:variables[5]: info: Expanding variable "pc2" into 4 locations in automaton "process2".
model.jani:variables[7]: info: Expanding variable "pc3" into 4 locations in automaton "process3".
model.jani:variables[9]: info: Expanding variable "pc4" into 4 locations in automaton "process4".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 43136 states.
Peak memory usage: 92 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 43136
Choices: 115840
Branches: 144352
Rate: 127245 states/s
Peak memory: 64.70 MB
Final size: 3.09 MB
Size on disk: 0.44 MB
Time (exploration): 0.4 s
Time (merging): 0.0 s
+ Property disagree
Probability: 0.15605633046939615
Bounds: [0.15605633046939615, 1]
Time: 0.6 s
+ Value iteration
Final error: 9.981462390211186E-07
Iterations: 1246
Time: 0.6 s
Log file: modest_from-jani_check_default_consensus.4-4_rep4.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 1.008 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4965432/tmp34sbnhxrmodest_from-jani_check_default_consensus.4-4_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[3]: info: Expanding variable "pc1" into 4 locations in automaton "process1".
model.jani:variables[5]: info: Expanding variable "pc2" into 4 locations in automaton "process2".
model.jani:variables[7]: info: Expanding variable "pc3" into 4 locations in automaton "process3".
model.jani:variables[9]: info: Expanding variable "pc4" into 4 locations in automaton "process4".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 43136 states.
Peak memory usage: 92 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 43136
Choices: 115840
Branches: 144352
Rate: 149778 states/s
Peak memory: 64.70 MB
Final size: 3.09 MB
Size on disk: 0.44 MB
Time (exploration): 0.3 s
Time (merging): 0.0 s
+ Property disagree
Probability: 0.15605633046939615
Bounds: [0.15605633046939615, 1]
Time: 0.5 s
+ Value iteration
Final error: 9.981462390211186E-07
Iterations: 1246
Time: 0.5 s
Log file: modest_from-jani_check_default_consensus.4-4_rep5.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 1.157 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4963290/tmpx3yrzxpjmodest_from-jani_check_default_consensus.4-4_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[3]: info: Expanding variable "pc1" into 4 locations in automaton "process1".
model.jani:variables[5]: info: Expanding variable "pc2" into 4 locations in automaton "process2".
model.jani:variables[7]: info: Expanding variable "pc3" into 4 locations in automaton "process3".
model.jani:variables[9]: info: Expanding variable "pc4" into 4 locations in automaton "process4".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 43136 states.
Peak memory usage: 92 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 43136
Choices: 115840
Branches: 144352
Rate: 129150 states/s
Peak memory: 64.70 MB
Final size: 3.09 MB
Size on disk: 0.44 MB
Time (exploration): 0.3 s
Time (merging): 0.0 s
+ Property disagree
Probability: 0.15605633046939615
Bounds: [0.15605633046939615, 1]
Time: 0.6 s
+ Value iteration
Final error: 9.981462390211186E-07
Iterations: 1246
Time: 0.6 s