Re: [tlaplus] Question about BlockingQueue tutorial step 16

Hi Gregory,

the spec passes because of the changes in steps v12 and v13. In preparation of step v17, step v16 uses TLC to validate our inductive invariant "candidate" IInv by model-checking IInv /\ [Next]_vars => IInv'. In step v17, we prove that the spec is deadlock-free with TLAPS. The first page of Lamport's "Using TLC to Check Inductive Invariance" [1] explains the validation of inductive invariants in detail.

Feel free to open issues at https://github.com/lemmy/BlockingQueue should you have more questions.

Markus

PS: With the necessary type annotations [2], Apalache should validate IInv for larger values of Producers, Consumers, and BufCapacity.

[1] https://lamport.azurewebsites.net/tla/inductive-invariant.pdf

[2] https://github.com/lemmy/BlockingQueue/blob/apalache.new/BlockingQueue.tla

On Feb 9, 2022, at 3:08 AM, Gregory SZUCS <gregory.z.szucs@xxxxxxxxx> wrote:

Hello,

First thanks Markus Kuppe for the BlockingQueue tutorial.

I have a question about what happens to IInv at step 16. I do not understand how adding the
2 conjuncts make the spec pass.

Checking the model with

IInv == /\ TypeInv
/\ Invariant

fails with :

> Error: Invariant IInv is violated.

How can adding the two conjuncts make IInv true for all states if TypeInv or
Invariant is false in some state ?

IInv == /\ TypeInv
/\ Invariant
/\ buffer = <<>> => \E p \in Producers : p \notin waitSet
/\ Len(buffer) = BufCapacity => \E c \in Consumers : c \notin waitSet

> Pass.

Thanks !

Greg Z.

--
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/9dcd7cb6-3b1e-4aa3-9c0f-c9074d8c7ac9n%40googlegroups.com.