Log files for model pacman.100 and tool configuration modest_from-jani_to-umb_default
[1.6, 1.1, 1.3, 1.1, 1.2]
Log file: modest_from-jani_to-umb_default_pacman.100_rep1.log
Command(s):
../bin/modest mcsta %indir/model.jani --umb %outdir/model.umb %outdir/umb.properties.txt --stop-after Exploration -D -Y --exhaustive
Wallclock time: 245.334 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4956044/tmpr2o0jpy4modest_from-jani_to-umb_default_pacman.100_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4956044/tmpu3knl17hmodest_from-jani_to-umb_default_pacman.100_tmp_outdir_/model.umb /w0/tmp/slurm_tq429871.4956044/tmpu3knl17hmodest_from-jani_to-umb_default_pacman.100_tmp_outdir_/umb.properties.txt --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.
Peak memory usage: 6427 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 338978 states/s
Peak memory: 3202.92 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 234.4 s
Time (merging): 8.1 s
+ UMB export
Time: 1.6 s
File size: 3067.54 MB
Compression: None
############################## Output files ##############################
model.umb: Size of output file is 3216545280 bytes
umb.properties.txt: Size of output file is 24 bytes
Log file: modest_from-jani_to-umb_default_pacman.100_rep2.log
Command(s):
../bin/modest mcsta %indir/model.jani --umb %outdir/model.umb %outdir/umb.properties.txt --stop-after Exploration -D -Y --exhaustive
Wallclock time: 246.078 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4955892/tmpi8qb7dklmodest_from-jani_to-umb_default_pacman.100_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4955892/tmpn50sbe1dmodest_from-jani_to-umb_default_pacman.100_tmp_outdir_/model.umb /w0/tmp/slurm_tq429871.4955892/tmpn50sbe1dmodest_from-jani_to-umb_default_pacman.100_tmp_outdir_/umb.properties.txt --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.
Peak memory usage: 6428 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 337233 states/s
Peak memory: 3202.67 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 235.6 s
Time (merging): 8.5 s
+ UMB export
Time: 1.1 s
File size: 3067.54 MB
Compression: None
############################## Output files ##############################
model.umb: Size of output file is 3216545280 bytes
umb.properties.txt: Size of output file is 24 bytes
Log file: modest_from-jani_to-umb_default_pacman.100_rep3.log
Command(s):
../bin/modest mcsta %indir/model.jani --umb %outdir/model.umb %outdir/umb.properties.txt --stop-after Exploration -D -Y --exhaustive
Wallclock time: 251.097 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4958289/tmp1_298chmmodest_from-jani_to-umb_default_pacman.100_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4958289/tmplnhrs8ysmodest_from-jani_to-umb_default_pacman.100_tmp_outdir_/model.umb /w0/tmp/slurm_tq429871.4958289/tmplnhrs8ysmodest_from-jani_to-umb_default_pacman.100_tmp_outdir_/umb.properties.txt --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.
Peak memory usage: 6427 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 330567 states/s
Peak memory: 3202.52 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 240.3 s
Time (merging): 8.0 s
+ UMB export
Time: 1.3 s
File size: 3067.54 MB
Compression: None
############################## Output files ##############################
model.umb: Size of output file is 3216545280 bytes
umb.properties.txt: Size of output file is 24 bytes
Log file: modest_from-jani_to-umb_default_pacman.100_rep4.log
Command(s):
../bin/modest mcsta %indir/model.jani --umb %outdir/model.umb %outdir/umb.properties.txt --stop-after Exploration -D -Y --exhaustive
Wallclock time: 242.309 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4955719/tmpeu0uaqxsmodest_from-jani_to-umb_default_pacman.100_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4955719/tmpfj1nwpwamodest_from-jani_to-umb_default_pacman.100_tmp_outdir_/model.umb /w0/tmp/slurm_tq429871.4955719/tmpfj1nwpwamodest_from-jani_to-umb_default_pacman.100_tmp_outdir_/umb.properties.txt --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.
Peak memory usage: 6426 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 342971 states/s
Peak memory: 3202.99 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 231.7 s
Time (merging): 7.8 s
+ UMB export
Time: 1.1 s
File size: 3067.54 MB
Compression: None
############################## Output files ##############################
model.umb: Size of output file is 3216545280 bytes
umb.properties.txt: Size of output file is 24 bytes
Log file: modest_from-jani_to-umb_default_pacman.100_rep5.log
Command(s):
../bin/modest mcsta %indir/model.jani --umb %outdir/model.umb %outdir/umb.properties.txt --stop-after Exploration -D -Y --exhaustive
Wallclock time: 257.508 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4957054/tmpsav0aflumodest_from-jani_to-umb_default_pacman.100_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4957054/tmp0cm9twsmmodest_from-jani_to-umb_default_pacman.100_tmp_outdir_/model.umb /w0/tmp/slurm_tq429871.4957054/tmp0cm9twsmmodest_from-jani_to-umb_default_pacman.100_tmp_outdir_/umb.properties.txt --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.
Peak memory usage: 6429 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 79440921
Choices: 100215175
Branches: 109963876
Rate: 323108 states/s
Peak memory: 3193.19 MB
Final size: 2442.50 MB
Size on disk: 398.95 MB
Time (exploration): 245.9 s
Time (merging): 8.7 s
+ UMB export
Time: 1.2 s
File size: 3067.54 MB
Compression: None
############################## Output files ##############################
model.umb: Size of output file is 3216545280 bytes
umb.properties.txt: Size of output file is 24 bytes