Overview
Tutorials
1.
Type Checker Tutorial
Apalache User Manual
2.
Introduction
3.
Getting Started
3.1.
Shall I use Apalache or TLC?
3.2.
System Requirements
3.3.
Installation
3.3.1.
Prebuilt Packages
3.3.2.
Docker
3.3.3.
Source
3.4.
Running the Tool
3.5.
An Example TLA+ Specification
3.6.
Specification Parameters
3.7.
Symbolic Model Checking with Apalache
3.7.1.
Assignments and symbolic transitions
3.7.2.
Folding sets and sequences
3.7.3.
Invariants: State, Action, Trace
3.7.4.
Enumeration of counterexamples
3.7.5.
The Apalache Module
3.7.6.
Recursive operators and functions
3.7.7.
Naturals
3.8.
Apalache global configuration file
3.9.
TLA+ Execution Statistics
3.10.
Profiling Your Specification
3.11.
Five minutes of theory
4.
TLC Configuration Files
5.
The Snowcat Type Checker
6.
Supported Features
7.
Known Issues
8.
Antipatterns
9.
TLA+ Preprocessing
10.
Fine Tuning
11.
Assignments and Symbolic Transitions in Depth
12.
KerA: kernel logic of actions
HOWTOs
13.
Overview
14.
How to write type annotations
15.
How to use uninterpreted types
Tutorials
16.
Overview
17.
The Snowcat❄🐱 Type Checker
18.
Symbolic Model Checking
TLA+ Language Manual for Engineers
19.
Introduction
20.
The standard operators of TLA+
20.1.
Booleans
20.2.
Control And Nondeterminism
20.3.
Conditionals
20.4.
Integers
20.5.
Sets
20.6.
Logic
20.7.
Functions
20.8.
Records
20.9.
Tuples
20.10.
Sequences
20.11.
Bags
21.
User-defined operators
21.1.
Top-level operator definitions
21.2.
LET-IN definitions
21.3.
Higher-order operators definitions
21.4.
Anonymous operator definitions
21.5.
Recursive operator definitions
21.6.
Local operator definitions
21.7.
Recursive functions
22.
Apalache operators
23.
Modules, Extends, and Instances
Idiomatic TLA+
24.
Introduction
25.
Keep state variables to the minimum
26.
Update state variables with assignments
27.
Apply primes only to state variables
28.
Avoid sets of mixed records
Design Documents
29.
ADR-002: types and type annotations
30.
ADR-003: transition executor (TRex)
31.
ADR-004: code annotations
32.
ADR-005: JSON Serialization Format
33.
RFC-006: unit tests and property-based tests
34.
ADR-007: restructuring
35.
ADR-008: exceptions
36.
ADR-009: outputs
37.
ADR-011: alternative SMT encoding using arrays
38.
ADR-015: ITF: informal trace format
39.
ADR-016: Uninterpreted first-order logic fragment encoding
Light (default)
Rust
Coal
Navy
Ayu
Apalache Documentation
Anonymous operator definitions
work in progress...
[Back to user operators]