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

[Jaak Ristioja <jaak.r...@xxxxxxxx>]

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.
>