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

*From*: Jaak Ristioja <jaak.r...@xxxxxxxx>*Date*: Fri, 16 Oct 2015 14:07:03 +0300*User-agent*: curl/7.42.1

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

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

- Prev by Date:
**Re: What do you think about the use of category theory for specifications?** - Next by Date:
**Re: RECURSIVE as a forward declaration** - Previous by thread:
**Re: RECURSIVE as a forward declaration** - Next by thread:
**Re: [tlaplus] TLAPS-proved invariant violated in TLC?** - Index(es):