-
Notifications
You must be signed in to change notification settings - Fork 199
/
TLAPS.tla
468 lines (394 loc) · 24.2 KB
/
TLAPS.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
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
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
------------------------------- MODULE TLAPS --------------------------------
(* Backend pragmas. *)
(***************************************************************************)
(* Each of these pragmas can be cited with a BY or a USE. The pragma that *)
(* is added to the context of an obligation most recently is the one whose *)
(* effects are triggered. *)
(***************************************************************************)
(***************************************************************************)
(* The following pragmas should be used only as a last resource. They are *)
(* dependent upon the particular backend provers, and are unlikely to have *)
(* any effect if the set of backend provers changes. Moreover, they are *)
(* meaningless to a reader of the proof. *)
(***************************************************************************)
(**************************************************************************)
(* Backend pragma: use the SMT solver for arithmetic. *)
(* *)
(* This method exists under this name for historical reasons. *)
(**************************************************************************)
SimpleArithmetic == TRUE (*{ by (prover:"smt3") }*)
(**************************************************************************)
(* Backend pragma: SMT solver *)
(* *)
(* This method translates the proof obligation to SMTLIB2. The supported *)
(* fragment includes first-order logic, set theory, functions and *)
(* records. *)
(* SMT calls the smt-solver with the default timeout of 5 seconds *)
(* while SMTT(n) calls the smt-solver with a timeout of n seconds. *)
(**************************************************************************)
SMT == TRUE (*{ by (prover:"smt3") }*)
SMTT(X) == TRUE (*{ by (prover:"smt3"; timeout:@) }*)
(**************************************************************************)
(* Backend pragma: CVC4 SMT solver *)
(* *)
(* These methods translate the proof obligation to SMTLIB2 and call CVC4. *)
(**************************************************************************)
(* The CVC3* methods are here for backward compatibility. They call CVC4. *)
CVC3 == TRUE (*{ by (prover: "cvc33") }*)
CVC3T(X) == TRUE (*{ by (prover:"cvc33"; timeout:@) }*)
CVC4 == TRUE (*{ by (prover: "cvc33") }*)
CVC4T(X) == TRUE (*{ by (prover:"cvc33"; timeout:@) }*)
(**************************************************************************)
(* Backend pragma: Yices SMT solver *)
(* *)
(* This method translates the proof obligation to Yices native language. *)
(**************************************************************************)
Yices == TRUE (*{ by (prover: "yices3") }*)
YicesT(X) == TRUE (*{ by (prover:"yices3"; timeout:@) }*)
(**************************************************************************)
(* Backend pragma: veriT SMT solver *)
(* *)
(* This method translates the proof obligation to SMTLIB2 and calls veriT.*)
(**************************************************************************)
veriT == TRUE (*{ by (prover: "verit") }*)
veriTT(X) == TRUE (*{ by (prover:"verit"; timeout:@) }*)
(**************************************************************************)
(* Backend pragma: Z3 SMT solver *)
(* *)
(* This method translates the proof obligation to SMTLIB2 and calls Z3. *)
(* Z3 is used by default but you can also explicitly call it. *)
(**************************************************************************)
Z3 == TRUE (*{ by (prover: "z33") }*)
Z3T(X) == TRUE (*{ by (prover:"z33"; timeout:@) }*)
(**************************************************************************)
(* Backend pragma: SPASS superposition prover *)
(* *)
(* This method translates the proof obligation to the DFG format language *)
(* supported by the ATP SPASS. The translation is based on the SMT one. *)
(**************************************************************************)
Spass == TRUE (*{ by (prover: "spass") }*)
SpassT(X) == TRUE (*{ by (prover:"spass"; timeout:@) }*)
(**************************************************************************)
(* Backend pragma: The PTL propositional linear time temporal logic *)
(* prover. It currently is the LS4 backend. *)
(* *)
(* This method translates the negetation of the proof obligation to *)
(* Seperated Normal Form (TRP++ format) and checks for unsatisfiability *)
(**************************************************************************)
LS4 == TRUE (*{ by (prover: "ls4") }*)
LS4T(X) == TRUE (*{ by (prover: "ls4"; timeout:@) }*)
PTL == TRUE (*{ by (prover: "ls4") }*)
(**************************************************************************)
(* Backend pragma: Zenon with different timeouts (default is 10 seconds) *)
(* *)
(**************************************************************************)
Zenon == TRUE (*{ by (prover:"zenon") }*)
ZenonT(X) == TRUE (*{ by (prover:"zenon"; timeout:@) }*)
(********************************************************************)
(* Backend pragma: Isabelle with different timeouts and tactics *)
(* (default is 30 seconds/auto) *)
(********************************************************************)
Isa == TRUE (*{ by (prover:"isabelle") }*)
IsaT(X) == TRUE (*{ by (prover:"isabelle"; timeout:@) }*)
IsaM(X) == TRUE (*{ by (prover:"isabelle"; tactic:@) }*)
IsaMT(X,Y) == TRUE (*{ by (prover:"isabelle"; tactic:@; timeout:@) }*)
(***************************************************************************)
(* The following theorem expresses the (useful implication of the) law of *)
(* set extensionality, which can be written as *)
(* *)
(* THEOREM \A S, T : (S = T) <=> (\A x : (x \in S) <=> (x \in T)) *)
(* *)
(* Theorem SetExtensionality is sometimes required by the SMT backend for *)
(* reasoning about sets. It is usually counterproductive to include *)
(* theorem SetExtensionality in a BY clause for the Zenon or Isabelle *)
(* backends. Instead, use the pragma IsaWithSetExtensionality to instruct *)
(* the Isabelle backend to use the rule of set extensionality. *)
(***************************************************************************)
IsaWithSetExtensionality == TRUE
(*{ by (prover:"isabelle"; tactic:"(auto intro: setEqualI)")}*)
THEOREM SetExtensionality == \A S,T : (\A x : x \in S <=> x \in T) => S = T
OBVIOUS
(***************************************************************************)
(* The following theorem is needed to deduce NotInSetS \notin SetS from *)
(* the definition *)
(* *)
(* NotInSetS == CHOOSE v : v \notin SetS *)
(***************************************************************************)
THEOREM NoSetContainsEverything == \A S : \E x : x \notin S
OBVIOUS (*{by (isabelle "(auto intro: inIrrefl)")}*)
-----------------------------------------------------------------------------
(********************************************************************)
(********************************************************************)
(********************************************************************)
(********************************************************************)
(* Old versions of Zenon and Isabelle pragmas below *)
(* (kept for compatibility) *)
(********************************************************************)
(**************************************************************************)
(* Backend pragma: Zenon with different timeouts (default is 10 seconds) *)
(* *)
(**************************************************************************)
SlowZenon == TRUE (*{ by (prover:"zenon"; timeout:20) }*)
SlowerZenon == TRUE (*{ by (prover:"zenon"; timeout:40) }*)
VerySlowZenon == TRUE (*{ by (prover:"zenon"; timeout:80) }*)
SlowestZenon == TRUE (*{ by (prover:"zenon"; timeout:160) }*)
(********************************************************************)
(* Backend pragma: Isabelle's automatic search ("auto") *)
(* *)
(* This pragma bypasses Zenon. It is useful in situations involving *)
(* essentially simplification and equational reasoning. *)
(* Default imeout for all isabelle tactics is 30 seconds. *)
(********************************************************************)
Auto == TRUE (*{ by (prover:"isabelle"; tactic:"auto") }*)
SlowAuto == TRUE (*{ by (prover:"isabelle"; tactic:"auto"; timeout:120) }*)
SlowerAuto == TRUE (*{ by (prover:"isabelle"; tactic:"auto"; timeout:480) }*)
SlowestAuto == TRUE (*{ by (prover:"isabelle"; tactic:"auto"; timeout:960) }*)
(********************************************************************)
(* Backend pragma: Isabelle's "force" tactic *)
(* *)
(* This pragma bypasses Zenon. It is useful in situations involving *)
(* quantifier reasoning. *)
(********************************************************************)
Force == TRUE (*{ by (prover:"isabelle"; tactic:"force") }*)
SlowForce == TRUE (*{ by (prover:"isabelle"; tactic:"force"; timeout:120) }*)
SlowerForce == TRUE (*{ by (prover:"isabelle"; tactic:"force"; timeout:480) }*)
SlowestForce == TRUE (*{ by (prover:"isabelle"; tactic:"force"; timeout:960) }*)
(***********************************************************************)
(* Backend pragma: Isabelle's "simplification" tactics *)
(* *)
(* These tactics simplify the goal before running one of the automated *)
(* tactics. They are often necessary for obligations involving record *)
(* or tuple projections. Use the SimplfyAndSolve tactic unless you're *)
(* sure you can get away with just Simplification *)
(***********************************************************************)
SimplifyAndSolve == TRUE
(*{ by (prover:"isabelle"; tactic:"clarsimp auto?") }*)
SlowSimplifyAndSolve == TRUE
(*{ by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:120) }*)
SlowerSimplifyAndSolve == TRUE
(*{ by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:480) }*)
SlowestSimplifyAndSolve == TRUE
(*{ by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:960) }*)
Simplification == TRUE (*{ by (prover:"isabelle"; tactic:"clarsimp") }*)
SlowSimplification == TRUE
(*{ by (prover:"isabelle"; tactic:"clarsimp"; timeout:120) }*)
SlowerSimplification == TRUE
(*{ by (prover:"isabelle"; tactic:"clarsimp"; timeout:480) }*)
SlowestSimplification == TRUE
(*{ by (prover:"isabelle"; tactic:"clarsimp"; timeout:960) }*)
(**************************************************************************)
(* Backend pragma: Isabelle's tableau prover ("blast") *)
(* *)
(* This pragma bypasses Zenon and uses Isabelle's built-in theorem *)
(* prover, Blast. It is almost never better than Zenon by itself, but *)
(* becomes very useful in combination with the Auto pragma above. The *)
(* AutoBlast pragma first attempts Auto and then uses Blast to prove what *)
(* Auto could not prove. (There is currently no way to use Zenon on the *)
(* results left over from Auto.) *)
(**************************************************************************)
Blast == TRUE (*{ by (prover:"isabelle"; tactic:"blast") }*)
SlowBlast == TRUE (*{ by (prover:"isabelle"; tactic:"blast"; timeout:120) }*)
SlowerBlast == TRUE (*{ by (prover:"isabelle"; tactic:"blast"; timeout:480) }*)
SlowestBlast == TRUE (*{ by (prover:"isabelle"; tactic:"blast"; timeout:960) }*)
AutoBlast == TRUE (*{ by (prover:"isabelle"; tactic:"auto, blast") }*)
(**************************************************************************)
(* Backend pragmas: multi-back-ends *)
(* *)
(* These pragmas just run a bunch of back-ends one after the other in the *)
(* hope that one will succeed. This saves time and effort for the user at *)
(* the expense of computation time. *)
(**************************************************************************)
(* CVC3 goes first because it's bundled with TLAPS, then the other SMT
solvers are unlikely to succeed if CVC3 fails, so we run zenon and
Isabelle before them. *)
AllProvers == TRUE (*{
by (prover:"cvc33")
by (prover:"zenon")
by (prover:"isabelle"; tactic:"auto")
by (prover:"spass")
by (prover:"smt3")
by (prover:"yices3")
by (prover:"verit")
by (prover:"z33")
by (prover:"isabelle"; tactic:"force")
by (prover:"isabelle"; tactic:"(auto intro: setEqualI)")
by (prover:"isabelle"; tactic:"clarsimp auto?")
by (prover:"isabelle"; tactic:"clarsimp")
by (prover:"isabelle"; tactic:"auto, blast")
}*)
AllProversT(X) == TRUE (*{
by (prover:"cvc33"; timeout:@)
by (prover:"zenon"; timeout:@)
by (prover:"isabelle"; tactic:"auto"; timeout:@)
by (prover:"spass"; timeout:@)
by (prover:"smt3"; timeout:@)
by (prover:"yices3"; timeout:@)
by (prover:"verit"; timeout:@)
by (prover:"z33"; timeout:@)
by (prover:"isabelle"; tactic:"force"; timeout:@)
by (prover:"isabelle"; tactic:"(auto intro: setEqualI)"; timeout:@)
by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:@)
by (prover:"isabelle"; tactic:"clarsimp"; timeout:@)
by (prover:"isabelle"; tactic:"auto, blast"; timeout:@)
}*)
AllSMT == TRUE (*{
by (prover:"cvc33")
by (prover:"smt3")
by (prover:"yices3")
by (prover:"verit")
by (prover:"z33")
}*)
AllSMTT(X) == TRUE (*{
by (prover:"cvc33"; timeout:@)
by (prover:"smt3"; timeout:@)
by (prover:"yices3"; timeout:@)
by (prover:"verit"; timeout:@)
by (prover:"z33"; timeout:@)
}*)
AllIsa == TRUE (*{
by (prover:"isabelle"; tactic:"auto")
by (prover:"isabelle"; tactic:"force")
by (prover:"isabelle"; tactic:"(auto intro: setEqualI)")
by (prover:"isabelle"; tactic:"clarsimp auto?")
by (prover:"isabelle"; tactic:"clarsimp")
by (prover:"isabelle"; tactic:"auto, blast")
}*)
AllIsaT(X) == TRUE (*{
by (prover:"isabelle"; tactic:"auto"; timeout:@)
by (prover:"isabelle"; tactic:"force"; timeout:@)
by (prover:"isabelle"; tactic:"(auto intro: setEqualI)"; timeout:@)
by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:@)
by (prover:"isabelle"; tactic:"clarsimp"; timeout:@)
by (prover:"isabelle"; tactic:"auto, blast"; timeout:@)
}*)
(**************************************************************************)
(* The pragma ExpandEnabled invokes expansion of the operator ENABLED. *)
(* *)
(* The pragma ExpandCdot invokes expansion of the operator \cdot. *)
(* *)
(* The pragma AutoUSE invokes automated expansion of definitions, *)
(* for both of ExpandEnabled and ExpandCdot, when each is present. *)
(* *)
(* The pragma Lambdify invokes expansion of the operators *)
(* ENABLED and \cdot to an intermediate form with bound VARIABLES, *)
(* which is a form before introducing rigid quantifiers. *)
(* The pragma Lambdify is sound for occurrences of ENABLED and \cdot *)
(* that are not nested. *)
(* *)
(* The pragma ENABLEDaxioms invokes axioms about the operator ENABLED. *)
(* *)
(* The pragma ENABLEDrules invokes two proof rules about the operator *)
(* ENABLED. *)
(* *)
(* The pragma LevelComparison allows proofs that change only the levels *)
(* of declared operators, or rename declared operators. *)
(**************************************************************************)
ExpandENABLED == TRUE (*{ by (prover:"expandenabled") }*)
ExpandCdot == TRUE (*{ by (prover:"expandcdot") }*)
AutoUSE == TRUE (*{ by (prover:"autouse") }*)
Lambdify == TRUE (*{ by (prover:"lambdify") }*)
ENABLEDaxioms == TRUE (*{ by (prover:"enabledaxioms") }*)
ENABLEDrewrites == TRUE (*{ by (prover:"enabledrewrites") }*)
ENABLEDrules == TRUE (*{ by (prover:"enabledrules") }*)
LevelComparison == TRUE (*{ by (prover:"levelcomparison") }*)
(* The operators EnabledWrapper and CdotWrapper occur in an intermediate *)
(* representation within TLAPM. *)
EnabledWrapper(Op(_)) == FALSE
CdotWrapper(Op(_)) == FALSE
(***************************************************************************)
(* The following may be used in a `BY ONLY ThmName` for unit testing the *)
(* triviality checks in TLAPM. *)
(***************************************************************************)
Trivial == TRUE (*{ by (prover:"trivial") }*)
=============================================================================
The material below is obsolete: the TLA proof rules below are superseded by
the PTL decision procedure, and their formulation is unsound for the semantics
of temporal reasoning that TLAPS adopts.
----------------------------------------------------------------------------
(***************************************************************************)
(* TEMPORAL LOGIC *)
(* *)
(* The following rules are intended to be used when TLAPS handles temporal *)
(* logic. They will not work now. Moreover when temporal reasoning is *)
(* implemented, these rules may be changed or omitted, and additional *)
(* rules will probably be added. However, they are included mainly so *)
(* their names will be defined, preventing the use of identifiers that are *)
(* likely to produce name clashes with future versions of this module. *)
(***************************************************************************)
(***************************************************************************)
(* The following proof rules (and their names) are from the paper "The *)
(* Temporal Logic of Actions". *)
(***************************************************************************)
THEOREM RuleTLA1 == ASSUME STATE P, STATE f,
P /\ (f' = f) => P'
PROVE []P <=> P /\ [][P => P']_f
THEOREM RuleTLA2 == ASSUME STATE P, STATE Q, STATE f, STATE g,
ACTION A, ACTION B,
P /\ [A]_f => Q /\ [B]_g
PROVE []P /\ [][A]_f => []Q /\ [][B]_g
THEOREM RuleINV1 == ASSUME STATE I, STATE F, ACTION N,
I /\ [N]_F => I'
PROVE I /\ [][N]_F => []I
THEOREM RuleINV2 == ASSUME STATE I, STATE f, ACTION N
PROVE []I => ([][N]_f <=> [][N /\ I /\ I']_f)
THEOREM RuleWF1 == ASSUME STATE P, STATE Q, STATE f, ACTION N, ACTION A,
P /\ [N]_f => (P' \/ Q'),
P /\ <<N /\ A>>_f => Q',
P => ENABLED <<A>>_f
PROVE [][N]_f /\ WF_f(A) => (P ~> Q)
THEOREM RuleSF1 == ASSUME STATE P, STATE Q, STATE f,
ACTION N, ACTION A, TEMPORAL F,
P /\ [N]_f => (P' \/ Q'),
P /\ <<N /\ A>>_f => Q',
[]P /\ [][N]_f /\ []F => <> ENABLED <<A>>_f
PROVE [][N]_f /\ SF_f(A) /\ []F => (P ~> Q)
(***************************************************************************)
(* The rules WF2 and SF2 in "The Temporal Logic of Actions" are obtained *)
(* from the following two rules by the following substitutions: `. *)
(* *)
(* ___ ___ _______________ *)
(* M <- M , g <- g , EM <- ENABLED <<M>>_g .' *)
(***************************************************************************)
THEOREM RuleWF2 == ASSUME STATE P, STATE f, STATE g, STATE EM,
ACTION A, ACTION B, ACTION N, ACTION M,
TEMPORAL F,
<<N /\ B>>_f => <<M>>_g,
P /\ P' /\ <<N /\ A>>_f /\ EM => B,
P /\ EM => ENABLED A,
[][N /\ ~B]_f /\ WF_f(A) /\ []F /\ <>[]EM => <>[]P
PROVE [][N]_f /\ WF_f(A) /\ []F => []<><<M>>_g \/ []<>(~EM)
THEOREM RuleSF2 == ASSUME STATE P, STATE f, STATE g, STATE EM,
ACTION A, ACTION B, ACTION N, ACTION M,
TEMPORAL F,
<<N /\ B>>_f => <<M>>_g,
P /\ P' /\ <<N /\ A>>_f /\ EM => B,
P /\ EM => ENABLED A,
[][N /\ ~B]_f /\ SF_f(A) /\ []F /\ []<>EM => <>[]P
PROVE [][N]_f /\ SF_f(A) /\ []F => []<><<M>>_g \/ <>[](~EM)
(***************************************************************************)
(* The following rule is a special case of the general temporal logic *)
(* proof rule STL4 from the paper "The Temporal Logic of Actions". The *)
(* general rule is for arbitrary temporal formulas F and G, but it cannot *)
(* yet be handled by TLAPS. *)
(***************************************************************************)
THEOREM RuleInvImplication ==
ASSUME STATE F, STATE G,
F => G
PROVE []F => []G
PROOF OMITTED
(***************************************************************************)
(* The following rule is a special case of rule TLA2 from the paper "The *)
(* Temporal Logic of Actions". *)
(***************************************************************************)
THEOREM RuleStepSimulation ==
ASSUME STATE I, STATE f, STATE g,
ACTION M, ACTION N,
I /\ I' /\ [M]_f => [N]_g
PROVE []I /\ [][M]_f => [][N]_g
PROOF OMITTED
(***************************************************************************)
(* The following may be used to invoke a decision procedure for *)
(* propositional temporal logic. *)
(***************************************************************************)
PropositionalTemporalLogic == TRUE
=============================================================================