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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Sat, 17 Oct 2015 09:32:06 +0200*References*: <5620DA57.6060204@cyber.ee>

Dear Jaak, what should not have worked in your proof are the level-2 steps that prove a non-temporal obligation "BY PTL". (Note that the proof does not even use the CASE assumption or the definitions of formulas NextComponent.) I just tried this and PTL indeed accepts these steps. It wrongly considers the assumption "Invariant" to occur in a boxed context (i.e., it assumes it to always hold) and therefore has no problem proving that Invariant' must be true. In fact, it even accepts the bogus proof <1>2. Invariant /\ [Next]_vars => Invariant' <2> SUFFICES ASSUME Invariant, [Next]_vars PROVE Invariant' OBVIOUS <2> QED BY PTL This is a serious bug in the handling of temporal contexts that we need to fix in the code of TLAPS. Until we do so, please be sure not to use PTL for a non-temporal proof in the context of a SUFFICES ASSUME ... PROOF step. Thanks for reporting this! Stephan > On 16 Oct 2015, at 13:07, Jaak Ristioja <jaak.r...@xxxxxxxx> wrote: > > Hello! > > During designing a (proprietary) protocol I've reached a point where > I've proved (all highlighted green in TLA+ Toolbox) an invariant like > > THEOREM InvariantHolds == Spec => []Invariant \* All green > <1>1. Init => Invariant PROOF OMITTED \* For this e-mail > <1>2. Invariant /\ [Next]_vars => Invariant' > <2> SUFFICES ASSUME Invariant > [Next]_vars > PROVE Invariant' > OBVIOUS > <2>1. CASE NextComponent BY PTL > <2>2. CASE NextComponent2 BY PTL > \* ... > <2>3. QED BY <2>1, <2>2 (* ... *) DEF Next > <1>3. QED BY <1>1, <1>2, PTL DEF Spec > > But when I run the protocol TLC it reports that the invariant Invariant > is violated. After debugging this for a while I found a bug in my > Invariant which explains why it failed in TLC. Is it incorrect of me to > assume TLAPS has successfully proved the theorem when the TLA+ Toolbox > hightlights the theorem all green a pressing CTRL+G on it twice? Am I > doing something wrong or is this a bug? > > Best regards, > Jaak > > -- > 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 http://groups.google.com/group/tlaplus. > For more options, visit https://groups.google.com/d/optout.

**Follow-Ups**:**Re: [tlaplus] TLAPS-proved invariant violated in TLC?***From:*Jaak Ristioja

**References**:**TLAPS-proved invariant violated in TLC?***From:*Jaak Ristioja

- Prev by Date:
**Re: RECURSIVE as a forward declaration** - Next by Date:
**Re: What should I do next in the Hyperbook?** - Previous by thread:
**TLAPS-proved invariant violated in TLC?** - Next by thread:
**Re: [tlaplus] TLAPS-proved invariant violated in TLC?** - Index(es):