[tlaplus] Question about BlockingQueue tutorial step 16

[Gregory SZUCS <gregory.z.szucs@xxxxxxxxx>]

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.