Skip to content

Commit a7971fd

Browse files
EricSpencer00EricSpencer00
committed
complete refactor to include separate processes for workers and customers
Signed-off-by: EricSpencer00 <espencer2@luc.edu>
1 parent 53f3daa commit a7971fd

1 file changed

Lines changed: 51 additions & 67 deletions

File tree

‎specifications/deli/deli.tla‎

Lines changed: 51 additions & 67 deletions
Original file line numberDiff line numberDiff line change
@@ -1,99 +1,83 @@
11
-------------------------------- MODULE deli --------------------------------
22
(***************************************************************************)
3-
(* A specification of a deli ordering system with a ticket-queue model. *)
4-
(* Customers arrive (TakeOrder), get assigned to a worker who prepares *)
5-
(* their order (PrepareOrder), then the order is served (Serve), and the *)
6-
(* system returns to Idle (ReturnToIdle) to process the next customer. *)
3+
(* A specification of a deli ordering system with concurrent workers. *)
4+
(* Customers arrive (Arrive) and join a queue. Idle workers asynchronously *)
5+
(* pick up waiting customers (AssignOrder), then complete their order *)
6+
(* (CompleteOrder) and return to Idle. Multiple workers process orders *)
7+
(* in parallel, and customers can arrive unboundedly. *)
78
(***************************************************************************)
89

910
EXTENDS Naturals, Sequences
1011

11-
CONSTANTS Processes, Null
12+
CONSTANTS Workers, Customers, Null
1213

13-
VARIABLES ticket, worker, customer, state, orderQueue
14+
VARIABLES orderQueue, \* Seq(Customers) — grows at any time
15+
workerState, \* [Workers -> {"Idle","Preparing"}]
16+
workerCustomer \* [Workers -> Customers ∪ {Null}]
1417

1518
(***************************************************************************)
1619
(* 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) *)
2220
(* - orderQueue: sequence of customers waiting to be served *)
21+
(* - workerState: mapping from workers to their current state *)
22+
(* (Idle or Preparing) *)
23+
(* - workerCustomer: mapping from workers to the customer they're *)
24+
(* serving, or Null if idle *)
2325
(***************************************************************************)
2426

27+
vars == <<orderQueue, workerState, workerCustomer>>
28+
2529
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)
30+
/\ orderQueue \in Seq(Customers)
31+
/\ workerState \in [Workers -> {"Idle", "Preparing"}]
32+
/\ workerCustomer \in [Workers -> Customers \cup {Null}]
3133

3234
Init ==
33-
/\ ticket = 0
34-
/\ worker = Null
35-
/\ customer = Null
36-
/\ state = "Idle"
3735
/\ orderQueue = <<>>
36+
/\ workerState = [w \in Workers |-> "Idle"]
37+
/\ workerCustomer = [w \in Workers |-> Null]
38+
39+
(* Customer arrives at any time — no guard on global state *)
40+
Arrive(c) ==
41+
/\ orderQueue' = Append(orderQueue, c)
42+
/\ UNCHANGED <<workerState, workerCustomer>>
3843

39-
(* Customer arrives, gets a ticket number, and joins the queue *)
40-
TakeOrder ==
41-
/\ state = "Idle"
42-
/\ \E c \in Processes :
43-
/\ ticket' = ticket + 1
44-
/\ orderQueue' = Append(orderQueue, c)
45-
/\ state' = "TakingOrder"
46-
/\ UNCHANGED <<worker, customer>>
47-
48-
(* The next customer from the queue is called and a worker is assigned *)
49-
PrepareOrder ==
50-
/\ state = "TakingOrder"
44+
(* Any idle worker picks up the next waiting customer *)
45+
AssignOrder(w) ==
46+
/\ workerState[w] = "Idle"
5147
/\ Len(orderQueue) > 0
52-
/\ LET c == Head(orderQueue) IN
53-
/\ \E w \in Processes :
54-
/\ customer' = c
55-
/\ worker' = w
56-
/\ orderQueue' = Tail(orderQueue)
57-
/\ state' = "PreparingOrder"
58-
/\ UNCHANGED ticket
59-
60-
(* The assigned worker serves the current customer *)
61-
Serve ==
62-
/\ state = "PreparingOrder"
63-
/\ state' = "Serving"
64-
/\ UNCHANGED <<ticket, worker, customer, orderQueue>>
65-
66-
(* Customer is served, worker and customer reset, ready for the next order *)
67-
ReturnToIdle ==
68-
/\ state = "Serving"
69-
/\ state' = "Idle"
70-
/\ worker' = Null
71-
/\ customer' = Null
72-
/\ UNCHANGED <<ticket, orderQueue>>
48+
/\ workerCustomer' = [workerCustomer EXCEPT ![w] = Head(orderQueue)]
49+
/\ orderQueue' = Tail(orderQueue)
50+
/\ workerState' = [workerState EXCEPT ![w] = "Preparing"]
51+
52+
(* Worker finishes serving and becomes idle again *)
53+
CompleteOrder(w) ==
54+
/\ workerState[w] = "Preparing"
55+
/\ workerState' = [workerState EXCEPT ![w] = "Idle"]
56+
/\ workerCustomer' = [workerCustomer EXCEPT ![w] = Null]
57+
/\ UNCHANGED orderQueue
7358

7459
Next ==
75-
TakeOrder \/ PrepareOrder \/ Serve \/ ReturnToIdle
60+
(\E c \in Customers : Arrive(c))
61+
\/ (\E w \in Workers : AssignOrder(w))
62+
\/ (\E w \in Workers : CompleteOrder(w))
7663

77-
(* Safety: System stays in one of the allowed states *)
78-
ValidStates ==
79-
state \in {"Idle", "TakingOrder", "PreparingOrder", "Serving"}
64+
(* Safety: Worker state is consistent with workerCustomer assignment *)
65+
Consistency ==
66+
\A w \in Workers : (workerState[w] = "Idle") => (workerCustomer[w] = Null)
8067

81-
(* Safety: At most one customer is being served at any given time *)
82-
MutualExclusion ==
83-
(state = "Idle") => (customer = Null /\ worker = Null)
68+
(* Liveness: Every customer who arrives is eventually served by some worker *)
69+
EventuallyServed ==
70+
\A c \in Customers : (c \in Range(orderQueue)) ~> (\E w \in Workers : workerCustomer[w] = c)
8471

85-
(* Liveness: The system eventually returns to Idle (progress) *)
86-
EventuallyIdle ==
87-
<> (state = "Idle")
72+
Fairness ==
73+
\A w \in Workers : WF_vars(AssignOrder(w)) /\ WF_vars(CompleteOrder(w))
8874

8975
Spec ==
90-
Init /\ [][Next]_<<ticket, worker, customer, state, orderQueue>>
76+
Init /\ [][Next]_vars /\ Fairness
9177

9278
(* Theorems *)
9379
THEOREM Spec => []TypeOK
94-
THEOREM Spec => []ValidStates
95-
THEOREM Spec => []MutualExclusion
96-
THEOREM Spec => EventuallyIdle
80+
THEOREM Spec => []Consistency
9781

9882
=============================================================================
9983

0 commit comments

Comments
 (0)