[701243392.0, 701243392.0, 701243392.0, 701243392.0, 701243392.0]

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 90.807 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Mon Oct 12 22:40:23 GMT+02:00 2026
Hostname: n23m0259.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955365/tmpeb8lfw7gprism_from-prism_to-umb_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955365/tmpd8amb2b5prism_from-prism_to-umb_ex_crowds.6-20_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955365/tmpeb8lfw7gprism_from-prism_to-umb_ex_crowds.6-20_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     crowds
Actions:     []
Variables:   launch new runCount start run lastSeen good bad recordLast badObserve deliver done observe0 observe1 observe2 observe3 observe4 observe5 observe6 observe7 observe8 observe9 observe10 observe11 observe12 observe13 observe14 observe15 observe16 observe17 observe18 observe19
Labels:      "target"

Building model (engine:explicit)...

Computing reachable states... 488763 809688 1361598 1667117 2073451 2508069 2895787 3372575 3855072 4072056 4253552 4523055 4774964 5237476 5747566 6283505 6794268 7370628 7638464 7883799 8117010 8367381 8616197 8834927 9043852 9464243 10308055 10633591 states
Reachable states exploration and model construction done in 82.679 secs.
Sorting reachable states list...

Time for model construction: 89.289 seconds.

Warning: Deadlocks detected and fixed in 230230 states

Type:        DTMC
States:      10633591 (1 initial)
Transitions: 38261191

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955365/tmpd8amb2b5prism_from-prism_to-umb_ex_crowds.6-20_tmp_outdir_/model.umb"...
Time for exporting: 0.886 seconds.

---------------------------------------------------------------------

Note: There was 1 warning during computation.


##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

############################## Output files ##############################
model.umb:	Size of output file is 701243392 bytes

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 92.579 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Mon Oct 12 23:33:59 GMT+02:00 2026
Hostname: n23m0358.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957532/tmphepedu92prism_from-prism_to-umb_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957532/tmpu8diyn0_prism_from-prism_to-umb_ex_crowds.6-20_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957532/tmphepedu92prism_from-prism_to-umb_ex_crowds.6-20_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     crowds
Actions:     []
Variables:   launch new runCount start run lastSeen good bad recordLast badObserve deliver done observe0 observe1 observe2 observe3 observe4 observe5 observe6 observe7 observe8 observe9 observe10 observe11 observe12 observe13 observe14 observe15 observe16 observe17 observe18 observe19
Labels:      "target"

Building model (engine:explicit)...

Computing reachable states... 470260 791016 1289060 1634357 1994969 2479359 2835359 3250268 3807973 4013308 4206347 4432591 4680207 5090280 5511175 6106276 6670149 7179780 7538413 7792967 8037092 8293294 8541518 8716511 8983652 9245954 9877421 10633591 states
Reachable states exploration and model construction done in 83.272 secs.
Sorting reachable states list...

Time for model construction: 90.995 seconds.

Warning: Deadlocks detected and fixed in 230230 states

Type:        DTMC
States:      10633591 (1 initial)
Transitions: 38261191

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957532/tmpu8diyn0_prism_from-prism_to-umb_ex_crowds.6-20_tmp_outdir_/model.umb"...
Time for exporting: 0.884 seconds.

---------------------------------------------------------------------

Note: There was 1 warning during computation.


##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

############################## Output files ##############################
model.umb:	Size of output file is 701243392 bytes

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 88.128 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Mon Oct 12 22:39:15 GMT+02:00 2026
Hostname: n23m0258.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955326/tmpcz_7b7joprism_from-prism_to-umb_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955326/tmp7_sw513bprism_from-prism_to-umb_ex_crowds.6-20_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955326/tmpcz_7b7joprism_from-prism_to-umb_ex_crowds.6-20_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     crowds
Actions:     []
Variables:   launch new runCount start run lastSeen good bad recordLast badObserve deliver done observe0 observe1 observe2 observe3 observe4 observe5 observe6 observe7 observe8 observe9 observe10 observe11 observe12 observe13 observe14 observe15 observe16 observe17 observe18 observe19
Labels:      "target"

Building model (engine:explicit)...

