[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Question about BlockingQueue tutorial step 16


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.