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"  explains the validation of inductive invariants in detail.
Feel free to open issues at https://github.com/lemmy/BlockingQueue should you have more questions.
PS: With the necessary type annotations , Apalache should validate IInv for larger values of Producers, Consumers, and BufCapacity.
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/B75C9A66-4F37-48E6-9303-BB5FCD740527%40lemmster.de.