Log files for model polling.18-16 and tool configuration modest_from-jani_check_default

Parsed values
[131.013, 124.406, 122.781, 124.388, 122.688]
Log file: modest_from-jani_check_default_polling.18-16_rep1.log
Command(s):
../bin/modest mcsta %indir/model.jani  -D -Y --exhaustive
Wallclock time: 131.013 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4962545/tmp2hjf6ov3modest_from-jani_check_default_polling.18-16_tmp_indir_/model.jani -D -Y --exhaustive




model.jani:model: info: model is a CTMC model.
model.jani:variables[3]: info: Expanding variable "a" into 2 locations in automaton "server".
model.jani:automata[1].variables[0]: info: Expanding variable "s1" into 2 locations in automaton "station1".
model.jani:automata[2].variables[0]: info: Expanding variable "s2" into 2 locations in automaton "station2".
model.jani:automata[3].variables[0]: info: Expanding variable "s3" into 2 locations in automaton "station3".
model.jani:automata[4].variables[0]: info: Expanding variable "s4" into 2 locations in automaton "station4".
model.jani:automata[5].variables[0]: info: Expanding variable "s5" into 2 locations in automaton "station5".
model.jani:automata[6].variables[0]: info: Expanding variable "s6" into 2 locations in automaton "station6".
model.jani:automata[7].variables[0]: info: Expanding variable "s7" into 2 locations in automaton "station7".
model.jani:automata[8].variables[0]: info: Expanding variable "s8" into 2 locations in automaton "station8".
model.jani:automata[9].variables[0]: info: Expanding variable "s9" into 2 locations in automaton "station9".
model.jani:automata[10].variables[0]: info: Expanding variable "s10" into 2 locations in automaton "station10".
model.jani:automata[11].variables[0]: info: Expanding variable "s11" into 2 locations in automaton "station11".
model.jani:automata[12].variables[0]: info: Expanding variable "s12" into 2 locations in automaton "station12".
model.jani:automata[13].variables[0]: info: Expanding variable "s13" into 2 locations in automaton "station13".
model.jani:automata[14].variables[0]: info: Expanding variable "s14" into 2 locations in automaton "station14".
model.jani:automata[15].variables[0]: info: Expanding variable "s15" into 2 locations in automaton "station15".
model.jani:automata[16].variables[0]: info: Expanding variable "s16" into 2 locations in automaton "station16".
model.jani:automata[17].variables[0]: info: Expanding variable "s17" into 2 locations in automaton "station17".
model.jani:automata[18].variables[0]: info: Expanding variable "s18" into 2 locations in automaton "station18".
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 7077888 states.
model.jani: warning: Encountered a value greater than 1 during value iteration. The final result for property "s1_before_s2" is likely affected by floating-point errors.

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

+ State space exploration
  State size:         24 bytes
  States:             7077888
  Choices:            7077888
  Branches:           69599232
  Rate:               109646 states/s
  Peak memory:        362.00 MB
  Final size:         1116.00 MB
  Size on disk:       223.88 MB
  Time (exploration): 64.6 s
  Time (merging):     4.1 s

+ Property s1_before_s2
  Probability: 0.5389863190184031
  Bounds:      [0.5389863190184031, 1]
  Time:        62.1 s

  + Value iteration
    Final error: 9.911481067918133E-07
    Iterations:  417
    Time:        62.0 s
Log file: modest_from-jani_check_default_polling.18-16_rep2.log
Command(s):
../bin/modest mcsta %indir/model.jani  -D -Y --exhaustive
Wallclock time: 124.406 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4964854/tmpgfcp7q6gmodest_from-jani_check_default_polling.18-16_tmp_indir_/model.jani -D -Y --exhaustive




