pingpong: incorporated NumberOfPings limit inside the model

eras · Nov 6, 2022 · ab21fbe · ab21fbe
1 parent 1f4a14b
commit ab21fbe
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/examples/pingpong.tla b/examples/pingpong.tla
@@ -44,6 +44,7 @@ ClientToServerChannel(Id) == INSTANCE MChannel WITH channels <- client_to_server
 
 (* Server sends ping to a client *)
 ServerSendPing ==
+   /\ num_pings_sent < NumberOfPings
    /\ \E client_id \in ClientIds:
       ServerToClientChannel(client_id)!Send([message |-> "ping"])
    /\ num_pings_sent' = num_pings_sent + 1
@@ -62,11 +63,14 @@ ClientHandlePing(client_id) ==
    /\ ClientToServerChannel(client_id)!Send([message |-> "pong"])
    /\ UNCHANGED<<num_pings_sent, num_pongs_received>>
 
+Stutter == UNCHANGED<<vars>>
+
 Next ==
    \/ ServerSendPing
    \/ ServerHandlePong
    \/ \E client_id \in ClientIds:
       ClientHandlePing(client_id)
+   \/ Stutter
 
 Init ==
    /\ server_to_client = [client_id \in ClientIds |-> ServerToClientChannel(client_id)!InitValue]