Log files for model pacman.60 and tool configuration modest_from-jani_to-umb-gz_default
[32.8, 34.6, 32.7, 33.0, 32.8]
Log file: modest_from-jani_to-umb-gz_default_pacman.60_rep1.log
Command(s):
../bin/modest mcsta %indir/model.jani --umb %outdir/model.umb.gz %outdir/umbgz.properties.txt --umb-compress GZIP --stop-after Exploration -D -Y --exhaustive
Wallclock time: 152.875 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4957844/tmp3ndxhkshmodest_from-jani_to-umb-gz_default_pacman.60_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4957844/tmpq6pfszy9modest_from-jani_to-umb-gz_default_pacman.60_tmp_outdir_/model.umb.gz /w0/tmp/slurm_tq429871.4957844/tmpq6pfszy9modest_from-jani_to-umb-gz_default_pacman.60_tmp_outdir_/umbgz.properties.txt --umb-compress GZIP --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 38786521 states.
Peak memory usage: 3259 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 38786521
Choices: 48926255
Branches: 53648196
Rate: 335721 states/s
Peak memory: 1683.60 MB
Final size: 1191.88 MB
Size on disk: 194.60 MB
Time (exploration): 115.6 s
Time (merging): 4.0 s
+ UMB export
Time: 32.8 s
File size: 225.98 MB
Compression: GZip (Optimal)
############################## Output files ##############################
model.umb.gz: Size of output file is 236959848 bytes
umbgz.properties.txt: Size of output file is 24 bytes
Log file: modest_from-jani_to-umb-gz_default_pacman.60_rep2.log
Command(s):
../bin/modest mcsta %indir/model.jani --umb %outdir/model.umb.gz %outdir/umbgz.properties.txt --umb-compress GZIP --stop-after Exploration -D -Y --exhaustive
Wallclock time: 149.748 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4957944/tmpaj8n_te7modest_from-jani_to-umb-gz_default_pacman.60_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4957944/tmp0pf8o2_6modest_from-jani_to-umb-gz_default_pacman.60_tmp_outdir_/model.umb.gz /w0/tmp/slurm_tq429871.4957944/tmp0pf8o2_6modest_from-jani_to-umb-gz_default_pacman.60_tmp_outdir_/umbgz.properties.txt --umb-compress GZIP --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 38786521 states.
Peak memory usage: 3259 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 38786521
Choices: 48926255
Branches: 53648196
Rate: 350214 states/s
Peak memory: 1683.44 MB
Final size: 1191.88 MB
Size on disk: 194.60 MB
Time (exploration): 110.8 s
Time (merging): 3.9 s
+ UMB export
Time: 34.6 s
File size: 225.98 MB
Compression: GZip (Optimal)
############################## Output files ##############################
model.umb.gz: Size of output file is 236959838 bytes
umbgz.properties.txt: Size of output file is 24 bytes
Log file: modest_from-jani_to-umb-gz_default_pacman.60_rep3.log
Command(s):
../bin/modest mcsta %indir/model.jani --umb %outdir/model.umb.gz %outdir/umbgz.properties.txt --umb-compress GZIP --stop-after Exploration -D -Y --exhaustive
Wallclock time: 155.292 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4956664/tmpyjaf3yykmodest_from-jani_to-umb-gz_default_pacman.60_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4956664/tmp39gmlej1modest_from-jani_to-umb-gz_default_pacman.60_tmp_outdir_/model.umb.gz /w0/tmp/slurm_tq429871.4956664/tmp39gmlej1modest_from-jani_to-umb-gz_default_pacman.60_tmp_outdir_/umbgz.properties.txt --umb-compress GZIP --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 38786521 states.
Peak memory usage: 3260 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 38786521
Choices: 48926255
Branches: 53648196
Rate: 328418 states/s
Peak memory: 1683.40 MB
Final size: 1191.88 MB
Size on disk: 194.60 MB
Time (exploration): 118.1 s
Time (merging): 3.9 s
+ UMB export
Time: 32.7 s
File size: 225.98 MB
Compression: GZip (Optimal)
############################## Output files ##############################
model.umb.gz: Size of output file is 236959845 bytes
umbgz.properties.txt: Size of output file is 24 bytes
Log file: modest_from-jani_to-umb-gz_default_pacman.60_rep4.log
Command(s):
../bin/modest mcsta %indir/model.jani --umb %outdir/model.umb.gz %outdir/umbgz.properties.txt --umb-compress GZIP --stop-after Exploration -D -Y --exhaustive
Wallclock time: 151.346 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4955907/tmp9x_q8c48modest_from-jani_to-umb-gz_default_pacman.60_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4955907/tmpr7a5isqumodest_from-jani_to-umb-gz_default_pacman.60_tmp_outdir_/model.umb.gz /w0/tmp/slurm_tq429871.4955907/tmpr7a5isqumodest_from-jani_to-umb-gz_default_pacman.60_tmp_outdir_/umbgz.properties.txt --umb-compress GZIP --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 38786521 states.
Peak memory usage: 3259 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 38786521
Choices: 48926255
Branches: 53648196
Rate: 340935 states/s
Peak memory: 1683.77 MB
Final size: 1191.88 MB
Size on disk: 194.60 MB
Time (exploration): 113.8 s
Time (merging): 3.9 s
+ UMB export
Time: 33.0 s
File size: 225.98 MB
Compression: GZip (Optimal)
############################## Output files ##############################
model.umb.gz: Size of output file is 236959846 bytes
umbgz.properties.txt: Size of output file is 24 bytes
Log file: modest_from-jani_to-umb-gz_default_pacman.60_rep5.log
Command(s):
../bin/modest mcsta %indir/model.jani --umb %outdir/model.umb.gz %outdir/umbgz.properties.txt --umb-compress GZIP --stop-after Exploration -D -Y --exhaustive
Wallclock time: 157.662 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4958173/tmpzn_bbqakmodest_from-jani_to-umb-gz_default_pacman.60_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4958173/tmpdd0z6_iemodest_from-jani_to-umb-gz_default_pacman.60_tmp_outdir_/model.umb.gz /w0/tmp/slurm_tq429871.4958173/tmpdd0z6_iemodest_from-jani_to-umb-gz_default_pacman.60_tmp_outdir_/umbgz.properties.txt --umb-compress GZIP --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 38786521 states.
Peak memory usage: 3260 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 38786521
Choices: 48926255
Branches: 53648196
Rate: 322702 states/s
Peak memory: 1683.84 MB
Final size: 1191.88 MB
Size on disk: 194.60 MB
Time (exploration): 120.2 s
Time (merging): 4.1 s
+ UMB export
Time: 32.8 s
File size: 225.98 MB
Compression: GZip (Optimal)
############################## Output files ##############################
model.umb.gz: Size of output file is 236959836 bytes
umbgz.properties.txt: Size of output file is 24 bytes