Log files for model cluster.64-2000-20 and tool configuration modest_from-jani_check_default
[1.0, 0.9, 1.1, 0.9, 0.9]
Log file: modest_from-jani_check_default_cluster.64-2000-20_rep1.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 1467.421 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4967409/tmpiv5xngqamodest_from-jani_check_default_cluster.64-2000-20_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 151060 states.
Peak memory usage: 141 MB
Analysis results for model.jani
+ State space exploration
State size: 24 bytes
States: 151060
Choices: 151060
Branches: 733216
Rate: 172838 states/s
Peak memory: 89.86 MB
Final size: 12.34 MB
Size on disk: 3.59 MB
Time (exploration): 0.9 s
Time (merging): 0.1 s
+ Property qos1
Probability: 0.0010695396728838996
Bounds: [0.0010445396728838941, 0.0010945396728839051]
Time: 1466.3 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 0.0 s
+ Unif+
Time: 1466.3 s
Max. exit rate: 50.252
Iterations: 1
Final unif. rate: 50.252
Log file: modest_from-jani_check_default_cluster.64-2000-20_rep2.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 1249.083 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4961572/tmponycwrnkmodest_from-jani_check_default_cluster.64-2000-20_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 151060 states.
Peak memory usage: 142 MB
Analysis results for model.jani
+ State space exploration
State size: 24 bytes
States: 151060
Choices: 151060
Branches: 733216
Rate: 189774 states/s
Peak memory: 83.13 MB
Final size: 12.34 MB
Size on disk: 3.59 MB
Time (exploration): 0.8 s
Time (merging): 0.1 s
+ Property qos1
Probability: 0.0010695396728838996
Bounds: [0.0010445396728838941, 0.0010945396728839051]
Time: 1248.0 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 0.0 s
+ Unif+
Time: 1248.0 s
Max. exit rate: 50.252
Iterations: 1
Final unif. rate: 50.252
Log file: modest_from-jani_check_default_cluster.64-2000-20_rep3.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 1595.383 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4962672/tmpe7bojh69modest_from-jani_check_default_cluster.64-2000-20_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 151060 states.
Peak memory usage: 141 MB
Analysis results for model.jani
+ State space exploration
State size: 24 bytes
States: 151060
Choices: 151060
Branches: 733216
Rate: 156215 states/s
Peak memory: 83.27 MB
Final size: 12.34 MB
Size on disk: 3.59 MB
Time (exploration): 1.0 s
Time (merging): 0.1 s
+ Property qos1
Probability: 0.0010695396728838996
Bounds: [0.0010445396728838941, 0.0010945396728839051]
Time: 1594.1 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 0.0 s
+ Unif+
Time: 1594.1 s
Max. exit rate: 50.252
Iterations: 1
Final unif. rate: 50.252
Log file: modest_from-jani_check_default_cluster.64-2000-20_rep4.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 1409.987 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4966299/tmprgyrbd1fmodest_from-jani_check_default_cluster.64-2000-20_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 151060 states.
Peak memory usage: 142 MB
Analysis results for model.jani
+ State space exploration
State size: 24 bytes
States: 151060
Choices: 151060
Branches: 733216
Rate: 186034 states/s
Peak memory: 83.79 MB
Final size: 12.34 MB
Size on disk: 3.59 MB
Time (exploration): 0.8 s
Time (merging): 0.1 s
+ Property qos1
Probability: 0.0010695396728838996
Bounds: [0.0010445396728838941, 0.0010945396728839051]
Time: 1408.9 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 0.0 s
+ Unif+
Time: 1408.9 s
Max. exit rate: 50.252
Iterations: 1
Final unif. rate: 50.252
Log file: modest_from-jani_check_default_cluster.64-2000-20_rep5.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 1215.847 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4964709/tmpwrddvl4wmodest_from-jani_check_default_cluster.64-2000-20_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 151060 states.
Peak memory usage: 142 MB
Analysis results for model.jani
+ State space exploration
State size: 24 bytes
States: 151060
Choices: 151060
Branches: 733216
Rate: 183995 states/s
Peak memory: 83.57 MB
Final size: 12.34 MB
Size on disk: 3.59 MB
Time (exploration): 0.8 s
Time (merging): 0.1 s
+ Property qos1
Probability: 0.0010695396728838996
Bounds: [0.0010445396728838941, 0.0010945396728839051]
Time: 1214.8 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 0.0 s
+ Unif+
Time: 1214.8 s
Max. exit rate: 50.252
Iterations: 1
Final unif. rate: 50.252