Whereas TLC enumerates the states produced by the behaviors of a TLA+ specification, Apalache translates the verification problem to a set of logical constraints. These constraints are solved by an SMT solver, for example, by Microsoft Z3. That is, Apalache operates on formulas (i.e., symbolically), not by enumerating states one by one (i.e., state enumeration).
Depending on the specification you wrote, either TLC or Apalache may be more efficient in checking it. While TLC is a mature tool, Apalache is still experimental, so be prepared to use the command-line and to help us discover bugs.
Apalache is working under the following assumptions:
- As in TLC, all specification parameters are fixed and finite, i.e., the system state is initialized with integers, finite sets, and functions of finite domains and co-domains.
- As in TLC, all data structures evaluated during an execution are finite, e.g., a system specification cannot operate on the set of all integers.
- Only finite executions of bounded length are analyzed.
Throughout this manual, we use the following conventions:
APALACHE_HOMEis used as shorthand for the path to a local copy of the Apalache source code.