[7.804, 7.996, 7.93, 7.664, 7.634]

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

Version: 4.11
Date: Mon Oct 12 23:44:30 GMT+02:00 2026
Hostname: n23m0272.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957840/tmpcun64yffprism_from-prism_to-umb_ex_polling.18-16_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957840/tmpi8wfnwc6prism_from-prism_to-umb_ex_polling.18-16_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957840/tmpcun64yffprism_from-prism_to-umb_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... 157071 347509 538509 724136 927914 1117875 1308408 1493941 1689121 1880081 2063340 2246601 2438100 2606332 2796694 2942067 3139812 3288114 3463789 3622135 3781453 3956846 4099360 4261067 4423297 4596387 4756556 4910961 5077474 5221182 5399922 5569030 5750619 5925398 6102599 6296017 6447796 6643632 6842032 7073562 7077888 states
Reachable states exploration and model construction done in 120.281 secs.
Sorting reachable states list...

Time for model construction: 126.875 seconds.

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

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957840/tmpi8wfnwc6prism_from-prism_to-umb_ex_polling.18-16_tmp_outdir_/model.umb"...
Time for exporting: 7.804 seconds.


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

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

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

Version: 4.11
Date: Mon Oct 12 22:44:59 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.4955551/tmprht24hakprism_from-prism_to-umb_ex_polling.18-16_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955551/tmp_4purxt_prism_from-prism_to-umb_ex_polling.18-16_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955551/tmprht24hakprism_from-prism_to-umb_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... 184590 393489 604427 823818 1023289 1263433 1458795 1686644 1909455 2095312 2317386 2508417 2722369 2909630 3128931 3310066 3525736 3704670 3913438 4094025 4305989 4485469 4699709 4884701 5094720 5271891 5466386 5643084 5865643 6075732 6288733 6512408 6735052 6971305 7077888 states
Reachable states exploration and model construction done in 103.4 secs.
Sorting reachable states list...

Time for model construction: 110.475 seconds.

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

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955551/tmp_4purxt_prism_from-prism_to-umb_ex_polling.18-16_tmp_outdir_/model.umb"...
Time for exporting: 7.996 seconds.


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

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

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

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

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955362/tmptqz75ztaprism_from-prism_to-umb_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... 181433 387908 595965 812125 1012983 1248810 1441753 1673252 1891877 2089360 2302636 2500327 2714390 2901857 3121500 3295854 3507076 3682188 3896565 4079585 4292280 4476886 4678704 4858616 5069745 5253732 5447049 5622168 5835354 6037963 6256228 6468308 6697412 6937616 7077888 states
Reachable states exploration and model construction done in 104.246 secs.
Sorting reachable states list...

Time for model construction: 111.241 seconds.

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

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955362/tmppnlv5ngpprism_from-prism_to-umb_ex_polling.18-16_tmp_outdir_/model.umb"...
Time for exporting: 7.93 seconds.


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

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

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

Version: 4.11
Date: Mon Oct 12 23:25:03 GMT+02:00 2026
Hostname: n23m0254.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957161/tmphjbk6qilprism_from-prism_to-umb_ex_polling.18-16_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957161/tmppzcv3e9sprism_from-prism_to-umb_ex_polling.18-16_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957161/tmphjbk6qilprism_from-prism_to-umb_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... 185571 397669 606795 825114 1022603 1261303 1456244 1682423 1904394 2099985 2316669 2505342 2711220 2894626 3108160 3291075 3488375 3667049 3875470 4059755 4263010 4434874 4643173 4830890 5014855 5201179 5385724 5592612 5806406 6003713 6222506 6450133 6626115 6880802 7077888 states
Reachable states exploration and model construction done in 104.929 secs.
Sorting reachable states list...

Time for model construction: 111.845 seconds.

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

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957161/tmppzcv3e9sprism_from-prism_to-umb_ex_polling.18-16_tmp_outdir_/model.umb"...
Time for exporting: 7.664 seconds.


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

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

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

Version: 4.11
Date: Mon Oct 12 23:07:41 GMT+02:00 2026
Hostname: n23m0306.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956489/tmptnksje00prism_from-prism_to-umb_ex_polling.18-16_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956489/tmpfszv8gwyprism_from-prism_to-umb_ex_polling.18-16_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956489/tmptnksje00prism_from-prism_to-umb_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... 186226 386862 601017 810326 1008261 1241949 1426295 1658989 1873041 2075284 2284307 2476869 2687568 2878680 3087653 3273711 3473057 3663800 3870634 4057778 4263640 4447870 4652821 4836971 5029320 5199902 5385783 5591437 5800840 5997738 6213117 6420602 6612442 6865288 7077888 states
Reachable states exploration and model construction done in 104.962 secs.
Sorting reachable states list...

Time for model construction: 111.949 seconds.

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

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956489/tmpfszv8gwyprism_from-prism_to-umb_ex_polling.18-16_tmp_outdir_/model.umb"...
Time for exporting: 7.634 seconds.


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

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