[0.574, 0.806, 0.626, 0.683, 0.577]

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

Version: 4.11
Date: Mon Oct 12 22:39:50 GMT+02:00 2026
Hostname: n23m0056.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955359/tmptcd6y282prism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955359/tmpeprpzylsprism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955359/tmptcd6y282prism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     oscillator_population
Actions:     [step]
Variables:   k_1 k_2 k_3 k_4 k_5 k_6 k_7 k_8 k_9 k_10
Labels:      "target"
Rewards:     "time_to_synch"

Building model (engine:explicit)...

Computing reachable states... 536 1143 1751 2357 2963 3573 4114 4687 5268 5885 6484 7021 7607 8199 8773 9364 9955 10550 11143 11747 12354 12992 13621 14263 14902 15539 16185 16828 17467 18116 18764 19406 20058 20666 21312 21960 22609 23261 23916 24311 states
Reachable states exploration and model construction done in 118.93 secs.
Sorting reachable states list...

Time for model construction: 119.599 seconds.

Type:        DTMC
States:      24311 (1 initial)
Transitions: 76623

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955359/tmpeprpzylsprism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_outdir_/model.umbxz"...
Time for exporting: 0.574 seconds.


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

############################## Output files ##############################
model.umbxz:	Size of output file is 89908 bytes

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

Version: 4.11
Date: Mon Oct 12 22:41:33 GMT+02:00 2026
Hostname: n23m0280.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955432/tmpxxedlo29prism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955432/tmpb1c480r9prism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955432/tmpxxedlo29prism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     oscillator_population
Actions:     [step]
Variables:   k_1 k_2 k_3 k_4 k_5 k_6 k_7 k_8 k_9 k_10
Labels:      "target"
Rewards:     "time_to_synch"

Building model (engine:explicit)...

Computing reachable states... 440 896 1356 1809 2259 2696 3162 3625 4108 4554 4905 5253 5656 6064 6493 7003 7493 7892 8300 8707 9140 9700 10246 10752 11221 11720 12223 12761 13246 13695 14107 14527 14944 15384 15843 16252 16579 16893 17366 17920 18450 18913 19387 19896 20407 20918 21379 21795 22225 22652 23102 23584 23927 24266 24311 states
Reachable states exploration and model construction done in 162.603 secs.
Sorting reachable states list...

Time for model construction: 163.419 seconds.

Type:        DTMC
States:      24311 (1 initial)
Transitions: 76623

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955432/tmpb1c480r9prism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_outdir_/model.umbxz"...
Time for exporting: 0.806 seconds.


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

############################## Output files ##############################
model.umbxz:	Size of output file is 89908 bytes

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

Version: 4.11
Date: Mon Oct 12 23:18:47 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.4956916/tmpwb87vxniprism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956916/tmpysv_y48kprism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956916/tmpwb87vxniprism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     oscillator_population
Actions:     [step]
Variables:   k_1 k_2 k_3 k_4 k_5 k_6 k_7 k_8 k_9 k_10
Labels:      "target"
Rewards:     "time_to_synch"

Building model (engine:explicit)...

Computing reachable states... 537 1154 1772 2386 3004 3626 4248 4872 5500 6131 6766 7396 8029 8665 9299 9935 10575 11212 11848 12497 13111 13737 14374 15008 15646 16286 16928 17571 18214 18860 19514 20163 20825 21484 22138 22803 23465 24125 24311 states
Reachable states exploration and model construction done in 114.943 secs.
Sorting reachable states list...

Time for model construction: 115.626 seconds.

Type:        DTMC
States:      24311 (1 initial)
Transitions: 76623

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956916/tmpysv_y48kprism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_outdir_/model.umbxz"...
Time for exporting: 0.626 seconds.


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

############################## Output files ##############################
model.umbxz:	Size of output file is 89908 bytes

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

Version: 4.11
Date: Mon Oct 12 22:36:24 GMT+02:00 2026
Hostname: n23m0060.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955209/tmpt0or8zuwprism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955209/tmpjs63jhoqprism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955209/tmpt0or8zuwprism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     oscillator_population
Actions:     [step]
Variables:   k_1 k_2 k_3 k_4 k_5 k_6 k_7 k_8 k_9 k_10
Labels:      "target"
Rewards:     "time_to_synch"

Building model (engine:explicit)...

Computing reachable states... 511 1099 1688 2276 2868 3462 4056 4652 5258 5862 6462 7068 7674 8277 8890 9500 10107 10724 11339 11944 12529 13141 13753 14365 14978 15592 16208 16825 17444 18066 18697 19325 19950 20584 21219 21850 22489 23127 23763 24311 states
Reachable states exploration and model construction done in 119.666 secs.
Sorting reachable states list...

Time for model construction: 120.376 seconds.

Type:        DTMC
States:      24311 (1 initial)
Transitions: 76623

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4955209/tmpjs63jhoqprism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_outdir_/model.umbxz"...
Time for exporting: 0.683 seconds.


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

############################## Output files ##############################
model.umbxz:	Size of output file is 89908 bytes

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

Version: 4.11
Date: Mon Oct 12 23:14:13 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.4956696/tmph_sdq01lprism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956696/tmprw3jjrhsprism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_outdir_/model.umbxz:format=umb,states=false,zip=xz'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956696/tmph_sdq01lprism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     oscillator_population
Actions:     [step]
Variables:   k_1 k_2 k_3 k_4 k_5 k_6 k_7 k_8 k_9 k_10
Labels:      "target"
Rewards:     "time_to_synch"

Building model (engine:explicit)...

Computing reachable states... 450 957 1464 1970 2477 2987 3499 4011 4517 5029 5546 6063 6581 7097 7609 8120 8635 9151 9669 10186 10700 11217 11735 12254 12775 13294 13815 14336 14855 15374 15892 16412 16932 17456 17975 18493 19013 19535 20059 20583 21107 21633 22157 22682 23206 23733 24261 24311 states
Reachable states exploration and model construction done in 141.428 secs.
Sorting reachable states list...

Time for model construction: 142.055 seconds.

Type:        DTMC
States:      24311 (1 initial)
Transitions: 76623

Exporting model in UMB format to file "/w0/tmp/slurm_tq429871.4956696/tmprw3jjrhsprism_from-prism_to-umb-xz_ex_oscillators.8-10-0.1-1-0.1-1.0_tmp_outdir_/model.umbxz"...
Time for exporting: 0.577 seconds.


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

############################## Output files ##############################
model.umbxz:	Size of output file is 90364 bytes