Log files for model cluster.128-2000-20 and tool configuration prism_from-prism_to-umb_ex
[67875328.0, 67875328.0, 67875328.0, 67875328.0, 67875328.0]
Log file: prism_from-prism_to-umb_ex_cluster.128-2000-20_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 4.412 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.4955372/tmpmgrnt5bkprism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955372/tmpabuxhbogprism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_outdir_/model.umb:format=umb,states=false,zip=false'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955372/tmpmgrnt5bkprism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_indir_/model.prism"...
Type: CTMC
Modules: Left Right Repairman Line ToLeft ToRight
Actions: [] [startLeft] [repairLeft] [startRight] [repairRight] [startToLeft] [startToRight] [startLine] [repairToLeft] [repairToRight] [repairLine]
Variables: left_n left right_n right r line line_n toleft toleft_n toright toright_n
Labels: "minimum"
Building model (engine:explicit)...
Computing reachable states... 597012 states
Reachable states exploration and model construction done in 2.771 secs.
Sorting reachable states list...
Time for model construction: 3.19 seconds.
Type: CTMC
States: 597012 (1 initial)
Transitions: 2908192
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955372/tmpabuxhbogprism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_outdir_/model.umb"...
Time for exporting: 0.581 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umb: Size of output file is 67875328 bytes
Log file: prism_from-prism_to-umb_ex_cluster.128-2000-20_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 4.391 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 22:40:24 GMT+02:00 2026
Hostname: n23m0048.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955374/tmphllonqgtprism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955374/tmpetmhaexkprism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_outdir_/model.umb:format=umb,states=false,zip=false'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955374/tmphllonqgtprism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_indir_/model.prism"...
Type: CTMC
Modules: Left Right Repairman Line ToLeft ToRight
Actions: [] [startLeft] [repairLeft] [startRight] [repairRight] [startToLeft] [startToRight] [startLine] [repairToLeft] [repairToRight] [repairLine]
Variables: left_n left right_n right r line line_n toleft toleft_n toright toright_n
Labels: "minimum"
Building model (engine:explicit)...
Computing reachable states... 597012 states
Reachable states exploration and model construction done in 2.816 secs.
Sorting reachable states list...
Time for model construction: 3.267 seconds.
Type: CTMC
States: 597012 (1 initial)
Transitions: 2908192
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955374/tmpetmhaexkprism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_outdir_/model.umb"...
Time for exporting: 0.533 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umb: Size of output file is 67875328 bytes
Log file: prism_from-prism_to-umb_ex_cluster.128-2000-20_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 4.346 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 22:45:33 GMT+02:00 2026
Hostname: n23m0258.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955576/tmp2003ekywprism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955576/tmpkm1adxc5prism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_outdir_/model.umb:format=umb,states=false,zip=false'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955576/tmp2003ekywprism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_indir_/model.prism"...
Type: CTMC
Modules: Left Right Repairman Line ToLeft ToRight
Actions: [] [startLeft] [repairLeft] [startRight] [repairRight] [startToLeft] [startToRight] [startLine] [repairToLeft] [repairToRight] [repairLine]
Variables: left_n left right_n right r line line_n toleft toleft_n toright toright_n
Labels: "minimum"
Building model (engine:explicit)...
Computing reachable states... 597012 states
Reachable states exploration and model construction done in 2.744 secs.
Sorting reachable states list...
Time for model construction: 3.16 seconds.
Type: CTMC
States: 597012 (1 initial)
Transitions: 2908192
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955576/tmpkm1adxc5prism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_outdir_/model.umb"...
Time for exporting: 0.587 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umb: Size of output file is 67875328 bytes
Log file: prism_from-prism_to-umb_ex_cluster.128-2000-20_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 4.456 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:23:19 GMT+02:00 2026
Hostname: n23m0327.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957097/tmp5q6f62y8prism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957097/tmpp53b14alprism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_outdir_/model.umb:format=umb,states=false,zip=false'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957097/tmp5q6f62y8prism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_indir_/model.prism"...
Type: CTMC
Modules: Left Right Repairman Line ToLeft ToRight
Actions: [] [startLeft] [repairLeft] [startRight] [repairRight] [startToLeft] [startToRight] [startLine] [repairToLeft] [repairToRight] [repairLine]
Variables: left_n left right_n right r line line_n toleft toleft_n toright toright_n
Labels: "minimum"
Building model (engine:explicit)...
Computing reachable states... 597012 states
Reachable states exploration and model construction done in 2.868 secs.
Sorting reachable states list...
Time for model construction: 3.281 seconds.
Type: CTMC
States: 597012 (1 initial)
Transitions: 2908192
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957097/tmpp53b14alprism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_outdir_/model.umb"...
Time for exporting: 0.585 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umb: Size of output file is 67875328 bytes
Log file: prism_from-prism_to-umb_ex_cluster.128-2000-20_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 4.402 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 22:56:33 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.4956017/tmpo8y42fgeprism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956017/tmpvcd55d_mprism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_outdir_/model.umb:format=umb,states=false,zip=false'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956017/tmpo8y42fgeprism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_indir_/model.prism"...
Type: CTMC
Modules: Left Right Repairman Line ToLeft ToRight
Actions: [] [startLeft] [repairLeft] [startRight] [repairRight] [startToLeft] [startToRight] [startLine] [repairToLeft] [repairToRight] [repairLine]
Variables: left_n left right_n right r line line_n toleft toleft_n toright toright_n
Labels: "minimum"
Building model (engine:explicit)...
Computing reachable states... 597012 states
Reachable states exploration and model construction done in 2.686 secs.
Sorting reachable states list...
Time for model construction: 3.151 seconds.
Type: CTMC
States: 597012 (1 initial)
Transitions: 2908192
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956017/tmpvcd55d_mprism_from-prism_to-umb_ex_cluster.128-2000-20_tmp_outdir_/model.umb"...
Time for exporting: 0.572 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umb: Size of output file is 67875328 bytes