[12096935.0, 12130667.0, 12004503.0, 12071827.0, 11606163.0]

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: 98.971 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4956773/tmpqvmln2vymodest_from-jani_to-umb-xz_default_crowds.6-20_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4956773/tmpb549mgx3modest_from-jani_to-umb-xz_default_crowds.6-20_tmp_outdir_/model.umb.xz /w0/tmp/slurm_tq429871.4956773/tmpb549mgx3modest_from-jani_to-umb-xz_default_crowds.6-20_tmp_outdir_/umbxz.properties.txt --umb-compress XZ --stop-after Exploration -D -Y --exhaustive




model.jani:model: info: model is a DTMC model.
model.jani: info: Need 40 bytes per state.
model.jani: warning: The probabilities for a transition labelled "τ" with 20 branches in state (crowds.location = l, observe0 = 0, crowds.runCount = 5, crowds.lastSeen = 0, crowds.observe1 = 0, crowds.observe2 = 0, crowds.observe3 = 0, crowds.observe4 = 0, crowds.observe5 = 0, crowds.observe6 = 0, crowds.observe7 = 0, crowds.observe8 = 0, crowds.observe9 = 0, crowds.observe10 = 0, crowds.observe11 = 0, crowds.observe12 = 0, crowds.observe13 = 0, crowds.observe14 = 0, crowds.observe15 = 0, crowds.observe16 = 0, crowds.observe17 = 0, crowds.observe18 = 0, crowds.observe19 = 0, crowds.launch = False, crowds.new = False, crowds.start = False, crowds.run = False, crowds.good = True, crowds.bad = False, crowds.recordLast = True, crowds.badObserve = False, crowds.deliver = False, crowds.done = False) do not sum up to the expected value of 1 (actual sum: 1.0000000000000002). Results will likely be affected by floating-point errors.
model.jani: info: Explored 10633591 states.

Peak memory usage: 1629 MB
Analysis results for model.jani

+ State space exploration
  State size:         40 bytes
  States:             10633591
  Choices:            10633591
  Branches:           38261191
  Rate:               604525 states/s
  Peak memory:        772.86 MB
  Final size:         664.95 MB
  Size on disk:       52.94 MB
  Time (exploration): 17.6 s
  Time (merging):     2.2 s

+ UMB export
  Time:        78.9 s
  File size:   11.54 MB
  Compression: XZ (Optimal)


############################## Output files ##############################
model.umb.xz:	Size of output file is 12096908 bytes
umbxz.properties.txt:	Size of output file is 27 bytes

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: 98.568 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4957740/tmpk5hhtyosmodest_from-jani_to-umb-xz_default_crowds.6-20_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4957740/tmpqjoiptjmmodest_from-jani_to-umb-xz_default_crowds.6-20_tmp_outdir_/model.umb.xz /w0/tmp/slurm_tq429871.4957740/tmpqjoiptjmmodest_from-jani_to-umb-xz_default_crowds.6-20_tmp_outdir_/umbxz.properties.txt --umb-compress XZ --stop-after Exploration -D -Y --exhaustive




model.jani:model: info: model is a DTMC model.
model.jani: info: Need 40 bytes per state.
model.jani: warning: The probabilities for a transition labelled "τ" with 20 branches in state (crowds.location = l, observe0 = 0, crowds.runCount = 5, crowds.lastSeen = 0, crowds.observe1 = 0, crowds.observe2 = 0, crowds.observe3 = 0, crowds.observe4 = 0, crowds.observe5 = 0, crowds.observe6 = 0, crowds.observe7 = 0, crowds.observe8 = 0, crowds.observe9 = 0, crowds.observe10 = 0, crowds.observe11 = 0, crowds.observe12 = 0, crowds.observe13 = 0, crowds.observe14 = 0, crowds.observe15 = 0, crowds.observe16 = 0, crowds.observe17 = 0, crowds.observe18 = 0, crowds.observe19 = 0, crowds.launch = False, crowds.new = False, crowds.start = False, crowds.run = False, crowds.good = True, crowds.bad = False, crowds.recordLast = True, crowds.badObserve = False, crowds.deliver = False, crowds.done = False) do not sum up to the expected value of 1 (actual sum: 1.0000000000000002). Results will likely be affected by floating-point errors.
model.jani: info: Explored 10633591 states.

