TLC moder checker 相关文档阅读笔记，专注于相关概念内容，省略 IDE 界面介绍部分。
The TLA+ Toolbox uses the TLC model checker to model check the current spec. More precisely, TLC checks a model of the specification.
1. Models
当我们写完 Spec 之后，可以使用 TLC 验证该 Spec。具体做法是先创建和 Spec 关联的 model (a spec may contain multiple models)，再使用 TLC 验证该 model，model 需给予 TLC 以下几个关键信息：
 What the behavior spec is ?
 What TLC should check ?
 What values to substitute for constant parameters ?
1.1. What the behavior spec is ?
In TLA+, the term specification (or spec) is used to mean one of two things, We take the word specification by itself to have the first meaning. We use the term behavior specification when we mean the second.
 Specification: The collection of modules consisting of the root module and and all modules that are imported by the root module, either directly or indirectly, with
EXTENDS
orINSTANCE
statements.In the context of the Toolbox, we exclude from this collection the standard TLA+ modules such as the
Naturals
module. All the specification’s module files must be in the same directory as the root module file.  Behavior Specification: The TLA formula that specifies the set of allowed behaviors of the system or algorithm being specified.
There are two ways to write the behavior spec:
 Init and Next: A pair of formulas that specify the initial state and the nextstate relation, respectively.
 Single formula: A single temporal formula of the form $Init \land \Box [Next]_{vars} \land F$.
 $Init$ is the initial predicate
 $Next$ is the nextstate relation
 $vars$ is the tuple of variables
 $F$ is an optional fairness formula
1.2. What TLC should check ?
There are three kinds of properties of the behavior spec that TLC can check:
Deadlock
 A deadlock is said to occur in a state for which the nextstate relation allows no successor states.
 Termination is deadlock that is not considered an error. If you want the behavior spec to allow termination, then you should uncheck the deadlock option.
Invariants
 An invariant is a state predicate that is true of all reachable states–that is, states that can occur in a behavior allowed by the behavior spec.
 You can include a list of invariants. The checking of each invariant can be enabled or disabled by checking or unchecking its box.
Properties
 TLC can check if the behavior spec satisfies (implies) a temporal property, which is expressed as a temporallogic formula.
 You can specify a list of such properties, each with a checkbox for enabling or disabling its checking.
1.3. What values to substitute for constant parameters ?
The most basic part of a model is an assignment of values to declared constants. A model must specify the values of all declared constants. There are three wasy to assign a value to a constant:
Ordinary assignment
 You can set the value of the constant to any constant TLA+ expression that contains only symbols defined in the spec.
 The expression can even include declared constants, as long as the value assigned to a constant does not depend on that constant.
Model value

Ordinary Model Values

A model value is an unspecified value that TLC considers to be unequal to any value that youcan express in TLA+.

Since TLC cannot evaluate the unbounded $CHOOSE$ expression, to allow TLC to handle the follow spec, you need to substitute a model value for $NotANat$. $$NotANat = CHOOSE \enspace n : n \notin Nat$$
这条要注意！！！


Typed Model Values
 TLC considers a typed model value to be unequal to any other model value of the same type.
 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 oridinary model value
普通的 model value 和其他值做比较时，只会返回 FALSE，但有可能比较行为本身就是错误的。为了发现这类错误，可以使用 typed model value，其只允许相同类型的 model value 之间的比较行为。
 A modelvalue type consists of a single letter, so there are $52$ different types because
a
andA
are different types.  A model value has type
T
if and only if its name begins with the two charactersT_
.
Set of model values
An important resson for substituting a set of model value for constants is to len TLC take advantage of symmetry. A set is a symmetry set meaning that permuting the elements in the set of values does not change whether or not a behavior satisfies that behavior spec. TLC can take advantage of this to speed up its check.
 You can declare more than one set of model values to be a symmetry set. However, the union of all the symmetry sets cannot contain two typed model values with different types.
 TLC does not check if a set you declare to be a symmetry set really is one.
 The only TLA+ operator that can produce a nonsymmetric expression when applied to a symmetric expression is $CHOOSE$.
Symmetry sets should not be used when checking liveness properties. Doing so can make TLC fail to find errors, or to report nonexistent errors.
2. Options
2.1. Spec Options

Additional Definitions
 不想在 Spec 内部定义的 operators 可以置于此处

State Constraint
 Spec 的状态空间大多是无限延伸的，可于此处限制遍历的状态空间范围
 A state constraint is a state predicate, which is a Booleanvalued expression that contains unprimed variables.

Action Constraint
 An action constraint is much like a state constraint, except that the constraint formula may also include primed variables.

Model Values

Definition Override
 类似于 C 的 define 语句
 If the operator whose definition you are overriding has arguments, you will be presented with a form for writing the new definition in the obvious way.
 If it has no arguments, you have two options. With the Ordinary assignment option, you just write the new definition.
2.2. TLC Options
Configuration

Number of worker threads
 not set it to be greater than the number of separate processors

Fraction of physical memory allocated to TLC
 Setting the this parameter too large may produce a Could not create the Java virtual machine error.

Log base 2 of number of disk storage files
Checking Mode

Modelchecking mode
 This is the normal method of running TLC, in which it essentially tries to check all possible behaviors allowed by the behavior spec.

Simulation Mode
 It checks an unending series of behaviors, each of which it constructs by starting from a randomly choosen initial state and repeatedly making a random choice of a possible next state.
 When run in simulation mode, the only statistics TLC reports are for States Found.
Features

Checkpoint Recovery
 TLC takes regular checkpoints, from which it can be restarted if it is stopped for any reason.

Profiling
 TLC supports detailed profiling at the action as well as the expression level.
 Profiling negatively impacts model checking performance and should thus be off when checking large models.

Visualize state graph after completion
 Can reasonably display only state graphs with at most around a hundred states.
Parameters

Verrify temporal properties upon termination only
 check temporal properties(liveness) only after the complete state space has been checked for invariant(safety) violations

Fingerprint seed index
 TLC saves only 64bit fingerprints (hashes) of the reachable states that it finds, not the complete states.
 If two different reachable states have the same fingerprint, a situation called a collision, TLC may not find all reachable states.
 The fingerprint seed index specifies which of 64 fingerprint functions TLC should use.

Cardinality of largest enumerable set
 If TLC tries to enumerate the elements of a set, it will report an error if the set contains more than this number of elements.

JVM arguments

TLC command line parameters
 There are options given to TLC when it is run on the model.
 A complete list of TLC options can be found in TLC.java
3. Model Checking
3.1. How TLC is Run
The Toolbox runs TLC on a module named MC
that it constructs from the model. It writes the module file MC.tla
and the TLC configuration file MC.cfg
when validating the model.
3.2. Statistics
State space progress
This show a history of TLC’s reachable state space computation.
 Diameter: The diameter of the reachablestate graph. It is the length of the longest behavior found so far.
 States Found: The total number of states TLC has examined so far.
 Distinct States: The number of distinct states among the states found.
 Queue Size: The number of (distinct) states found whose successor states TLC has not yet determined.
SubActions of nextstate
 A common error in writing a behavior spec is for an action not to be enabled when it should be, so the spec cannot reach states that represent reachable states of the actual system being specified.
 This kind of error leads to a violation of desired liveness properties, but does not cause any violation of safety.
 SubActions of nextstate shows the number of states generated by each subaction of the nextstate relation.
 The action statistics give you a way of catching such an error even if you’re not checking liveness.