[92667196.0, 92667195.0, 92667195.0, 92667196.0, 92667196.0]

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

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

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955999/tmpx9nnbg9sprism_from-prism_to-umb-gz_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... 492149 859254 1410062 1683246 2077033 2555376 2902503 3374604 3873212 4062393 4264061 4527156 4821344 5264268 5793480 6341134 6887297 7403664 7653530 7890053 8115613 8344584 8580569 8810298 8986564 9352904 10213908 10633591 states
Reachable states exploration and model construction done in 82.333 secs.
Sorting reachable states list...

Time for model construction: 89.776 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.4955999/tmp4rzyeqcjprism_from-prism_to-umb-gz_ex_crowds.6-20_tmp_outdir_/model.umbgz"...
Time for exporting: 3.646 seconds.

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

Note: There was 1 warning during computation.


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

############################## Output files ##############################
model.umbgz:	Size of output file is 92667196 bytes

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

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

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957079/tmp01iqmik0prism_from-prism_to-umb-gz_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... 483912 853875 1408424 1690554 2065278 2569980 2897547 3363643 3849052 4044582 4234993 4495245 4745006 5192058 5654727 6216669 6714479 7227980 7582263 7834604 8073552 8332416 8511293 8747534 8968842 9186453 9976893 10633591 states
Reachable states exploration and model construction done in 82.924 secs.
Sorting reachable states list...

Time for model construction: 89.451 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.4957079/tmpnbmu9bc7prism_from-prism_to-umb-gz_ex_crowds.6-20_tmp_outdir_/model.umbgz"...
Time for exporting: 3.765 seconds.

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

Note: There was 1 warning during computation.


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

############################## Output files ##############################
model.umbgz:	Size of output file is 92667195 bytes

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

Version: 4.11
Date: Mon Oct 12 22:57:44 GMT+02:00 2026
Hostname: n23m0248.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956065/tmp6ddw_mnfprism_from-prism_to-umb-gz_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956065/tmp4fjpf8z6prism_from-prism_to-umb-gz_ex_crowds.6-20_tmp_outdir_/model.umbgz:format=umb,states=false,zip=gzip'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956065/tmp6ddw_mnfprism_from-prism_to-umb-gz_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... 432683 821861 1388432 1677426 2148771 2579319 2927757 3461156 3890867 4108899 4345920 4614000 5002844 5461743 5999413 6572920 7126227 7544581 7803316 8050823 8313757 8572638 8833513 9081469 9646238 10246645 10633591 states
Reachable states exploration and model construction done in 78.917 secs.
Sorting reachable states list...

Time for model construction: 87.215 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.4956065/tmp4fjpf8z6prism_from-prism_to-umb-gz_ex_crowds.6-20_tmp_outdir_/model.umbgz"...
Time for exporting: 3.648 seconds.

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

Note: There was 1 warning during computation.


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

############################## Output files ##############################
model.umbgz:	Size of output file is 92667195 bytes

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

Version: 4.11
Date: Mon Oct 12 22:28:58 GMT+02:00 2026
Hostname: n23m0237.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4954901/tmp8gdpj_z2prism_from-prism_to-umb-gz_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4954901/tmp6u_17g3dprism_from-prism_to-umb-gz_ex_crowds.6-20_tmp_outdir_/model.umbgz:format=umb,states=false,zip=gzip'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4954901/tmp8gdpj_z2prism_from-prism_to-umb-gz_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... 452294 836344 1419025 1733602 2312186 2659298 3118627 3736799 4010426 4247020 4548142 4919123 5437496 5982002 6557763 7072379 7532361 7821879 8117090 8406612 8619545 8888278 9138944 9800208 10633591 states
Reachable states exploration and model construction done in 73.921 secs.
Sorting reachable states list...

Time for model construction: 80.761 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.4954901/tmp6u_17g3dprism_from-prism_to-umb-gz_ex_crowds.6-20_tmp_outdir_/model.umbgz"...
Time for exporting: 3.554 seconds.

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

Note: There was 1 warning during computation.


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

############################## Output files ##############################
model.umbgz:	Size of output file is 92667196 bytes

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

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

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955316/tmpt8tzs5crprism_from-prism_to-umb-gz_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... 457875 843483 1414632 1717076 2270192 2628112 3041486 3643261 3979618 4197765 4485638 4781141 5308722 5867045 6402576 6928213 7443539 7732827 8016605 8293147 8496180 8760191 9003232 9384902 10233886 10633591 states
Reachable states exploration and model construction done in 75.764 secs.
Sorting reachable states list...

Time for model construction: 82.46 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.4955316/tmptvn00muqprism_from-prism_to-umb-gz_ex_crowds.6-20_tmp_outdir_/model.umbgz"...
Time for exporting: 3.574 seconds.

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

Note: There was 1 warning during computation.


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

############################## Output files ##############################
model.umbgz:	Size of output file is 92667196 bytes