Peak memory usage: 1630 MB
Analysis results for model.jani

+ State space exploration
  State size:         40 bytes
  States:             10633591
  Choices:            10633591
  Branches:           38261191
  Rate:               604250 states/s
  Peak memory:        772.76 MB
  Final size:         664.95 MB
  Size on disk:       52.94 MB
  Time (exploration): 17.6 s
  Time (merging):     2.3 s

+ UMB export
  Time:        78.4 s
  File size:   11.57 MB
  Compression: XZ (Optimal)


############################## Output files ##############################
model.umb.xz:	Size of output file is 12130640 bytes
umbxz.properties.txt:	Size of output file is 27 bytes

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: 86.447 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4955708/tmpb1e9955gmodest_from-jani_to-umb-xz_default_crowds.6-20_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4955708/tmpnzd5yjiimodest_from-jani_to-umb-xz_default_crowds.6-20_tmp_outdir_/model.umb.xz /w0/tmp/slurm_tq429871.4955708/tmpnzd5yjiimodest_from-jani_to-umb-xz_default_crowds.6-20_tmp_outdir_/umbxz.properties.txt --umb-compress XZ --stop-after Exploration -D -Y --exhaustive




model.jani:model: info: model is a DTMC model.
model.jani: info: Need 40 bytes per state.
model.jani: warning: The probabilities for a transition labelled "τ" with 20 branches in state (crowds.location = l, observe0 = 0, crowds.runCount = 5, crowds.lastSeen = 0, crowds.observe1 = 0, crowds.observe2 = 0, crowds.observe3 = 0, crowds.observe4 = 0, crowds.observe5 = 0, crowds.observe6 = 0, crowds.observe7 = 0, crowds.observe8 = 0, crowds.observe9 = 0, crowds.observe10 = 0, crowds.observe11 = 0, crowds.observe12 = 0, crowds.observe13 = 0, crowds.observe14 = 0, crowds.observe15 = 0, crowds.observe16 = 0, crowds.observe17 = 0, crowds.observe18 = 0, crowds.observe19 = 0, crowds.launch = False, crowds.new = False, crowds.start = False, crowds.run = False, crowds.good = True, crowds.bad = False, crowds.recordLast = True, crowds.badObserve = False, crowds.deliver = False, crowds.done = False) do not sum up to the expected value of 1 (actual sum: 1.0000000000000002). Results will likely be affected by floating-point errors.
model.jani: info: Explored 10633591 states.

Peak memory usage: 1627 MB
Analysis results for model.jani

+ State space exploration
  State size:         40 bytes
  States:             10633591
  Choices:            10633591
  Branches:           38261191
  Rate:               651289 states/s
  Peak memory:        773.44 MB
  Final size:         664.95 MB
  Size on disk:       52.94 MB
  Time (exploration): 16.3 s
  Time (merging):     2.1 s

+ UMB export
  Time:        67.8 s
  File size:   11.45 MB
  Compression: XZ (Optimal)


############################## Output files ##############################
model.umb.xz:	Size of output file is 12004476 bytes
umbxz.properties.txt:	Size of output file is 27 bytes

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: 88.992 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4956392/tmpewrzju32modest_from-jani_to-umb-xz_default_crowds.6-20_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4956392/tmpj7xlu_t9modest_from-jani_to-umb-xz_default_crowds.6-20_tmp_outdir_/model.umb.xz /w0/tmp/slurm_tq429871.4956392/tmpj7xlu_t9modest_from-jani_to-umb-xz_default_crowds.6-20_tmp_outdir_/umbxz.properties.txt --umb-compress XZ --stop-after Exploration -D -Y --exhaustive




