Skip to content

Commit 63f0ffe

Browse files
fhackettfhackett
committed
update dqueue TLA+ after years, oops
1 parent 874d087 commit 63f0ffe

File tree

1 file changed

+32
-73
lines changed

1 file changed

+32
-73
lines changed

‎systems/dqueue/dqueue.tla

+32-73
Original file line numberDiff line numberDiff line change
@@ -143,36 +143,21 @@ CONSTANTS BUFFER_SIZE, NUM_CONSUMERS, PRODUCER
143143

144144
\* BEGIN TRANSLATION PCal-e64ab9284c1a4c5172f564abb6f099c4
145145
CONSTANT defaultInitValue
146-
VARIABLES network, processor, stream, netWrite, netRead, procWrite, netWrite0,
147-
procWrite0, netRead0, netWrite1, sRead, sWrite, netWrite2, sWrite0,
148-
pc
146+
VARIABLES network, processor, stream, pc
149147

150148
(* define statement *)
151149
NUM_NODES == (NUM_CONSUMERS) + (1)
152150

153151
VARIABLE requester
154152

155-
vars == << network, processor, stream, netWrite, netRead, procWrite,
156-
netWrite0, procWrite0, netRead0, netWrite1, sRead, sWrite,
157-
netWrite2, sWrite0, pc, requester >>
153+
vars == << network, processor, stream, pc, requester >>
158154

159155
ProcSet == ((1) .. (NUM_CONSUMERS)) \cup ({PRODUCER})
160156

