[405.532, 404.382, 351.466, 403.605, 344.834]

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

Version: 4.11
Date: Mon Oct 12 22:54:46 GMT+02:00 2026
Hostname: n23m0255.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955942/tmpocco3vyyprism_from-prism_to-umb-xz_ex_polling.18-16_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955942/tmprkawl1hhprism_from-prism_to-umb-xz_ex_polling.18-16_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955942/tmpocco3vyyprism_from-prism_to-umb-xz_ex_polling.18-16_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     server station1 station2 station3 station4 station5 station6 station7 station8 station9 station10 station11 station12 station13 station14 station15 station16 station17 station18
Actions:     [] [loop1a] [loop1b] [serve1] [loop2a] [loop2b] [serve2] [loop3a] [loop3b] [serve3] [loop4a] [loop4b] [serve4] [loop5a] [loop5b] [serve5] [loop6a] [loop6b] [serve6] [loop7a] [loop7b] [serve7] [loop8a] [loop8b] [serve8] [loop9a] [loop9b] [serve9] [loop10a] [loop10b] [serve10] [loop11a] [loop11b] [serve11] [loop12a] [loop12b] [serve12] [loop13a] [loop13b] [serve13] [loop14a] [loop14b] [serve14] [loop15a] [loop15b] [serve15] [loop16a] [loop16b] [serve16] [loop17a] [loop17b] [serve17] [loop18a] [loop18b] [serve18]
Variables:   s a s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18
Labels:      "serve_s2" "serve_s1"

Building model (engine:explicit)...

Computing reachable states... 166832 367266 558728 742317 955237 1146023 1329372 1546809 1740880 1950369 2124697 2329770 2505015 2699284 2868786 3048362 3197061 3343840 3533806 3667427 3847990 3988705 4120630 4312487 4450085 4610611 4774256 4922532 5085417 5248969 5428977 5603465 5798318 5981201 6175943 6377092 6550545 6755421 6944937 7077888 states
Reachable states exploration and model construction done in 118.759 secs.
Sorting reachable states list...

Time for model construction: 126.721 seconds.

Type:        CTMC
States:      7077888 (1 initial)
Transitions: 69599232

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955942/tmprkawl1hhprism_from-prism_to-umb-xz_ex_polling.18-16_tmp_outdir_/model.umbxz"...
Time for exporting: 405.532 seconds.


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

############################## Output files ##############################
model.umbxz:	Size of output file is 29842528 bytes

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

Version: 4.11
Date: Mon Oct 12 23:10:05 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.4956578/tmp9bluwidfprism_from-prism_to-umb-xz_ex_polling.18-16_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956578/tmpjw635980prism_from-prism_to-umb-xz_ex_polling.18-16_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956578/tmp9bluwidfprism_from-prism_to-umb-xz_ex_polling.18-16_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     server station1 station2 station3 station4 station5 station6 station7 station8 station9 station10 station11 station12 station13 station14 station15 station16 station17 station18
Actions:     [] [loop1a] [loop1b] [serve1] [loop2a] [loop2b] [serve2] [loop3a] [loop3b] [serve3] [loop4a] [loop4b] [serve4] [loop5a] [loop5b] [serve5] [loop6a] [loop6b] [serve6] [loop7a] [loop7b] [serve7] [loop8a] [loop8b] [serve8] [loop9a] [loop9b] [serve9] [loop10a] [loop10b] [serve10] [loop11a] [loop11b] [serve11] [loop12a] [loop12b] [serve12] [loop13a] [loop13b] [serve13] [loop14a] [loop14b] [serve14] [loop15a] [loop15b] [serve15] [loop16a] [loop16b] [serve16] [loop17a] [loop17b] [serve17] [loop18a] [loop18b] [serve18]
Variables:   s a s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18
Labels:      "serve_s2" "serve_s1"

Building model (engine:explicit)...

