[0.983, 0.78, 0.896, 0.893, 0.896]

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

Version: 4.11
Date: Mon Oct 12 23:00:05 GMT+02:00 2026
Hostname: n23m0307.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956163/tmp20c872ghprism_from-prism_to-umb_ex_speed-ind.2100_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956163/tmpfwiy6cl1prism_from-prism_to-umb_ex_speed-ind.2100_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956163/tmp20c872ghprism_from-prism_to-umb_ex_speed-ind.2100_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     S1_def S2_def S3_def S4_def Y_def Z_def CC_def XX_def
Actions:     []
Variables:   S1 S2 S3 S4 Y Z CC XX
Labels:      "target"

Building model (engine:explicit)...

Computing reachable states... 319021 617075 743424 states
Reachable states exploration and model construction done in 7.118 secs.
Sorting reachable states list...

Time for model construction: 7.778 seconds.

Type:        CTMC
States:      743424 (1 initial)
Transitions: 9518080

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956163/tmpfwiy6cl1prism_from-prism_to-umb_ex_speed-ind.2100_tmp_outdir_/model.umb"...
Time for exporting: 0.983 seconds.


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

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

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

Version: 4.11
Date: Mon Oct 12 23:08:51 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.4956528/tmpqfsn6h89prism_from-prism_to-umb_ex_speed-ind.2100_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956528/tmptg3uivjgprism_from-prism_to-umb_ex_speed-ind.2100_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956528/tmpqfsn6h89prism_from-prism_to-umb_ex_speed-ind.2100_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     S1_def S2_def S3_def S4_def Y_def Z_def CC_def XX_def
Actions:     []
Variables:   S1 S2 S3 S4 Y Z CC XX
Labels:      "target"

Building model (engine:explicit)...

Computing reachable states... 352246 706470 743424 states
Reachable states exploration and model construction done in 6.325 secs.
Sorting reachable states list...

Time for model construction: 6.987 seconds.

Type:        CTMC
States:      743424 (1 initial)
Transitions: 9518080

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956528/tmptg3uivjgprism_from-prism_to-umb_ex_speed-ind.2100_tmp_outdir_/model.umb"...
Time for exporting: 0.78 seconds.


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

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

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

Version: 4.11
Date: Mon Oct 12 23:05:55 GMT+02:00 2026
Hostname: n23m0303.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956403/tmpzpw32xjgprism_from-prism_to-umb_ex_speed-ind.2100_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956403/tmpieceb1i1prism_from-prism_to-umb_ex_speed-ind.2100_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956403/tmpzpw32xjgprism_from-prism_to-umb_ex_speed-ind.2100_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     S1_def S2_def S3_def S4_def Y_def Z_def CC_def XX_def
Actions:     []
Variables:   S1 S2 S3 S4 Y Z CC XX
Labels:      "target"

Building model (engine:explicit)...

Computing reachable states... 314850 637545 743424 states
Reachable states exploration and model construction done in 6.996 secs.
Sorting reachable states list...

Time for model construction: 7.693 seconds.

Type:        CTMC
States:      743424 (1 initial)
Transitions: 9518080

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956403/tmpieceb1i1prism_from-prism_to-umb_ex_speed-ind.2100_tmp_outdir_/model.umb"...
Time for exporting: 0.896 seconds.


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

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

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

Version: 4.11
Date: Mon Oct 12 23:47:57 GMT+02:00 2026
Hostname: r23m0202.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957931/tmpioscbyzqprism_from-prism_to-umb_ex_speed-ind.2100_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957931/tmp1echamynprism_from-prism_to-umb_ex_speed-ind.2100_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957931/tmpioscbyzqprism_from-prism_to-umb_ex_speed-ind.2100_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     S1_def S2_def S3_def S4_def Y_def Z_def CC_def XX_def
Actions:     []
Variables:   S1 S2 S3 S4 Y Z CC XX
Labels:      "target"

Building model (engine:explicit)...

Computing reachable states... 320046 646056 743424 states
Reachable states exploration and model construction done in 6.981 secs.
Sorting reachable states list...

Time for model construction: 8.068 seconds.

Type:        CTMC
States:      743424 (1 initial)
Transitions: 9518080

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957931/tmp1echamynprism_from-prism_to-umb_ex_speed-ind.2100_tmp_outdir_/model.umb"...
Time for exporting: 0.893 seconds.


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

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

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

Version: 4.11
Date: Mon Oct 12 23:59:36 GMT+02:00 2026
Hostname: n23m0120.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4958376/tmpoxc2qz7hprism_from-prism_to-umb_ex_speed-ind.2100_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4958376/tmpu_bsz02aprism_from-prism_to-umb_ex_speed-ind.2100_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4958376/tmpoxc2qz7hprism_from-prism_to-umb_ex_speed-ind.2100_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     S1_def S2_def S3_def S4_def Y_def Z_def CC_def XX_def
Actions:     []
Variables:   S1 S2 S3 S4 Y Z CC XX
Labels:      "target"

Building model (engine:explicit)...

Computing reachable states... 328094 658963 743424 states
Reachable states exploration and model construction done in 6.734 secs.
Sorting reachable states list...

Time for model construction: 7.408 seconds.

Type:        CTMC
States:      743424 (1 initial)
Transitions: 9518080

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4958376/tmpu_bsz02aprism_from-prism_to-umb_ex_speed-ind.2100_tmp_outdir_/model.umb"...
Time for exporting: 0.896 seconds.


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

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