-
Notifications
You must be signed in to change notification settings - Fork 1
/
v2-no-grief.txt
322 lines (280 loc) · 14.3 KB
/
v2-no-grief.txt
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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
TLC2 Version 2.14 of 10 July 2019 (rev: 0cae24f)
Running breadth-first search Model-Checking with fp 125 and seed 6349797062896713821 with 1 worker on 12 cores with 3641MB heap and 64MB offheap memory [pid: 20376] (Mac OS X 10.13.6 x86_64, Oracle Corporation 11.0.2 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /Users/andrewstewart/Code/magmo/tla-specs/Version2NoGrief.tla
Parsing file /Users/andrewstewart/Code/magmo/tla-specs/ForceMove.tla
Parsing file /private/var/folders/qp/rsls0bwn2p99qffhs69_ffbc0000gn/T/TLC.tla
Parsing file /private/var/folders/qp/rsls0bwn2p99qffhs69_ffbc0000gn/T/Integers.tla
Parsing file /Users/andrewstewart/Code/magmo/tla-specs/Utils.tla
Parsing file /private/var/folders/qp/rsls0bwn2p99qffhs69_ffbc0000gn/T/Naturals.tla
Parsing file /private/var/folders/qp/rsls0bwn2p99qffhs69_ffbc0000gn/T/Sequences.tla
Parsing file /private/var/folders/qp/rsls0bwn2p99qffhs69_ffbc0000gn/T/FiniteSets.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module Utils
Semantic processing of module ForceMove
Semantic processing of module Version2NoGrief
Starting... (2020-06-09 21:55:27)
Implied-temporal checking--satisfiability problem has 2 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2020-06-09 21:55:27.
Error: Invariant AliceCannotBeGriefed is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 0, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 0
State 2: <A line 400, col 6 to line 450, col 38 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 0, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 1
State 3: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 0, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 1
State 4: <TransactionProcessor line 323, col 16 to line 396, col 58 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 0, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 1
State 5: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 1, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 1
State 6: <A line 400, col 6 to line 450, col 38 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 1, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 2
State 7: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 1, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 2
State 8: <TransactionProcessor line 323, col 16 to line 396, col 58 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 1, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 2
State 9: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 2, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 2
State 10: <A line 400, col 6 to line 450, col 38 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 2, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 3
State 11: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 2, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 3
State 12: <TransactionProcessor line 323, col 16 to line 396, col 58 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 2, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 3
State 13: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 3, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 3
State 14: <A line 400, col 6 to line 450, col 38 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 3, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 4
State 15: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 3, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 4
State 16: <TransactionProcessor line 323, col 16 to line 396, col 58 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 3, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 4
State 17: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 4, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 4
State 18: <A line 400, col 6 to line 450, col 38 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 4, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 5
State 19: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 4, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 5
State 20: <TransactionProcessor line 323, col 16 to line 396, col 58 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 4, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 5
State 21: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 5, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 5
State 22: <A line 400, col 6 to line 450, col 38 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 5, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 6
State 23: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 5, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 6
State 24: <TransactionProcessor line 323, col 16 to line 396, col 58 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 5, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 6
State 25: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 6, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 6
State 26: <A line 400, col 6 to line 450, col 38 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 6, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 7
State 27: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 6, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 7
State 28: <TransactionProcessor line 323, col 16 to line 396, col 58 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 6, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 7
State 29: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 7, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 7
State 30: <A line 400, col 6 to line 450, col 38 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 7, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 8
State 31: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 7, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 8
State 32: <TransactionProcessor line 323, col 16 to line 396, col 58 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 7, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 8
State 33: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 8, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 8
State 34: <A line 400, col 6 to line 450, col 38 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 8, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 9
State 35: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 8, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 9
State 36: <TransactionProcessor line 323, col 16 to line 396, col 58 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 8, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 9
State 37: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 9, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 9
State 38: <A line 400, col 6 to line 450, col 38 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 9, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 10
State 39: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 9, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 10
State 40: <TransactionProcessor line 323, col 16 to line 396, col 58 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 9, mode |-> "CHALLENGE"]
/\ Alice = 1
/\ alicesActionCount = 10
State 41: <E line 454, col 6 to line 529, col 61 of module ForceMove>
/\ TransactionPool = NULL
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 10, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 10
State 42: <A line 400, col 6 to line 450, col 38 of module ForceMove>
/\ TransactionPool = [state |-> [turnNumber |-> 11], type |-> "FORCE_MOVE"]
/\ pc = [Alice |-> "A", TransactionProcessor |-> "TransactionProcessor", Eve |-> "E"]
/\ adjudicator = [turnNumber |-> 10, mode |-> "OPEN"]
/\ Alice = 1
/\ alicesActionCount = 11
9483 states generated, 565 distinct states found, 10 states left on queue.
The depth of the complete state graph search is 42.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 14 and the 95th percentile is 3).
Finished in 01s at (2020-06-09 21:55:29)