[631676928.0, 631676928.0, 631676928.0, 631676928.0, 631676928.0]

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

Version: 4.11
Date: Mon Oct 12 23:10:40 GMT+02:00 2026
Hostname: n23m0269.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956599/tmpz6i69ae7prism_from-prism_to-umb_ex_nand.60-4_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956599/tmp8hcnpltxprism_from-prism_to-umb_ex_nand.60-4_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956599/tmpz6i69ae7prism_from-prism_to-umb_ex_nand.60-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... 1869302 3865355 5739106 7775467 9619803 11531463 13361904 15328230 17294522 18826082 states
Reachable states exploration and model construction done in 29.862 secs.
Sorting reachable states list...

Time for model construction: 33.368 seconds.

Type:        DTMC
States:      18826082 (1 initial)
Transitions: 29772212

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956599/tmp8hcnpltxprism_from-prism_to-umb_ex_nand.60-4_tmp_outdir_/model.umb"...
Time for exporting: 0.547 seconds.


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

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

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

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

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957848/tmpnfq1x8duprism_from-prism_to-umb_ex_nand.60-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... 1696621 3458074 5255419 6893974 8636389 10349739 12078803 13873829 15589419 17394948 18826082 states
Reachable states exploration and model construction done in 32.758 secs.
Sorting reachable states list...

Time for model construction: 37.862 seconds.

Type:        DTMC
States:      18826082 (1 initial)
Transitions: 29772212

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957848/tmpnonck2oaprism_from-prism_to-umb_ex_nand.60-4_tmp_outdir_/model.umb"...
Time for exporting: 0.57 seconds.


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

############################## Output files ##############################
model.umb:	Size of output file is 631676928 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.357 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Mon Oct 12 22:45:33 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.4955584/tmpy28z3dcfprism_from-prism_to-umb_ex_nand.60-4_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955584/tmp8__1f_uvprism_from-prism_to-umb_ex_nand.60-4_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955584/tmpy28z3dcfprism_from-prism_to-umb_ex_nand.60-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... 1915879 3892665 5890462 7954187 9901903 11983532 13913023 15967759 17980025 18826082 states
Reachable states exploration and model construction done in 28.448 secs.
Sorting reachable states list...

Time for model construction: 33.235 seconds.

Type:        DTMC
States:      18826082 (1 initial)
Transitions: 29772212

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955584/tmp8__1f_uvprism_from-prism_to-umb_ex_nand.60-4_tmp_outdir_/model.umb"...
Time for exporting: 0.521 seconds.


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

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

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

Version: 4.11
Date: Mon Oct 12 23:56:10 GMT+02:00 2026
Hostname: n23m0291.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4958246/tmpcor6yycjprism_from-prism_to-umb_ex_nand.60-4_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4958246/tmp0ungj4m7prism_from-prism_to-umb_ex_nand.60-4_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4958246/tmpcor6yycjprism_from-prism_to-umb_ex_nand.60-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... 1813925 3674688 5590891 7417956 9137463 11120247 12917837 14715165 16534360 18295938 18826082 states
Reachable states exploration and model construction done in 30.792 secs.
Sorting reachable states list...

Time for model construction: 35.744 seconds.

Type:        DTMC
States:      18826082 (1 initial)
Transitions: 29772212

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4958246/tmp0ungj4m7prism_from-prism_to-umb_ex_nand.60-4_tmp_outdir_/model.umb"...
Time for exporting: 0.66 seconds.


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

############################## Output files ##############################
model.umb:	Size of output file is 631676928 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.114 seconds
Return code: 0
##############################
PRISM
=====

Version: 4.11
Date: Mon Oct 12 22:36:27 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.4955214/tmp33tnjuuxprism_from-prism_to-umb_ex_nand.60-4_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955214/tmpyn3l7l24prism_from-prism_to-umb_ex_nand.60-4_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955214/tmp33tnjuuxprism_from-prism_to-umb_ex_nand.60-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... 1635883 3392065 5198818 6795391 8607722 10381669 12131703 13775890 15585116 17355945 18826082 states
Reachable states exploration and model construction done in 32.785 secs.
Sorting reachable states list...

Time for model construction: 37.59 seconds.

Type:        DTMC
States:      18826082 (1 initial)
Transitions: 29772212

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955214/tmpyn3l7l24prism_from-prism_to-umb_ex_nand.60-4_tmp_outdir_/model.umb"...
Time for exporting: 0.603 seconds.


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

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