TLC can check the following kinds of properties.
1. A state predicate I (an initial predicate)
2. []I for a state predicate I (an invariant)
3. [][A]_vars for an action A, vars the tuple of all variables.
4. Any TLA temporal formula that is the conjunction of disjunctions
of the following kinds of formulas:
- One containing only temporal operators and state predicates.
(Those predicates can be of the form ENABLED A for an arbitrary
action A.)
- A formula of the form []<><<A>>_vars or <>[][A]_vars for some
action A.
Symmetry sets define a group of permutations Sym on the model values
in those sets. For any permutation P in Sym and any state s, let P(s)
be the state obtained from s by replacing each model value m in M that
appears in s by P(m). For example, if there are two variables x and y
and two model values m1 and m2, and P is the permutation that
exchanges m1 and m2, then P([x <- {m1, 1}, y <- <<m1, m2>>]) equals
[x <- {m2, 1}, y <- <<m2, m1>>]. A state predicate I is symmetric iff
for every state s and every P in Sym, I is satisfied by s iff it is
satisfied by P(s). An action A is symmetric iff for every pair of
states s and t and every P in Sym, A is satisfied by s -> t iff it is
satisfied by P(s) -> P(t). A spec is symmetric iff its initial
predicate, next-state action, and all actions in its fairness
conditions are symmetric.
For properties of types 1-3, if TLC catches an error, then it produces
an error trace that is a counterexample to that property. If the spec
and the predicate or action of the property are symmetric, then TLC
will catch any error if it runs long enough (for example, if it
terminates). If the spec and property are not symmetric, then TLC
might not find an error even though the property doesn't hold.
For a property of type 4, if the spec and all actions and predicates
in the property are symmetric, then if TLC terminates, then
- If TLC reports an error, I BELIEVE that the property does not
hold. However, the error trace may not be a correct
counterexample. In fact, the counterexample might not even
satisfy the spec's next-state relation. A simple modification
to the way TLC computes error traces will ensure that it doesn't
report an incorrect counterexample.
- TLC may fail to report an error even though the property does
not hold. This can be corrected, but requires TLC to gather
additional information when it builds its graph of fingerprints
of reachable states.
We expect that, in the fullness of time, these problems will be
corrected.
For a property of type 4, if the spec or the property is not
symmetric, then:
- IF TLC reports an error, I BELIEVE that the property does
not hold. However, TLC may produce an incorrect error trace.
It may even fail to find an error trace, reporting an error
saying something like "Cannot construct state from its
fingerprint."
- TLC may fail to report an error even though the property does
not hold.
There is no way to get TLC to do any better in this case.
Note: A fingerprint collision acts like an additional symmetry reduction
for which the spec and the properties being checked are not symmetric.