[48.189, 52.106, 57.225, 54.629, 52.971]

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

Version: 4.11
Date: Mon Oct 12 22:46:08 GMT+02:00 2026
Hostname: n23m0134.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955598/tmpdmv9cwk8prism_from-prism_to-tra_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955598/tmpweivyrugprism_from-prism_to-tra_ex_crowds.6-20_tmp_outdir_/model.pexp:format=explicit,states=false,zip=false,precision=17'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955598/tmpdmv9cwk8prism_from-prism_to-tra_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... 544887 975207 1536257 1942007 2504554 2961970 3541842 3959566 4219552 4522862 4918945 5419342 6076945 6662956 7370577 7703458 8024295 8343363 8674190 8956969 9386631 10377250 10633591 states
Reachable states exploration and model construction done in 66.549 secs.
Sorting reachable states list...

Time for model construction: 74.97 seconds.

Warning: Deadlocks detected and fixed in 230230 states

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

Exporting model in plain text format to file "/w0/tmp/slurm_tq429871.4955598/tmpweivyrugprism_from-prism_to-tra_ex_crowds.6-20_tmp_outdir_/model.pexp"...
Time for exporting: 48.189 seconds.

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

Note: There was 1 warning during computation.


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

############################## Output files ##############################
model.pexp:	Size of output file is 1203712247 bytes

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

Version: 4.11
Date: Mon Oct 12 22:45:34 GMT+02:00 2026
Hostname: n23m0033.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955582/tmplefajbmpprism_from-prism_to-tra_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955582/tmpehgcu98nprism_from-prism_to-tra_ex_crowds.6-20_tmp_outdir_/model.pexp:format=explicit,states=false,zip=false,precision=17'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955582/tmplefajbmpprism_from-prism_to-tra_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... 492456 870940 1412274 1690103 2132501 2582491 2933526 3449436 3891961 4086949 4283592 4551393 4864959 5321561 5801545 6336492 6866074 7387214 7655747 7895747 8137144 8318185 8558322 8781555 8990143 9250633 10036841 10633591 states
Reachable states exploration and model construction done in 82.442 secs.
Sorting reachable states list...

Time for model construction: 89.287 seconds.

Warning: Deadlocks detected and fixed in 230230 states

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

Exporting model in plain text format to file "/w0/tmp/slurm_tq429871.4955582/tmpehgcu98nprism_from-prism_to-tra_ex_crowds.6-20_tmp_outdir_/model.pexp"...
Time for exporting: 52.106 seconds.

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

Note: There was 1 warning during computation.


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

############################## Output files ##############################
model.pexp:	Size of output file is 1203712247 bytes

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

Version: 4.11
Date: Mon Oct 12 22:44:59 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.4955561/tmpx3gdpgc7prism_from-prism_to-tra_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955561/tmp7tkdtbk3prism_from-prism_to-tra_ex_crowds.6-20_tmp_outdir_/model.pexp:format=explicit,states=false,zip=false,precision=17'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955561/tmpx3gdpgc7prism_from-prism_to-tra_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... 432303 787213 1294811 1642946 2039781 2508562 2897488 3383609 3855041 4068889 4282272 4568575 4902004 5335281 5835613 6378791 6879489 7396687 7657088 7906378 8167065 8443585 8704056 8957211 9254298 10045710 10633591 states
Reachable states exploration and model construction done in 79.55 secs.
Sorting reachable states list...

Time for model construction: 86.826 seconds.

Warning: Deadlocks detected and fixed in 230230 states

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

Exporting model in plain text format to file "/w0/tmp/slurm_tq429871.4955561/tmp7tkdtbk3prism_from-prism_to-tra_ex_crowds.6-20_tmp_outdir_/model.pexp"...
Time for exporting: 57.225 seconds.

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

Note: There was 1 warning during computation.


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

############################## Output files ##############################
model.pexp:	Size of output file is 1203712247 bytes

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

Version: 4.11
Date: Mon Oct 12 23:14:13 GMT+02:00 2026
Hostname: n23m0242.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956694/tmpnq07hyguprism_from-prism_to-tra_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956694/tmp45psli30prism_from-prism_to-tra_ex_crowds.6-20_tmp_outdir_/model.pexp:format=explicit,states=false,zip=false,precision=17'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956694/tmpnq07hyguprism_from-prism_to-tra_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... 451046 800505 1347786 1666209 2089731 2549184 2921789 3431545 3881669 4102408 4340455 4608711 4982742 5410334 5967465 6476421 6998685 7475307 7731313 7993441 8250153 8434148 8673016 8900171 9121872 9760387 10633591 states
Reachable states exploration and model construction done in 80.433 secs.
Sorting reachable states list...

Time for model construction: 87.128 seconds.

Warning: Deadlocks detected and fixed in 230230 states

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

Exporting model in plain text format to file "/w0/tmp/slurm_tq429871.4956694/tmp45psli30prism_from-prism_to-tra_ex_crowds.6-20_tmp_outdir_/model.pexp"...
Time for exporting: 54.629 seconds.

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

Note: There was 1 warning during computation.


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

############################## Output files ##############################
model.pexp:	Size of output file is 1203712247 bytes

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

Version: 4.11
Date: Mon Oct 12 23:49:52 GMT+02:00 2026
Hostname: n23m0043.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957988/tmpia9u8pv2prism_from-prism_to-tra_ex_crowds.6-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957988/tmp046kvcv0prism_from-prism_to-tra_ex_crowds.6-20_tmp_outdir_/model.pexp:format=explicit,states=false,zip=false,precision=17'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957988/tmpia9u8pv2prism_from-prism_to-tra_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... 493817 835472 1391001 1672412 2076019 2574405 2926321 3454025 3896270 4094595 4312049 4569660 4900172 5397499 5955736 6511374 6998348 7461563 7709759 7952387 8204767 8379498 8617078 8817946 9038759 9460590 10292803 10633591 states
Reachable states exploration and model construction done in 81.979 secs.
Sorting reachable states list...

Time for model construction: 88.516 seconds.

Warning: Deadlocks detected and fixed in 230230 states

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

Exporting model in plain text format to file "/w0/tmp/slurm_tq429871.4957988/tmp046kvcv0prism_from-prism_to-tra_ex_crowds.6-20_tmp_outdir_/model.pexp"...
Time for exporting: 52.971 seconds.

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

Note: There was 1 warning during computation.


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

############################## Output files ##############################
model.pexp:	Size of output file is 1203712247 bytes