Log pnueli-zuck.10_prism_from-prism_check

Log file: prism_from-prism_check_ex_pnueli-zuck.10_rep1.log

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 141.226 seconds
Return code: -9
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 09:10:46 GMT+02:00 2026
Hostname: n23m0263.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4964963/tmpikbsdwkdprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4964963/tmpikbsdwkdprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4964963/tmpikbsdwkdprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/model.prism"...

Type:        MDP
Modules:     process0 process1 process2 process3 process4 process5 process6 process7 process8 process9
Actions:     []
Variables:   p0 p1 p2 p3 p4 p5 p6 p7 p8 p9
Labels:      "target"

Parsing properties file "/w0/tmp/slurm_tq429871.4964963/tmpikbsdwkdprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/property.props"...

1 property:
(1) "live": Pmax=? [ F "target" ]

---------------------------------------------------------------------

Model checking: "live": Pmax=? [ F "target" ]

Building model (engine:explicit)...

Computing reachable states... 200441 410270 612597 807073 1019248 1200628 1401074 1600178 1792476 1986726 2155651 2334573 2516470 2681597 2875728 3033129 3192612 3379526 3545039 3725973 3905070 4104728 4275997 4456709 4628133 4776260 4950591 5111511 5286848 5457235 5607995 5787330 5969159 6137364 6326639 6525399 6704349 6911715 7103970 7263302 7439297 7602221 7773882 7925379 8081846 8235431
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

Log file: prism_from-prism_check_ex_pnueli-zuck.10_rep2.log

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 122.512 seconds
Return code: -9
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 07:27:04 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.4962264/tmpsqvlfwcsprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4962264/tmpsqvlfwcsprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4962264/tmpsqvlfwcsprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/model.prism"...

Type:        MDP
Modules:     process0 process1 process2 process3 process4 process5 process6 process7 process8 process9
Actions:     []
Variables:   p0 p1 p2 p3 p4 p5 p6 p7 p8 p9
Labels:      "target"

Parsing properties file "/w0/tmp/slurm_tq429871.4962264/tmpsqvlfwcsprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/property.props"...

1 property:
(1) "live": Pmax=? [ F "target" ]

---------------------------------------------------------------------

Model checking: "live": Pmax=? [ F "target" ]

Building model (engine:explicit)...

Computing reachable states... 232220 463854 696997 920677 1129353 1356899 1565364 1777045 1979361 2208107 2407150 2625401 2822902 3052466 3272265 3469535 3638445 3842641 4025394 4247933 4459188 4672867 4881280 5085298 5256626 5467541 5649063 5839908 6032912 6228569 6400707 6628492 6850368 7075434 7288514 7513093 7724937 7923577 8103912 8306219
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

Log file: prism_from-prism_check_ex_pnueli-zuck.10_rep3.log

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 121.286 seconds
Return code: -9
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 07:18:07 GMT+02:00 2026
Hostname: n23m0042.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4961893/tmpvpdon1wdprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4961893/tmpvpdon1wdprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4961893/tmpvpdon1wdprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/model.prism"...

Type:        MDP
Modules:     process0 process1 process2 process3 process4 process5 process6 process7 process8 process9
Actions:     []
Variables:   p0 p1 p2 p3 p4 p5 p6 p7 p8 p9
Labels:      "target"

Parsing properties file "/w0/tmp/slurm_tq429871.4961893/tmpvpdon1wdprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/property.props"...

1 property:
(1) "live": Pmax=? [ F "target" ]

---------------------------------------------------------------------

Model checking: "live": Pmax=? [ F "target" ]

Building model (engine:explicit)...

Computing reachable states... 203393 417713 627981 832782 1047167 1251487 1460021 1663395 1879818 2082164 2284266 2476050 2672170 2854084 3031031 3219455 3407458 3603697 3807434 3952645 4168167 4356374 4534392 4727102 4899091 5069503 5264655 5477246 5667319 5864598 6055801 6227827 6407181 6583041 6770007 6954360 7139983 7320055 7480947
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

Log file: prism_from-prism_check_ex_pnueli-zuck.10_rep4.log

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 144.003 seconds
Return code: -9
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 07:44:46 GMT+02:00 2026
Hostname: n23m0255.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4963048/tmpf_1flgxgprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4963048/tmpf_1flgxgprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4963048/tmpf_1flgxgprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/model.prism"...

Type:        MDP
Modules:     process0 process1 process2 process3 process4 process5 process6 process7 process8 process9
Actions:     []
Variables:   p0 p1 p2 p3 p4 p5 p6 p7 p8 p9
Labels:      "target"

Parsing properties file "/w0/tmp/slurm_tq429871.4963048/tmpf_1flgxgprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/property.props"...

1 property:
(1) "live": Pmax=? [ F "target" ]

---------------------------------------------------------------------

Model checking: "live": Pmax=? [ F "target" ]

Building model (engine:explicit)...

Computing reachable states... 188608 381857 583131 780879 967519 1156670 1359213 1555428 1750393 1952567 2163904 2349084 2542668 2720345 2911012 3095756 3265780 3442369 3605874 3781268 3960988 4140723 4307687 4476038 4658842 4790405 4942690 5091297 5244000 5421330 5598666 5738661 5892829 6073295 6263206 6440573 6643022 6846063 7026048 7200648 7377262 7535584 7696413 7836883 7992694 8129612 8279572
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

Log file: prism_from-prism_check_ex_pnueli-zuck.10_rep5.log

Command(s):
../bin/prism -javamaxmem 32g -buildall -ex %indir/model.prism %indir/property.props
Wallclock time: 114.403 seconds
Return code: -9
##############################
PRISM
=====

Version: 4.11
Date: Tue Oct 13 09:02:57 GMT+02:00 2026
Hostname: n23m0111.hpc.itc.rwth-aachen.de
Memory limits: cudd=1g, java(heap)=32g
Command line: prism -javamaxmem 32g -buildall -ex /w0/tmp/slurm_tq429871.4964597/tmpbir4h57lprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/model.prism /w0/tmp/slurm_tq429871.4964597/tmpbir4h57lprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/property.props

Parsing PRISM model file "/w0/tmp/slurm_tq429871.4964597/tmpbir4h57lprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/model.prism"...

Type:        MDP
Modules:     process0 process1 process2 process3 process4 process5 process6 process7 process8 process9
Actions:     []
Variables:   p0 p1 p2 p3 p4 p5 p6 p7 p8 p9
Labels:      "target"

Parsing properties file "/w0/tmp/slurm_tq429871.4964597/tmpbir4h57lprism_from-prism_check_ex_pnueli-zuck.10_tmp_indir_/property.props"...

1 property:
(1) "live": Pmax=? [ F "target" ]

---------------------------------------------------------------------

Model checking: "live": Pmax=? [ F "target" ]

Building model (engine:explicit)...

Computing reachable states... 235958 483074 720408 950041 1196839 1423006 1665912 1890596 2120288 2332786 2561748 2779029 2975964 3195751 3415999 3635554 3860197 4066464 4259328 4445050 4640473 4846176 5046590 5227688 5469061 5690578 5897660 6131506 6333841 6540059 6757587 6953140 7173046 7375160 7582805 7757075
##############################Output to stderr##############################
Picked up JAVA_TOOL_OPTIONS: -Xmx32g

Log files for model pnueli-zuck.10 and tool configuration prism_from-prism_check_ex