161157
Init == (* Global variables *)
162158
/\ network = [id \in (0) .. ((NUM_NODES) - (1)) |-> <<>>]
163159
/\ processor = 0
164160
/\ stream = 0
165-
/\ netWrite = defaultInitValue
166-
/\ netRead = defaultInitValue
167-
/\ procWrite = defaultInitValue
168-
/\ netWrite0 = defaultInitValue
169-
/\ procWrite0 = defaultInitValue
170-
/\ netRead0 = defaultInitValue
171-
/\ netWrite1 = defaultInitValue
172-
/\ sRead = defaultInitValue
173-
/\ sWrite = defaultInitValue
174-
/\ netWrite2 = defaultInitValue
175-
/\ sWrite0 = defaultInitValue
176161
(* Process Producer *)
177162
/\ requester = [self \in {PRODUCER} |-> defaultInitValue]
178163
/\ pc = [self \in ProcSet |-> CASE self \in (1) .. (NUM_CONSUMERS) -> "c"
@@ -181,76 +166,50 @@ Init == (* Global variables *)
181166
c(self) == /\ pc[self] = "c"
182167
/\ IF TRUE
183168
THEN /\ pc' = [pc EXCEPT ![self] = "c1"]
184-
/\ UNCHANGED << network, processor, netWrite0,
185-
procWrite0 >>
186-
ELSE /\ netWrite0' = network
187-
/\ procWrite0' = processor
188-
/\ network' = netWrite0'
189-
/\ processor' = procWrite0'
190-
/\ pc' = [pc EXCEPT ![self] = "Done"]
191-
/\ UNCHANGED << stream, netWrite, netRead, procWrite, netRead0,
192-
netWrite1, sRead, sWrite, netWrite2, sWrite0,
193-
requester >>
169+
ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
170+
/\ UNCHANGED << network, processor, stream, requester >>
194171

195172
c1(self) == /\ pc[self] = "c1"
196-
/\ (Len(network[PRODUCER])) < (BUFFER_SIZE)
197-
/\ netWrite' = [network EXCEPT ![PRODUCER] = Append(network[PRODUCER], self)]
198-
/\ network' = netWrite'
199-
/\ pc' = [pc EXCEPT ![self] = "c2"]
200-
/\ UNCHANGED << processor, stream, netRead, procWrite, netWrite0,
201-
procWrite0, netRead0, netWrite1, sRead, sWrite,
202-
netWrite2, sWrite0, requester >>
173+
/\ LET value1 == self IN
174+
/\ (Len((network)[PRODUCER])) < (BUFFER_SIZE)
175+
/\ network' = [network EXCEPT ![PRODUCER] = Append((network)[PRODUCER], value1)]
176+
/\ pc' = [pc EXCEPT ![self] = "c2"]
177+
/\ UNCHANGED << processor, stream, requester >>
203178

204179
c2(self) == /\ pc[self] = "c2"
205-
/\ (Len(network[self])) > (0)
206-
/\ LET msg0 == Head(network[self]) IN
207-
/\ netWrite' = [network EXCEPT ![self] = Tail(network[self])]
208-
/\ netRead' = msg0
209-
/\ procWrite' = netRead'
210-
/\ network' = netWrite'
211-
/\ processor' = procWrite'
212-
/\ pc' = [pc EXCEPT ![self] = "c"]
213-
/\ UNCHANGED << stream, netWrite0, procWrite0, netRead0, netWrite1,
214-
sRead, sWrite, netWrite2, sWrite0, requester >>
180+
/\ (Len((network)[self])) > (0)
181+
/\ LET msg00 == Head((network)[self]) IN
182+
/\ network' = [network EXCEPT ![self] = Tail((network)[self])]
183+
/\ LET yielded_network1 == msg00 IN
184+
/\ processor' = yielded_network1
185+
/\ pc' = [pc EXCEPT ![self] = "c"]
186+
/\ UNCHANGED << stream, requester >>
215187

216188
Consumer(self) == c(self) \/ c1(self) \/ c2(self)
217189

218190
p(self) == /\ pc[self] = "p"
219191
/\ IF TRUE
220192
THEN /\ pc' = [pc EXCEPT ![self] = "p1"]
221-
/\ UNCHANGED << network, stream, netWrite2, sWrite0 >>
222-
ELSE /\ netWrite2' = network
223-
/\ sWrite0' = stream
224-
/\ network' = netWrite2'
225-
/\ stream' = sWrite0'
226-
/\ pc' = [pc EXCEPT ![self] = "Done"]
227-
/\ UNCHANGED << processor, netWrite, netRead, procWrite, netWrite0,
228-
procWrite0, netRead0, netWrite1, sRead, sWrite,
229-
requester >>
193+
ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
194+
/\ UNCHANGED << network, processor, stream, requester >>
230195

231196
p1(self) == /\ pc[self] = "p1"
232-
/\ (Len(network[self])) > (0)
233-
/\ LET msg1 == Head(network[self]) IN
234-
/\ netWrite1' = [network EXCEPT ![self] = Tail(network[self])]
235-
/\ netRead0' = msg1
236-
/\ requester' = [requester EXCEPT ![self] = netRead0']
237-
/\ network' = netWrite1'
238-
/\ pc' = [pc EXCEPT ![self] = "p2"]
239-
/\ UNCHANGED << processor, stream, netWrite, netRead, procWrite,
240-
netWrite0, procWrite0, sRead, sWrite, netWrite2,
241-
sWrite0 >>
197+
/\ (Len((network)[self])) > (0)
198+
/\ LET msg10 == Head((network)[self]) IN
199+
/\ network' = [network EXCEPT ![self] = Tail((network)[self])]
200+
/\ LET yielded_network00 == msg10 IN
201+
/\ requester' = [requester EXCEPT ![self] = yielded_network00]
202+
/\ pc' = [pc EXCEPT ![self] = "p2"]
203+
/\ UNCHANGED << processor, stream >>
242204

243205
p2(self) == /\ pc[self] = "p2"
244-
/\ sWrite' = ((stream) + (1)) % (BUFFER_SIZE)
245-
/\ sRead' = sWrite'
246-
/\ (Len(network[requester[self]])) < (BUFFER_SIZE)
247-
/\ netWrite1' = [network EXCEPT ![requester[self]] = Append(network[requester[self]], sRead')]
248-
/\ network' = netWrite1'
249-
/\ stream' = sWrite'
250-
/\ pc' = [pc EXCEPT ![self] = "p"]
251-
/\ UNCHANGED << processor, netWrite, netRead, procWrite, netWrite0,
252-
procWrite0, netRead0, netWrite2, sWrite0,
253-
requester >>
206+
/\ stream' = ((stream) + (1)) % (BUFFER_SIZE)
207+
/\ LET yielded_stream0 == stream' IN
208+
LET value00 == yielded_stream0 IN
209+
/\ (Len((network)[requester[self]])) < (BUFFER_SIZE)
210+
/\ network' = [network EXCEPT ![requester[self]] = Append((network)[requester[self]], value00)]
211+
/\ pc' = [pc EXCEPT ![self] = "p"]
212+
/\ UNCHANGED << processor, requester >>
254213

255214
Producer(self) == p(self) \/ p1(self) \/ p2(self)
256215

0 commit comments

Comments
 (0)