[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Help with proving an obligation


Line 3403 of the attached tla file has the following obligation which fails on TLAPS(Version 1.5.6 of 29 January 2018) on my machine (Ubuntu 17.10):

  <5>6. Next BY <2>6 DEF Next


  Next == \/ \E p \in Proposers : Phase1a(p) \/ Phase2a1(p) \/ Phase2a11(p) \/ Phase2a12(p) \/ Phase2a13(p)
          \/ \E a \in Acceptors : Phase1b(a) \/ Phase2b(a)  \/ PhasePr(a)

and <2>6 is

  <2>6. ASSUME NEW a \in Acceptors,
        PROVE  Inv'

Also attached is the screenshot showing the interesting obligations. I'm wondering if I'm making a really dumb mistake here or is it something else?

Saksham Chand

Attachment: Screenshot_tla_Next.png
Description: PNG image

Attachment: vRAMultiPaxos.tla
Description: Binary data