Computing reachable states... 488974 891022 1423775 1707893 2184772 2605519 2961607 3533838 3929114 4136594 4389766 4636826 5024538 5510128 6123470 6678035 7181208 7568549 7814498 8039587 8261434 8523412 8752074 9021179 9503209 10448796 10633591 states
Reachable states exploration and model construction done in 79.322 secs.
Sorting reachable states list...

Time for model construction: 86.583 seconds.

Warning: Deadlocks detected and fixed in 230230 states

Type:        DTMC
States:      10633591 (1 initial)
Transitions: 38261191

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955326/tmp7_sw513bprism_from-prism_to-umb_ex_crowds.6-20_tmp_outdir_/model.umb"...
Time for exporting: 0.914 seconds.

---------------------------------------------------------------------

Note: There was 1 warning during computation.


##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

############################## Output files ##############################
model.umb:	Size of output file is 701243392 bytes

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 85.499 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Mon Oct 12 22:56:33 GMT+02:00 2026
Hostname: n23m0303.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956022/tmpp2_6v8ujprism_from-prism_to-umb_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956022/tmpx93mw1f7prism_from-prism_to-umb_ex_crowds.6-20_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956022/tmpp2_6v8ujprism_from-prism_to-umb_ex_crowds.6-20_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     crowds
Actions:     []
Variables:   launch new runCount start run lastSeen good bad recordLast badObserve deliver done observe0 observe1 observe2 observe3 observe4 observe5 observe6 observe7 observe8 observe9 observe10 observe11 observe12 observe13 observe14 observe15 observe16 observe17 observe18 observe19
Labels:      "target"

Building model (engine:explicit)...

Computing reachable states... 486131 860020 1422009 1718598 2242711 2628929 3021082 3581980 3949885 4166626 4429710 4684455 5156519 5646574 6263913 6859561 7378325 7656901 7923185 8202265 8472677 8745266 8992128 9416272 10219662 10633591 states
Reachable states exploration and model construction done in 76.929 secs.
Sorting reachable states list...

Time for model construction: 83.959 seconds.

Warning: Deadlocks detected and fixed in 230230 states

Type:        DTMC
States:      10633591 (1 initial)
Transitions: 38261191

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956022/tmpx93mw1f7prism_from-prism_to-umb_ex_crowds.6-20_tmp_outdir_/model.umb"...
Time for exporting: 0.887 seconds.

---------------------------------------------------------------------

Note: There was 1 warning during computation.


##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

############################## Output files ##############################
model.umb:	Size of output file is 701243392 bytes

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 100.505 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Mon Oct 12 22:56:33 GMT+02:00 2026
Hostname: n23m0280.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956014/tmp_qimkn5fprism_from-prism_to-umb_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956014/tmprdyhyyyrprism_from-prism_to-umb_ex_crowds.6-20_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956014/tmp_qimkn5fprism_from-prism_to-umb_ex_crowds.6-20_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     crowds
Actions:     []
Variables:   launch new runCount start run lastSeen good bad recordLast badObserve deliver done observe0 observe1 observe2 observe3 observe4 observe5 observe6 observe7 observe8 observe9 observe10 observe11 observe12 observe13 observe14 observe15 observe16 observe17 observe18 observe19
Labels:      "target"

Building model (engine:explicit)...

Computing reachable states... 465726 827443 1328216 1609232 1840257 2414411 2667081 3022335 3517783 3910561 4094916 4255148 4461335 4669926 5033797 5408843 5912078 6397415 6868080 7369383 7596217 7806421 8010860 8232589 8384260 8588232 8783249 8982439 9168547 9797988 10633591 states
Reachable states exploration and model construction done in 92.407 secs.
Sorting reachable states list...

Time for model construction: 98.919 seconds.

Warning: Deadlocks detected and fixed in 230230 states

Type:        DTMC
States:      10633591 (1 initial)
Transitions: 38261191

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956014/tmprdyhyyyrprism_from-prism_to-umb_ex_crowds.6-20_tmp_outdir_/model.umb"...
Time for exporting: 0.932 seconds.

---------------------------------------------------------------------

Note: There was 1 warning during computation.


##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

############################## Output files ##############################
model.umb:	Size of output file is 701243392 bytes