Log files for model polling.18-16 and tool configuration modest_from-jani_to-umb-xz_default
[224.3, 223.3, 223.8, 228.9, 265.1]
Log file: modest_from-jani_to-umb-xz_default_polling.18-16_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: 293.973 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4958435/tmphpqtyk0nmodest_from-jani_to-umb-xz_default_polling.18-16_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4958435/tmptccbrlbhmodest_from-jani_to-umb-xz_default_polling.18-16_tmp_outdir_/model.umb.xz /w0/tmp/slurm_tq429871.4958435/tmptccbrlbhmodest_from-jani_to-umb-xz_default_polling.18-16_tmp_outdir_/umbxz.properties.txt --umb-compress XZ --stop-after Exploration -D -Y --exhaustive
model.jani:model: info: model is a CTMC model.
model.jani:variables[3]: info: Expanding variable "a" into 2 locations in automaton "server".
model.jani:automata[1].variables[0]: info: Expanding variable "s1" into 2 locations in automaton "station1".
model.jani:automata[2].variables[0]: info: Expanding variable "s2" into 2 locations in automaton "station2".
model.jani:automata[3].variables[0]: info: Expanding variable "s3" into 2 locations in automaton "station3".
model.jani:automata[4].variables[0]: info: Expanding variable "s4" into 2 locations in automaton "station4".
model.jani:automata[5].variables[0]: info: Expanding variable "s5" into 2 locations in automaton "station5".
model.jani:automata[6].variables[0]: info: Expanding variable "s6" into 2 locations in automaton "station6".
model.jani:automata[7].variables[0]: info: Expanding variable "s7" into 2 locations in automaton "station7".
model.jani:automata[8].variables[0]: info: Expanding variable "s8" into 2 locations in automaton "station8".
model.jani:automata[9].variables[0]: info: Expanding variable "s9" into 2 locations in automaton "station9".
model.jani:automata[10].variables[0]: info: Expanding variable "s10" into 2 locations in automaton "station10".
model.jani:automata[11].variables[0]: info: Expanding variable "s11" into 2 locations in automaton "station11".
model.jani:automata[12].variables[0]: info: Expanding variable "s12" into 2 locations in automaton "station12".
model.jani:automata[13].variables[0]: info: Expanding variable "s13" into 2 locations in automaton "station13".
model.jani:automata[14].variables[0]: info: Expanding variable "s14" into 2 locations in automaton "station14".
model.jani:automata[15].variables[0]: info: Expanding variable "s15" into 2 locations in automaton "station15".
model.jani:automata[16].variables[0]: info: Expanding variable "s16" into 2 locations in automaton "station16".
model.jani:automata[17].variables[0]: info: Expanding variable "s17" into 2 locations in automaton "station17".
model.jani:automata[18].variables[0]: info: Expanding variable "s18" into 2 locations in automaton "station18".
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 7077888 states.
Peak memory usage: 1753 MB
Analysis results for model.jani
+ State space exploration
State size: 24 bytes
States: 7077888
Choices: 7077888
Branches: 69599232
Rate: 108306 states/s
Peak memory: 362.01 MB
Final size: 1116.00 MB
Size on disk: 223.88 MB
Time (exploration): 65.4 s
Time (merging): 4.0 s
+ UMB export
Time: 224.3 s
File size: 46.61 MB
Compression: XZ (Optimal)
############################## Output files ##############################
model.umb.xz: Size of output file is 48872992 bytes
umbxz.properties.txt: Size of output file is 36 bytes
Log file: modest_from-jani_to-umb-xz_default_polling.18-16_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: 295.151 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4957199/tmp9clivttfmodest_from-jani_to-umb-xz_default_polling.18-16_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4957199/tmplwvz7ailmodest_from-jani_to-umb-xz_default_polling.18-16_tmp_outdir_/model.umb.xz /w0/tmp/slurm_tq429871.4957199/tmplwvz7ailmodest_from-jani_to-umb-xz_default_polling.18-16_tmp_outdir_/umbxz.properties.txt --umb-compress XZ --stop-after Exploration -D -Y --exhaustive
model.jani:model: info: model is a CTMC model.
model.jani:variables[3]: info: Expanding variable "a" into 2 locations in automaton "server".
model.jani:automata[1].variables[0]: info: Expanding variable "s1" into 2 locations in automaton "station1".
model.jani:automata[2].variables[0]: info: Expanding variable "s2" into 2 locations in automaton "station2".
model.jani:automata[3].variables[0]: info: Expanding variable "s3" into 2 locations in automaton "station3".
model.jani:automata[4].variables[0]: info: Expanding variable "s4" into 2 locations in automaton "station4".
model.jani:automata[5].variables[0]: info: Expanding variable "s5" into 2 locations in automaton "station5".
model.jani:automata[6].variables[0]: info: Expanding variable "s6" into 2 locations in automaton "station6".
model.jani:automata[7].variables[0]: info: Expanding variable "s7" into 2 locations in automaton "station7".
model.jani:automata[8].variables[0]: info: Expanding variable "s8" into 2 locations in automaton "station8".
model.jani:automata[9].variables[0]: info: Expanding variable "s9" into 2 locations in automaton "station9".
model.jani:automata[10].variables[0]: info: Expanding variable "s10" into 2 locations in automaton "station10".
model.jani:automata[11].variables[0]: info: Expanding variable "s11" into 2 locations in automaton "station11".
model.jani:automata[12].variables[0]: info: Expanding variable "s12" into 2 locations in automaton "station12".
model.jani:automata[13].variables[0]: info: Expanding variable "s13" into 2 locations in automaton "station13".
model.jani:automata[14].variables[0]: info: Expanding variable "s14" into 2 locations in automaton "station14".
model.jani:automata[15].variables[0]: info: Expanding variable "s15" into 2 locations in automaton "station15".
model.jani:automata[16].variables[0]: info: Expanding variable "s16" into 2 locations in automaton "station16".
model.jani:automata[17].variables[0]: info: Expanding variable "s17" into 2 locations in automaton "station17".
model.jani:automata[18].variables[0]: info: Expanding variable "s18" into 2 locations in automaton "station18".
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 7077888 states.
Peak memory usage: 1753 MB
Analysis results for model.jani
+ State space exploration
State size: 24 bytes
States: 7077888
Choices: 7077888
Branches: 69599232
Rate: 105524 states/s
Peak memory: 360.55 MB
Final size: 1116.00 MB
Size on disk: 223.88 MB
Time (exploration): 67.1 s
Time (merging): 4.0 s
+ UMB export
Time: 223.3 s
File size: 46.65 MB
Compression: XZ (Optimal)
############################## Output files ##############################
model.umb.xz: Size of output file is 48911468 bytes
umbxz.properties.txt: Size of output file is 36 bytes
Log file: modest_from-jani_to-umb-xz_default_polling.18-16_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: 294.480 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4955699/tmp_i90tuvimodest_from-jani_to-umb-xz_default_polling.18-16_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4955699/tmplau8upaamodest_from-jani_to-umb-xz_default_polling.18-16_tmp_outdir_/model.umb.xz /w0/tmp/slurm_tq429871.4955699/tmplau8upaamodest_from-jani_to-umb-xz_default_polling.18-16_tmp_outdir_/umbxz.properties.txt --umb-compress XZ --stop-after Exploration -D -Y --exhaustive
model.jani:model: info: model is a CTMC model.
model.jani:variables[3]: info: Expanding variable "a" into 2 locations in automaton "server".
model.jani:automata[1].variables[0]: info: Expanding variable "s1" into 2 locations in automaton "station1".
model.jani:automata[2].variables[0]: info: Expanding variable "s2" into 2 locations in automaton "station2".
model.jani:automata[3].variables[0]: info: Expanding variable "s3" into 2 locations in automaton "station3".
model.jani:automata[4].variables[0]: info: Expanding variable "s4" into 2 locations in automaton "station4".
model.jani:automata[5].variables[0]: info: Expanding variable "s5" into 2 locations in automaton "station5".
model.jani:automata[6].variables[0]: info: Expanding variable "s6" into 2 locations in automaton "station6".
model.jani:automata[7].variables[0]: info: Expanding variable "s7" into 2 locations in automaton "station7".
model.jani:automata[8].variables[0]: info: Expanding variable "s8" into 2 locations in automaton "station8".
model.jani:automata[9].variables[0]: info: Expanding variable "s9" into 2 locations in automaton "station9".
model.jani:automata[10].variables[0]: info: Expanding variable "s10" into 2 locations in automaton "station10".
model.jani:automata[11].variables[0]: info: Expanding variable "s11" into 2 locations in automaton "station11".
model.jani:automata[12].variables[0]: info: Expanding variable "s12" into 2 locations in automaton "station12".
model.jani:automata[13].variables[0]: info: Expanding variable "s13" into 2 locations in automaton "station13".
model.jani:automata[14].variables[0]: info: Expanding variable "s14" into 2 locations in automaton "station14".
model.jani:automata[15].variables[0]: info: Expanding variable "s15" into 2 locations in automaton "station15".
model.jani:automata[16].variables[0]: info: Expanding variable "s16" into 2 locations in automaton "station16".
model.jani:automata[17].variables[0]: info: Expanding variable "s17" into 2 locations in automaton "station17".
model.jani:automata[18].variables[0]: info: Expanding variable "s18" into 2 locations in automaton "station18".
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 7077888 states.
Peak memory usage: 1753 MB
Analysis results for model.jani
+ State space exploration
State size: 24 bytes
States: 7077888
Choices: 7077888
Branches: 69599232
Rate: 106797 states/s
Peak memory: 361.96 MB
Final size: 1116.00 MB
Size on disk: 223.88 MB
Time (exploration): 66.3 s
Time (merging): 4.1 s
+ UMB export
Time: 223.8 s
File size: 46.79 MB
Compression: XZ (Optimal)
############################## Output files ##############################
model.umb.xz: Size of output file is 49065392 bytes
umbxz.properties.txt: Size of output file is 36 bytes
Log file: modest_from-jani_to-umb-xz_default_polling.18-16_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: 298.148 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4955940/tmpffs5j4ivmodest_from-jani_to-umb-xz_default_polling.18-16_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4955940/tmp5r6hi016modest_from-jani_to-umb-xz_default_polling.18-16_tmp_outdir_/model.umb.xz /w0/tmp/slurm_tq429871.4955940/tmp5r6hi016modest_from-jani_to-umb-xz_default_polling.18-16_tmp_outdir_/umbxz.properties.txt --umb-compress XZ --stop-after Exploration -D -Y --exhaustive
model.jani:model: info: model is a CTMC model.
model.jani:variables[3]: info: Expanding variable "a" into 2 locations in automaton "server".
model.jani:automata[1].variables[0]: info: Expanding variable "s1" into 2 locations in automaton "station1".
model.jani:automata[2].variables[0]: info: Expanding variable "s2" into 2 locations in automaton "station2".
model.jani:automata[3].variables[0]: info: Expanding variable "s3" into 2 locations in automaton "station3".
model.jani:automata[4].variables[0]: info: Expanding variable "s4" into 2 locations in automaton "station4".
model.jani:automata[5].variables[0]: info: Expanding variable "s5" into 2 locations in automaton "station5".
model.jani:automata[6].variables[0]: info: Expanding variable "s6" into 2 locations in automaton "station6".
model.jani:automata[7].variables[0]: info: Expanding variable "s7" into 2 locations in automaton "station7".
model.jani:automata[8].variables[0]: info: Expanding variable "s8" into 2 locations in automaton "station8".
model.jani:automata[9].variables[0]: info: Expanding variable "s9" into 2 locations in automaton "station9".
model.jani:automata[10].variables[0]: info: Expanding variable "s10" into 2 locations in automaton "station10".
model.jani:automata[11].variables[0]: info: Expanding variable "s11" into 2 locations in automaton "station11".
model.jani:automata[12].variables[0]: info: Expanding variable "s12" into 2 locations in automaton "station12".
model.jani:automata[13].variables[0]: info: Expanding variable "s13" into 2 locations in automaton "station13".
model.jani:automata[14].variables[0]: info: Expanding variable "s14" into 2 locations in automaton "station14".
model.jani:automata[15].variables[0]: info: Expanding variable "s15" into 2 locations in automaton "station15".
model.jani:automata[16].variables[0]: info: Expanding variable "s16" into 2 locations in automaton "station16".
model.jani:automata[17].variables[0]: info: Expanding variable "s17" into 2 locations in automaton "station17".
model.jani:automata[18].variables[0]: info: Expanding variable "s18" into 2 locations in automaton "station18".
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 7077888 states.
Peak memory usage: 1756 MB
Analysis results for model.jani
+ State space exploration
State size: 24 bytes
States: 7077888
Choices: 7077888
Branches: 69599232
Rate: 109181 states/s
Peak memory: 362.13 MB
Final size: 1116.00 MB
Size on disk: 223.88 MB
Time (exploration): 64.8 s
Time (merging): 4.1 s
+ UMB export
Time: 228.9 s
File size: 46.65 MB
Compression: XZ (Optimal)
############################## Output files ##############################
model.umb.xz: Size of output file is 48916920 bytes
umbxz.properties.txt: Size of output file is 36 bytes
Log file: modest_from-jani_to-umb-xz_default_polling.18-16_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: 339.904 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4958297/tmp2y3ap0z6modest_from-jani_to-umb-xz_default_polling.18-16_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4958297/tmpi9nt2m6qmodest_from-jani_to-umb-xz_default_polling.18-16_tmp_outdir_/model.umb.xz /w0/tmp/slurm_tq429871.4958297/tmpi9nt2m6qmodest_from-jani_to-umb-xz_default_polling.18-16_tmp_outdir_/umbxz.properties.txt --umb-compress XZ --stop-after Exploration -D -Y --exhaustive
model.jani:model: info: model is a CTMC model.
model.jani:variables[3]: info: Expanding variable "a" into 2 locations in automaton "server".
model.jani:automata[1].variables[0]: info: Expanding variable "s1" into 2 locations in automaton "station1".
model.jani:automata[2].variables[0]: info: Expanding variable "s2" into 2 locations in automaton "station2".
model.jani:automata[3].variables[0]: info: Expanding variable "s3" into 2 locations in automaton "station3".
model.jani:automata[4].variables[0]: info: Expanding variable "s4" into 2 locations in automaton "station4".
model.jani:automata[5].variables[0]: info: Expanding variable "s5" into 2 locations in automaton "station5".
model.jani:automata[6].variables[0]: info: Expanding variable "s6" into 2 locations in automaton "station6".
model.jani:automata[7].variables[0]: info: Expanding variable "s7" into 2 locations in automaton "station7".
model.jani:automata[8].variables[0]: info: Expanding variable "s8" into 2 locations in automaton "station8".
model.jani:automata[9].variables[0]: info: Expanding variable "s9" into 2 locations in automaton "station9".
model.jani:automata[10].variables[0]: info: Expanding variable "s10" into 2 locations in automaton "station10".
model.jani:automata[11].variables[0]: info: Expanding variable "s11" into 2 locations in automaton "station11".
model.jani:automata[12].variables[0]: info: Expanding variable "s12" into 2 locations in automaton "station12".
model.jani:automata[13].variables[0]: info: Expanding variable "s13" into 2 locations in automaton "station13".
model.jani:automata[14].variables[0]: info: Expanding variable "s14" into 2 locations in automaton "station14".
model.jani:automata[15].variables[0]: info: Expanding variable "s15" into 2 locations in automaton "station15".
model.jani:automata[16].variables[0]: info: Expanding variable "s16" into 2 locations in automaton "station16".
model.jani:automata[17].variables[0]: info: Expanding variable "s17" into 2 locations in automaton "station17".
model.jani:automata[18].variables[0]: info: Expanding variable "s18" into 2 locations in automaton "station18".
model.jani: info: Need 24 bytes per state.
model.jani: info: Explored 7077888 states.
Peak memory usage: 1755 MB
Analysis results for model.jani
+ State space exploration
State size: 24 bytes
States: 7077888
Choices: 7077888
Branches: 69599232
Rate: 100894 states/s
Peak memory: 361.99 MB
Final size: 1116.00 MB
Size on disk: 223.88 MB
Time (exploration): 70.2 s
Time (merging): 4.4 s
+ UMB export
Time: 265.1 s
File size: 46.76 MB
Compression: XZ (Optimal)
############################## Output files ##############################
model.umb.xz: Size of output file is 49032076 bytes
umbxz.properties.txt: Size of output file is 36 bytes