model.jani:model: info: model is a CTMC model.
model.jani:variables[3]: info: Expanding variable "a" into 2 locations in automaton "server".
model.jani:automata[1].variables[0]: info: Expanding variable "s1" into 2 locations in automaton "station1".
model.jani:automata[2].variables[0]: info: Expanding variable "s2" into 2 locations in automaton "station2".
model.jani:automata[3].variables[0]: info: Expanding variable "s3" into 2 locations in automaton "station3".
model.jani:automata[4].variables[0]: info: Expanding variable "s4" into 2 locations in automaton "station4".
model.jani:automata[5].variables[0]: info: Expanding variable "s5" into 2 locations in automaton "station5".
model.jani:automata[6].variables[0]: info: Expanding variable "s6" into 2 locations in automaton "station6".
model.jani:automata[7].variables[0]: info: Expanding variable "s7" into 2 locations in automaton "station7".
model.jani:automata[8].variables[0]: info: Expanding variable "s8" into 2 locations in automaton "station8".
model.jani:automata[9].variables[0]: info: Expanding variable "s9" into 2 locations in automaton "station9".
model.jani:automata[10].variables[0]: info: Expanding variable "s10" into 2 locations in automaton "station10".
model.jani:automata[11].variables[0]: info: Expanding variable "s11" into 2 locations in automaton "station11".
model.jani:automata[12].variables[0]: info: Expanding variable "s12" into 2 locations in automaton "station12".
model.jani:automata[13].variables[0]: info: Expanding variable "s13" into 2 locations in automaton "station13".
model.jani:automata[14].variables[0]: info: Expanding variable "s14" into 2 locations in automaton "station14".
model.jani:automata[15].variables[0]: info: Expanding variable "s15" into 2 locations in automaton "station15".
model.jani:automata[16].variables[0]: info: Expanding variable "s16" into 2 locations in automaton "station16".
model.jani:automata[17].variables[0]: info: Expanding variable "s17" into 2 locations in automaton "station17".
model.jani:automata[18].variables[0]: info: Expanding variable "s18" into 2 locations in automaton "station18".
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 7077888 states.
model.jani: warning: Encountered a value greater than 1 during value iteration. The final result for property "s1_before_s2" is likely affected by floating-point errors.

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

+ State space exploration
  State size:         24 bytes
  States:             7077888
  Choices:            7077888
  Branches:           69599232
  Rate:               120732 states/s
  Peak memory:        361.11 MB
  Final size:         1116.00 MB
  Size on disk:       223.88 MB
  Time (exploration): 58.6 s
  Time (merging):     3.8 s

+ Property s1_before_s2
  Probability: 0.5389863190184031
  Bounds:      [0.5389863190184031, 1]
  Time:        61.7 s

  + Value iteration
    Final error: 9.911481067918133E-07
    Iterations:  417
    Time:        61.7 s
Log file: modest_from-jani_check_default_polling.18-16_rep3.log
Command(s):
../bin/modest mcsta %indir/model.jani  -D -Y --exhaustive
Wallclock time: 122.781 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4966522/tmpuanws19nmodest_from-jani_check_default_polling.18-16_tmp_indir_/model.jani -D -Y --exhaustive




model.jani:model: info: model is a CTMC model.
model.jani:variables[3]: info: Expanding variable "a" into 2 locations in automaton "server".
model.jani:automata[1].variables[0]: info: Expanding variable "s1" into 2 locations in automaton "station1".
model.jani:automata[2].variables[0]: info: Expanding variable "s2" into 2 locations in automaton "station2".
model.jani:automata[3].variables[0]: info: Expanding variable "s3" into 2 locations in automaton "station3".
model.jani:automata[4].variables[0]: info: Expanding variable "s4" into 2 locations in automaton "station4".
model.jani:automata[5].variables[0]: info: Expanding variable "s5" into 2 locations in automaton "station5".
model.jani:automata[6].variables[0]: info: Expanding variable "s6" into 2 locations in automaton "station6".
model.jani:automata[7].variables[0]: info: Expanding variable "s7" into 2 locations in automaton "station7".
model.jani:automata[8].variables[0]: info: Expanding variable "s8" into 2 locations in automaton "station8".
model.jani:automata[9].variables[0]: info: Expanding variable "s9" into 2 locations in automaton "station9".
model.jani:automata[10].variables[0]: info: Expanding variable "s10" into 2 locations in automaton "station10".
model.jani:automata[11].variables[0]: info: Expanding variable "s11" into 2 locations in automaton "station11".
model.jani:automata[12].variables[0]: info: Expanding variable "s12" into 2 locations in automaton "station12".
model.jani:automata[13].variables[0]: info: Expanding variable "s13" into 2 locations in automaton "station13".
model.jani:automata[14].variables[0]: info: Expanding variable "s14" into 2 locations in automaton "station14".
model.jani:automata[15].variables[0]: info: Expanding variable "s15" into 2 locations in automaton "station15".
model.jani:automata[16].variables[0]: info: Expanding variable "s16" into 2 locations in automaton "station16".
model.jani:automata[17].variables[0]: info: Expanding variable "s17" into 2 locations in automaton "station17".
model.jani:automata[18].variables[0]: info: Expanding variable "s18" into 2 locations in automaton "station18".
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 7077888 states.
model.jani: warning: Encountered a value greater than 1 during value iteration. The final result for property "s1_before_s2" is likely affected by floating-point errors.

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

