-
Notifications
You must be signed in to change notification settings - Fork 47
/
O.tla
127 lines (97 loc) · 3.45 KB
/
O.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
Run `tlapm O.tla` on the terminal to verify the
theorems below with TLAPS.
---- MODULE O ----
CONSTANT O(_)
\* THEOREM T1 == O(1) /\ O(2) <=> \E i \in {1,2}: O(i) OBVIOUS
THEOREM T2 == O(1) /\ O(2) <=> \A i \in {1,2}: O(i) OBVIOUS
THEOREM T3 == O(1) \/ O(2) <=> \E i \in {1,2}: O(i) OBVIOUS
\* THEOREM T4 == O(1) \/ O(2) <=> \A i \in {1,2}: O(i) OBVIOUS
------------------
\* Implication
CONSTANT
P, \* It's raining
Q \* The street is wet (street is not in a tunnel!)
\* If it rains (P), the street is wet (Q)
THEOREM TRUE => TRUE <=> TRUE OBVIOUS
\* It cannot be that it rains, but the street is dry
THEOREM TRUE => FALSE <=> FALSE OBVIOUS
\* The street might be wet, even without rain (somebody spilled some water)
THEOREM FALSE => TRUE <=> TRUE OBVIOUS
\* No rain and a dry street
THEOREM FALSE => FALSE <=> TRUE OBVIOUS
\* Contraposition (Street not wet implies no rain).
\* https://en.wikipedia.org/wiki/Contraposition
THEOREM P => Q <=> ~Q => ~P OBVIOUS
\* Or-and-if.
THEOREM P => Q <=> (~P) \/ Q OBVIOUS
\* Negated conditionals.
THEOREM ~(P => Q) <=> P /\ (~Q) OBVIOUS
------------------
\* Action operators
THEOREM ASSUME NEW ACTION A, NEW VARIABLE v
PROVE [A]_v <=> A \/ v' = v OBVIOUS
THEOREM ASSUME NEW ACTION A, NEW VARIABLE v
PROVE <<A>>_v <=> A /\ v' # v OBVIOUS
\* ExpandENABLED requires TLAPS version greater than 1.4
\* ENABLED A \/ v=v' is a tautology.
INSTANCE TLAPS
THEOREM ASSUME NEW VARIABLE v
PROVE (ENABLED [FALSE]_v) (*BY ExpandENABLED*)
THEOREM ASSUME NEW VARIABLE v
PROVE (ENABLED [TRUE]_v) (*BY ExpandENABLED*)
THEOREM ASSUME NEW VARIABLE v
PROVE (ENABLED [FALSE]_TRUE) (*BY ExpandENABLED*)
THEOREM ASSUME NEW VARIABLE v
PROVE (ENABLED [TRUE]_TRUE) (*BY ExpandENABLED*)
------------------
\* Dual Box and Diamond operators
THEOREM ASSUME NEW F
PROVE <>F <=> ~[]~F OBVIOUS
THEOREM ASSUME NEW F
PROVE ~<>F <=> []~F OBVIOUS
\* see Specifying Systems page 92
THEOREM ASSUME NEW F
PROVE ~[]F <=> <>~F OBVIOUS
\* see Specifying Systems page 93
THEOREM ASSUME NEW F, NEW G
PROVE
/\ [](F /\ G) <=> ([]F) /\ ([]G)
/\ <>(F \/ G) <=> (<>F) \/ (<>G)
OBVIOUS
THEOREM ASSUME NEW F, NEW G
PROVE
/\ ([]F) \/ ([]G) => [](F \/ G)
/\ <>(F /\ G) => (<>F) /\ (<>G)
OBVIOUS
\* see Specifying Systems page 94
THEOREM ASSUME NEW ACTION A, NEW ACTION B, NEW VARIABLE v
PROVE
/\ [A /\ B]_v <=> [A]_v /\ [B]_v
/\ <<A \/ B>>_v <=> <<A>>_v \/ <<B>>_v
\* 8.5
/\ ([]<><<A>>_v) \/ ([]<><<B>>_v) <=> ([]<><<A>>_v) \/ ([]<><<B>>_v)
OBVIOUS
\* see Specifying Systems page 95
THEOREM ASSUME NEW ACTION A, NEW ACTION B, NEW VARIABLE v
PROVE
/\ []<><<A \/ B>>_v <=> ([]<><<A>>_v) \/ ([]<><<B>>_v)
BY PTL
------------------
\* (Weak) Fairness (see Specifying Systems page 97ff for more equivalent formulae)
THEOREM ASSUME NEW ACTION A, NEW VARIABLE v
PROVE ( <>[](ENABLED <<A>>_v) => []<><<A>>_v ) <=> ( []([]ENABLED <<A>>_v => <><<A>>_v) ) BY PTL
THEOREM ASSUME NEW ACTION A, NEW VARIABLE v
PROVE ( <>[](ENABLED <<A>>_v) => []<><<A>>_v ) <=> ( WF_v(A) ) BY PTL
THEOREM ASSUME NEW ACTION A, NEW VARIABLE v
PROVE ( []<>(~ENABLED <<A>>_v) \/ []<><<A>>_v ) <=> ( WF_v(A) ) BY PTL
THEOREM ASSUME NEW ACTION A, NEW VARIABLE v
PROVE ( []<>(ENABLED <<A>>_v) => []<><<A>>_v ) <=>( SF_v(A) ) BY PTL
------------------
\* Leads-to
THEOREM ASSUME NEW F, NEW G
PROVE [](F => <>G) <=> (F ~> G) OMITTED
------------------
\* CHOOSE
THEOREM ASSUME NEW P(_), NEW S
PROVE ( \E c: P(c) ) <=> ( P(CHOOSE c: P(c)) ) OBVIOUS
====