Log files for model csma.3-4 and tool configuration modest_from-jani_check_default
[3.0, 2.8000000000000003, 2.8000000000000003, 2.4000000000000004, 2.8000000000000003]
Log file: modest_from-jani_check_default_csma.3-4_rep1.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 3.849 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4965073/tmp59udxjjamodest_from-jani_check_default_csma.3-4_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 1460287 states.
Peak memory usage: 244 MB
Analysis results for model.jani
+ State space exploration
State size: 24 bytes
States: 1460287
Choices: 1471059
Branches: 2396727
Rate: 533926 states/s
Peak memory: 141.54 MB
Final size: 47.79 MB
Size on disk: 7.94 MB
Time (exploration): 2.8 s
Time (merging): 0.2 s
+ Property all_before_max
Probability: 0.9324469288458123
Bounds: [0.9324469288458123, 1]
Time: 0.6 s
+ Value iteration
Final error: 3.001709289030008E-07
Iterations: 55
Time: 0.6 s
Log file: modest_from-jani_check_default_csma.3-4_rep2.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 3.629 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4965059/tmp_rlvll52modest_from-jani_check_default_csma.3-4_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 1460287 states.
Peak memory usage: 245 MB
Analysis results for model.jani
+ State space exploration
State size: 24 bytes
States: 1460287
Choices: 1471059
Branches: 2396727
Rate: 566662 states/s
Peak memory: 141.76 MB
Final size: 47.79 MB
Size on disk: 7.94 MB
Time (exploration): 2.6 s
Time (merging): 0.2 s
+ Property all_before_max
Probability: 0.9324469288458123
Bounds: [0.9324469288458123, 1]
Time: 0.6 s
+ Value iteration
Final error: 3.001709289030008E-07
Iterations: 55
Time: 0.6 s
Log file: modest_from-jani_check_default_csma.3-4_rep3.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 3.779 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4966037/tmpkv7h7nmrmodest_from-jani_check_default_csma.3-4_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 1460287 states.
Peak memory usage: 245 MB
Analysis results for model.jani
+ State space exploration
State size: 24 bytes
States: 1460287
Choices: 1471059
Branches: 2396727
Rate: 568869 states/s
Peak memory: 141.13 MB
Final size: 47.79 MB
Size on disk: 7.94 MB
Time (exploration): 2.6 s
Time (merging): 0.2 s
+ Property all_before_max
Probability: 0.9324469288458123
Bounds: [0.9324469288458123, 1]
Time: 0.6 s
+ Value iteration
Final error: 3.001709289030008E-07
Iterations: 55
Time: 0.6 s
Log file: modest_from-jani_check_default_csma.3-4_rep4.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 3.204 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4964855/tmpdr9cnt9vmodest_from-jani_check_default_csma.3-4_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 1460287 states.
Peak memory usage: 246 MB
Analysis results for model.jani
+ State space exploration
State size: 24 bytes
States: 1460287
Choices: 1471059
Branches: 2396727
Rate: 655425 states/s
Peak memory: 141.57 MB
Final size: 47.79 MB
Size on disk: 7.94 MB
Time (exploration): 2.2 s
Time (merging): 0.2 s
+ Property all_before_max
Probability: 0.9324469288458123
Bounds: [0.9324469288458123, 1]
Time: 0.5 s
+ Value iteration
Final error: 3.001709289030008E-07
Iterations: 55
Time: 0.5 s
Log file: modest_from-jani_check_default_csma.3-4_rep5.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 3.680 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4966926/tmpr5k_x9igmodest_from-jani_check_default_csma.3-4_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 1460287 states.
Peak memory usage: 244 MB
Analysis results for model.jani
+ State space exploration
State size: 24 bytes
States: 1460287
Choices: 1471059
Branches: 2396727
Rate: 570425 states/s
Peak memory: 141.53 MB
Final size: 47.79 MB
Size on disk: 7.94 MB
Time (exploration): 2.6 s
Time (merging): 0.2 s
+ Property all_before_max
Probability: 0.9324469288458123
Bounds: [0.9324469288458123, 1]
Time: 0.6 s
+ Value iteration
Final error: 3.001709289030008E-07
Iterations: 55
Time: 0.6 s