Log files for model egl.10-2 and tool configuration prism_from-prism_to-umb_ex

Parsed values
[MO, MO, MO, MO, MO]
Log file: prism_from-prism_to-umb_ex_egl.10-2_rep1.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 154.083 seconds
Return code: -9
##############################
PRISM
=====

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

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4957704/tmpdzgolknnprism_from-prism_to-umb_ex_egl.10-2_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     counter partyA partyB
Actions:     [] [receiveB] [receiveA]
Variables:   b n phase party b0 b20 b1 b21 b2 b22 b3 b23 b4 b24 b5 b25 b6 b26 b7 b27 b8 b28 b9 b29 b10 b30 b11 b31 b12 b32 b13 b33 b14 b34 b15 b35 b16 b36 b17 b37 b18 b38 b19 b39 a0 a20 a1 a21 a2 a22 a3 a23 a4 a24 a5 a25 a6 a26 a7 a27 a8 a28 a9 a29 a10 a30 a11 a31 a12 a32 a13 a33 a14 a34 a15 a35 a16 a36 a17 a37 a18 a38 a19 a39
Labels:      "knowB" "knowA"

Building model (engine:explicit)...

Computing reachable states... 349640 681250 1014482 1479348 1957607 2448485 2949332 3425521 3914886 4412196 4918980 5357503 5835686 6318249 6823409 7290716 7802983 7866818 8329928 8780791 9195796 9673993 10157042 10648347 11122185 11613306 12125880 12616255 13078222 13507166 13955093 14400916 14854331 15358009 15878123 16360130 16832800 17282718 17737854 18271365 18735995 19206495 19660399 20114957 20566299 20951040 21389342 21800863 22269220 22664816
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

############################## Output files ##############################
model.umb:	File does not exist.
Log file: prism_from-prism_to-umb_ex_egl.10-2_rep2.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 161.536 seconds
Return code: -9
##############################
PRISM
=====

Version: 4.11
Date: Mon Oct 12 23:51:01 GMT+02:00 2026
Hostname: n23m0046.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4958039/tmpr0un0vglprism_from-prism_to-umb_ex_egl.10-2_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4958039/tmph92tthphprism_from-prism_to-umb_ex_egl.10-2_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4958039/tmpr0un0vglprism_from-prism_to-umb_ex_egl.10-2_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     counter partyA partyB
Actions:     [] [receiveB] [receiveA]
Variables:   b n phase party b0 b20 b1 b21 b2 b22 b3 b23 b4 b24 b5 b25 b6 b26 b7 b27 b8 b28 b9 b29 b10 b30 b11 b31 b12 b32 b13 b33 b14 b34 b15 b35 b16 b36 b17 b37 b18 b38 b19 b39 a0 a20 a1 a21 a2 a22 a3 a23 a4 a24 a5 a25 a6 a26 a7 a27 a8 a28 a9 a29 a10 a30 a11 a31 a12 a32 a13 a33 a14 a34 a15 a35 a16 a36 a17 a37 a18 a38 a19 a39
Labels:      "knowB" "knowA"

Building model (engine:explicit)...

Computing reachable states... 349312 681929 1006511 1472143 1924347 2376760 2863225 3342443 3832451 4288932 4712120 5170345 5640582 6112145 6587665 6712318 7163435 7589031 8029868 8499713 8974943 9439951 9907758 10375281 10840840 11265805 11696904 12149046 12608655 13095053 13559614 14042898 14504322 14981859 15452599 15907518 16344555 16767127 17201982 17660953 18106830 18541265 19048780 19508486 19968363 20444766 20886343 21403233 21841047 22287948 22747317 23253364 23719279
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

############################## Output files ##############################
model.umb:	File does not exist.
Log file: prism_from-prism_to-umb_ex_egl.10-2_rep3.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 181.667 seconds
Return code: -9
##############################
PRISM
=====

Version: 4.11
Date: Mon Oct 12 22:59:31 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.4956137/tmp9py02m_kprism_from-prism_to-umb_ex_egl.10-2_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956137/tmp3ca_82nyprism_from-prism_to-umb_ex_egl.10-2_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956137/tmp9py02m_kprism_from-prism_to-umb_ex_egl.10-2_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     counter partyA partyB
Actions:     [] [receiveB] [receiveA]
Variables:   b n phase party b0 b20 b1 b21 b2 b22 b3 b23 b4 b24 b5 b25 b6 b26 b7 b27 b8 b28 b9 b29 b10 b30 b11 b31 b12 b32 b13 b33 b14 b34 b15 b35 b16 b36 b17 b37 b18 b38 b19 b39 a0 a20 a1 a21 a2 a22 a3 a23 a4 a24 a5 a25 a6 a26 a7 a27 a8 a28 a9 a29 a10 a30 a11 a31 a12 a32 a13 a33 a14 a34 a15 a35 a16 a36 a17 a37 a18 a38 a19 a39
Labels:      "knowB" "knowA"