model.jani:model: info: model is a DTMC model.
model.jani: info: Need 40 bytes per state.
model.jani: warning: The probabilities for a transition labelled "τ" with 20 branches in state (crowds.location = l, observe0 = 0, crowds.runCount = 5, crowds.lastSeen = 0, crowds.observe1 = 0, crowds.observe2 = 0, crowds.observe3 = 0, crowds.observe4 = 0, crowds.observe5 = 0, crowds.observe6 = 0, crowds.observe7 = 0, crowds.observe8 = 0, crowds.observe9 = 0, crowds.observe10 = 0, crowds.observe11 = 0, crowds.observe12 = 0, crowds.observe13 = 0, crowds.observe14 = 0, crowds.observe15 = 0, crowds.observe16 = 0, crowds.observe17 = 0, crowds.observe18 = 0, crowds.observe19 = 0, crowds.launch = False, crowds.new = False, crowds.start = False, crowds.run = False, crowds.good = True, crowds.bad = False, crowds.recordLast = True, crowds.badObserve = False, crowds.deliver = False, crowds.done = False) do not sum up to the expected value of 1 (actual sum: 1.0000000000000002). Results will likely be affected by floating-point errors.
model.jani: info: Explored 10633591 states.

Peak memory usage: 1630 MB
Analysis results for model.jani

+ State space exploration
  State size:         40 bytes
  States:             10633591
  Choices:            10633591
  Branches:           38261191
  Rate:               624917 states/s
  Peak memory:        772.70 MB
  Final size:         664.95 MB
  Size on disk:       52.94 MB
  Time (exploration): 17.0 s
  Time (merging):     2.2 s

+ UMB export
  Time:        69.5 s
  File size:   11.51 MB
  Compression: XZ (Optimal)


############################## Output files ##############################
model.umb.xz:	Size of output file is 12071800 bytes
umbxz.properties.txt:	Size of output file is 27 bytes

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: 88.297 seconds
Return code: 0
##############################
The Modest Toolset (www.modestchecker.net), version v3.1.311-g14c460466+14c4604667cea0a04631c853eb09e474e24dc368.
Command: modest mcsta /w0/tmp/slurm_tq429871.4955484/tmp6qk7wq50modest_from-jani_to-umb-xz_default_crowds.6-20_tmp_indir_/model.jani --umb /w0/tmp/slurm_tq429871.4955484/tmpt4hojog2modest_from-jani_to-umb-xz_default_crowds.6-20_tmp_outdir_/model.umb.xz /w0/tmp/slurm_tq429871.4955484/tmpt4hojog2modest_from-jani_to-umb-xz_default_crowds.6-20_tmp_outdir_/umbxz.properties.txt --umb-compress XZ --stop-after Exploration -D -Y --exhaustive




model.jani:model: info: model is a DTMC model.
model.jani: info: Need 40 bytes per state.
model.jani: warning: The probabilities for a transition labelled "τ" with 20 branches in state (crowds.location = l, observe0 = 0, crowds.runCount = 5, crowds.lastSeen = 0, crowds.observe1 = 0, crowds.observe2 = 0, crowds.observe3 = 0, crowds.observe4 = 0, crowds.observe5 = 0, crowds.observe6 = 0, crowds.observe7 = 0, crowds.observe8 = 0, crowds.observe9 = 0, crowds.observe10 = 0, crowds.observe11 = 0, crowds.observe12 = 0, crowds.observe13 = 0, crowds.observe14 = 0, crowds.observe15 = 0, crowds.observe16 = 0, crowds.observe17 = 0, crowds.observe18 = 0, crowds.observe19 = 0, crowds.launch = False, crowds.new = False, crowds.start = False, crowds.run = False, crowds.good = True, crowds.bad = False, crowds.recordLast = True, crowds.badObserve = False, crowds.deliver = False, crowds.done = False) do not sum up to the expected value of 1 (actual sum: 1.0000000000000002). Results will likely be affected by floating-point errors.
model.jani: info: Explored 10633591 states.

Peak memory usage: 1630 MB
Analysis results for model.jani

+ State space exploration
  State size:         40 bytes
  States:             10633591
  Choices:            10633591
  Branches:           38261191
  Rate:               619854 states/s
  Peak memory:        773.10 MB
  Final size:         664.95 MB
  Size on disk:       52.94 MB
  Time (exploration): 17.2 s
  Time (merging):     2.2 s

+ UMB export
  Time:        68.7 s
  File size:   11.07 MB
  Compression: XZ (Optimal)


############################## Output files ##############################
model.umb.xz:	Size of output file is 11606136 bytes
umbxz.properties.txt:	Size of output file is 27 bytes