Re: [tlaplus] TLAPS-proved invariant violated in TLC?

[Stephan Merz <stepha...@xxxxxxxxx>]

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.