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.
Best,
Markus
[1]
https://github.com/lemmy/BlockingQueue/blob/03fe04a9d63d0c92c77547bc10063e83e39a1878/BlockingQueue.tla#L96
[2]
https://github.com/lemmy/BlockingQueue/commit/c7adc434e02ed6a667396fc76194ca43df4172a3
[3]
https://github.com/lemmy/BlockingQueue/#v18-tlaps-co-domain-of-buffer-not-relevant-for-proof