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
HOWTOs
8.
Overview
9.
How to write type annotations
10.
How to use uninterpreted types
Apalache User Manual
11.
Getting Started
11.1.
Installation
11.1.1.
Prebuilt Packages
11.1.2.
Docker
11.1.3.
Build from Source
11.2.
Running the Tool
11.3.
An Example TLA+ Specification
11.4.
Specification Parameters
11.5.
Symbolic Model Checking with Apalache
11.5.1.
Assignments and symbolic transitions
11.5.2.
Folding sets and sequences
11.5.3.
Invariants: State, Action, Trace
11.5.4.
Enumeration of counterexamples
11.5.5.
The Apalache Module
11.5.6.
Naturals
11.6.
Apalache global configuration file
11.7.
TLA+ Execution Statistics
11.8.
Profiling Your Specification
11.9.
Five minutes of theory
12.
TLC Configuration Files
13.
The Snowcat Type Checker
14.
Supported Features
15.
Obsolete: Recursive operators and functions
16.
Known Issues
17.
Antipatterns
18.
TLA+ Preprocessing
19.
Fine Tuning
20.
Assignments and Symbolic Transitions in Depth
21.
KerA: kernel logic of actions
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.
Apalache extensions
24.1.
Apalache module
24.2.
Variants
24.3.
Option types
25.
User-defined operators
25.1.
Top-level operator definitions
25.2.
LET-IN definitions
25.3.
Higher-order operators definitions
25.4.
Anonymous operator definitions
25.5.
Local operator definitions
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.
RFC 001: types and type annotations
34.
ADR-002: types and type annotations
35.
ADR-003: transition executor (TRex)
36.
ADR-004: code annotations
37.
ADR-005: JSON Serialization Format
38.
RFC-006: unit tests and property-based tests
39.
ADR-007: restructuring
40.
ADR-008: exceptions
41.
ADR-009: outputs
42.
RFC-010: Implementation of Transition Exploration Server
43.
ADR-011: alternative SMT encoding using arrays
44.
ADR-012: Adopt an ADR Template
45.
ADR-013: Configuration Management Component
46.
ADR-014: Precise type inference for records and variants
47.
ADR-015: ITF: informal trace format
48.
ADR-016: ReTLA: Relational TLA
49.
PDR-017: Checking temporal properties
50.
ADR-018: Inlining in Apalache
51.
ADR-019: Harmonize changelog management
52.
ADR-020: Improving membership in arenas
53.
RFC-021: Prioritization of Work
54.
ADR-022: Unify Configuration Management and "Pass Options"
55.
ADR-023: Trace evaluation
56.
ADR-024: Arena computation isolation
Light (default)
Rust
Coal
Navy
Ayu
Apalache Documentation
Anonymous operator definitions
work in progress...
[Back to user operators]