-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathpingpong.tla
114 lines (89 loc) · 3.93 KB
/
pingpong.tla
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
---- MODULE pingpong -----------------------------------------------------------
(* pingpong is a model where there exists one server and multiple
clients. The server my send the clients a "ping" message, which
they will always respond with a "pong" message.
Once NumberOfPings pings have been sent and the same number of
pongs have been received by the server, is the INVARIANT
NotFinished violated and a state trace is produced. The state trace
is transformed from the actual system state via the ALIAS
AliasMessage, which only shows the messages in a format expected by
the tool.
Copyright 2022 Erkki Seppälä <[email protected]>
*)
--------------------------------------------------------------------------------
LOCAL INSTANCE Naturals (* .. *)
LOCAL INSTANCE Json (* ToJson *)
CONSTANT
NumberOfClients
(* Number of pings the server sends and receives before we consider the
scenario Finished *)
, NumberOfPings
VARIABLES
server_to_client (* channels from the server to the clients *)
, client_to_server (* channels from the clients to the server *)
, num_pings_sent (* number of pings sent by the server *)
, num_pongs_received (* number of pongs received by the server *)
ClientIds == 1..NumberOfClients
vars == <<server_to_client, client_to_server, num_pings_sent, num_pongs_received>>
Data == [message: {"ping"}] \cup [message: {"pong"}]
(* Channels for messages from the server to the clients *)
ServerToClientChannel(Id) == INSTANCE MChannel WITH channels <- server_to_client
(* Channels for messages from the clients to the server *)
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
/\ UNCHANGED<<client_to_server, num_pongs_received>>
(* Server receives a ping from a client *)
ServerHandlePong ==
/\ \E client_id \in ClientIds:
/\ ClientToServerChannel(client_id)!Recv([message |-> "pong"])
/\ num_pongs_received' = num_pongs_received + 1
/\ UNCHANGED<<server_to_client, num_pings_sent>>
(* Handle pings one client at a time: upon receiving ping, respond with pong *)
ClientHandlePing(client_id) ==
/\ ServerToClientChannel(client_id)!Recv([message |-> "ping"])
/\ 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]
/\ client_to_server = [client_id \in ClientIds |-> ClientToServerChannel(client_id)!InitValue]
/\ num_pings_sent = 0
/\ num_pongs_received = 0
Spec ==
/\ Init
/\ [][Next]_vars
TypeOK ==
/\ num_pings_sent \in Nat
/\ num_pongs_received \in Nat
/\ \A client_id \in ClientIds:
/\ ServerToClientChannel(client_id)!TypeOK
/\ ClientToServerChannel(client_id)!TypeOK
Finished ==
/\ num_pings_sent = num_pongs_received
/\ num_pings_sent = NumberOfPings
NotFinished == \lnot Finished
AllMessages ==
UNION({UNION({
{{<<"server", 1>>} \X {<<"client", client_id>>} \X ServerToClientChannel(client_id)!Sending}
, {{<<"client", client_id>>} \X {<<"server", 1>>} \X ClientToServerChannel(client_id)!Sending}
}) : client_id \in ClientIds})
State ==
[server |-> <<[pings |-> num_pings_sent,
pongs |-> num_pongs_received]>>]
AliasMessages ==
[lane_order_json |-> ToJson(<<"client", "server">>),
messages_json |-> ToJson(AllMessages),
state_json |-> ToJson(State)
]
================================================================================