Log files for model polling.18-16 and tool configuration modest_from-umb_check_default
[59.617, 59.21, 65.344, 71.65, 67.218]
Log file: modest_from-umb_check_default_polling.18-16_rep1.log
Command(s):
../bin/modest mcsta %indir/modest.model.umb %indir/modest.umb.properties.txt -D -Y --exhaustive
Wallclock time: 59.617 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4973536/tmpz2g8ueapmodest_from-umb_check_default_polling.18-16_tmp_indir_/modest.model.umb /w0/tmp/slurm_tq429871.4973536/tmpz2g8ueapmodest_from-umb_check_default_polling.18-16_tmp_indir_/modest.umb.properties.txt -D -Y --exhaustive
UMB: 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: 1312 MB
Analysis results for UMB
+ State space (UMB)
States: 7077888
Choices: 7077888
Branches: 69599232
Time (decompress): 0.0 s
Time (validate): 0.2 s
Time (load): 0.3 s
+ Property s1_before_s2
Probability: 0.5389863190184031
Bounds: [0.5389863190184031, 1]
Time: 59.2 s
+ Value iteration
Final error: 9.911481067918133E-07
Iterations: 417
Time: 59.2 s
Log file: modest_from-umb_check_default_polling.18-16_rep2.log
Command(s):
../bin/modest mcsta %indir/modest.model.umb %indir/modest.umb.properties.txt -D -Y --exhaustive
Wallclock time: 59.210 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4973470/tmpmfqygpgrmodest_from-umb_check_default_polling.18-16_tmp_indir_/modest.model.umb /w0/tmp/slurm_tq429871.4973470/tmpmfqygpgrmodest_from-umb_check_default_polling.18-16_tmp_indir_/modest.umb.properties.txt -D -Y --exhaustive
UMB: 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: 1312 MB
Analysis results for UMB
+ State space (UMB)
States: 7077888
Choices: 7077888
Branches: 69599232
Time (decompress): 0.0 s
Time (validate): 0.2 s
Time (load): 0.3 s
+ Property s1_before_s2
Probability: 0.5389863190184031
Bounds: [0.5389863190184031, 1]
Time: 58.8 s
+ Value iteration
Final error: 9.911481067918133E-07
Iterations: 417
Time: 58.8 s
Log file: modest_from-umb_check_default_polling.18-16_rep3.log
Command(s):
../bin/modest mcsta %indir/modest.model.umb %indir/modest.umb.properties.txt -D -Y --exhaustive
Wallclock time: 65.344 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4973396/tmpu4g89sv2modest_from-umb_check_default_polling.18-16_tmp_indir_/modest.model.umb /w0/tmp/slurm_tq429871.4973396/tmpu4g89sv2modest_from-umb_check_default_polling.18-16_tmp_indir_/modest.umb.properties.txt -D -Y --exhaustive
UMB: 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: 1312 MB
Analysis results for UMB
+ State space (UMB)
States: 7077888
Choices: 7077888
Branches: 69599232
Time (decompress): 0.0 s
Time (validate): 0.2 s
Time (load): 0.3 s
+ Property s1_before_s2
Probability: 0.5389863190184031
Bounds: [0.5389863190184031, 1]
Time: 64.9 s
+ Value iteration
Final error: 9.911481067918133E-07
Iterations: 417
Time: 64.9 s
Log file: modest_from-umb_check_default_polling.18-16_rep4.log
Command(s):
../bin/modest mcsta %indir/modest.model.umb %indir/modest.umb.properties.txt -D -Y --exhaustive
Wallclock time: 71.650 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4973516/tmpiv2vvkynmodest_from-umb_check_default_polling.18-16_tmp_indir_/modest.model.umb /w0/tmp/slurm_tq429871.4973516/tmpiv2vvkynmodest_from-umb_check_default_polling.18-16_tmp_indir_/modest.umb.properties.txt -D -Y --exhaustive
UMB: 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: 1312 MB
Analysis results for UMB
+ State space (UMB)
States: 7077888
Choices: 7077888
Branches: 69599232
Time (decompress): 0.0 s
Time (validate): 0.2 s
Time (load): 0.3 s
+ Property s1_before_s2
Probability: 0.5389863190184031
Bounds: [0.5389863190184031, 1]
Time: 71.2 s
+ Value iteration
Final error: 9.911481067918133E-07
Iterations: 417
Time: 71.2 s
Log file: modest_from-umb_check_default_polling.18-16_rep5.log
Command(s):
../bin/modest mcsta %indir/modest.model.umb %indir/modest.umb.properties.txt -D -Y --exhaustive
Wallclock time: 67.218 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4973501/tmptnjsx3j9modest_from-umb_check_default_polling.18-16_tmp_indir_/modest.model.umb /w0/tmp/slurm_tq429871.4973501/tmptnjsx3j9modest_from-umb_check_default_polling.18-16_tmp_indir_/modest.umb.properties.txt -D -Y --exhaustive
UMB: 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: 1311 MB
Analysis results for UMB
+ State space (UMB)
States: 7077888
Choices: 7077888
Branches: 69599232
Time (decompress): 0.0 s
Time (validate): 0.2 s
Time (load): 0.3 s
+ Property s1_before_s2
Probability: 0.5389863190184031
Bounds: [0.5389863190184031, 1]
Time: 66.8 s
+ Value iteration
Final error: 9.911481067918133E-07
Iterations: 417
Time: 66.7 s