v06 (continue): Convert constants into variables.

BlockingQueue.tla

@@ -13,10 +13,10 @@ ASSUME Assumption ==
 
 -----------------------------------------------------------------------------
 
-VARIABLES buffer, waitSet
-vars == <<buffer, waitSet>>
+VARIABLES buffer, waitSet, producers, consumers, bufCapacity
+vars == <<buffer, waitSet, producers, consumers, bufCapacity>>
 
-RunningThreads == (Producers \cup Consumers) \ waitSet
+RunningThreads == (producers \cup consumers) \ waitSet
 
 (* @see java.lang.Object#notify *)       
 Notify == IF waitSet # {}
@@ -30,10 +30,10 @@ Wait(t) == /\ waitSet' = waitSet \cup {t}
 -----------------------------------------------------------------------------
 
 Put(t, d) ==
-   \/ /\ Len(buffer) < BufCapacity
+   \/ /\ Len(buffer) < bufCapacity
       /\ buffer' = Append(buffer, d)
       /\ Notify
-   \/ /\ Len(buffer) = BufCapacity
+   \/ /\ Len(buffer) = bufCapacity
       /\ Wait(t)
 
 Get(t) ==
@@ -48,21 +48,26 @@ Get(t) ==
 (* Initially, the buffer is empty and no thread is waiting. *)
 Init == /\ buffer = <<>>
         /\ waitSet = {}
+        /\ producers \in (SUBSET Producers) \ {{}}
+        /\ consumers \in (SUBSET Consumers) \ {{}}
+        /\ bufCapacity \in 1..BufCapacity
 
 (* Then, pick a thread out of all running threads and have it do its thing. *)
-Next == \E t \in RunningThreads: \/ /\ t \in Producers
+Next == 
+    /\  UNCHANGED <<producers, consumers, bufCapacity>>
+    /\ \E t \in RunningThreads: \/ /\ t \in producers
                                     /\ Put(t, t) \* Add some data to buffer
-                                 \/ /\ t \in Consumers
+                                 \/ /\ t \in consumers
                                     /\ Get(t)
 
 -----------------------------------------------------------------------------
 
 (* TLA+ is untyped, thus lets verify the range of some values in each state. *)
 TypeInv == /\ buffer \in Seq(Producers)
-           /\ Len(buffer) \in 0..BufCapacity
-           /\ waitSet \subseteq (Producers \cup Consumers)
+           /\ Len(buffer) \in 0..bufCapacity
+           /\ waitSet \subseteq (producers \cup consumers)
 
 (* No Deadlock *)
-Invariant == waitSet # (Producers \cup Consumers)
+Invariant == waitSet # (producers \cup consumers)
 
 =============================================================================

README.md

@@ -12,6 +12,17 @@ Click either one of the buttons to launch a zero-install IDE to give the TLA+ sp
 This tutorial is work in progress. More chapters will be added in the future. In the meantime, feel free to open issues with questions, clarifications, and recommendations. You can also reach out to me on [twitter](https://twitter.com/lemmster).  Basic TLA+ learning material can be found over at [Lamport's TLA+ page](http://lamport.azurewebsites.net/tla/learning.html).
 
 --------------------------------------------------------------------------
+
+### v06 (continue): Convert constants into variables.
+
+In the section ["Limitations of Model-Checking"](http://www.cs.unh.edu/~charpov/programming-tlabuffer.html), Michel Charpentier points out that ```BlockingQueue``` is deadlock-free under some configurations, but that model checking is not helpful with finding the underlying mathematical function.  This observation is true in general because we cannot ask TLC to compute the set of all configurations for which ```BlockingQueue``` is deadlock-free, but at least we can ask it to find as many data points as possible. From those data points, we can try to infer/learn the function.
+
+In this step, we rewrite ```BlockingQueue``` to check multiple configurations instead of a single one (p1c2b1) at once. Note that the rewrite increases the complete state space to 57254 distinct states, but TLC continues to find the behavior shown in the previous step. This is because TLC - by default - explores the state space with [breadth-first search](https://en.wikipedia.org/wiki/Breadth-first_search). This [search mode](https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/tlc-options-page.html#checking) guarantees to always find the shortest counterexample (if TLC runs ```-workers N``` with N > 1, it only returns the shortest counterexample with high probability).
+
+We hope to [better support checking different constant values](https://github.com/tlaplus/tlaplus/issues/272) in the future.
+
+--------------------------------------------------------------------------
+
 ### v05: Add Invariant to detect deadlocks.
 
 Add Invariant to detect deadlocks (and TypeInv). TLC now finds the deadlock