Log files for model wlan.5-0 and tool configuration modest_from-jani_to-umb_default
[0.0, 0.0, 0.0, 0.0, 0.0]
Log file: modest_from-jani_to-umb_default_wlan.5-0_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: 3.318 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4955707/tmpg0gicw4dmodest_from-jani_to-umb_default_wlan.5-0_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4955707/tmpc9_eew9jmodest_from-jani_to-umb_default_wlan.5-0_tmp_outdir_/model.umb /w0/tmp/slurm_tq429871.4955707/tmpc9_eew9jmodest_from-jani_to-umb_default_wlan.5-0_tmp_outdir_/umb.properties.txt --stop-after Exploration -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[3]: info: Expanding variable "s1" into 12 locations in automaton "station1".
model.jani:variables[4]: info: Expanding variable "s2" into 12 locations in automaton "station2".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 1295218 states.
Peak memory usage: 238 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 1295218
Choices: 1646074
Branches: 2929960
Rate: 486376 states/s
Peak memory: 82.56 MB
Final size: 57.27 MB
Size on disk: 10.42 MB
Time (exploration): 2.7 s
Time (merging): 0.3 s
+ UMB export
Time: 0.0 s
File size: 67.47 MB
Compression: None
############################## Output files ##############################
model.umb: Size of output file is 70747648 bytes
umb.properties.txt: Size of output file is 28 bytes
Log file: modest_from-jani_to-umb_default_wlan.5-0_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: 3.246 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4957386/tmpm6n69bqvmodest_from-jani_to-umb_default_wlan.5-0_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4957386/tmpyaqxlsenmodest_from-jani_to-umb_default_wlan.5-0_tmp_outdir_/model.umb /w0/tmp/slurm_tq429871.4957386/tmpyaqxlsenmodest_from-jani_to-umb_default_wlan.5-0_tmp_outdir_/umb.properties.txt --stop-after Exploration -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[3]: info: Expanding variable "s1" into 12 locations in automaton "station1".
model.jani:variables[4]: info: Expanding variable "s2" into 12 locations in automaton "station2".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 1295218 states.
Peak memory usage: 238 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 1295218
Choices: 1646074
Branches: 2929960
Rate: 501439 states/s
Peak memory: 82.99 MB
Final size: 57.27 MB
Size on disk: 10.42 MB
Time (exploration): 2.6 s
Time (merging): 0.3 s
+ UMB export
Time: 0.0 s
File size: 67.47 MB
Compression: None
############################## Output files ##############################
model.umb: Size of output file is 70747648 bytes
umb.properties.txt: Size of output file is 28 bytes
Log file: modest_from-jani_to-umb_default_wlan.5-0_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: 3.536 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4957614/tmpf9togtqqmodest_from-jani_to-umb_default_wlan.5-0_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4957614/tmphprxiox5modest_from-jani_to-umb_default_wlan.5-0_tmp_outdir_/model.umb /w0/tmp/slurm_tq429871.4957614/tmphprxiox5modest_from-jani_to-umb_default_wlan.5-0_tmp_outdir_/umb.properties.txt --stop-after Exploration -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[3]: info: Expanding variable "s1" into 12 locations in automaton "station1".
model.jani:variables[4]: info: Expanding variable "s2" into 12 locations in automaton "station2".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 1295218 states.
Peak memory usage: 238 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 1295218
Choices: 1646074
Branches: 2929960
Rate: 448017 states/s
Peak memory: 83.13 MB
Final size: 57.27 MB
Size on disk: 10.42 MB
Time (exploration): 2.9 s
Time (merging): 0.3 s
+ UMB export
Time: 0.0 s
File size: 67.47 MB
Compression: None
############################## Output files ##############################
model.umb: Size of output file is 70747648 bytes
umb.properties.txt: Size of output file is 28 bytes
Log file: modest_from-jani_to-umb_default_wlan.5-0_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: 3.416 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4957410/tmp011rb1iumodest_from-jani_to-umb_default_wlan.5-0_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4957410/tmphma9p5pimodest_from-jani_to-umb_default_wlan.5-0_tmp_outdir_/model.umb /w0/tmp/slurm_tq429871.4957410/tmphma9p5pimodest_from-jani_to-umb_default_wlan.5-0_tmp_outdir_/umb.properties.txt --stop-after Exploration -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[3]: info: Expanding variable "s1" into 12 locations in automaton "station1".
model.jani:variables[4]: info: Expanding variable "s2" into 12 locations in automaton "station2".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 1295218 states.
Peak memory usage: 238 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 1295218
Choices: 1646074
Branches: 2929960
Rate: 472363 states/s
Peak memory: 82.47 MB
Final size: 57.27 MB
Size on disk: 10.42 MB
Time (exploration): 2.8 s
Time (merging): 0.3 s
+ UMB export
Time: 0.0 s
File size: 67.47 MB
Compression: None
############################## Output files ##############################
model.umb: Size of output file is 70747648 bytes
umb.properties.txt: Size of output file is 28 bytes
Log file: modest_from-jani_to-umb_default_wlan.5-0_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: 3.136 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4957865/tmpubzt9__kmodest_from-jani_to-umb_default_wlan.5-0_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4957865/tmpxjeeqsc8modest_from-jani_to-umb_default_wlan.5-0_tmp_outdir_/model.umb /w0/tmp/slurm_tq429871.4957865/tmpxjeeqsc8modest_from-jani_to-umb_default_wlan.5-0_tmp_outdir_/umb.properties.txt --stop-after Exploration -D -Y --exhaustive
model.jani:model: info: model is an MDP model.
model.jani:variables[3]: info: Expanding variable "s1" into 12 locations in automaton "station1".
model.jani:variables[4]: info: Expanding variable "s2" into 12 locations in automaton "station2".
model.jani: info: Need 16 bytes per state.
model.jani: info: Explored 1295218 states.
Peak memory usage: 239 MB
Analysis results for model.jani
+ State space exploration
State size: 16 bytes
States: 1295218
Choices: 1646074
Branches: 2929960
Rate: 518917 states/s
Peak memory: 83.38 MB
Final size: 57.27 MB
Size on disk: 10.42 MB
Time (exploration): 2.5 s
Time (merging): 0.3 s
+ UMB export
Time: 0.0 s
File size: 67.47 MB
Compression: None
############################## Output files ##############################
model.umb: Size of output file is 70747648 bytes
umb.properties.txt: Size of output file is 28 bytes