v02 (FSM): State graph for minimum configuration.

.github/workflows/main.yml

@@ -0,0 +1,16 @@
+name: CI
+
+on: [push]
+
+jobs:
+  build:
+
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: actions/checkout@v1
+    - name: Get (nightly) TLC
+      run: wget https://nightly.tlapl.us/dist/tla2tools.jar
+    - name: Run TLC
+      run: java -Dtlc2.TLC.stopAfter=1800 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=1efd5c60f238424fa70d124d0c77bbf1 -cp tla2tools.jar tlc2.TLC -workers auto -lncheck final -checkpoint 60 -coverage 60 -tool -deadlock BlockingQueue
+

BlockingQueue.cfg

@@ -0,0 +1,8 @@
+\* SPECIFICATION
+CONSTANTS
+    BufCapacity = 1
+    Producers = {p1}
+    Consumers = {c1}
+
+INIT Init
+NEXT Next

BlockingQueue.tla

@@ -0,0 +1,62 @@
+--------------------------- MODULE BlockingQueue ---------------------------
+(***************************************************************************)
+(* Original problem and spec by Michel Charpentier                         *)
+(* http://www.cs.unh.edu/~charpov/programming-tlabuffer.html               *)
+(***************************************************************************)
+EXTENDS Naturals, Sequences, FiniteSets
+
+CONSTANTS Producers,   (* the (nonempty) set of producers                       *)
+          Consumers,   (* the (nonempty) set of consumers                       *)
+          BufCapacity  (* the maximum number of messages in the bounded buffer  *)
+
+ASSUME Assumption ==
+       /\ Producers # {}                      (* at least one producer *)
+       /\ Consumers # {}                      (* at least one consumer *)
+       /\ Producers \intersect Consumers = {} (* no thread is both consumer and producer *)
+       /\ BufCapacity \in (Nat \ {0})         (* buffer capacity is at least 1 *)
+
+-----------------------------------------------------------------------------
+
+VARIABLES buffer, waitSet
+vars == <<buffer, waitSet>>
+
+RunningThreads == (Producers \cup Consumers) \ waitSet
+
+(* @see java.lang.Object#notify *)       
+Notify == IF waitSet # {}
+          THEN \E x \in waitSet: waitSet' = waitSet \ {x}
+          ELSE UNCHANGED waitSet
+
+(* @see java.lang.Object#wait *)
+Wait(t) == /\ waitSet' = waitSet \cup {t}
+           /\ UNCHANGED <<buffer>>
+
+-----------------------------------------------------------------------------
+
+Put(t, d) ==
+   \/ /\ Len(buffer) < BufCapacity
+      /\ buffer' = Append(buffer, d)
+      /\ Notify
+   \/ /\ Len(buffer) = BufCapacity
+      /\ Wait(t)
+
+Get(t) ==
+   \/ /\ buffer # <<>>
+      /\ buffer' = Tail(buffer)
+      /\ Notify
+   \/ /\ buffer = <<>>
+      /\ Wait(t)
+
+-----------------------------------------------------------------------------
+
+(* Initially, the buffer is empty and no thread is waiting. *)
+Init == /\ buffer = <<>>
+        /\ waitSet = {}
+
+(* Then, pick a thread out of all running threads and have it do its thing. *)
+Next == \E t \in RunningThreads: \/ /\ t \in Producers
+                                    /\ Put(t, t) \* Add some data to buffer
+                                 \/ /\ t \in Consumers
+                                    /\ Get(t)
+
+=============================================================================

README.md

@@ -13,6 +13,17 @@ This tutorial is work in progress. More chapters will be added in the future. In
 
 --------------------------------------------------------------------------
 
+### v02: State graph for minimum configuration p1c1b1.
+
+Initial TLA+ spec that models the existing (Java) code with all its
+bugs and shortcomings.
+
+The model uses the minimal parameters (1 producer, 1 consumer, and
+a buffer of size one) possible.  When TLC generates the state graph with
+```java -jar tla2tools.jar -deadlock -dump dot p1c1b1.dot BlockingQueue```,
+we can visually verify that no deadlock is possible with this
+configuration: ![p1c1b1](./p1c1b1.svg).
+
 ### v01: Java and C implementations with configuration p4c3b3.
 
 Legacy Java code with all its bugs and shortcomings.  At this point

p1c1b1.dot

@@ -0,0 +1,19 @@
+strict digraph DiskGraph {
+nodesep=0.35;
+subgraph cluster_graph {
+color="white";
+1361886694690155653 [label="/\\ buffer = <<>>\n/\\ waitSet = {}",style = filled]
+1361886694690155653 -> 8427788535082373079 [label="",color="black",fontcolor="black"];
+8427788535082373079 [label="/\\ buffer = <<p1>>\n/\\ waitSet = {}"];
+1361886694690155653 -> -7172793711072072991 [label="",color="black",fontcolor="black"];
+-7172793711072072991 [label="/\\ buffer = <<>>\n/\\ waitSet = {c1}"];
+8427788535082373079 -> -6634559038400111083 [label="",color="black",fontcolor="black"];
+-6634559038400111083 [label="/\\ buffer = <<p1>>\n/\\ waitSet = {p1}"];
+8427788535082373079 -> 1361886694690155653 [label="",color="black",fontcolor="black"];
+-7172793711072072991 -> 8427788535082373079 [label="",color="black",fontcolor="black"];
+-6634559038400111083 -> 1361886694690155653 [label="",color="black",fontcolor="black"];
+{rank = same; 1361886694690155653;}
+{rank = same; 8427788535082373079;-7172793711072072991;}
+{rank = same; -6634559038400111083;}
+}
+}