Skip to content

Commit 0625ec8

Browse files
EricSpencer00EricSpencer00
committed
Re-add parallelism to model
Refactor deli specification: enhance README, update model constraints, and improve state tracking
1 parent 6233004 commit 0625ec8

File tree

4 files changed

+166
-95
lines changed

4 files changed

+166
-95
lines changed

‎specifications/deli/README.md‎

Lines changed: 14 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,25 @@
11
# Deli
22

3-
A TLA⁺ specification of a simple deli ordering system with a bounded ticket-queue model.
3+
A TLA⁺ specification of a deli ordering system with ticket-based queuing and parallel service.
44

5-
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.
5+
Customers arrive at any time, take a ticket number, and join a FIFO queue. Multiple workers independently pick up the next waiting customer, prepare their order, serve them, and return to idle. Because each worker tracks its own state, several customers can be served concurrently when multiple workers are available.
66

77
## Design
88

9-
- **Bounded arrivals**: The `MaxArrivals` constant limits customer arrivals for tractable model checking
10-
- **Queue discipline**: Customers join the orderQueue in FIFO order
11-
- **Worker assignment**: Any available worker processes the next customer from the queue
12-
- **Cyclic state machine**: The system explicitly cycles back to Idle after each service, preventing deadlock
9+
- **No global state**: Instead of a single shop-wide phase variable, each worker has its own state (`Idle`, `Preparing`, `Serving`), enabling true parallelism
10+
- **Ticket-based customers**: Customers are identified by ticket numbers (1, 2, 3, …) rather than named processes, keeping the model simple and the `Arrive` action always enabled
11+
- **FIFO queue discipline**: Customers are served in arrival order; the `QueueOrdered` invariant verifies this
12+
- **State constraint for bounding**: The `arrivals` counter has no guard in the spec itself; a `CONSTRAINT arrivals <= 3` in the config file bounds exploration for model checking without polluting the specification
13+
- **No `CHECK_DEADLOCK FALSE`**: Because `Arrive` is always enabled (ungated), every reachable state has at least one successor, so deadlock checking works naturally
1314

1415
## Properties Verified
1516

16-
The specification includes three safety invariants, all verified by TLC:
17+
The specification includes five safety invariants, all verified by TLC:
1718

18-
1. **TypeOK**: All state variables maintain their declared types throughout execution
19-
2. **ValidStates**: The system's state variable remains one of the four allowed values
20-
3. **ConsistentIdle**: When in the Idle state, no customer or worker is assigned
19+
1. **TypeOK**: All state variables maintain their declared types
20+
2. **IdleConsistency**: A worker is idle if and only if it has no customer assignment
21+
3. **NoDoubleAssignment**: No two workers are ever assigned the same customer
22+
4. **TicketStatePartition**: Every issued ticket is in exactly one logical state—queued, assigned to a worker, or served—with no overlaps and no lost tickets
23+
5. **QueueOrdered**: Ticket numbers in the queue are strictly increasing (FIFO preserved)
2124

22-
With `MaxArrivals = 2` and `Processes = {p1, p2, p3}`, the model contains **45 distinct states** and completes exhaustive model checking in under 1 second.
25+
The spec also defines `FairSpec` with weak fairness on each worker's actions, suitable for verifying liveness properties (e.g., every arriving customer is eventually served).

‎specifications/deli/deli.cfg‎

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,14 @@
11
SPECIFICATION Spec
22

33
CONSTANT
4-
Processes = {p1, p2, p3}
5-
Null = null
6-
MaxArrivals = 2
4+
Workers = {w1, w2}
5+
MaxArrivals = 3
76

8-
INVARIANT TypeOK
9-
INVARIANT ValidStates
10-
INVARIANT ConsistentIdle
7+
CONSTRAINT
8+
StateConstraint
119

12-
CHECK_DEADLOCK FALSE
10+
INVARIANT TypeOK
11+
INVARIANT IdleConsistency
12+
INVARIANT NoDoubleAssignment
13+
INVARIANT TicketStatePartition
14+
INVARIANT QueueOrdered

‎specifications/deli/deli.tla‎

Lines changed: 140 additions & 74 deletions
Original file line numberDiff line numberDiff line change
@@ -1,98 +1,164 @@
11
-------------------------------- MODULE deli --------------------------------
22
(***************************************************************************)
3-
(* A specification of a simple deli ordering system with a ticket queue. *)
4-
(* Customers arrive, get assigned to a worker, their order is prepared, *)
5-
(* and then served. The system cycles through Idle → TakingOrder → *)
6-
(* PreparingOrder → Serving → ReturnToIdle to serve the next customer. *)
3+
(* A specification of a deli ordering system with ticket-based queuing *)
4+
(* and parallel service by multiple workers. *)
5+
(* *)
6+
(* Customers arrive at any time, take the next ticket number, and join a *)
7+
(* FIFO queue. Idle workers independently pick up the next waiting *)
8+
(* customer, prepare their order, serve them, and return to idle. *)
9+
(* Multiple workers operate concurrently, allowing several customers to *)
10+
(* be served in parallel. *)
711
(***************************************************************************)
812