Building model (engine:explicit)...

Computing reachable states... 310789 646558 951978 1320752 1761264 2208876 2634026 3065254 3530440 3947116 4367511 4762372 5182447 5637887 6072970 6514019 6944155 7049267 7486202 7874307 8283446 8694296 9126116 9561218 10018587 10439861 10900553 11324026 11743094 12132352 12521630 12930528 13334498 13744996 14165142 14611020 15077069 15503021 15929207 16342760 16756124 17188738 17595413 18017046 18442896 18887432 19276283 19641951 20013854 20433782 20787775 21154475 21597045 21992448 22436874 22905437 23332019 23760951
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

############################## Output files ##############################
model.umb:	File does not exist.
Log file: prism_from-prism_to-umb_ex_egl.10-2_rep4.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 164.509 seconds
Return code: -9
##############################
PRISM
=====

Version: 4.11
Date: Mon Oct 12 22:42:07 GMT+02:00 2026
Hostname: n23m0258.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4955457/tmpbmou_s83prism_from-prism_to-umb_ex_egl.10-2_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4955457/tmp1nlka7fgprism_from-prism_to-umb_ex_egl.10-2_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4955457/tmpbmou_s83prism_from-prism_to-umb_ex_egl.10-2_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     counter partyA partyB
Actions:     [] [receiveB] [receiveA]
Variables:   b n phase party b0 b20 b1 b21 b2 b22 b3 b23 b4 b24 b5 b25 b6 b26 b7 b27 b8 b28 b9 b29 b10 b30 b11 b31 b12 b32 b13 b33 b14 b34 b15 b35 b16 b36 b17 b37 b18 b38 b19 b39 a0 a20 a1 a21 a2 a22 a3 a23 a4 a24 a5 a25 a6 a26 a7 a27 a8 a28 a9 a29 a10 a30 a11 a31 a12 a32 a13 a33 a14 a34 a15 a35 a16 a36 a17 a37 a18 a38 a19 a39
Labels:      "knowB" "knowA"

Building model (engine:explicit)...

Computing reachable states... 355796 691382 1021729 1498079 1959508 2432954 2913567 3399907 3857186 4322321 4775159 5215676 5709965 6179387 6672696 7090200 7570714 8018370 8458391 8927518 9397693 9900934 10355983 10852259 11323935 11779616 12239718 12670414 13124034 13556151 14026108 14526000 14997405 15459241 15923153 16398864 16843483 17326268 17819844 18300894 18748528 19193027 19610426 20071982 20494175 20886560 21305325 21746588 22172107 22639339 23079829 23596482 24044878
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

############################## Output files ##############################
model.umb:	File does not exist.
Log file: prism_from-prism_to-umb_ex_egl.10-2_rep5.log
Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism -exportmodel %outdir/model.umb:format=umb,states=false,zip=false
Wallclock time: 172.494 seconds
Return code: -9
##############################
PRISM
=====

Version: 4.11
Date: Mon Oct 12 23:06:29 GMT+02:00 2026
Hostname: n23m0023.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4956424/tmpzevuqvifprism_from-prism_to-umb_ex_egl.10-2_tmp_indir_/model.prism -exportmodel '/w0/tmp/slurm_tq429871.4956424/tmpur9rmhbvprism_from-prism_to-umb_ex_egl.10-2_tmp_outdir_/model.umb:format=umb,states=false,zip=false'

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4956424/tmpzevuqvifprism_from-prism_to-umb_ex_egl.10-2_tmp_indir_/model.prism"...

Type:        DTMC
Modules:     counter partyA partyB
Actions:     [] [receiveB] [receiveA]
Variables:   b n phase party b0 b20 b1 b21 b2 b22 b3 b23 b4 b24 b5 b25 b6 b26 b7 b27 b8 b28 b9 b29 b10 b30 b11 b31 b12 b32 b13 b33 b14 b34 b15 b35 b16 b36 b17 b37 b18 b38 b19 b39 a0 a20 a1 a21 a2 a22 a3 a23 a4 a24 a5 a25 a6 a26 a7 a27 a8 a28 a9 a29 a10 a30 a11 a31 a12 a32 a13 a33 a14 a34 a15 a35 a16 a36 a17 a37 a18 a38 a19 a39
Labels:      "knowB" "knowA"

Building model (engine:explicit)...

Computing reachable states... 321557 637698 949927 1337607 1779726 2223902 2662225 3106943 3543215 3993605 4443888 4883479 5276159 5697047 6139532 6594484 7013205 7468521 7932725 8044505 8487427 8899139 9289029 9709667 10144060 10577349 11025720 11466727 11925127 12361422 12815986 13283509 13751032 14185540 14583502 14989469 15400438 15784846 16253132 16648304 17026924 17504262 17919894 18353937 18813771 19262946 19684157 20110289 20588571 20968465 21409842 21868632 22254063 22656261 23093491 23486528
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

############################## Output files ##############################
model.umb:	File does not exist.