Address code review: fix property naming and documentation

- Rename MutualExclusion to ConsistentIdle to accurately describe what is checked (Idle state consistency, not Serving state mutual exclusion)
- Update README to clarify state machine: four states with explicit ReturnToIdle transition
- Remove misleading ticket-based ordering from documentation
- Add CHECK_DEADLOCK FALSE to config since deadlock is expected at MaxArrivals boundary
- Update manifest with verified state metrics (45 distinct, 61 total states)

Signed-off-by: EricSpencer00 <espencer2@luc.edu>

Author: EricSpencer00

specifications/deli/README.md

@@ -2,21 +2,21 @@
 
 A TLA⁺ specification of a simple deli ordering system with a bounded ticket-queue model.
 
-The spec models customers arriving and being served sequentially. Customers arrive (bounded by `MaxArrivals`), receive a ticket number, join an order queue, get assigned to a worker, receive service, and the system resets to serve the next customer. The system cycles through states: Idle → TakingOrder → PreparingOrder → Serving → ReturnToIdle.
+The spec models customers arriving and being served sequentially. Customers arrive (bounded by `MaxArrivals`), receive a ticket number, join an order queue, get assigned to a worker, receive service, and the system resets to serve the next customer. The system progresses through four states: Idle, TakingOrder, PreparingOrder, and Serving; transitions include ReturnToIdle which moves from Serving back to Idle.
 
 ## Design
 
-- **Ticket-based ordering**: Customers get monotonically increasing ticket numbers as they arrive
-- **Queue discipline**: Customers are served in FIFO order from the queue
 - **Bounded arrivals**: The `MaxArrivals` constant limits customer arrivals for tractable model checking
-- **State machine with return cycle**: The system explicitly cycles back to Idle after each service, preventing deadlock and allowing new orders
+- **Queue discipline**: Customers join the orderQueue in FIFO order
+- **Worker assignment**: Any available worker processes the next customer from the queue
+- **Cyclic state machine**: The system explicitly cycles back to Idle after each service, preventing deadlock
 
 ## Properties Verified
 
 The specification includes three safety invariants, all verified by TLC:
 
-1. **TypeOK**: State variables maintain correct types throughout execution
-2. **ValidStates**: The system never enters an undefined state
-3. **MutualExclusion**: At most one customer is being served at any time; idle workers cannot be assigned
+1. **TypeOK**: All state variables maintain their declared types throughout execution
+2. **ValidStates**: The system's state variable remains one of the four allowed values
+3. **ConsistentIdle**: When in the Idle state, no customer or worker is assigned
 
-The `.tla` file includes formal THEOREM declarations for each property. With `MaxArrivals = 2` and `Processes = {p1, p2, p3}`, the model contains **30 distinct states** and completes exhaustive model checking in under 1 second.
+With `MaxArrivals = 2` and `Processes = {p1, p2, p3}`, the model contains **45 distinct states** and completes exhaustive model checking in under 1 second.

specifications/deli/deli.cfg

@@ -7,4 +7,6 @@ CONSTANT
 
 INVARIANT TypeOK
 INVARIANT ValidStates
-INVARIANT MutualExclusion
+INVARIANT ConsistentIdle
+
+CHECK_DEADLOCK FALSE

specifications/deli/deli.tla

@@ -82,8 +82,8 @@ Next ==
 ValidStates ==
     state \in {"Idle", "TakingOrder", "PreparingOrder", "Serving"}
 
-(* Safety: At most one customer is being served at any given time *)
-MutualExclusion ==
+(* Safety: No customer is assigned when the system is Idle *)
+ConsistentIdle ==
     (state = "Idle") => (customer = Null /\ worker = Null)
 
 Spec ==
@@ -92,7 +92,7 @@ Spec ==
 (* Theorems *)
 THEOREM Spec => []TypeOK
 THEOREM Spec => []ValidStates  
-THEOREM Spec => []MutualExclusion
+THEOREM Spec => []ConsistentIdle
 
 =============================================================================
 

specifications/deli/manifest.json

@@ -14,8 +14,8 @@
           "runtime": "00:00:01",
           "mode": "exhaustive search",
           "result": "success",
-          "distinctStates": 30,
-          "totalStates": 78,
+          "distinctStates": 45,
+          "totalStates": 61,
           "stateDepth": 1
         }
       ]