Computing reachable states... 166587 365876 551799 734104 942367 1141130 1323779 1533679 1725973 1923766 2096914 2300376 2484777 2675941 2855017 3032222 3211755 3367645 3561092 3704149 3876347 4034276 4185090 4348725 4502302 4674596 4820042 5003067 5156362 5310434 5482636 5637052 5830853 6016336 6218796 6421602 6589481 6807305 7021682 7077888 states
Reachable states exploration and model construction done in 118.006 secs.
Sorting reachable states list...

Time for model construction: 125.295 seconds.

Type:        CTMC
States:      7077888 (1 initial)
Transitions: 69599232

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956578/tmpjw635980prism_from-prism_to-umb-xz_ex_polling.18-16_tmp_outdir_/model.umbxz"...
Time for exporting: 404.382 seconds.


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

############################## Output files ##############################
model.umbxz:	Size of output file is 29842528 bytes

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

Version: 4.11
Date: Mon Oct 12 23:55:35 GMT+02:00 2026
Hostname: r23m0214.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4958226/tmpunyubh13prism_from-prism_to-umb-xz_ex_polling.18-16_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4958226/tmpf7g24olzprism_from-prism_to-umb-xz_ex_polling.18-16_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4958226/tmpunyubh13prism_from-prism_to-umb-xz_ex_polling.18-16_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     server station1 station2 station3 station4 station5 station6 station7 station8 station9 station10 station11 station12 station13 station14 station15 station16 station17 station18
Actions:     [] [loop1a] [loop1b] [serve1] [loop2a] [loop2b] [serve2] [loop3a] [loop3b] [serve3] [loop4a] [loop4b] [serve4] [loop5a] [loop5b] [serve5] [loop6a] [loop6b] [serve6] [loop7a] [loop7b] [serve7] [loop8a] [loop8b] [serve8] [loop9a] [loop9b] [serve9] [loop10a] [loop10b] [serve10] [loop11a] [loop11b] [serve11] [loop12a] [loop12b] [serve12] [loop13a] [loop13b] [serve13] [loop14a] [loop14b] [serve14] [loop15a] [loop15b] [serve15] [loop16a] [loop16b] [serve16] [loop17a] [loop17b] [serve17] [loop18a] [loop18b] [serve18]
Variables:   s a s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18
Labels:      "serve_s2" "serve_s1"

Building model (engine:explicit)...

Computing reachable states... 188482 395336 607507 822647 1030197 1264625 1475311 1694138 1895607 2099890 2321708 2517329 2742865 2918229 3143919 3325383 3541357 3719024 3943159 4120602 4339084 4519319 4735473 4922913 5131853 5324080 5516078 5693814 5892909 6107840 6308200 6542902 6778076 7027460 7077888 states
Reachable states exploration and model construction done in 102.797 secs.
Sorting reachable states list...

Time for model construction: 110.134 seconds.

Type:        CTMC
States:      7077888 (1 initial)
Transitions: 69599232

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4958226/tmpf7g24olzprism_from-prism_to-umb-xz_ex_polling.18-16_tmp_outdir_/model.umbxz"...
Time for exporting: 351.466 seconds.


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

############################## Output files ##############################
model.umbxz:	Size of output file is 29842528 bytes

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

Version: 4.11
Date: Mon Oct 12 22:40:23 GMT+02:00 2026
Hostname: n23m0045.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955371/tmpt9ilizwzprism_from-prism_to-umb-xz_ex_polling.18-16_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955371/tmpy76rhnb8prism_from-prism_to-umb-xz_ex_polling.18-16_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955371/tmpt9ilizwzprism_from-prism_to-umb-xz_ex_polling.18-16_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     server station1 station2 station3 station4 station5 station6 station7 station8 station9 station10 station11 station12 station13 station14 station15 station16 station17 station18
Actions:     [] [loop1a] [loop1b] [serve1] [loop2a] [loop2b] [serve2] [loop3a] [loop3b] [serve3] [loop4a] [loop4b] [serve4] [loop5a] [loop5b] [serve5] [loop6a] [loop6b] [serve6] [loop7a] [loop7b] [serve7] [loop8a] [loop8b] [serve8] [loop9a] [loop9b] [serve9] [loop10a] [loop10b] [serve10] [loop11a] [loop11b] [serve11] [loop12a] [loop12b] [serve12] [loop13a] [loop13b] [serve13] [loop14a] [loop14b] [serve14] [loop15a] [loop15b] [serve15] [loop16a] [loop16b] [serve16] [loop17a] [loop17b] [serve17] [loop18a] [loop18b] [serve18]
Variables:   s a s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18
Labels:      "serve_s2" "serve_s1"

