Log files for model pacman.100 and tool configuration modest_from-jani_to-aut_default
[23.2, 23.3, 23.7, 22.4, 20.9]
Log file: modest_from-jani_to-aut_default_pacman.100_rep1.log
Command(s):
../bin/modest mcsta %indir/model.jani --statespace %outdir/model.aut AUT --stop-after Exploration -D -Y --exhaustive
Wallclock time: 258.989 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4956499/tmpwp86ho6wmodest_from-jani_to-aut_default_pacman.100_tmp_indir_/model.jani --statespace /w0/tmp/slurm_tq429871.4956499/tmpgwz8yw_9modest_from-jani_to-aut_default_pacman.100_tmp_outdir_/model.aut AUT --stop-after Exploration -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.
model.jani: info: Exported state space to file "/w0/tmp/slurm_tq429871.4956499/tmpgwz8yw_9modest_from-jani_to-aut_default_pacman.100_tmp_outdir_/model.aut".
Peak memory usage: 6425 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 349430 states/s
Peak memory: 3174.35 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 227.4 s
Time (merging): 7.8 s
+ Export to AUT
Time: 23.2 s
File size: 5372.51 MB
############################## Output files ##############################
model.aut: Size of output file is 5633489486 bytes
Log file: modest_from-jani_to-aut_default_pacman.100_rep2.log
Command(s):
../bin/modest mcsta %indir/model.jani --statespace %outdir/model.aut AUT --stop-after Exploration -D -Y --exhaustive
Wallclock time: 269.331 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4956128/tmp62mvf9jrmodest_from-jani_to-aut_default_pacman.100_tmp_indir_/model.jani --statespace /w0/tmp/slurm_tq429871.4956128/tmpp2q63gdymodest_from-jani_to-aut_default_pacman.100_tmp_outdir_/model.aut AUT --stop-after Exploration -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.
model.jani: info: Exported state space to file "/w0/tmp/slurm_tq429871.4956128/tmpp2q63gdymodest_from-jani_to-aut_default_pacman.100_tmp_outdir_/model.aut".
Peak memory usage: 6429 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 336447 states/s
Peak memory: 3202.66 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 236.1 s
Time (merging): 8.2 s
+ Export to AUT
Time: 23.3 s
File size: 5372.51 MB
############################## Output files ##############################
model.aut: Size of output file is 5633489486 bytes
Log file: modest_from-jani_to-aut_default_pacman.100_rep3.log
Command(s):
../bin/modest mcsta %indir/model.jani --statespace %outdir/model.aut AUT --stop-after Exploration -D -Y --exhaustive
Wallclock time: 269.079 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4957355/tmp3r3bijmmmodest_from-jani_to-aut_default_pacman.100_tmp_indir_/model.jani --statespace /w0/tmp/slurm_tq429871.4957355/tmpx2cpm3d4modest_from-jani_to-aut_default_pacman.100_tmp_outdir_/model.aut AUT --stop-after Exploration -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.
model.jani: info: Exported state space to file "/w0/tmp/slurm_tq429871.4957355/tmpx2cpm3d4modest_from-jani_to-aut_default_pacman.100_tmp_outdir_/model.aut".
Peak memory usage: 6427 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 336985 states/s
Peak memory: 3203.05 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 235.8 s
Time (merging): 8.9 s
+ Export to AUT
Time: 23.7 s
File size: 5372.51 MB
############################## Output files ##############################
model.aut: Size of output file is 5633489486 bytes
Log file: modest_from-jani_to-aut_default_pacman.100_rep4.log
Command(s):
../bin/modest mcsta %indir/model.jani --statespace %outdir/model.aut AUT --stop-after Exploration -D -Y --exhaustive
Wallclock time: 269.829 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4956107/tmp47shovlpmodest_from-jani_to-aut_default_pacman.100_tmp_indir_/model.jani --statespace /w0/tmp/slurm_tq429871.4956107/tmpm4r35r9imodest_from-jani_to-aut_default_pacman.100_tmp_outdir_/model.aut AUT --stop-after Exploration -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.
model.jani: info: Exported state space to file "/w0/tmp/slurm_tq429871.4956107/tmpm4r35r9imodest_from-jani_to-aut_default_pacman.100_tmp_outdir_/model.aut".
Peak memory usage: 6427 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 334501 states/s
Peak memory: 3203.26 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 237.5 s
Time (merging): 9.1 s
+ Export to AUT
Time: 22.4 s
File size: 5372.51 MB
############################## Output files ##############################
model.aut: Size of output file is 5633489486 bytes
Log file: modest_from-jani_to-aut_default_pacman.100_rep5.log
Command(s):
../bin/modest mcsta %indir/model.jani --statespace %outdir/model.aut AUT --stop-after Exploration -D -Y --exhaustive
Wallclock time: 237.955 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4955681/tmpda31_w2vmodest_from-jani_to-aut_default_pacman.100_tmp_indir_/model.jani --statespace /w0/tmp/slurm_tq429871.4955681/tmpog55os3nmodest_from-jani_to-aut_default_pacman.100_tmp_outdir_/model.aut AUT --stop-after Exploration -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.
model.jani: info: Exported state space to file "/w0/tmp/slurm_tq429871.4955681/tmpog55os3nmodest_from-jani_to-aut_default_pacman.100_tmp_outdir_/model.aut".
Peak memory usage: 6428 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 379602 states/s
Peak memory: 3175.13 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 209.3 s
Time (merging): 7.2 s
+ Export to AUT
Time: 20.9 s
File size: 5372.51 MB
############################## Output files ##############################
model.aut: Size of output file is 5633489486 bytes