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

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

-- 
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/a9b78c6b-b5ae-a8af-f281-d95cfd586c1f%40lemmster.de.