+ State space exploration
  State size:         24 bytes
  States:             7077888
  Choices:            7077888
  Branches:           69599232
  Rate:               120440 states/s
  Peak memory:        362.65 MB
  Final size:         1116.00 MB
  Size on disk:       223.88 MB
  Time (exploration): 58.8 s
  Time (merging):     3.6 s

+ Property s1_before_s2
  Probability: 0.5389863190184031
  Bounds:      [0.5389863190184031, 1]
  Time:        60.1 s

  + Value iteration
    Final error: 9.911481067918133E-07
    Iterations:  417
    Time:        60.0 s
Log file: modest_from-jani_check_default_polling.18-16_rep4.log
Command(s):
../bin/modest mcsta %indir/model.jani  -D -Y --exhaustive
Wallclock time: 124.388 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4966776/tmpi3kxu9ckmodest_from-jani_check_default_polling.18-16_tmp_indir_/model.jani -D -Y --exhaustive




model.jani:model: info: model is a CTMC model.
model.jani:variables[3]: info: Expanding variable "a" into 2 locations in automaton "server".
model.jani:automata[1].variables[0]: info: Expanding variable "s1" into 2 locations in automaton "station1".
model.jani:automata[2].variables[0]: info: Expanding variable "s2" into 2 locations in automaton "station2".
model.jani:automata[3].variables[0]: info: Expanding variable "s3" into 2 locations in automaton "station3".
model.jani:automata[4].variables[0]: info: Expanding variable "s4" into 2 locations in automaton "station4".
model.jani:automata[5].variables[0]: info: Expanding variable "s5" into 2 locations in automaton "station5".
model.jani:automata[6].variables[0]: info: Expanding variable "s6" into 2 locations in automaton "station6".
model.jani:automata[7].variables[0]: info: Expanding variable "s7" into 2 locations in automaton "station7".
model.jani:automata[8].variables[0]: info: Expanding variable "s8" into 2 locations in automaton "station8".
model.jani:automata[9].variables[0]: info: Expanding variable "s9" into 2 locations in automaton "station9".
model.jani:automata[10].variables[0]: info: Expanding variable "s10" into 2 locations in automaton "station10".
model.jani:automata[11].variables[0]: info: Expanding variable "s11" into 2 locations in automaton "station11".
model.jani:automata[12].variables[0]: info: Expanding variable "s12" into 2 locations in automaton "station12".
model.jani:automata[13].variables[0]: info: Expanding variable "s13" into 2 locations in automaton "station13".
model.jani:automata[14].variables[0]: info: Expanding variable "s14" into 2 locations in automaton "station14".
model.jani:automata[15].variables[0]: info: Expanding variable "s15" into 2 locations in automaton "station15".
model.jani:automata[16].variables[0]: info: Expanding variable "s16" into 2 locations in automaton "station16".
model.jani:automata[17].variables[0]: info: Expanding variable "s17" into 2 locations in automaton "station17".
model.jani:automata[18].variables[0]: info: Expanding variable "s18" into 2 locations in automaton "station18".
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 7077888 states.
model.jani: warning: Encountered a value greater than 1 during value iteration. The final result for property "s1_before_s2" is likely affected by floating-point errors.

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

