Log files for model nand.40-4 and tool configuration prism_from-prism_to-umb_ex
[0.275, 0.282, 0.222, 0.387, 0.283]
Log file: prism_from-prism_to-umb_ex_nand.40-4_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: 8.929 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:46:46 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.4957894/tmpyikm0h2qprism_from-prism_to-umb_ex_nand.40-4_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957894/tmpe90pproaprism_from-prism_to-umb_ex_nand.40-4_tmp_outdir_/model.umb:format=umb,states=false,zip=false'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957894/tmpyikm0h2qprism_from-prism_to-umb_ex_nand.40-4_tmp_indir_/model.prism"...
Type: DTMC
Modules: multiplex
Actions: []
Variables: u c s z zx zy x y
Labels: "target"
Building model (engine:explicit)...
Computing reachable states... 1773420 3565947 3999522 states
Reachable states exploration and model construction done in 6.763 secs.
Sorting reachable states list...
Time for model construction: 7.964 seconds.
Type: DTMC
States: 3999522 (1 initial)
Transitions: 6288542
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957894/tmpe90pproaprism_from-prism_to-umb_ex_nand.40-4_tmp_outdir_/model.umb"...
Time for exporting: 0.275 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umb: Size of output file is 133619200 bytes
Log file: prism_from-prism_to-umb_ex_nand.40-4_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: 9.293 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:24:29 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.4957152/tmprz2rfdykprism_from-prism_to-umb_ex_nand.40-4_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957152/tmpkn05f3e1prism_from-prism_to-umb_ex_nand.40-4_tmp_outdir_/model.umb:format=umb,states=false,zip=false'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957152/tmprz2rfdykprism_from-prism_to-umb_ex_nand.40-4_tmp_indir_/model.prism"...
Type: DTMC
Modules: multiplex
Actions: []
Variables: u c s z zx zy x y
Labels: "target"
Building model (engine:explicit)...
Computing reachable states... 1883603 3820885 3999522 states
Reachable states exploration and model construction done in 6.273 secs.
Sorting reachable states list...
Time for model construction: 7.714 seconds.
Type: DTMC
States: 3999522 (1 initial)
Transitions: 6288542
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957152/tmpkn05f3e1prism_from-prism_to-umb_ex_nand.40-4_tmp_outdir_/model.umb"...
Time for exporting: 0.282 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umb: Size of output file is 133619200 bytes
Log file: prism_from-prism_to-umb_ex_nand.40-4_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: 8.126 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:15:22 GMT+02:00 2026
Hostname: r23m0217.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956736/tmp8x4zxmc_prism_from-prism_to-umb_ex_nand.40-4_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956736/tmp1g3sqe7cprism_from-prism_to-umb_ex_nand.40-4_tmp_outdir_/model.umb:format=umb,states=false,zip=false'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956736/tmp8x4zxmc_prism_from-prism_to-umb_ex_nand.40-4_tmp_indir_/model.prism"...
Type: DTMC
Modules: multiplex
Actions: []
Variables: u c s z zx zy x y
Labels: "target"
Building model (engine:explicit)...
Computing reachable states... 1930996 3894753 3999522 states
Reachable states exploration and model construction done in 6.289 secs.
Sorting reachable states list...
Time for model construction: 7.312 seconds.
Type: DTMC
States: 3999522 (1 initial)
Transitions: 6288542
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956736/tmp1g3sqe7cprism_from-prism_to-umb_ex_nand.40-4_tmp_outdir_/model.umb"...
Time for exporting: 0.222 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umb: Size of output file is 133619200 bytes
Log file: prism_from-prism_to-umb_ex_nand.40-4_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: 10.608 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 22:29:36 GMT+02:00 2026
Hostname: n23m0034.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4954940/tmpih196sg9prism_from-prism_to-umb_ex_nand.40-4_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4954940/tmprp5raribprism_from-prism_to-umb_ex_nand.40-4_tmp_outdir_/model.umb:format=umb,states=false,zip=false'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4954940/tmpih196sg9prism_from-prism_to-umb_ex_nand.40-4_tmp_indir_/model.prism"...
Type: DTMC
Modules: multiplex
Actions: []
Variables: u c s z zx zy x y
Labels: "target"
Building model (engine:explicit)...
Computing reachable states... 1793313 3544917 3999522 states
Reachable states exploration and model construction done in 6.602 secs.
Sorting reachable states list...
Time for model construction: 8.145 seconds.
Type: DTMC
States: 3999522 (1 initial)
Transitions: 6288542
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4954940/tmprp5raribprism_from-prism_to-umb_ex_nand.40-4_tmp_outdir_/model.umb"...
Time for exporting: 0.387 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umb: Size of output file is 133619200 bytes
Log file: prism_from-prism_to-umb_ex_nand.40-4_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: 9.144 seconds
Return code: 0
##############################
PRISM
=====
Version: 4.11
Date: Mon Oct 12 23:17:04 GMT+02:00 2026
Hostname: n23m0049.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956841/tmpsvkxcveuprism_from-prism_to-umb_ex_nand.40-4_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956841/tmpscn7pulhprism_from-prism_to-umb_ex_nand.40-4_tmp_outdir_/model.umb:format=umb,states=false,zip=false'
Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956841/tmpsvkxcveuprism_from-prism_to-umb_ex_nand.40-4_tmp_indir_/model.prism"...
Type: DTMC
Modules: multiplex
Actions: []
Variables: u c s z zx zy x y
Labels: "target"
Building model (engine:explicit)...
Computing reachable states... 1761328 3594573 3999522 states
Reachable states exploration and model construction done in 6.681 secs.
Sorting reachable states list...
Time for model construction: 8.198 seconds.
Type: DTMC
States: 3999522 (1 initial)
Transitions: 6288542
Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956841/tmpscn7pulhprism_from-prism_to-umb_ex_nand.40-4_tmp_outdir_/model.umb"...
Time for exporting: 0.283 seconds.
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g
############################## Output files ##############################
model.umb: Size of output file is 133619200 bytes