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

Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS

Thanks Markus.  Yes, by including the conjunct in IInv, TLC was able to IInv again.
It helped me to understand to find an inductive invariant using TLC for my simplified version of the spec.
Now I am trying to prove the inductive invariant using TLAPS.


On Friday, November 6, 2020 at 1:42:56 PM UTC-6 Markus Alexander Kuppe wrote:
On 06.11.20 11:03, Smruti Padhy wrote:
> Thanks for pointing that out. I redefined Seq with MySeq. Now I am
> getting, a different error: 
> -------------------------------------------
> In evaluation, the identifier buffer is either undefined or not an operator.
> line 64, col 19 to line 64, col 24 of module BlockingQueue
> -------------------------------------------
> I am not sure what I am missing here.

Hi Smruti,

if you compare git commit v16 [1] with v18 [2], you will find that the
first conjunct of TypeInv has been excluded from IInv (see [3]). If you
include the conjunct in IInv, TLC will be able to check IInv again.



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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/14047959-eaa6-4691-995d-4d6aa27cbec5n%40googlegroups.com.