[725950976.0, 725950976.0, 725950976.0, 725950976.0, 725950976.0]

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 33.775 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.4957533/tmpphframxgprism_from-prism_to-umb_ex_kanban.5_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957533/tmpjps_c7z6prism_from-prism_to-umb_ex_kanban.5_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957533/tmpphframxgprism_from-prism_to-umb_ex_kanban.5_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     k1 k2 k3 k4
Actions:     [] [in] [s1] [s2]
Variables:   w1 x1 y1 z1 w2 x2 y2 z2 w3 x3 y3 z3 w4 x4 y4 z4
Rewards:     "throughput"

Building model (engine:explicit)...

Computing reachable states... 355476 679093 975388 1256509 1523679 1792605 2063847 2361106 2546432 states
Reachable states exploration and model construction done in 25.633 secs.
Sorting reachable states list...

Time for model construction: 29.215 seconds.

Type:        CTMC
States:      2546432 (1 initial)
Transitions: 24460016

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957533/tmpjps_c7z6prism_from-prism_to-umb_ex_kanban.5_tmp_outdir_/model.umb"...
Time for exporting: 3.913 seconds.


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

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

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

Version: 4.11
Date: Tue Oct 13 00:02:28 GMT+02:00 2026
Hostname: n23m0071.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4958516/tmp_cuzxlavprism_from-prism_to-umb_ex_kanban.5_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4958516/tmp79bbj5goprism_from-prism_to-umb_ex_kanban.5_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4958516/tmp_cuzxlavprism_from-prism_to-umb_ex_kanban.5_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     k1 k2 k3 k4
Actions:     [] [in] [s1] [s2]
Variables:   w1 x1 y1 z1 w2 x2 y2 z2 w3 x3 y3 z3 w4 x4 y4 z4
Rewards:     "throughput"

Building model (engine:explicit)...

Computing reachable states... 355537 677382 967949 1246073 1507506 1785773 2055659 2334176 2546432 states
Reachable states exploration and model construction done in 25.842 secs.
Sorting reachable states list...

Time for model construction: 29.498 seconds.

Type:        CTMC
States:      2546432 (1 initial)
Transitions: 24460016

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4958516/tmp79bbj5goprism_from-prism_to-umb_ex_kanban.5_tmp_outdir_/model.umb"...
Time for exporting: 3.828 seconds.


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

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

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

Version: 4.11
Date: Mon Oct 12 22:30:40 GMT+02:00 2026
Hostname: n23m0042.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4954974/tmplvpjj9qvprism_from-prism_to-umb_ex_kanban.5_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4954974/tmpv6ph17trprism_from-prism_to-umb_ex_kanban.5_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4954974/tmplvpjj9qvprism_from-prism_to-umb_ex_kanban.5_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     k1 k2 k3 k4
Actions:     [] [in] [s1] [s2]
Variables:   w1 x1 y1 z1 w2 x2 y2 z2 w3 x3 y3 z3 w4 x4 y4 z4
Rewards:     "throughput"

Building model (engine:explicit)...

Computing reachable states... 397218 741317 1057966 1350468 1636395 1944005 2231431 2546432 states
Reachable states exploration and model construction done in 23.737 secs.
Sorting reachable states list...

Time for model construction: 27.113 seconds.

Type:        CTMC
States:      2546432 (1 initial)
Transitions: 24460016

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4954974/tmpv6ph17trprism_from-prism_to-umb_ex_kanban.5_tmp_outdir_/model.umb"...
Time for exporting: 3.665 seconds.


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

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

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

Version: 4.11
Date: Mon Oct 12 23:34:00 GMT+02:00 2026
Hostname: n23m0040.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957515/tmpayif_sjmprism_from-prism_to-umb_ex_kanban.5_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957515/tmpolzkv2apprism_from-prism_to-umb_ex_kanban.5_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957515/tmpayif_sjmprism_from-prism_to-umb_ex_kanban.5_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     k1 k2 k3 k4
Actions:     [] [in] [s1] [s2]
Variables:   w1 x1 y1 z1 w2 x2 y2 z2 w3 x3 y3 z3 w4 x4 y4 z4
Rewards:     "throughput"

Building model (engine:explicit)...

Computing reachable states... 354727 663188 955962 1224406 1482224 1745816 2004050 2291607 2546432 states
Reachable states exploration and model construction done in 26.349 secs.
Sorting reachable states list...

Time for model construction: 29.997 seconds.

Type:        CTMC
States:      2546432 (1 initial)
Transitions: 24460016

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957515/tmpolzkv2apprism_from-prism_to-umb_ex_kanban.5_tmp_outdir_/model.umb"...
Time for exporting: 3.84 seconds.


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

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

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

Version: 4.11
Date: Tue Oct 13 00:00:10 GMT+02:00 2026
Hostname: n23m0307.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4958416/tmp26okava7prism_from-prism_to-umb_ex_kanban.5_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4958416/tmpzfq5h7vhprism_from-prism_to-umb_ex_kanban.5_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4958416/tmp26okava7prism_from-prism_to-umb_ex_kanban.5_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     k1 k2 k3 k4
Actions:     [] [in] [s1] [s2]
Variables:   w1 x1 y1 z1 w2 x2 y2 z2 w3 x3 y3 z3 w4 x4 y4 z4
Rewards:     "throughput"

Building model (engine:explicit)...

Computing reachable states... 332533 627716 904292 1143388 1385018 1596945 1830765 2033371 2248891 2536930 2546432 states
Reachable states exploration and model construction done in 30.069 secs.
Sorting reachable states list...

Time for model construction: 35.152 seconds.

Type:        CTMC
States:      2546432 (1 initial)
Transitions: 24460016

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4958416/tmpzfq5h7vhprism_from-prism_to-umb_ex_kanban.5_tmp_outdir_/model.umb"...
Time for exporting: 4.382 seconds.


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

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