[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Thu, 28 May 2015 02:47:44 -0700 (PDT)*References*: <af8807eb-54a0-48d8-9e0f-5f5e12e288e8@googlegroups.com>

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.

**Follow-Ups**:**Re: Symmetry and Liveness***From:*Y2i

**References**:**Symmetry and Liveness***From:*Y2i

- Prev by Date:
**Re: [tlaplus] TLA+ wikipedia article** - Next by Date:
**BagOfAll? SetOfAll?** - Previous by thread:
**Re: Symmetry and Liveness** - Next by thread:
**Re: Symmetry and Liveness** - Index(es):