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

Re: [tlaplus] Help with proving an obligation



Hi,

the reason that the step fails is that for the backends your hypothesis Phase1b(a) gets coalesced into an anonymous predicate. For example, here is the input that Zenon receives:

;; obligation #1
$hyp "a_in" (TLA.in a Acceptors)
$hyp "m_in" (TLA.in m a_msgshash_primea)
$hyp "a_m1a_in" (TLA.in a_m1a msgs)
$hyp "v'152" (a_h97e32460362eba8559dabb07ccf5e9a a)
$goal (\/ (TLA.bEx Proposers ((p) (\/ (\/ (\/ (\/ (Phase1a p)
(a_Phase2a1a p)) (a_Phase2a11a p)) (a_Phase2a12a p)) (a_Phase2a13a p))))
(TLA.bEx Acceptors ((a_1) (\/ (\/ (Phase1b a_1) (Phase2b a_1)) (PhasePr a_1)))))

The hypothesis named "v'152" corresponds to Phase1b(a), and you can see that the predicate has been renamed and doesn't correspond to the one that appears in the conclusion. I don't have a clear explanation yet for why that happens, and I believe it is an error. My hunch is that the PM gets confused by the primed hypotheses in the enclosing SUFFICES steps <4> or <5> and then plays overly cautious. However, I can offer two workarounds:

1. Move your step further up in the proof hierarchy. For example, insert it immediately after step <2>6, like so:

    <3>0. Next  BY <2>6 DEF Next

Then, replace <5>6 by <3>0 in the justification of step <5>7.

2. Change lemma SafeAtStable by replacing "Next" on the left-hand side of the implication by "[Next]_vars", then you can omit step <5>6 altogether.

We'll again investigate the coalescing algorithm to understand what went wrong here. Thanks for reporting this.

Regards,
Stephan


On 12 Feb 2018, at 19:36, saksha...@xxxxxxxxxxxxxx wrote:

Hi,

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

where

  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,
               Phase1b(a)
        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?

Thanks,
Saksham Chand


--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
<Screenshot_tla_Next.png><vRAMultiPaxos.tla>