]>
Rather than enforce hard resource limits (e.g., maximum queue depth),
use CONSTRAINT
s 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.)
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.
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 EXTEND
s 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
ASSUME
s 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.
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.
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
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.
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+2 Preliminary Guide section 8.3) which is necessary
to infer global truths from constant truths.
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.
The following tables summarize TLA+2’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:
Proof | Rule |
---|---|
(PROOF) OBVIOUS |
(Γ ⊢ G) |
(PROOF) OMITTED |
Γ ⊢ G |
(PROOF) BY F |
(Γ ⊢ F) (Γ, F ⊢ G) Γ ⊢ G |
(PROOF) BY ONLY F |
(Γ ⊢ F) (Γ′, F ⊢ G) Γ ⊢ G (Γ′ being Γ with all facts removed) |
(PROOF) BY DEF F |
(Γ, F ≜ H ⊢ G) Γ ⊢ G |
(PROOF) BY ONLY DEF F |
(Γ′, F ≜ H ⊢ G) Γ ⊢ G (Γ′ being Γ with all facts removed) |
(PROOF) |
Σn
⋮ Σ1 Γ ⊢ G |
Steps which take proofs:
Step | Rule |
---|---|
F |
(Π) &qquad;Γ, F ⊢ G
Γ ⊢ F Γ ⊢ G |
ASSUME H PROVE F |
(Π) &qquad;Γ, Γ, H ⊢ F ASSUME H
PROVE F ⊢ G
Γ ⊢ G |
CASE F |
(Π)
&qquad;Γ, Γ, F ⊢ G ASSUME F
PROVE G ⊢ G
Γ ⊢ G |
SUFFICES F |
(Π)
&qquad;Γ ⊢ F
Γ, F ⊢ G Γ ⊢ G |
SUFFICES ASSUME H PROVE F |
(Π)
&qquad;Γ, H ⊢ F
Γ, ASSUME H PROVE F
⊢ GΓ ⊢ G |
PICK x: F |
(Π)
&qquad;Γ, NEW x,
F ⊢ G
Γ ⊢ ∃ x: F Γ ⊢ G |
PICK x ∈ S: F |
(Π)
&qquad;Γ, NEW
x ∈ S, F ⊢ G
Γ ⊢ ∃ x ∈ S: F Γ ⊢ G |
QED |
(Π)
Γ ⊢ G |
Steps which do not take proofs:
Step | Rule |
---|---|
(DEFINE) F ≜ H |
Γ, F ≜ H ⊢ G
Γ ⊢ G |
USE F |
(Γ ⊢ F) Γ ⊢ G |
USE ONLY F |
(Γ ⊢ F) Γ ⊢ G (Γ′ being Γ with all facts removed) |
USE DEF F |
Γ, F ≜ H ⊢ G
Γ ⊢ G |
USE ONLY DEF F |
Γ′, F ≜ H ⊢ G
Γ ⊢ G (Γ′ being Γ with all facts removed) |
HIDE F |
Γ ⊢ G
Γ, F ⊢ G |
HIDE DEF F |
Γ ⊢ G
Γ, F ≜ H ⊢ G |
HAVE F |
(Γ ⊢ H ⇒ F) Γ ⊢ H ⇒ G |
TAKE x |
Γ, NEW x ⊢ G
Γ ⊢ ∀ x: G |
TAKE x ∈ S |
Γ, NEW x ∈ S ⊢ G
Γ ⊢ ∀ x ∈ S: G |
WITNESS e |
Γ ⊢ G[e/x]
Γ ⊢ ∃ x: G |
WITNESS e ∈ S |
(Γ ⊢ e ∈ S) Γ ⊢ ∃ x ∈ S: G |
Note that most of the above steps also work with more than one argument, with the obvious extension of meaning.
From the TLA+ Summary hyperbook.
∧ | /\ or \land |
∨ | \/ or \lor |
⇒ | => |
¬ | ~ or \lnot or \neg |
≡ | <=> or \equiv |
≜ | == |
∈ | \in |
∉ | \notin |
≠ | # or /= |
⟨ | << |
⟩ | >> |
◻ | [] |
< | < |
> | > |
◇ | <> |
≤ | \leq or =< or <= |
≥ | \geq or >= |
⤳ | ~> |
≪ | \ll |
≫ | \gg |
⇾⃰ * | -+-> |
≺ | \prec |
≻ | \succ |
↦ | |-> |
⪯ | \preceq |
⪰ | \succeq |
÷ | \div |
⊆ | \subseteq |
⊇ | \supseteq |
⋅ | \cdot |
⊂ | \subset |
⊃ | \supset |
∘ | \o or \circ |
⊏ | \sqsubset |
⊐ | \sqsupset |
∙ | \bullet |
⊑ | \sqsubseteq |
⊒ | \sqsupseteq |
⋆ | \star |
⊢ | |- |
⊣ | -| |
◯ | \bigcirc |
⊨ | |= |
⫤ | =| |
∼ | \sim |
→ | -> |
← | <- |
≃ | \simeq |
∩ | \cap or \intersect |
∪ | \cup or \union |
≍ | \asymp |
⊓ | \sqcap |
⊔ | \sqcup |
≈ | \approx |
⊕ | (+) or \oplus |
⊎ | \uplus |
≅ | \cong |
⊖ | (-) or \ominus |
× | \X or \times |
≐ | \doteq |
⊙ | (.) or \odot |
≀ | \wr |
xy | x^y |
⊗ | (\X) or \otimes |
∝ | \propto |
x+ | x^+ |
⊘ | (/) or \oslash |
“s” | "s" |
x∗ | x^* |
∃ | \E |
∀ | \A |
x# | x^# |
∃ | \EE |
∀ | \AA |
′ | ' |
]v | ]_v |
⟩v | >>_v |
||
WFv | WF_v |
SFv | SF_v |
┌─────── | -------- |
───────┐ | -------- |
├──────┤ | -------- |
└──────┘ | ======== |
* no exact Unicode equivalent