Building model (engine:explicit)...

Computing reachable states... 176575 371523 565038 763014 959872 1164076 1345860 1547547 1722287 1935498 2114304 2302160 2475534 2670878 2852873 3028770 3205522 3374349 3568311 3715908 3912479 4064127 4224468 4390644 4533828 4700415 4859373 5023671 5169339 5348039 5511609 5680886 5878794 6046693 6241504 6411963 6616709 6820753 7053298 7077888 states
Reachable states exploration and model construction done in 117.737 secs.
Sorting reachable states list...

Time for model construction: 124.54 seconds.

Type:        CTMC
States:      7077888 (1 initial)
Transitions: 69599232

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955371/tmpy76rhnb8prism_from-prism_to-umb-xz_ex_polling.18-16_tmp_outdir_/model.umbxz"...
Time for exporting: 403.605 seconds.


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

############################## Output files ##############################
model.umbxz:	Size of output file is 29842528 bytes

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

Version: 4.11
Date: Mon Oct 12 23:55:00 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.4958190/tmp82eya32eprism_from-prism_to-umb-xz_ex_polling.18-16_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4958190/tmpbdeski9_prism_from-prism_to-umb-xz_ex_polling.18-16_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4958190/tmp82eya32eprism_from-prism_to-umb-xz_ex_polling.18-16_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     server station1 station2 station3 station4 station5 station6 station7 station8 station9 station10 station11 station12 station13 station14 station15 station16 station17 station18
Actions:     [] [loop1a] [loop1b] [serve1] [loop2a] [loop2b] [serve2] [loop3a] [loop3b] [serve3] [loop4a] [loop4b] [serve4] [loop5a] [loop5b] [serve5] [loop6a] [loop6b] [serve6] [loop7a] [loop7b] [serve7] [loop8a] [loop8b] [serve8] [loop9a] [loop9b] [serve9] [loop10a] [loop10b] [serve10] [loop11a] [loop11b] [serve11] [loop12a] [loop12b] [serve12] [loop13a] [loop13b] [serve13] [loop14a] [loop14b] [serve14] [loop15a] [loop15b] [serve15] [loop16a] [loop16b] [serve16] [loop17a] [loop17b] [serve17] [loop18a] [loop18b] [serve18]
Variables:   s a s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18
Labels:      "serve_s2" "serve_s1"

Building model (engine:explicit)...

Computing reachable states... 185106 407374 637785 866718 1059877 1290535 1485442 1699801 1918921 2121341 2358223 2541720 2769619 2943602 3176469 3325024 3551468 3697027 3882460 4035844 4207238 4372501 4590088 4798504 4974229 5094720 5213161 5361274 5491471 5632564 5791570 5947381 6086277 6214833 6394602 6585593 6789378 6987239 7077888 states
Reachable states exploration and model construction done in 115.408 secs.
Sorting reachable states list...

Time for model construction: 122.872 seconds.

Type:        CTMC
States:      7077888 (1 initial)
Transitions: 69599232

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4958190/tmpbdeski9_prism_from-prism_to-umb-xz_ex_polling.18-16_tmp_outdir_/model.umbxz"...
Time for exporting: 344.834 seconds.


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

############################## Output files ##############################
model.umbxz:	Size of output file is 28843352 bytes