Overview
Tutorials
1.
Overview
2.
Entry-level Model Checker Tutorial
3.
Type Checker Tutorial
4.
Checking Pluscal specifications
5.
Apalache trail tips: how to check your specs faster
6.
Symbolic Model Checking
7.
Specifying temporal properties and understanding counterexamples
Apalache User Manual
8.
Getting Started
8.1.
Installation
8.1.1.
Prebuilt Packages
8.1.2.
Docker
8.1.3.
Build from Source
8.2.
Running the Tool
8.3.
An Example TLA+ Specification
8.4.
Specification Parameters
8.5.
Symbolic Model Checking with Apalache
8.5.1.
Assignments and symbolic transitions
8.5.2.
Folding sets and sequences
8.5.3.
Invariants: State, Action, Trace
8.5.4.
Enumeration of counterexamples
8.5.5.
The Apalache Module
8.5.6.
Naturals
8.6.
Apalache global configuration file
8.7.
TLA+ Execution Statistics
8.8.
Profiling Your Specification
8.9.
Five minutes of theory
9.
TLC Configuration Files
10.
The Snowcat Type Checker
11.
Supported Features
12.
Obsolete: Recursive operators and functions
13.
Known Issues
14.
Antipatterns
15.
TLA+ Preprocessing
16.
Fine Tuning
17.
Assignments and Symbolic Transitions in Depth
18.
KerA: kernel logic of actions
HOWTOs
19.
Overview
20.
How to write type annotations
21.
How to use uninterpreted types
TLA+ Language Manual for Engineers
22.
Introduction
23.
The standard operators of TLA+
23.1.
Booleans
23.2.
Control And Nondeterminism
23.3.
Conditionals
23.4.
Integers
23.5.
Sets
23.6.
Logic
23.7.
Functions
23.8.
Records
23.9.
Tuples
23.10.
Sequences
23.11.
Bags
24.
User-defined operators
24.1.
Top-level operator definitions
24.2.
LET-IN definitions
24.3.
Higher-order operators definitions
24.4.
Anonymous operator definitions
24.5.
Local operator definitions
25.
Apalache operators
26.
Modules, Extends, and Instances
Idiomatic TLA+
27.
Introduction
28.
Keep state variables to the minimum
29.
Update state variables with assignments
30.
Apply primes only to state variables
31.
Use Boolean operators in actions, not IF-THEN-ELSE
32.
Avoid sets of mixed records
Design Documents
33.
ADR-002: types and type annotations
34.
ADR-003: transition executor (TRex)
35.
ADR-004: code annotations
36.
ADR-005: JSON Serialization Format
37.
RFC-006: unit tests and property-based tests
38.
ADR-007: restructuring
39.
ADR-008: exceptions
40.
ADR-009: outputs
41.
ADR-011: alternative SMT encoding using arrays
42.
ADR-015: ITF: informal trace format
43.
ADR-016: ReTLA: Relational TLA
44.
PDR-017: Checking temporal properties
45.
ADR-018: Inlining in Apalache
46.
ADR-020: Improving membership in arenas
Light (default)
Rust
Coal
Navy
Ayu
Apalache Documentation
Anonymous operator definitions
work in progress...
[Back to user operators]