Log files for model pacman.100 and tool configuration modest_from-jani_to-imca_default
[16.0, 18.1, 16.8, 14.7, 16.7]
Log file: modest_from-jani_to-imca_default_pacman.100_rep1.log
Command(s):
../bin/modest mcsta %indir/model.jani --statespace %outdir/model.mrm IMCA --stop-after Exploration -D -Y --exhaustive
Wallclock time: 235.457 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4955778/tmpvglncplxmodest_from-jani_to-imca_default_pacman.100_tmp_indir_/model.jani --statespace /w0/tmp/slurm_tq429871.4955778/tmpwju_2aesmodest_from-jani_to-imca_default_pacman.100_tmp_outdir_/model.mrm IMCA --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.4955778/tmpwju_2aesmodest_from-jani_to-imca_default_pacman.100_tmp_outdir_/model.mrm".
Peak memory usage: 6427 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 375684 states/s
Peak memory: 3174.34 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 211.5 s
Time (merging): 7.3 s
+ Export to IMCA
Time: 16.0 s
File size: 2655.38 MB
############################## Output files ##############################
model.mrm: Size of output file is 2784367052 bytes
Log file: modest_from-jani_to-imca_default_pacman.100_rep2.log
Command(s):
../bin/modest mcsta %indir/model.jani --statespace %outdir/model.mrm IMCA --stop-after Exploration -D -Y --exhaustive
Wallclock time: 272.557 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4957547/tmpbfny1o96modest_from-jani_to-imca_default_pacman.100_tmp_indir_/model.jani --statespace /w0/tmp/slurm_tq429871.4957547/tmps39v087umodest_from-jani_to-imca_default_pacman.100_tmp_outdir_/model.mrm IMCA --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.4957547/tmps39v087umodest_from-jani_to-imca_default_pacman.100_tmp_outdir_/model.mrm".
Peak memory usage: 6426 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 323632 states/s
Peak memory: 3193.10 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 245.5 s
Time (merging): 8.3 s
+ Export to IMCA
Time: 18.1 s
File size: 2655.38 MB
############################## Output files ##############################
model.mrm: Size of output file is 2784367052 bytes
Log file: modest_from-jani_to-imca_default_pacman.100_rep3.log
Command(s):
../bin/modest mcsta %indir/model.jani --statespace %outdir/model.mrm IMCA --stop-after Exploration -D -Y --exhaustive
Wallclock time: 257.539 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4957796/tmpxx59hr1imodest_from-jani_to-imca_default_pacman.100_tmp_indir_/model.jani --statespace /w0/tmp/slurm_tq429871.4957796/tmpcd5zygv7modest_from-jani_to-imca_default_pacman.100_tmp_outdir_/model.mrm IMCA --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.4957796/tmpcd5zygv7modest_from-jani_to-imca_default_pacman.100_tmp_outdir_/model.mrm".
Peak memory usage: 6426 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 342636 states/s
Peak memory: 3203.03 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 231.9 s
Time (merging): 8.2 s
+ Export to IMCA
Time: 16.8 s
File size: 2655.38 MB
############################## Output files ##############################
model.mrm: Size of output file is 2784367052 bytes
Log file: modest_from-jani_to-imca_default_pacman.100_rep4.log
Command(s):
../bin/modest mcsta %indir/model.jani --statespace %outdir/model.mrm IMCA --stop-after Exploration -D -Y --exhaustive
Wallclock time: 233.473 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4957872/tmpeylim7pcmodest_from-jani_to-imca_default_pacman.100_tmp_indir_/model.jani --statespace /w0/tmp/slurm_tq429871.4957872/tmpi8269mo1modest_from-jani_to-imca_default_pacman.100_tmp_outdir_/model.mrm IMCA --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.4957872/tmpi8269mo1modest_from-jani_to-imca_default_pacman.100_tmp_outdir_/model.mrm".
Peak memory usage: 6425 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 377749 states/s
Peak memory: 3174.57 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 210.3 s
Time (merging): 7.7 s
+ Export to IMCA
Time: 14.7 s
File size: 2655.38 MB
############################## Output files ##############################
model.mrm: Size of output file is 2784367052 bytes
Log file: modest_from-jani_to-imca_default_pacman.100_rep5.log
Command(s):
../bin/modest mcsta %indir/model.jani --statespace %outdir/model.mrm IMCA --stop-after Exploration -D -Y --exhaustive
Wallclock time: 259.576 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4958206/tmpzpemfmq2modest_from-jani_to-imca_default_pacman.100_tmp_indir_/model.jani --statespace /w0/tmp/slurm_tq429871.4958206/tmpsaim40b7modest_from-jani_to-imca_default_pacman.100_tmp_outdir_/model.mrm IMCA --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.4958206/tmpsaim40b7modest_from-jani_to-imca_default_pacman.100_tmp_outdir_/model.mrm".
Peak memory usage: 6427 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 338890 states/s
Peak memory: 3203.25 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 234.4 s
Time (merging): 7.8 s
+ Export to IMCA
Time: 16.7 s
File size: 2655.38 MB
############################## Output files ##############################
model.mrm: Size of output file is 2784367052 bytes