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 or INSTANCE 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 next-state 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 next-state 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 next-state 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 temporal-logic formula.
  • You can specify a list of such properties, each with a check-box 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 model-value type consists of a single letter, so there are $52$ different types because a and A are different types.
    • A model value has type T if and only if its name begins with the two characters T_.

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 non-symmetric 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 Boolean-valued 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

  • Model-checking 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 64-bit 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 reachable-state 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.

Sub-Actions of next-state

  • 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.
  • Sub-Actions of next-state shows the number of states generated by each sub-action of the next-state relation.
  • The action statistics give you a way of catching such an error even if you’re not checking liveness.