Log files for model pacman.60 and tool configuration modest_from-jani_to-umb-xz_default
[333.0, 300.7, 299.4, 342.4, 303.1]
Log file: modest_from-jani_to-umb-xz_default_pacman.60_rep1.log
Command(s):
../bin/modest mcsta %indir/model.jani --umb %outdir/model.umb.xz %outdir/umbxz.properties.txt --umb-compress XZ --stop-after Exploration -D -Y --exhaustive
Wallclock time: 457.594 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4958148/tmpdvt1l_i3modest_from-jani_to-umb-xz_default_pacman.60_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4958148/tmpgpttlqnimodest_from-jani_to-umb-xz_default_pacman.60_tmp_outdir_/model.umb.xz /w0/tmp/slurm_tq429871.4958148/tmpgpttlqnimodest_from-jani_to-umb-xz_default_pacman.60_tmp_outdir_/umbxz.properties.txt --umb-compress XZ --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: 3353 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 38786521
Choices: 48926255
Branches: 53648196
Rate: 323224 states/s
Peak memory: 1683.48 MB
Final size: 1191.88 MB
Size on disk: 194.60 MB
Time (exploration): 120.0 s
Time (merging): 4.0 s
+ UMB export
Time: 333.0 s
File size: 65.40 MB
Compression: XZ (Optimal)
############################## Output files ##############################
model.umb.xz: Size of output file is 68576868 bytes
umbxz.properties.txt: Size of output file is 24 bytes
Log file: modest_from-jani_to-umb-xz_default_pacman.60_rep2.log
Command(s):
../bin/modest mcsta %indir/model.jani --umb %outdir/model.umb.xz %outdir/umbxz.properties.txt --umb-compress XZ --stop-after Exploration -D -Y --exhaustive
Wallclock time: 418.551 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4955265/tmpadpv6h15modest_from-jani_to-umb-xz_default_pacman.60_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4955265/tmp3bz7_xhpmodest_from-jani_to-umb-xz_default_pacman.60_tmp_outdir_/model.umb.xz /w0/tmp/slurm_tq429871.4955265/tmp3bz7_xhpmodest_from-jani_to-umb-xz_default_pacman.60_tmp_outdir_/umbxz.properties.txt --umb-compress XZ --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: 3353 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 38786521
Choices: 48926255
Branches: 53648196
Rate: 343408 states/s
Peak memory: 1683.33 MB
Final size: 1191.88 MB
Size on disk: 194.60 MB
Time (exploration): 113.0 s
Time (merging): 3.9 s
+ UMB export
Time: 300.7 s
File size: 65.34 MB
Compression: XZ (Optimal)
############################## Output files ##############################
model.umb.xz: Size of output file is 68516028 bytes
umbxz.properties.txt: Size of output file is 24 bytes
Log file: modest_from-jani_to-umb-xz_default_pacman.60_rep3.log
Command(s):
../bin/modest mcsta %indir/model.jani --umb %outdir/model.umb.xz %outdir/umbxz.properties.txt --umb-compress XZ --stop-after Exploration -D -Y --exhaustive
Wallclock time: 416.421 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4958307/tmp3g2gdmenmodest_from-jani_to-umb-xz_default_pacman.60_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4958307/tmpsx22lx5vmodest_from-jani_to-umb-xz_default_pacman.60_tmp_outdir_/model.umb.xz /w0/tmp/slurm_tq429871.4958307/tmpsx22lx5vmodest_from-jani_to-umb-xz_default_pacman.60_tmp_outdir_/umbxz.properties.txt --umb-compress XZ --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: 3353 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 38786521
Choices: 48926255
Branches: 53648196
Rate: 345150 states/s
Peak memory: 1683.18 MB
Final size: 1191.88 MB
Size on disk: 194.60 MB
Time (exploration): 112.4 s
Time (merging): 4.1 s
+ UMB export
Time: 299.4 s
File size: 65.29 MB
Compression: XZ (Optimal)
############################## Output files ##############################
model.umb.xz: Size of output file is 68462256 bytes
umbxz.properties.txt: Size of output file is 24 bytes
Log file: modest_from-jani_to-umb-xz_default_pacman.60_rep4.log
Command(s):
../bin/modest mcsta %indir/model.jani --umb %outdir/model.umb.xz %outdir/umbxz.properties.txt --umb-compress XZ --stop-after Exploration -D -Y --exhaustive
Wallclock time: 461.076 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4957077/tmpa6i0_tvnmodest_from-jani_to-umb-xz_default_pacman.60_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4957077/tmpqucusrb1modest_from-jani_to-umb-xz_default_pacman.60_tmp_outdir_/model.umb.xz /w0/tmp/slurm_tq429871.4957077/tmpqucusrb1modest_from-jani_to-umb-xz_default_pacman.60_tmp_outdir_/umbxz.properties.txt --umb-compress XZ --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: 3354 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 38786521
Choices: 48926255
Branches: 53648196
Rate: 339887 states/s
Peak memory: 1683.73 MB
Final size: 1191.88 MB
Size on disk: 194.60 MB
Time (exploration): 114.2 s
Time (merging): 3.9 s
+ UMB export
Time: 342.4 s
File size: 65.24 MB
Compression: XZ (Optimal)
############################## Output files ##############################
model.umb.xz: Size of output file is 68405136 bytes
umbxz.properties.txt: Size of output file is 24 bytes
Log file: modest_from-jani_to-umb-xz_default_pacman.60_rep5.log
Command(s):
../bin/modest mcsta %indir/model.jani --umb %outdir/model.umb.xz %outdir/umbxz.properties.txt --umb-compress XZ --stop-after Exploration -D -Y --exhaustive
Wallclock time: 421.699 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4958449/tmprty9tflvmodest_from-jani_to-umb-xz_default_pacman.60_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4958449/tmpouln32o7modest_from-jani_to-umb-xz_default_pacman.60_tmp_outdir_/model.umb.xz /w0/tmp/slurm_tq429871.4958449/tmpouln32o7modest_from-jani_to-umb-xz_default_pacman.60_tmp_outdir_/umbxz.properties.txt --umb-compress XZ --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: 3352 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 38786521
Choices: 48926255
Branches: 53648196
Rate: 340161 states/s
Peak memory: 1683.16 MB
Final size: 1191.88 MB
Size on disk: 194.60 MB
Time (exploration): 114.0 s
Time (merging): 4.0 s
+ UMB export
Time: 303.1 s
File size: 65.20 MB
Compression: XZ (Optimal)
############################## Output files ##############################
model.umb.xz: Size of output file is 68363856 bytes
umbxz.properties.txt: Size of output file is 24 bytes