Log files for model kanban.5 and tool configuration prism_from-prism_to-umb-xz_ex
[16154756.0, 16116864.0, 16116864.0, 16125988.0, 16116864.0]
Log file: prism_from-prism_to-umb-xz_ex_kanban.5_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umbxz:format=umb,states=false,zip=xz
Wallclock time: 211.930 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:51:01 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.4958037/tmpq_emyz6jprism_from-prism_to-umb-xz_ex_kanban.5_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4958037/tmp3bt0gz63prism_from-prism_to-umb-xz_ex_kanban.5_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4958037/tmpq_emyz6jprism_from-prism_to-umb-xz_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... 336992 631121 905314 1146321 1396575 1642629 1874424 2130392 2388060 2546432 states
Reachable states exploration and model construction done in 28.7 secs.
Sorting reachable states list...
Time for model construction: 32.519 seconds.
Type: CTMC
States: 2546432 (1 initial)
Transitions: 24460016
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4958037/tmp3bt0gz63prism_from-prism_to-umb-xz_ex_kanban.5_tmp_outdir_/model.umbxz"...
Time for exporting: 178.766 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umbxz: Size of output file is 16154756 bytes
Log file: prism_from-prism_to-umb-xz_ex_kanban.5_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umbxz:format=umb,states=false,zip=xz
Wallclock time: 212.886 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 22:35:16 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.4955153/tmpz80r_8scprism_from-prism_to-umb-xz_ex_kanban.5_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955153/tmpc8sommhxprism_from-prism_to-umb-xz_ex_kanban.5_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955153/tmpz80r_8scprism_from-prism_to-umb-xz_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... 339490 633182 917380 1162913 1412830 1657532 1857796 2102744 2313231 2546432 states
Reachable states exploration and model construction done in 29.362 secs.
Sorting reachable states list...
Time for model construction: 33.478 seconds.
Type: CTMC
States: 2546432 (1 initial)
Transitions: 24460016
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955153/tmpc8sommhxprism_from-prism_to-umb-xz_ex_kanban.5_tmp_outdir_/model.umbxz"...
Time for exporting: 178.734 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umbxz: Size of output file is 16116864 bytes
Log file: prism_from-prism_to-umb-xz_ex_kanban.5_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umbxz:format=umb,states=false,zip=xz
Wallclock time: 183.737 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:25:02 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.4957163/tmp29bjl9hpprism_from-prism_to-umb-xz_ex_kanban.5_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957163/tmp1sdj1t8bprism_from-prism_to-umb-xz_ex_kanban.5_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957163/tmp29bjl9hpprism_from-prism_to-umb-xz_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... 356454 680233 976255 1253455 1520520 1786093 2065281 2346826 2546432 states
Reachable states exploration and model construction done in 25.816 secs.
Sorting reachable states list...
Time for model construction: 29.309 seconds.
Type: CTMC
States: 2546432 (1 initial)
Transitions: 24460016
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957163/tmp1sdj1t8bprism_from-prism_to-umb-xz_ex_kanban.5_tmp_outdir_/model.umbxz"...
Time for exporting: 153.781 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umbxz: Size of output file is 16116864 bytes
Log file: prism_from-prism_to-umb-xz_ex_kanban.5_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umbxz:format=umb,states=false,zip=xz
Wallclock time: 193.570 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 22:50:08 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.4955760/tmp5u76kdz8prism_from-prism_to-umb-xz_ex_kanban.5_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955760/tmpinby5kk8prism_from-prism_to-umb-xz_ex_kanban.5_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955760/tmp5u76kdz8prism_from-prism_to-umb-xz_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... 269085 504372 717445 931048 1194692 1446545 1706510 1968394 2227048 2535346 2546432 states
Reachable states exploration and model construction done in 30.072 secs.
Sorting reachable states list...
Time for model construction: 33.817 seconds.
Type: CTMC
States: 2546432 (1 initial)
Transitions: 24460016
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955760/tmpinby5kk8prism_from-prism_to-umb-xz_ex_kanban.5_tmp_outdir_/model.umbxz"...
Time for exporting: 159.006 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umbxz: Size of output file is 16125988 bytes
Log file: prism_from-prism_to-umb-xz_ex_kanban.5_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umbxz:format=umb,states=false,zip=xz
Wallclock time: 181.364 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:52:44 GMT+02:00 2026
Hostname: n23m0295.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4958112/tmp7gf1hj41prism_from-prism_to-umb-xz_ex_kanban.5_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4958112/tmpvc6ywg8aprism_from-prism_to-umb-xz_ex_kanban.5_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4958112/tmp7gf1hj41prism_from-prism_to-umb-xz_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... 361651 685366 981263 1259566 1529420 1786796 2053919 2328589 2546432 states
Reachable states exploration and model construction done in 25.933 secs.
Sorting reachable states list...
Time for model construction: 29.341 seconds.
Type: CTMC
States: 2546432 (1 initial)
Transitions: 24460016
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4958112/tmpvc6ywg8aprism_from-prism_to-umb-xz_ex_kanban.5_tmp_outdir_/model.umbxz"...
Time for exporting: 151.367 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umbxz: Size of output file is 16116864 bytes