[0.134, 0.165, 0.132, 0.126, 0.129]

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

Version: 4.11
Date: Mon Oct 12 23:53:17 GMT+02:00 2026
Hostname: r23m0206.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4958135/tmpaqvdya96prism_from-prism_to-umb_ex_embedded.8-12_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4958135/tmprqx1ejyeprism_from-prism_to-umb_ex_embedded.8-12_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4958135/tmpaqvdya96prism_from-prism_to-umb_ex_embedded.8-12_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     sensors proci actuators proco procm bus
Actions:     [] [input_reboot] [output_reboot] [timeout]
Variables:   s i a o m count comp reqi reqo
Labels:      "fail_actuators" "l_down"

Building model (engine:explicit)...

Computing reachable states... 8548 states
Reachable states exploration and model construction done in 0.108 secs.
Sorting reachable states list...

Time for model construction: 0.155 seconds.

Type:        CTMC
States:      8548 (1 initial)
Transitions: 36041

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4958135/tmprqx1ejyeprism_from-prism_to-umb_ex_embedded.8-12_tmp_outdir_/model.umb"...
Time for exporting: 0.134 seconds.


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

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

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

Version: 4.11
Date: Mon Oct 12 22:32:25 GMT+02:00 2026
Hostname: n23m0054.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955056/tmp36kr8jnjprism_from-prism_to-umb_ex_embedded.8-12_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955056/tmpap_mdyzyprism_from-prism_to-umb_ex_embedded.8-12_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955056/tmp36kr8jnjprism_from-prism_to-umb_ex_embedded.8-12_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     sensors proci actuators proco procm bus
Actions:     [] [input_reboot] [output_reboot] [timeout]
Variables:   s i a o m count comp reqi reqo
Labels:      "fail_actuators" "l_down"

Building model (engine:explicit)...

Computing reachable states... 8548 states
Reachable states exploration and model construction done in 0.105 secs.
Sorting reachable states list...

Time for model construction: 0.21 seconds.

Type:        CTMC
States:      8548 (1 initial)
Transitions: 36041

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955056/tmpap_mdyzyprism_from-prism_to-umb_ex_embedded.8-12_tmp_outdir_/model.umb"...
Time for exporting: 0.165 seconds.


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

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

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

Version: 4.11
Date: Mon Oct 12 23:33:59 GMT+02:00 2026
Hostname: n23m0357.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957530/tmpy_bqu6_iprism_from-prism_to-umb_ex_embedded.8-12_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957530/tmpqabtfg0lprism_from-prism_to-umb_ex_embedded.8-12_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957530/tmpy_bqu6_iprism_from-prism_to-umb_ex_embedded.8-12_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     sensors proci actuators proco procm bus
Actions:     [] [input_reboot] [output_reboot] [timeout]
Variables:   s i a o m count comp reqi reqo
Labels:      "fail_actuators" "l_down"

Building model (engine:explicit)...

Computing reachable states... 8548 states
Reachable states exploration and model construction done in 0.107 secs.
Sorting reachable states list...

Time for model construction: 0.153 seconds.

Type:        CTMC
States:      8548 (1 initial)
Transitions: 36041

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957530/tmpqabtfg0lprism_from-prism_to-umb_ex_embedded.8-12_tmp_outdir_/model.umb"...
Time for exporting: 0.132 seconds.


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

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

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

Version: 4.11
Date: Mon Oct 12 23:27:27 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.4957277/tmpip0_ejzsprism_from-prism_to-umb_ex_embedded.8-12_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957277/tmpsdgs1r1mprism_from-prism_to-umb_ex_embedded.8-12_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957277/tmpip0_ejzsprism_from-prism_to-umb_ex_embedded.8-12_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     sensors proci actuators proco procm bus
Actions:     [] [input_reboot] [output_reboot] [timeout]
Variables:   s i a o m count comp reqi reqo
Labels:      "fail_actuators" "l_down"

Building model (engine:explicit)...

Computing reachable states... 8548 states
Reachable states exploration and model construction done in 0.107 secs.
Sorting reachable states list...

Time for model construction: 0.151 seconds.

Type:        CTMC
States:      8548 (1 initial)
Transitions: 36041

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957277/tmpsdgs1r1mprism_from-prism_to-umb_ex_embedded.8-12_tmp_outdir_/model.umb"...
Time for exporting: 0.126 seconds.


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

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

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

Version: 4.11
Date: Mon Oct 12 23:47:55 GMT+02:00 2026
Hostname: r23m0215.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4957935/tmp76rvgm5hprism_from-prism_to-umb_ex_embedded.8-12_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4957935/tmpm0d5iz7lprism_from-prism_to-umb_ex_embedded.8-12_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957935/tmp76rvgm5hprism_from-prism_to-umb_ex_embedded.8-12_tmp_indir_/model.prism"...

Type:        CTMC
Modules:     sensors proci actuators proco procm bus
Actions:     [] [input_reboot] [output_reboot] [timeout]
Variables:   s i a o m count comp reqi reqo
Labels:      "fail_actuators" "l_down"

Building model (engine:explicit)...

Computing reachable states... 8548 states
Reachable states exploration and model construction done in 0.102 secs.
Sorting reachable states list...

Time for model construction: 0.147 seconds.

Type:        CTMC
States:      8548 (1 initial)
Transitions: 36041

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4957935/tmpm0d5iz7lprism_from-prism_to-umb_ex_embedded.8-12_tmp_outdir_/model.umb"...
Time for exporting: 0.129 seconds.


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

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