Add Deli Queue Example

README.md

@@ -106,6 +106,7 @@ Here is a list of specs included in this repository which are validated by the C
 | [Buffered Random Access File](specifications/braf)                                                  | Calvin Loncaric                                     |          |             |         |     ✔     |          |
 | [Disruptor](specifications/Disruptor)                                                               | Nicholas Schultz-Møller                             |          |             |         |     ✔     |          |
 | [DAG-based Consensus](specifications/dag-consensus)                                                 | Giuliano Losa                                       |          |             |    ✔    |     ✔     |          |
+| [Deli](specifications/deli)                                                                          | Eric Spencer                                        |          |             |         |     ✔     |          |
 
 
 ## Other Examples

specifications/deli/README.md

@@ -0,0 +1,23 @@
+# Deli
+
+A TLA⁺ specification of a simple deli ordering system with a ticket-queue model.
+
+The spec models a single worker serving customers in queue order. Customers arrive, receive a ticket number, join an order queue, get assigned to the worker, receive service, and the system resets to serve the next customer. The system cycles through four states: Idle → TakingOrder → PreparingOrder → Serving → ReturnToIdle.
+
+## Key Features
+
+- **Ticket-based ordering**: Customers get monotonically increasing ticket numbers as they arrive
+- **Queue discipline**: Customers are served in FIFO order from the queue
+- **Worker assignment**: A dedicated worker is assigned in the PrepareOrder phase
+- **State machine with return cycle**: Unlike simpler queue models, the system explicitly returns to Idle, enabling liveness properties
+
+## Properties Checked
+
+The specification includes three safety invariants and one liveness property:
+
+1. **TypeOK**: State variables maintain correct types throughout execution
+2. **ValidStates**: The system never enters an undefined state
+3. **MutualExclusion**: At most one customer-worker pair is in the Serving state at any time
+4. **EventuallyIdle**: The system eventually returns to the Idle state (progress/fairness)
+
+The `.tla` file includes formal THEOREM declarations for each property, making the spec suitable for TLC model checking and serving as a test case for the TLC toolchain.

specifications/deli/deli.cfg

@@ -0,0 +1,10 @@
+SPECIFICATION Spec
+
+CONSTANT
+    Processes = {p1, p2, p3}
+    Null = null
+    MaxArrivals = 2
+
+INVARIANT TypeOK
+INVARIANT ValidStates
+INVARIANT MutualExclusion

specifications/deli/deli.tla

@@ -0,0 +1,98 @@
+-------------------------------- MODULE deli --------------------------------
+(***************************************************************************)
+(* A specification of a simple deli ordering system with a ticket queue.   *)
+(* Customers arrive, get assigned to a worker, their order is prepared,    *)
+(* and then served. The system cycles through Idle → TakingOrder →         *)
+(* PreparingOrder → Serving → ReturnToIdle to serve the next customer.     *)
+(***************************************************************************)
+
+EXTENDS Naturals, Sequences
+
+CONSTANTS Processes, Null, MaxArrivals
+
+VARIABLES ticket, worker, customer, state, orderQueue, arrivals
+
+(***************************************************************************)
+(* State variables:                                                        *)
+(*  - ticket: increasing counter issued to arriving customers              *)
+(*  - worker: the current worker serving an order, or Null if idle         *)
+(*  - customer: the current customer being served, or Null if idle         *)
+(*  - state: the system's current phase:                                   *)
+(*          (Idle | TakingOrder | PreparingOrder | Serving)                *)
+(*  - orderQueue: sequence of customers waiting to be served               *)
+(***************************************************************************)
+
+TypeOK == 
+    /\ ticket \in Nat
+    /\ worker \in Processes \cup {Null}
+    /\ customer \in Processes \cup {Null}
+    /\ state \in {"Idle", "TakingOrder", "PreparingOrder", "Serving"}
+    /\ orderQueue \in Seq(Processes)
+    /\ arrivals \in Nat
+
+Init ==
+    /\ ticket = 0
+    /\ worker = Null
+    /\ customer = Null
+    /\ state = "Idle"
+    /\ orderQueue = <<>>
+    /\ arrivals = 0
+
+(* Customer arrives, gets a ticket number, and joins the queue *)
+TakeOrder ==
+    /\ state = "Idle"
+    /\ arrivals < MaxArrivals
+    /\ \E c \in Processes :
+        /\ ticket' = ticket + 1
+        /\ arrivals' = arrivals + 1
+        /\ orderQueue' = Append(orderQueue, c)
+        /\ state' = "TakingOrder"
+        /\ UNCHANGED <<worker, customer>>
+
+(* The next customer from the queue is called and a worker is assigned *)
+PrepareOrder ==
+    /\ state = "TakingOrder"
+    /\ Len(orderQueue) > 0
+    /\ LET c == Head(orderQueue) IN
+        /\ \E w \in Processes :
+            /\ customer' = c
+            /\ worker' = w
+            /\ orderQueue' = Tail(orderQueue)
+            /\ state' = "PreparingOrder"
+        /\ UNCHANGED <<ticket, arrivals>>
+
+(* The assigned worker serves the current customer *)
+Serve ==
+    /\ state = "PreparingOrder"
+    /\ state' = "Serving"
+    /\ UNCHANGED <<ticket, worker, customer, orderQueue, arrivals>>
+
+(* Customer is served, worker and customer reset, ready for the next order *)
+ReturnToIdle ==
+    /\ state = "Serving"
+    /\ state' = "Idle"
+    /\ worker' = Null
+    /\ customer' = Null
+    /\ UNCHANGED <<ticket, orderQueue, arrivals>>
+
+Next ==
+    TakeOrder \/ PrepareOrder \/ Serve \/ ReturnToIdle
+
+(* Safety: System stays in one of the allowed states *)
+ValidStates ==
+    state \in {"Idle", "TakingOrder", "PreparingOrder", "Serving"}
+
+(* Safety: At most one customer is being served at any given time *)
+MutualExclusion ==
+    (state = "Idle") => (customer = Null /\ worker = Null)
+
+Spec ==
+    Init /\ [][Next]_<<ticket, worker, customer, state, orderQueue, arrivals>>
+
+(* Theorems *)
+THEOREM Spec => []TypeOK
+THEOREM Spec => []ValidStates  
+THEOREM Spec => []MutualExclusion
+
+=============================================================================
+

specifications/deli/manifest.json

@@ -0,0 +1,24 @@
+{
+  "sources": [],
+  "authors": [
+    "Eric Spencer"
+  ],
+  "tags": [],
+  "modules": [
+    {
+      "path": "specifications/deli/deli.tla",
+      "features": [],
+      "models": [
+        {
+          "path": "specifications/deli/deli.cfg",
+          "runtime": "00:00:01",
+          "mode": "exhaustive search",
+          "result": "success",
+          "distinctStates": 30,
+          "totalStates": 78,
+          "stateDepth": 1
+        }
+      ]
+    }
+  ]
+}