Apalache Documentation

Shai (Server for Human-Apalache Interaction) is a component of Apalache designed to support human interaction with the symbolic model checker. It provides a server-based interface for clients to interact with Apalache's core logic.

One of its primary services is TransEX, which allows users to interactively drive the Apalache TransitionExecutor via Remote Procedure Calls (RPCs).

The Apalache documentation is organized into five distinct sections depending on your needs:

• Apalache User Manual: Core operational guidance including Installation, Running the Tool, and Fine Tuning.
• Apalache Tutorials: Step-by-step guides for learning the tool.
• Apalache HOWTOs: Practical solutions for specific tasks.
• TLA+ Language Reference Manual: Detailed technical specifications of the TLA+ language.
• Guidelines for Idiomatic TLA+: Best practices for writing clean and effective TLA+ code.

To effectively use Apalache's symbolic model checking capabilities, TLA+ specifications must be written following specific principles. A critical requirement is the use of type annotations for all variables and constants.

For guidance on implementing these principles, refer to the following core topics:

• Assignments and symbolic transitions: How to structure state changes.
• Folding sets and sequences: Techniques for handling collections.
• Invariants (State, Action, Trace): Defining properties to check.
• Enumeration of counterexamples: Understanding how Apalache presents violations.
• The Apalache Module: Using the specialized Apalache module.
• Naturals module: Using the specialized Naturals module.

Apalache supports several modes of execution depending on your goal:

• parse: Reads a TLA+ specification and flattens it by instantiating all modules. Terminates if there are no parse errors.
• typecheck: Performs parse and runs the Snowcat type checker to infer types of all expressions.
• simulate: Performs typecheck and runs the model checker in simulation mode. It randomly picks a sequence of actions and checks invariants for that subset of executions. This is typically much faster than the check command.
• check: Performs typecheck and runs bounded model checking. It checks invariants for all executions up to the length specified by --length.
• test: Performs check in a mode designed to test a single action.

$ apalache-mc --help

Relational TLA (reTLA) is a severely restricted fragment of TLA+ supported by Apalache. It covers uninterpreted first-order logic and is designed to allow for a more direct and efficient encoding compared to standard TLA+.

Key Benefits

• Simplified Encoding: Avoids the complex SMT encodings required for standard TLA+ data structures (like sets, records, and sequences) and the need for 'arena' bookkeeping.
• Standalone Constraints: Running Apalache with reTLA encoding skips the model-checking pass and instead produces a standalone file containing all generated constraints. This file can be consumed by other tools or alternative backend solvers (e.g., IVy or VMT).
• Performance: By rewriting specifications to use predicates (functions) instead of complex data structures, users can achieve more efficient SMT encodings.

The Informal Trace Format (ITF) is a simplified JSON-based format used by Apalache and Quint to represent counterexamples (traces). Unlike the standard TLA+ or Apalache IR serialization, ITF is designed to be easily readable by engineers unfamiliar with TLA+ and simple for external tools to parse.

Traces in ITF represent executions in two possible shapes:

1. Finite execution: A simple sequence of states.
2. Lasso execution: A finite sequence of states (the prefix) followed by an infinitely repeated sequence of states (the loop).

Each state in a trace is a mapping from variable names to expressions. These expressions use a minimal subset of TLA operators, including integer/string literals, set/sequence/record constructors, and the function operators :> and @@.

You can express types in TLA+ using native set membership (\in) syntax. This is known as the TypeOK style. Common patterns include:

• Integers: x \in Int
• Functions: f \in [Int -> Int]
• Subsets: f \in [SUBSET Int -> SUBSET Int]
• Records: r \in [a: Int, b: STRING]
• Tuples: f \in SUBSET [Int \X Int -> Int]
• Higher-order operators: Use THEOREM to define the type of an operator.

Example of a higher-order operator type definition:

THEOREM BarType ==
  ASSUME NEW G(_,_),
         \A x \in Int, y \in STRING : G(x,y) \in Int
         PROVE  Bar(G) \in BOOLEAN

THEOREM FooType ==
  \A a \in Int: \A b \in STRING: Foo(a, b) \in Int

When writing TLA+ specifications for use with Apalache, you will typically encounter two patterns for using records:

1. Plain Records: Records with a fixed, consistent set of fields that are passed around. The type checker expects these to have the same shape.
2. Variants (Discriminated Unions): Records of different shapes collected in a single set. These are distinguished by a special field called a discriminator (commonly named type). This pattern is frequently used in protocols like Paxos or Raft to represent different types of messages (e.g., Prepare, Promise, Accept) within a single set of messages.

Precise type inference for these patterns helps prevent spurious counterexamples caused by accessing fields that do not exist in certain variants of a record.