[6.7, 6.0, 5.6000000000000005, 5.800000000000001, 6.6]

Command(s):
../bin/modest mcsta %indir/model.jani  -D -Y --exhaustive
Wallclock time: 26.214 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4966201/tmpj6bh1lm2modest_from-jani_check_default_consensus.6-2_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:variables[11]: info: Expanding variable "pc5" into 4 locations in automaton "process5".
model.jani:variables[13]: info: Expanding variable "pc6" into 4 locations in automaton "process6".
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 1258240 states.

Peak memory usage: 315 MB
Analysis results for model.jani

+ State space exploration
  State size:         24 bytes
  States:             1258240
  Choices:            5008128
  Branches:           6236736
  Rate:               202452 states/s
  Peak memory:        105.30 MB
  Final size:         133.37 MB
  Size on disk:       19.72 MB
  Time (exploration): 6.2 s
  Time (merging):     0.5 s

+ Property disagree
  Probability: 0.36362422496221386
  Bounds:      [0.36362422496221386, 1]
  Time:        19.2 s

  + Value iteration
    Final error: 9.857326206509403E-07
    Iterations:  736
    Time:        19.2 s

Command(s):
../bin/modest mcsta %indir/model.jani  -D -Y --exhaustive
Wallclock time: 23.170 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4965782/tmpebsyocykmodest_from-jani_check_default_consensus.6-2_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:variables[11]: info: Expanding variable "pc5" into 4 locations in automaton "process5".
model.jani:variables[13]: info: Expanding variable "pc6" into 4 locations in automaton "process6".
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 1258240 states.

Peak memory usage: 316 MB
Analysis results for model.jani

+ State space exploration
  State size:         24 bytes
  States:             1258240
  Choices:            5008128
  Branches:           6236736
  Rate:               223251 states/s
  Peak memory:        105.39 MB
  Final size:         133.37 MB
  Size on disk:       19.72 MB
  Time (exploration): 5.6 s
  Time (merging):     0.4 s

+ Property disagree
  Probability: 0.36362422496221386
  Bounds:      [0.36362422496221386, 1]
  Time:        16.9 s

  + Value iteration
    Final error: 9.857326206509403E-07
    Iterations:  736
    Time:        16.9 s

Command(s):
../bin/modest mcsta %indir/model.jani  -D -Y --exhaustive
Wallclock time: 21.663 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4966767/tmp3otz8ow1modest_from-jani_check_default_consensus.6-2_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:variables[11]: info: Expanding variable "pc5" into 4 locations in automaton "process5".
model.jani:variables[13]: info: Expanding variable "pc6" into 4 locations in automaton "process6".
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 1258240 states.

Peak memory usage: 316 MB
Analysis results for model.jani

+ State space exploration
  State size:         24 bytes
  States:             1258240
  Choices:            5008128
  Branches:           6236736
  Rate:               240489 states/s
  Peak memory:        106.12 MB
  Final size:         133.37 MB
  Size on disk:       19.72 MB
  Time (exploration): 5.2 s
  Time (merging):     0.4 s

+ Property disagree
  Probability: 0.36362422496221386
  Bounds:      [0.36362422496221386, 1]
  Time:        15.8 s

  + Value iteration
    Final error: 9.857326206509403E-07
    Iterations:  736
    Time:        15.8 s

Command(s):
../bin/modest mcsta %indir/model.jani  -D -Y --exhaustive
Wallclock time: 22.036 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4967114/tmpm2bhtib2modest_from-jani_check_default_consensus.6-2_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:variables[11]: info: Expanding variable "pc5" into 4 locations in automaton "process5".
model.jani:variables[13]: info: Expanding variable "pc6" into 4 locations in automaton "process6".
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 1258240 states.

Peak memory usage: 315 MB
Analysis results for model.jani

+ State space exploration
  State size:         24 bytes
  States:             1258240
  Choices:            5008128
  Branches:           6236736
  Rate:               235581 states/s
  Peak memory:        105.91 MB
  Final size:         133.37 MB
  Size on disk:       19.72 MB
  Time (exploration): 5.4 s
  Time (merging):     0.4 s

+ Property disagree
  Probability: 0.36362422496221386
  Bounds:      [0.36362422496221386, 1]
  Time:        16.1 s

  + Value iteration
    Final error: 9.857326206509403E-07
    Iterations:  736
    Time:        16.1 s

Command(s):
../bin/modest mcsta %indir/model.jani  -D -Y --exhaustive
Wallclock time: 25.499 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4964478/tmpci_zn0qcmodest_from-jani_check_default_consensus.6-2_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:variables[11]: info: Expanding variable "pc5" into 4 locations in automaton "process5".
model.jani:variables[13]: info: Expanding variable "pc6" into 4 locations in automaton "process6".
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 1258240 states.

Peak memory usage: 316 MB
Analysis results for model.jani

+ State space exploration
  State size:         24 bytes
  States:             1258240
  Choices:            5008128
  Branches:           6236736
  Rate:               205293 states/s
  Peak memory:        104.71 MB
  Final size:         133.37 MB
  Size on disk:       19.72 MB
  Time (exploration): 6.1 s
  Time (merging):     0.5 s

+ Property disagree
  Probability: 0.36362422496221386
  Bounds:      [0.36362422496221386, 1]
  Time:        18.7 s

  + Value iteration
    Final error: 9.857326206509403E-07
    Iterations:  736
    Time:        18.7 s