/
TLCExt.tla
180 lines (154 loc) · 10.2 KB
/
TLCExt.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
------------------------------- MODULE TLCExt -------------------------------
LOCAL INSTANCE TLC
LOCAL INSTANCE Integers
(*************************************************************************)
(* Imports the definitions from the modules, but doesn't export them. *)
(*************************************************************************)
-----------------------------------------------------------------------------
\* AssertEq(a, b) is logically equivalent to the expression 'a = b'. If a and b are not equal,
\* however, AssertEq(a, b) will print out the values of 'a' and 'b'. If the two values are equal,
\* nothing will be printed.
AssertEq(a, b) ==
IF a # b THEN
/\ PrintT("Assertion failed")
/\ PrintT(a)
/\ PrintT(b)
/\ a = b
ELSE a = b
AssertError(err, exp) ==
LET FailsEval(e) == CHOOSE b \in BOOLEAN : TRUE \* Expression failed to evaluate.
TLCError == CHOOSE s \in STRING : TRUE \* TLC error string.
IN IF FailsEval(exp) THEN Assert(err = TLCError, TLCError) ELSE TRUE
-----------------------------------------------------------------------------
TLCGetAndSet(key, Op(_,_), val, defaultVal) ==
LET oldVal == IF key \in DOMAIN TLCGet("all") THEN TLCGet(key) ELSE defaultVal
IN CHOOSE v \in {oldVal} : TLCSet(key, Op(oldVal, val))
-----------------------------------------------------------------------------
Trace ==
(******************************************************************************)
(* The sequence of states (represented as a record whose DOMAIN is the set of *)
(* a spec's variables) from an initial state to the current state. In other *)
(* words, a prefix - of a behavior - ending with the current state. A way to *)
(* think about this operator is to see it as an implicit history variable *)
(* that does not have to be explicitly specified at the level of the spec. *)
(* *)
(* Note that op is incompatible with TLC!RandomElement and Randomization (see *)
(* tlc2.tool.TLCTrace.getTrace(LongVec)) and will cause TLC to crash. This *)
(* technical limitation could be removed though. *)
(* *)
(* Beware that Trace is prohibitively expensive when evaluated as part of *)
(* the next-state relation or constraints in model-checking mode. *)
(******************************************************************************)
TRUE \* TODO
-----------------------------------------------------------------------------
(* HERE BE DRAGONS! The operators below are experimental! You will probably not need them! *)
CounterExample ==
(****************************************************************************)
(* In the scope of POSTCONDITION, the operator CounterExample is equivalent *)
(* to a (directed) graph represented as [state: States, action: Actions] *)
(* with *)
(* States \subseteq [ Variables -> Values ] *)
(* and *)
(* Actions \subseteq *)
(* (CounterExample.state \X Action \X CounterExample.state). *)
(* If TLC found no violations, then CounterExample.states equals {} and *)
(* CounterExample.actions equals {}. If only initial state violates a *)
(* (safety) property, CounterExample.state is a set of those states, and *)
(* CounterExample.actions = {}. *)
(****************************************************************************)
TRUE
ToTrace(CE) ==
(*
This definition is implemented by the TLCExt#toTrace Java module override. It
is commented because FiniteSetsExt is part of the CommunityModules, but not
tla2tools.
LET F == INSTANCE FiniteSetsExt
IN F!FoldSet(LAMBDA a, acc: acc @@ [n \in {a[1]} |-> a[2]], [n \in {} |-> n], CounterExample.state)
*)
TRUE
-----------------------------------------------------------------------------
TLCModelValue(str) ==
(******************************************************************************)
(* A model value is an unspecified value that TLC considers to be unequal to *)
(* any value that you can express in TLA+. *)
(* *)
(* In most cases, TLC model values can and should be declared via the TLC *)
(* config file. However, for large sets of model values, it can become *)
(* tedious to enumerate them explicitly. Large sets of model values usually *)
(* appear when simulating TLA+ specs with TLC. The following example defines *)
(* a set of 32 model values: *)
(* *)
(* SetOfModelValues == {TLCModelValue("T_MV" \o ToString(i)) : i \in 1..32} *)
(* *)
(* As a matter of fact, the example defines a set of "typed" model values: *)
(* TLC considers a typed model value to be unequal to any other model value *)
(* of the same type. However, it produces an error when evaluating an *)
(* expression requires it to determine if a typed model value is equal to any *)
(* value other than a model value of the same type or an ordinary model *)
(* value. *)
(* *)
(* A model-value type consists of a single letter, so there are 52 different *)
(* types because a and A are different types. (TLC actually accepts *)
(* digits and underscore as types; don't use them.) A model value has type *)
(* T if and only if its name begins with the two characters T_ . *)
(* *)
(* TLCModelValue may only appear in constant definitions! Expect bogus *)
(* behavior if TLCModelValue appears in the behavior spec, constraints, *)
(* invariants, or properties. *)
(******************************************************************************)
CHOOSE v: ToString(v) = str
TLCDefer(expression) ==
(******************************************************************************)
(* Defer evaluation of expression to some later time or never. *)
(* *)
(* For TLC's simulation mode, later is defined as the point of time when *)
(* simulation has chosen a successor state to extend the prefix of the *)
(* current behavior. *)
(* *)
(* A use case is TLCDefer(TLCSet(42, someVal)), which sets someVal only *)
(* for the states of the behavior and not the set of all successor states *)
(* of all states in the behavior. *)
(******************************************************************************)
TRUE
-----------------------------------------------------------------------------
TLCNoOp(val) ==
(******************************************************************************)
(* No-operation operator (does nothing). Only useful to debug TLC's *)
(* evaluator that is written in Java: Insert TLCNoOp into the expression *)
(* whose evaluation you wish to debug and set a breakpoint in this *)
(* operator's Java module override TLCExt#tlcNoOp in TLCExt.java. *)
(******************************************************************************)
val
PickSuccessor(exp) ==
(******************************************************************************)
(* When set as an action constraint in the configuration file, interactively *)
(* pick successor states during state exploration, iff the expression exp *)
(* evaluates to FALSE. To always pick successor states manually, use *)
(* PickSuccessor(FALSE). To pick successor states when the current prefix of *)
(* behaviors exceeds 22 states, use PickSuccessor(TLCGet("level") < 23). *)
(* Evaluates to TRUE when evaluated in the context of a constant- or *)
(* state-level formula. Also evaluates to TRUE if PickSuccessor appears as *)
(* part of the next-state relation and the successor state has not been *)
(* fully determined yet. *)
(******************************************************************************)
IF (exp)
THEN TRUE
ELSE CHOOSE bool \in BOOLEAN : TRUE
-----------------------------------------------------------------------------
TLCCache(expression, closure) ==
(******************************************************************************)
(* Equals the value that an earlier evaluation of the expression evaluated to *)
(* iff the closure of the earlier evaluation and this evaluation are equal. *)
(* *)
(* Currently only implemented for state-level formulas. See TLC!TLCEval for *)
(* constant-level formulas. *)
(******************************************************************************)
expression
TLCFP(var) ==
(******************************************************************************)
(* Equals the value that TLC gives to the given input when the value is *)
(* being fingerprinted. *)
(* Implementation note: Equals the lower 32 bits until TLC supports longs *)
(******************************************************************************)
CHOOSE i \in Int: TRUE
============================================================================