v35 (Termination): Check refinement of BlockingQueue by BlockingQueuePoisonPill.

Author: lemmy

BlockingQueuePoisonPill.cfg

@@ -13,3 +13,5 @@ INVARIANT NoDeadlock
 INVARIANT QueueEmpty
 
 PROPERTIES GlobalTermination
+
+PROPERTIES BQSpec

BlockingQueuePoisonPill.tla

@@ -122,4 +122,22 @@ GlobalTermination ==
 Spec ==
     Init /\ [][Next]_vars /\ WF_vars(Next) 
 
+-----------------------------------------------------------------------------
+\* This spec still implementes the high-level BlockingQueue spec.
+
+BQ == INSTANCE BlockingQueue
+                \* Replace Poison with some Producer. The high-level
+                \* BlockingQueue spec is a peculiar about the elements
+                \* in its buffer.  If this wouldn't be a tutotial but
+                \* a real-world spec, the high-level spec would be
+                \* corrected to be oblivious to the elements in buffer.
+                WITH buffer <-
+                    [ i \in DOMAIN buffer |-> IF buffer[i] = Poison
+                                              THEN CHOOSE p \in Producers: TRUE
+                                              ELSE buffer[i] ]
+
+BQSpec == BQ!Spec
+
+THEOREM Spec => BQSpec
+
 =============================================================================

README.md

@@ -13,6 +13,8 @@ This tutorial is work in progress. More chapters will be added in the future. In
 
 --------------------------------------------------------------------------
 
+### v35 (Termination): Check refinement of BlockingQueue by BlockingQueuePoisonPill.
+
 ### v34 (Termination): Terminate Consumers when Producers are done by sending a poison pill in a termination stage.
 
 ### v33 (Refinement Fair): Prove BlockingQueueFair implements BlockingQueueSplit.