Log files for model pacman.100 and tool configuration modest_from-jani_check_default
[245.306, 247.403, 248.969, 261.539, 245.647]
Log file: modest_from-jani_check_default_pacman.100_rep1.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 245.306 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4965753/tmpl300i0iymodest_from-jani_check_default_pacman.100_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[1]: info: Expanding variable "pMove" into 3 locations in automaton "arbiter".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 79440921 states.
Peak memory usage: 7033 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 341055 states/s
Peak memory: 3202.84 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 233.0 s
Time (merging): 7.9 s
+ Property crash
Probability: 0.5511176224662503
Bounds: [0.5511176224662503, 0.5511176224662503]
Time: 3.0 s
+ Value iteration
Final error: 0
Iterations: 2
Time: 2.5 s
Log file: modest_from-jani_check_default_pacman.100_rep2.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 247.403 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4966313/tmp35rd182gmodest_from-jani_check_default_pacman.100_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[1]: info: Expanding variable "pMove" into 3 locations in automaton "arbiter".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 79440921 states.
Peak memory usage: 7032 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 337755 states/s
Peak memory: 3203.32 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 235.2 s
Time (merging): 8.6 s
+ Property crash
Probability: 0.5511176224662503
Bounds: [0.5511176224662503, 0.5511176224662503]
Time: 2.7 s
+ Value iteration
Final error: 0
Iterations: 2
Time: 2.4 s
Log file: modest_from-jani_check_default_pacman.100_rep3.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 248.969 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4966715/tmp8t9br1slmodest_from-jani_check_default_pacman.100_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[1]: info: Expanding variable "pMove" into 3 locations in automaton "arbiter".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 79440921 states.
Peak memory usage: 7033 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 335400 states/s
Peak memory: 3203.08 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 236.9 s
Time (merging): 8.0 s
+ Property crash
Probability: 0.5511176224662503
Bounds: [0.5511176224662503, 0.5511176224662503]
Time: 3.4 s
+ Value iteration
Final error: 0
Iterations: 2
Time: 3.1 s
Log file: modest_from-jani_check_default_pacman.100_rep4.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 261.539 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4966869/tmpt4m5z20fmodest_from-jani_check_default_pacman.100_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[1]: info: Expanding variable "pMove" into 3 locations in automaton "arbiter".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 79440921 states.
Peak memory usage: 7032 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 319213 states/s
Peak memory: 3203.37 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 248.9 s
Time (merging): 7.9 s
+ Property crash
Probability: 0.5511176224662503
Bounds: [0.5511176224662503, 0.5511176224662503]
Time: 4.1 s
+ Value iteration
Final error: 0
Iterations: 2
Time: 3.8 s
Log file: modest_from-jani_check_default_pacman.100_rep5.log
Command(s):
../bin/modest mcsta %indir/model.jani -D -Y --exhaustive
Wallclock time: 245.647 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4966403/tmpbqj32dyqmodest_from-jani_check_default_pacman.100_tmp_indir_/model.jani -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[1]: info: Expanding variable "pMove" into 3 locations in automaton "arbiter".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 79440921 states.
Peak memory usage: 7032 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 341056 states/s
Peak memory: 3174.34 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 233.0 s
Time (merging): 8.1 s
+ Property crash
Probability: 0.5511176224662503
Bounds: [0.5511176224662503, 0.5511176224662503]
Time: 2.9 s
+ Value iteration
Final error: 0
Iterations: 2
Time: 2.6 s