[2.718, 3.007, 2.974, 3.065, 3.027]

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

Version: 4.11
Date: Mon Oct 12 23:47:20 GMT+02:00 2026
Hostname: n23m0057.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957920/tmpvgbpxhynprism_from-prism_to-umb-gz_ex_nand.60-4_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957920/tmpkyqi75gvprism_from-prism_to-umb-gz_ex_nand.60-4_tmp_outdir_/model.umbgz:format=umb,states=false,zip=gzip'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957920/tmpvgbpxhynprism_from-prism_to-umb-gz_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... 1911693 3871884 5982686 8064357 10066973 12032568 14204839 16145621 17982361 18826082 states
Reachable states exploration and model construction done in 28.306 secs.
Sorting reachable states list...

Time for model construction: 32.955 seconds.

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

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957920/tmpkyqi75gvprism_from-prism_to-umb-gz_ex_nand.60-4_tmp_outdir_/model.umbgz"...
Time for exporting: 2.718 seconds.


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

############################## Output files ##############################
model.umbgz:	Size of output file is 74433824 bytes

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

Version: 4.11
Date: Mon Oct 12 22:57:09 GMT+02:00 2026
Hostname: n23m0050.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956040/tmp9wm7slonprism_from-prism_to-umb-gz_ex_nand.60-4_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956040/tmpfm6vxucaprism_from-prism_to-umb-gz_ex_nand.60-4_tmp_outdir_/model.umbgz:format=umb,states=false,zip=gzip'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956040/tmp9wm7slonprism_from-prism_to-umb-gz_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... 1641193 3394852 5146402 6893917 8781661 10571116 12377133 14132216 15948853 17706906 18826082 states
Reachable states exploration and model construction done in 32.09 secs.
Sorting reachable states list...

Time for model construction: 37.456 seconds.

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

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956040/tmpfm6vxucaprism_from-prism_to-umb-gz_ex_nand.60-4_tmp_outdir_/model.umbgz"...
Time for exporting: 3.007 seconds.


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

############################## Output files ##############################
model.umbgz:	Size of output file is 74433625 bytes

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

Version: 4.11
Date: Mon Oct 12 23:04:11 GMT+02:00 2026
Hostname: n23m0237.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956314/tmpuw3gntubprism_from-prism_to-umb-gz_ex_nand.60-4_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956314/tmpjdpbp13hprism_from-prism_to-umb-gz_ex_nand.60-4_tmp_outdir_/model.umbgz:format=umb,states=false,zip=gzip'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956314/tmpuw3gntubprism_from-prism_to-umb-gz_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... 1618244 3377157 5129786 6831748 8667008 10454604 12168026 13815740 15610514 17364168 18826082 states
Reachable states exploration and model construction done in 32.74 secs.
Sorting reachable states list...

Time for model construction: 37.747 seconds.

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

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956314/tmpjdpbp13hprism_from-prism_to-umb-gz_ex_nand.60-4_tmp_outdir_/model.umbgz"...
Time for exporting: 2.974 seconds.


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

############################## Output files ##############################
model.umbgz:	Size of output file is 74433625 bytes

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

Version: 4.11
Date: Mon Oct 12 23:33:24 GMT+02:00 2026
Hostname: n23m0314.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957510/tmp_77p9y3wprism_from-prism_to-umb-gz_ex_nand.60-4_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957510/tmpj5e3n_r9prism_from-prism_to-umb-gz_ex_nand.60-4_tmp_outdir_/model.umbgz:format=umb,states=false,zip=gzip'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957510/tmp_77p9y3wprism_from-prism_to-umb-gz_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... 1766998 3595015 5471756 7258798 8963623 10729497 12379201 14168400 15948256 17697279 18826082 states
Reachable states exploration and model construction done in 32.034 secs.
Sorting reachable states list...

Time for model construction: 37.597 seconds.

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

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957510/tmpj5e3n_r9prism_from-prism_to-umb-gz_ex_nand.60-4_tmp_outdir_/model.umbgz"...
Time for exporting: 3.065 seconds.


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

############################## Output files ##############################
model.umbgz:	Size of output file is 74433625 bytes

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

Version: 4.11
Date: Mon Oct 12 22:32:23 GMT+02:00 2026
Hostname: n23m0260.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955042/tmpub8za9ohprism_from-prism_to-umb-gz_ex_nand.60-4_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955042/tmp6_mhtgr5prism_from-prism_to-umb-gz_ex_nand.60-4_tmp_outdir_/model.umbgz:format=umb,states=false,zip=gzip'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955042/tmpub8za9ohprism_from-prism_to-umb-gz_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... 1694350 3425608 5135684 6940122 8721755 10466817 12148167 13896599 15633528 17476229 18826082 states
Reachable states exploration and model construction done in 32.813 secs.
Sorting reachable states list...

Time for model construction: 37.901 seconds.

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

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955042/tmp6_mhtgr5prism_from-prism_to-umb-gz_ex_nand.60-4_tmp_outdir_/model.umbgz"...
Time for exporting: 3.027 seconds.


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

############################## Output files ##############################
model.umbgz:	Size of output file is 74433626 bytes