Add MaxArrivals constant to bound state space for tractable model checking

Author: EricSpencer00

specifications/deli/deli.cfg

@@ -3,6 +3,7 @@ SPECIFICATION Spec
 CONSTANT
     Processes = {p1, p2, p3}
     Null = null
+    MaxArrivals = 2
 
 INVARIANT TypeOK
 INVARIANT ValidStates

specifications/deli/deli.tla

@@ -8,9 +8,9 @@
 
 EXTENDS Naturals, Sequences
 
-CONSTANTS Processes, Null
+CONSTANTS Processes, Null, MaxArrivals
 
-VARIABLES ticket, worker, customer, state, orderQueue
+VARIABLES ticket, worker, customer, state, orderQueue, arrivals
 
 (***************************************************************************)
 (* State variables:                                                        *)
@@ -28,19 +28,23 @@ TypeOK ==
     /\ 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>>
@@ -55,21 +59,21 @@ PrepareOrder ==
             /\ worker' = w
             /\ orderQueue' = Tail(orderQueue)
             /\ state' = "PreparingOrder"
-        /\ UNCHANGED ticket
+        /\ UNCHANGED <<ticket, arrivals>>
 
 (* The assigned worker serves the current customer *)
 Serve ==
     /\ state = "PreparingOrder"
     /\ state' = "Serving"
-    /\ UNCHANGED <<ticket, worker, customer, orderQueue>>
+    /\ 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>>
+    /\ UNCHANGED <<ticket, orderQueue, arrivals>>
 
 Next ==
     TakeOrder \/ PrepareOrder \/ Serve \/ ReturnToIdle
@@ -83,7 +87,7 @@ MutualExclusion ==
     (state = "Idle") => (customer = Null /\ worker = Null)
 
 Spec ==
-    Init /\ [][Next]_<<ticket, worker, customer, state, orderQueue>>
+    Init /\ [][Next]_<<ticket, worker, customer, state, orderQueue, arrivals>>
 
 (* Theorems *)
 THEOREM Spec => []TypeOK