TLA⁺ tips

Use constraints

Rather than enforce hard resource limits (e.g., maximum queue depth), use CONSTRAINTs to enforce such limits. Hard resource limits cause TLC to assume that certain transitions are not possible, leading to false violations of deadlock and temporal checking. In contrast, constraints merely instruct TLC not to visit states which do not match the constraint, so deadlock and temporal properties are not falsely violated. (Of course, true violations will not be reported for the states which are not visited.)

Use symmetry, but not too much

Declaring a SYMMETRY can drastically reduce the search space, but at the cost of checking the symmetry for every state generated. For symmetries of more than 4 or 5 values, this check quickly becomes more costly than the brute‐force search itself. Beyond 6 values, startup becomes quite costly as TLC computes the permutation set. If you do have a large set whose symmetry you wish to exploit, instead, declare as the SYMMETRY the union of permutations of several sets which partition the large set.

When using symmetries, don’t forget that you must never treat any member of the symmetry set specially. This includes using CHOOSE to select an element from the set! Instead of CHOOSE, use the existential operator (∃) to select an element. However, if you are using CHOOSE at the constant level, e.g. to select a fencepost or null value, it is better to simply exclude the chosen value from the symmetry set.

Recognize also cases where nothing is gained from breaking symmetry. One common case is with a pool of unique identifiers which are handed out during execution. The pool should necessarily be finite so that a symmetry may be applied, but can be made to appear infinite by use of a CONSTRAINT which excludes states in which the pool is empty. However, note that in this case, the final identifier handed out is never actually used, since the constraint causes the search to immediately terminate. To reduce the size of the symmetry set, predetermine the identifier which will be the last to be handed out and exclude it from the symmetry set.

Check types using TLAPS

While TLC can be used to check type invariance, you can alternatively use TLAPS to more robustly verify such properties. In addition, TLAPS can verify the types and semantics of your operators.

For each module you wish to typecheck, create a separate module (perhaps in a special directory) which EXTENDs it. In this module, you will define the type invariant and prove type judgements.

In the module being typechecked, you will need to name any ASSUMEs your proofs will need. It’s also a good idea in the typechecking module to USE these assumptions, and USE DEF the type invariant and any type definitions, so you do not need to do so repeatedly in the proofs.

I find it makes sense to divide the proofs into five sections: basic typechecking, dependent typechecking, action type invariance, API type invariance, and operator semantics.

Basic typechecking

In this section, prove for each operator of the module, that given arguments of the expected types, it evalutes to a value of the expected type. (For action operators, this is always BOOLEAN.)

These proofs will generally take the following form:

THEOREM
&i;ASSUME
&i;&i;TypeInvariant,
&i;&i;NEW arg1 ∈ Arg1Type, NEW arg2 ∈ Arg2Type
&i;PROVE
&i;&i;Op(arg1, arg2) ∈ OpType
PROOF
&i;BY DEFS Op, TypeInvariant

These proofs may of course be parametric over one or more types, in which case you will need a NEW T in the ASSUME clause for each such type T.

Dependent typechecking

In this section, place any proofs which refine the type of each operator when applied to specific arguments, or under some other constraint. You may have none or many; just define whichever refined type judgements you feel are worthwhile to the user of the module.

These proofs will generally look something like this:

THEOREM
&i;ASSUME
&i;&i;TypeInvariant,
&i;&i;NEW arg1 ∈ Arg1Type, NEW arg2 ∈ Arg2Type,
&i;&i;SomeProperty(arg1)
&i;PROVE
&i;&i;Op(arg1, arg2) ≠ special_value
PROOF
&i;BY DEFS Op, TypeInvariant, SomeProperty, special_value

Action type invariance

In this section, prove that the action operators which comprise the module’s API maintain the module’s type invariant. Most of these proofs will look like the following:

THEOREM Action1TypeInvariance ≜
&i;ASSUME
&i;&i;TypeInvariant,
&i;&i;NEW arg1 ∈ Arg1Type, NEW arg2 ∈ Arg2Type,
&i;&i;Action1(arg1, arg2)
&i;PROVE
&i;&i;TypeInvariant′
PROOF
&i;BY DEFS Action1, TypeInvariant

You may also wish to include a proof that the module’s initialization operator establishes the type invariant (though usually this is sufficiently trivial that you may prove it inline in the proof of API type invariance). Such a proof will look like this:

THEOREM InitTypeInvariance ≜
&i;ASSUME Init PROVE TypeInvariant
PROOF
&i;BY DEFS Init, TypeInvariant

You will want to name these theorems so they can be referred to in the following section.

API type invariance

Next, you will want to prove that type invariance is maintained when the module is used in accordance with its API. This is what negates the need to check type invariance for this module with TLC.

First, define a local operator Next which entails all possible applications of the action operators which comprise the module’s API, as if you were defining a next‐state operator for TLC which was exercising the module:

LOCAL Next ≜
&i;∨ ∃ x ∈ T, y ∈ U:
&i;&i;&i;Action1(x, y)
&i;∨ ∃ x ∈ T:
&i;&i;&i;Cond(x) ∧ Action2(x)

Next you can prove type invariance of ◻[Next]_vars, using the action type invariance theorems you established earlier:

THEOREM NextTypeInvariance ≜
&i;ASSUME
&i;&i;TypeInvariant,
&i;&i;◻[Next]vars
&i;PROVE
&i;&i;TypeInvariant′
PROOF
&i;BY Action1TypeInvariance, Action2TypeInvariance
&i;&i;DEFS Next, vars

Finally you can prove type invariance of the system as a whole, using temporal reasoning:

LOCAL INSTANCE TLAPS
THEOREM
&i;Init ∧ ◻[Next]vars ⇒ ◻TypeInvariant
PROOF
&i;BY PTL, InitTypeInvariance, NextTypeInvariance


PTL is the propositional temporal logic proof tactic and is found in the built‐in TLAPS module.

Note that it is important to represent temporal theorems as implications (⇒), rather than as sequents (ASSUME/PROVE). This is because, unlike with an implication, the antecedents (ASSUME formulae) of a sequent automatically become hypotheses of the proof. When this happens, it prevents application of the Generalized Necessitation Rule (TLA⁺² Preliminary Guide section 8.3) which is necessary to infer global truths from constant truths.

Operator semantics

In this section you will want to prove that the state and action operators do what you intend them to do. This is not possible in the general case, and will be difficult in many cases. In such cases, you will want to instead check the desired properties for a finite domain using TLC (though you may of course still include the theorems here with an OMITTED proof).

The form of such proofs will vary dependening on the particular property, so no general form is given here.

Note also that the current version of the TLA⁺ Proof Manager has limited capability for reasoning about temporal statements, so verifying many of the more interesting properties of your operators may require the use of TLC even if the proof is conceptually simple.

Proof step quick reference

The following tables summarize TLA⁺²’s proof steps using sequent calculus.

In all cases, a rule is only valid if its parenthesized portions are also valid (that is, can be readily proved via automated means).

Any proof Π must be complete (that is, start with an inference line).

Proofs:

Steps which take proofs:

Steps which do not take proofs:

Note that most of the above steps also work with more than one argument, with the obvious extension of meaning.

Appendix

ASCII Representation of Typeset Symbols

From the TLA⁺ Summary hyperbook.

* no exact Unicode equivalent