Skip to content

Commit 2564308

Browse files
EricSpencer00EricSpencer00
committed
Revert to simple, bounded deli specification for tractable model checking
Signed-off-by: EricSpencer00 <espencer2@luc.edu>
1 parent dad6d5b commit 2564308

2 files changed

Lines changed: 66 additions & 59 deletions

File tree

‎specifications/deli/deli.cfg‎

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

33
CONSTANT
4-
Workers = {w1, w2}
5-
Customers = {c1, c2, c3}
4+
Processes = {p1, p2, p3}
65
Null = null
76

87
INVARIANT TypeOK
9-
INVARIANT Consistency
10-
11-
PROPERTY EventuallyServed
8+
INVARIANT ValidStates
9+
INVARIANT MutualExclusion

‎specifications/deli/deli.tla‎

Lines changed: 63 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -1,85 +1,94 @@
11
-------------------------------- MODULE deli --------------------------------
22
(***************************************************************************)
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. *)
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. *)
87
(***************************************************************************)
98

109
EXTENDS Naturals, Sequences
1110

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

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

1815
(***************************************************************************)
1916
(* 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) *)
2022
(* - 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 *)
2523
(***************************************************************************)
2624

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

3432
Init ==
33+
/\ ticket = 0
34+
/\ worker = Null
35+
/\ customer = Null
36+
/\ state = "Idle"
3537
/\ 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>>
4338

44-
(* Any idle worker picks up the next waiting customer *)
45-
AssignOrder(w) ==
46-
/\ workerState[w] = "Idle"
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"
4751
/\ Len(orderQueue) > 0
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
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>>
5873

5974
Next ==
60-
(\E c \in Customers : Arrive(c))
61-
\/ (\E w \in Workers : AssignOrder(w))
62-
\/ (\E w \in Workers : CompleteOrder(w))
63-
64-
(* Safety: Worker state is consistent with workerCustomer assignment *)
65-
Consistency ==
66-
\A w \in Workers : (workerState[w] = "Idle") => (workerCustomer[w] = Null)
75+
TakeOrder \/ PrepareOrder \/ Serve \/ ReturnToIdle
6776

68-
(* Liveness: Every customer in the queue is eventually served *)
69-
EventuallyServed ==
70-
\A i \in DOMAIN orderQueue :
71-
LET c == orderQueue[i] IN
72-
<> (\E w \in Workers : workerCustomer[w] = c)
77+
(* Safety: System stays in one of the allowed states *)
78+
ValidStates ==
79+
state \in {"Idle", "TakingOrder", "PreparingOrder", "Serving"}
7380

74-
Fairness ==
75-
\A w \in Workers : WF_vars(AssignOrder(w)) /\ WF_vars(CompleteOrder(w))
81+
(* Safety: At most one customer is being served at any given time *)
82+
MutualExclusion ==
83+
(state = "Idle") => (customer = Null /\ worker = Null)
7684

7785
Spec ==
78-
Init /\ [][Next]_vars /\ Fairness
86+
Init /\ [][Next]_<<ticket, worker, customer, state, orderQueue>>
7987

8088
(* Theorems *)
8189
THEOREM Spec => []TypeOK
82-
THEOREM Spec => []Consistency
90+
THEOREM Spec => []ValidStates
91+
THEOREM Spec => []MutualExclusion
8392

8493
=============================================================================
8594

0 commit comments

Comments
 (0)