Log files for model nand.60-4 and tool configuration modest_from-jani_check_default
[24.1, 23.900000000000002, 24.900000000000002, 23.900000000000002, 21.2]
Log file: modest_from-jani_check_default_nand.60-4_rep1.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 25.008 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4961300/tmpf492po9jmodest_from-jani_check_default_nand.60-4_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is a DTMC model.
model.jani:variables[1]: info: Expanding variable "s" into 5 locations in automaton "multiplex".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 18826082 states.
Peak memory usage: 1795 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 18826082
Choices: 18826082
Branches: 29772212
Rate: 856588 states/s
Peak memory: 794.27 MB
Final size: 597.92 MB
Size on disk: 100.44 MB
Time (exploration): 22.0 s
Time (merging): 2.1 s
+ Property reliable
Probability: 0.6867214589192275
Bounds: [0.6867214589192275, 0.6867214589192275]
Time: 0.4 s
+ Value iteration
Final error: 0
Iterations: 2
Time: 0.3 s
Log file: modest_from-jani_check_default_nand.60-4_rep2.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 24.766 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4961725/tmp1fi1f76gmodest_from-jani_check_default_nand.60-4_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is a DTMC model.
model.jani:variables[1]: info: Expanding variable "s" into 5 locations in automaton "multiplex".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 18826082 states.
Peak memory usage: 1795 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 18826082
Choices: 18826082
Branches: 29772212
Rate: 865567 states/s
Peak memory: 792.42 MB
Final size: 597.92 MB
Size on disk: 100.44 MB
Time (exploration): 21.8 s
Time (merging): 2.1 s
+ Property reliable
Probability: 0.6867214589192275
Bounds: [0.6867214589192275, 0.6867214589192275]
Time: 0.4 s
+ Value iteration
Final error: 0
Iterations: 2
Time: 0.3 s
Log file: modest_from-jani_check_default_nand.60-4_rep3.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 25.846 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4965680/tmpphr3twadmodest_from-jani_check_default_nand.60-4_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is a DTMC model.
model.jani:variables[1]: info: Expanding variable "s" into 5 locations in automaton "multiplex".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 18826082 states.
Peak memory usage: 1795 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 18826082
Choices: 18826082
Branches: 29772212
Rate: 825199 states/s
Peak memory: 792.59 MB
Final size: 597.92 MB
Size on disk: 100.44 MB
Time (exploration): 22.8 s
Time (merging): 2.1 s
+ Property reliable
Probability: 0.6867214589192275
Bounds: [0.6867214589192275, 0.6867214589192275]
Time: 0.4 s
+ Value iteration
Final error: 0
Iterations: 2
Time: 0.3 s
Log file: modest_from-jani_check_default_nand.60-4_rep4.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 25.674 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4962675/tmprbmhfer7modest_from-jani_check_default_nand.60-4_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is a DTMC model.
model.jani:variables[1]: info: Expanding variable "s" into 5 locations in automaton "multiplex".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 18826082 states.
Peak memory usage: 1795 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 18826082
Choices: 18826082
Branches: 29772212
Rate: 864851 states/s
Peak memory: 792.58 MB
Final size: 597.92 MB
Size on disk: 100.44 MB
Time (exploration): 21.8 s
Time (merging): 2.1 s
+ Property reliable
Probability: 0.6867214589192275
Bounds: [0.6867214589192275, 0.6867214589192275]
Time: 0.4 s
+ Value iteration
Final error: 0
Iterations: 2
Time: 0.3 s
Log file: modest_from-jani_check_default_nand.60-4_rep5.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 21.973 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4961547/tmpa6o_6r37modest_from-jani_check_default_nand.60-4_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is a DTMC model.
model.jani:variables[1]: info: Expanding variable "s" into 5 locations in automaton "multiplex".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 18826082 states.
Peak memory usage: 1795 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 18826082
Choices: 18826082
Branches: 29772212
Rate: 976052 states/s
Peak memory: 793.97 MB
Final size: 597.92 MB
Size on disk: 100.44 MB
Time (exploration): 19.3 s
Time (merging): 1.9 s
+ Property reliable
Probability: 0.6867214589192275
Bounds: [0.6867214589192275, 0.6867214589192275]
Time: 0.3 s
+ Value iteration
Final error: 0
Iterations: 2
Time: 0.3 s