Log fms.8_modest_from-jani_check

Log file: modest_from-jani_check_default_fms.8_rep1.log

Command(s):
../bin/modest mcsta %indir/model.jani  -D -Y --exhaustive
Wallclock time: 50.361 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4967416/tmpw6u1itnymodest_from-jani_check_default_fms.8_tmp_indir_/model.jani -D -Y --exhaustive




model.jani:model: info: model is a CTMC model.
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 4459455 states.
model.jani:properties[0]: error: Analysis of long-run average reward properties is currently not supported.

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

+ State space exploration
  State size:         24 bytes
  States:             4459455
  Choices:            4459455
  Branches:           38533968
  Rate:               95062 states/s
  Peak memory:        267.00 MB
  Final size:         916.00 MB
  Size on disk:       183.97 MB
  Time (exploration): 46.9 s
  Time (merging):     2.8 s

+ productivity
  Time: 0.0 s

Log file: modest_from-jani_check_default_fms.8_rep2.log

Command(s):
../bin/modest mcsta %indir/model.jani  -D -Y --exhaustive
Wallclock time: 51.092 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4961446/tmpw08m6feimodest_from-jani_check_default_fms.8_tmp_indir_/model.jani -D -Y --exhaustive




model.jani:model: info: model is a CTMC model.
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 4459455 states.
model.jani:properties[0]: error: Analysis of long-run average reward properties is currently not supported.

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

+ State space exploration
  State size:         24 bytes
  States:             4459455
  Choices:            4459455
  Branches:           38533968
  Rate:               93862 states/s
  Peak memory:        281.29 MB
  Final size:         916.00 MB
  Size on disk:       183.97 MB
  Time (exploration): 47.5 s
  Time (merging):     2.9 s

+ productivity
  Time: 0.0 s

Log file: modest_from-jani_check_default_fms.8_rep3.log

Command(s):
../bin/modest mcsta %indir/model.jani  -D -Y --exhaustive
Wallclock time: 48.802 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4967238/tmpei071sxvmodest_from-jani_check_default_fms.8_tmp_indir_/model.jani -D -Y --exhaustive




model.jani:model: info: model is a CTMC model.
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 4459455 states.
model.jani:properties[0]: error: Analysis of long-run average reward properties is currently not supported.

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

+ State space exploration
  State size:         24 bytes
  States:             4459455
  Choices:            4459455
  Branches:           38533968
  Rate:               98425 states/s
  Peak memory:        281.23 MB
  Final size:         916.00 MB
  Size on disk:       183.97 MB
  Time (exploration): 45.3 s
  Time (merging):     2.9 s

+ productivity
  Time: 0.0 s

Log file: modest_from-jani_check_default_fms.8_rep4.log

Command(s):
../bin/modest mcsta %indir/model.jani  -D -Y --exhaustive
Wallclock time: 50.183 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4966160/tmplv8gscynmodest_from-jani_check_default_fms.8_tmp_indir_/model.jani -D -Y --exhaustive




model.jani:model: info: model is a CTMC model.
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 4459455 states.
model.jani:properties[0]: error: Analysis of long-run average reward properties is currently not supported.

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

+ State space exploration
  State size:         24 bytes
  States:             4459455
  Choices:            4459455
  Branches:           38533968
  Rate:               97999 states/s
  Peak memory:        280.39 MB
  Final size:         916.00 MB
  Size on disk:       183.97 MB
  Time (exploration): 45.5 s
  Time (merging):     2.8 s

+ productivity
  Time: 0.0 s

Log file: modest_from-jani_check_default_fms.8_rep5.log

Command(s):
../bin/modest mcsta %indir/model.jani  -D -Y --exhaustive
Wallclock time: 50.646 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4964201/tmpa_lft72jmodest_from-jani_check_default_fms.8_tmp_indir_/model.jani -D -Y --exhaustive




model.jani:model: info: model is a CTMC model.
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 4459455 states.
model.jani:properties[0]: error: Analysis of long-run average reward properties is currently not supported.

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

+ State space exploration
  State size:         24 bytes
  States:             4459455
  Choices:            4459455
  Branches:           38533968
  Rate:               94671 states/s
  Peak memory:        279.95 MB
  Final size:         916.00 MB
  Size on disk:       183.97 MB
  Time (exploration): 47.1 s
  Time (merging):     2.9 s

+ productivity
  Time: 0.0 s

Log files for model fms.8 and tool configuration modest_from-jani_check_default