+ State space exploration
  State size:         24 bytes
  States:             7077888
  Choices:            7077888
  Branches:           69599232
  Rate:               118964 states/s
  Peak memory:        361.34 MB
  Final size:         1116.00 MB
  Size on disk:       223.88 MB
  Time (exploration): 59.5 s
  Time (merging):     3.5 s

+ Property s1_before_s2
  Probability: 0.5389863190184031
  Bounds:      [0.5389863190184031, 1]
  Time:        61.1 s

  + Value iteration
    Final error: 9.911481067918133E-07
    Iterations:  417
    Time:        61.0 s
Log file: modest_from-jani_check_default_polling.18-16_rep5.log
Command(s):
../bin/modest mcsta %indir/model.jani  -D -Y --exhaustive
Wallclock time: 122.688 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4964658/tmpqgx199n_modest_from-jani_check_default_polling.18-16_tmp_indir_/model.jani -D -Y --exhaustive




model.jani:model: info: model is a CTMC model.
model.jani:variables[3]: info: Expanding variable "a" into 2 locations in automaton "server".
model.jani:automata[1].variables[0]: info: Expanding variable "s1" into 2 locations in automaton "station1".
model.jani:automata[2].variables[0]: info: Expanding variable "s2" into 2 locations in automaton "station2".
model.jani:automata[3].variables[0]: info: Expanding variable "s3" into 2 locations in automaton "station3".
model.jani:automata[4].variables[0]: info: Expanding variable "s4" into 2 locations in automaton "station4".
model.jani:automata[5].variables[0]: info: Expanding variable "s5" into 2 locations in automaton "station5".
model.jani:automata[6].variables[0]: info: Expanding variable "s6" into 2 locations in automaton "station6".
model.jani:automata[7].variables[0]: info: Expanding variable "s7" into 2 locations in automaton "station7".
model.jani:automata[8].variables[0]: info: Expanding variable "s8" into 2 locations in automaton "station8".
model.jani:automata[9].variables[0]: info: Expanding variable "s9" into 2 locations in automaton "station9".
model.jani:automata[10].variables[0]: info: Expanding variable "s10" into 2 locations in automaton "station10".
model.jani:automata[11].variables[0]: info: Expanding variable "s11" into 2 locations in automaton "station11".
model.jani:automata[12].variables[0]: info: Expanding variable "s12" into 2 locations in automaton "station12".
model.jani:automata[13].variables[0]: info: Expanding variable "s13" into 2 locations in automaton "station13".
model.jani:automata[14].variables[0]: info: Expanding variable "s14" into 2 locations in automaton "station14".
model.jani:automata[15].variables[0]: info: Expanding variable "s15" into 2 locations in automaton "station15".
model.jani:automata[16].variables[0]: info: Expanding variable "s16" into 2 locations in automaton "station16".
model.jani:automata[17].variables[0]: info: Expanding variable "s17" into 2 locations in automaton "station17".
model.jani:automata[18].variables[0]: info: Expanding variable "s18" into 2 locations in automaton "station18".
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 7077888 states.
model.jani: warning: Encountered a value greater than 1 during value iteration. The final result for property "s1_before_s2" is likely affected by floating-point errors.

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

+ State space exploration
  State size:         24 bytes
  States:             7077888
  Choices:            7077888
  Branches:           69599232
  Rate:               121544 states/s
  Peak memory:        362.62 MB
  Final size:         1116.00 MB
  Size on disk:       223.88 MB
  Time (exploration): 58.2 s
  Time (merging):     3.6 s

+ Property s1_before_s2
  Probability: 0.5389863190184031
  Bounds:      [0.5389863190184031, 1]
  Time:        60.6 s

  + Value iteration
    Final error: 9.911481067918133E-07
    Iterations:  417
    Time:        60.6 s