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

*From*: Jaak Ristioja <jaak.r...@xxxxxxxx>*Date*: Mon, 19 Oct 2015 10:55:36 +0300*References*: <5620DA57.6060204@cyber.ee> <032E3EF6-9EB3-45AD-AD03-C7C20E85814F@gmail.com>*User-agent*: curl/7.42.1

Hehe, I never thought my cargo cult approach could be of any good use. :D Best regards, J On 17.10.2015 10:32, Stephan Merz wrote: > 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. >

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

**Re: [tlaplus] TLAPS-proved invariant violated in TLC?***From:*Stephan Merz

- Prev by Date:
**Re: What should I do next in the Hyperbook?** - Next by Date:
**Re: What should I do next in the Hyperbook?** - Previous by thread:
**Re: [tlaplus] TLAPS-proved invariant violated in TLC?** - Next by thread:
**Unclear TLC evaluation behavior** - Index(es):