9-
EXTENDS Naturals, Sequences
13+
EXTENDS Naturals, Sequences, FiniteSets
1014

11-
CONSTANTS Processes, Null, MaxArrivals
15+
CONSTANTS Workers, MaxArrivals
1216

13-
VARIABLES ticket, worker, customer, state, orderQueue, arrivals
17+
VARIABLES
18+
arrivals, \* Nat: count of customers who have arrived
19+
queue, \* Seq(Nat): FIFO queue of ticket numbers waiting
20+
workerState, \* [Workers -> {"Idle", "Preparing", "Serving"}]
21+
workerCustomer, \* [Workers -> Nat]: ticket number each worker handles (0 = none)
22+
served \* Set of ticket numbers already served
23+
24+
vars == <<arrivals, queue, workerState, workerCustomer, served>>
1425

1526
(***************************************************************************)
16-
(* State variables: *)
17-
(* - ticket: increasing counter issued to arriving customers *)
18-
(* - worker: the current worker serving an order, or Null if idle *)
19-
(* - customer: the current customer being served, or Null if idle *)
20-
(* - state: the system's current phase: *)
21-
(* (Idle | TakingOrder | PreparingOrder | Serving) *)
22-
(* - orderQueue: sequence of customers waiting to be served *)
27+
(* Helper: the set of elements in a sequence. *)
2328
(***************************************************************************)
29+
Range(s) == { s[i] : i \in DOMAIN s }
30+
31+
---------------------------------------------------------------------------
2432

25-
TypeOK ==
26-
/\ ticket \in Nat
27-
/\ worker \in Processes \cup {Null}
28-
/\ customer \in Processes \cup {Null}
29-
/\ state \in {"Idle", "TakingOrder", "PreparingOrder", "Serving"}
30-
/\ orderQueue \in Seq(Processes)
33+
(***************)
34+
(* Type check *)
35+
(***************)
36+
37+
TypeOK ==
3138
/\ arrivals \in Nat
39+
/\ queue \in Seq(1..arrivals)
40+
/\ workerState \in [Workers -> {"Idle", "Preparing", "Serving"}]
41+
/\ workerCustomer \in [Workers -> Nat]
42+
/\ served \subseteq 1..arrivals
43+
44+
---------------------------------------------------------------------------
45+
46+
(*****************)
47+
(* Initial state *)
48+
(*****************)
3249

3350
Init ==
34-
/\ ticket = 0
35-
/\ worker = Null
36-
/\ customer = Null
37-
/\ state = "Idle"
38-
/\ orderQueue = <<>>
3951
/\ arrivals = 0
40-
41-
(* Customer arrives, gets a ticket number, and joins the queue *)
42-
TakeOrder ==
43-
/\ state = "Idle"
44-
/\ arrivals < MaxArrivals
45-
/\ \E c \in Processes :
46-
/\ ticket' = ticket + 1
47-
/\ arrivals' = arrivals + 1
48-
/\ orderQueue' = Append(orderQueue, c)
49-
/\ state' = "TakingOrder"
50-
/\ UNCHANGED <<worker, customer>>
51-
52-
(* The next customer from the queue is called and a worker is assigned *)
53-
PrepareOrder ==
54-
/\ state = "TakingOrder"
55-
/\ Len(orderQueue) > 0
56-
/\ LET c == Head(orderQueue) IN
57-
/\ \E w \in Processes :
58-
/\ customer' = c
59-
/\ worker' = w
60-
/\ orderQueue' = Tail(orderQueue)
61-
/\ state' = "PreparingOrder"
62-
/\ UNCHANGED <<ticket, arrivals>>
63-
64-
(* The assigned worker serves the current customer *)
65-
Serve ==
66-
/\ state = "PreparingOrder"
67-
/\ state' = "Serving"
68-
/\ UNCHANGED <<ticket, worker, customer, orderQueue, arrivals>>
69-
70-
(* Customer is served, worker and customer reset, ready for the next order *)
71-
ReturnToIdle ==
72-
/\ state = "Serving"
73-
/\ state' = "Idle"
74-
/\ worker' = Null
75-
/\ customer' = Null
76-
/\ UNCHANGED <<ticket, orderQueue, arrivals>>
52+
/\ queue = <<>>
53+
/\ workerState = [w \in Workers |-> "Idle"]
54+
/\ workerCustomer = [w \in Workers |-> 0]
55+
/\ served = {}
56+
57+
---------------------------------------------------------------------------
58+
59+
(***********)
60+
(* Actions *)
61+
(***********)
62+
63+
(* A new customer arrives, takes the next ticket, and joins the queue. *)
64+
(* This action has no guard and is always enabled; the arrivals count *)
65+
(* is bounded only by the state constraint in the model config. *)
66+
Arrive ==
67+
/\ arrivals' = arrivals + 1
68+
/\ queue' = Append(queue, arrivals + 1)
69+
/\ UNCHANGED <<workerState, workerCustomer, served>>
70+
71+
(* An idle worker picks up the next customer from the head of the queue *)
72+
AssignWorker(w) ==
73+
/\ workerState[w] = "Idle"
74+
/\ queue /= <<>>
75+
/\ workerCustomer' = [workerCustomer EXCEPT ![w] = Head(queue)]
76+
/\ workerState' = [workerState EXCEPT ![w] = "Preparing"]
77+
/\ queue' = Tail(queue)
78+
/\ UNCHANGED <<arrivals, served>>
79+
80+
(* A worker finishes preparing and begins serving *)
81+
FinishPreparing(w) ==
82+
/\ workerState[w] = "Preparing"
83+
/\ workerState' = [workerState EXCEPT ![w] = "Serving"]
84+
/\ UNCHANGED <<arrivals, queue, workerCustomer, served>>
85+
86+
(* A worker completes service: customer is marked served, worker goes idle *)
87+
CompleteService(w) ==
88+
/\ workerState[w] = "Serving"
89+
/\ served' = served \cup {workerCustomer[w]}
90+
/\ workerState' = [workerState EXCEPT ![w] = "Idle"]
91+
/\ workerCustomer' = [workerCustomer EXCEPT ![w] = 0]
92+
/\ UNCHANGED <<arrivals, queue>>
93+
94+
---------------------------------------------------------------------------
95+
96+
(*****************)
97+
(* Specification *)
98+
(*****************)
7799

78100
Next ==
79-
TakeOrder \/ PrepareOrder \/ Serve \/ ReturnToIdle
101+
\/ Arrive
102+
\/ \E w \in Workers : AssignWorker(w) \/ FinishPreparing(w) \/ CompleteService(w)
103+
104+
Spec == Init /\ [][Next]_vars
105+
106+
---------------------------------------------------------------------------
107+
108+
(************)
109+
(* Fairness *)
110+
(************)
111+
112+
(* Under weak fairness on each worker's actions, every queued customer *)
113+
(* is eventually served. Without fairness, workers could idle forever. *)
114+
FairSpec == Spec /\ \A w \in Workers :
115+
/\ WF_vars(AssignWorker(w))
116+
/\ WF_vars(FinishPreparing(w))
117+
/\ WF_vars(CompleteService(w))
118+
119+
---------------------------------------------------------------------------
120+
121+
(**************)
122+
(* Invariants *)
123+
(**************)
124+
125+
(* An idle worker has no customer; a busy worker always has one *)
126+
IdleConsistency ==
127+
\A w \in Workers : workerState[w] = "Idle" <=> workerCustomer[w] = 0
128+
129+
(* No two workers handle the same customer simultaneously *)
130+
NoDoubleAssignment ==
131+
\A w1, w2 \in Workers :
132+
w1 /= w2 /\ workerCustomer[w1] /= 0
133+
=> workerCustomer[w1] /= workerCustomer[w2]
134+
135+
(* Every issued ticket is in exactly one logical state: *)
136+
(* queued (waiting), assigned (being prepared or served), or served. *)
137+
TicketStatePartition ==
138+
LET assigned == { workerCustomer[w] : w \in { x \in Workers : workerCustomer[x] /= 0 } }
139+
queued == Range(queue)
140+
issued == 1..arrivals
141+
IN /\ queued \cup assigned \cup served = issued
142+
/\ queued \cap assigned = {}
143+
/\ queued \cap served = {}
144+
/\ assigned \cap served = {}
145+
146+
(* The queue preserves FIFO order: earlier tickets always appear first *)
147+
QueueOrdered ==
148+
\A i, j \in DOMAIN queue : i < j => queue[i] < queue[j]
80149

81-
(* Safety: System stays in one of the allowed states *)
82-
ValidStates ==
83-
state \in {"Idle", "TakingOrder", "PreparingOrder", "Serving"}
150+
---------------------------------------------------------------------------
84151

85-
(* Safety: No customer is assigned when the system is Idle *)
86-
ConsistentIdle ==
87-
(state = "Idle") => (customer = Null /\ worker = Null)
152+
(* State constraint for bounding model checking; not part of the spec. *)
153+
StateConstraint == arrivals <= MaxArrivals
88154

89-
Spec ==
90-
Init /\ [][Next]_<<ticket, worker, customer, state, orderQueue, arrivals>>
155+
---------------------------------------------------------------------------
91156

92-
(* Theorems *)
93157
THEOREM Spec => []TypeOK
94-
THEOREM Spec => []ValidStates
95-
THEOREM Spec => []ConsistentIdle
158+
THEOREM Spec => []IdleConsistency
159+
THEOREM Spec => []NoDoubleAssignment
160+
THEOREM Spec => []TicketStatePartition
161+
THEOREM Spec => []QueueOrdered
96162

97163
=============================================================================
98164

‎specifications/deli/manifest.json‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,9 +14,9 @@
1414
"runtime": "00:00:01",
1515
"mode": "exhaustive search",
1616
"result": "success",
17-
"distinctStates": 45,
18-
"totalStates": 61,
19-
"stateDepth": 1
17+
"distinctStates": 82,
18+
"totalStates": 215,
19+
"stateDepth": 13
2020
}
2121
]
2222
}

0 commit comments

Comments
 (0)