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.
Invariants: State, Action, Trace
3.6.
Enumeration of counterexamples
3.7.
TLA+ Execution Statistics
3.8.
An Example TLA+ Specification
3.9.
Specification Parameters
3.10.
Principles of Symbolic Model Checking with Apalache
3.11.
The Apalache Module
3.12.
Profiling Your Specification
3.13.
Five minutes of theory
4.
TLC Configuration Files
5.
The Snowcat Type Checker
6.
Supported Features
7.
Known Issues
8.
TLA+ Preprocessing
9.
Fine Tuning
10.
KerA: kernel logic of actions
11.
Assignments in Apalache
HOWTOs
12.
Overview
13.
How to write type annotations
Tutorials
14.
Overview
15.
The Snowcat❄🐱 Type Checker
TLA+ Language Manual for Engineers
16.
Introduction
17.
The standard operators of TLA+
17.1.
Booleans
17.2.
Control And Nondeterminism
17.3.
Conditionals
17.4.
Integers
17.5.
Sets
17.6.
Logic
17.7.
Functions
17.8.
Records
17.9.
Tuples
17.10.
Sequences
17.11.
Bags
18.
User-defined operators
18.1.
Top-level operator definitions
18.2.
LET-IN definitions
18.3.
Higher-order operators definitions
18.4.
Anonymous operator definitions
18.5.
Recursive operator definitions
18.6.
Local operator definitions
18.7.
Recursive functions
19.
Modules, Extends, and Instances
Idiomatic TLA+
20.
Introduction
21.
Keep state variables to the minimum
22.
Update state variables with assignments
23.
Apply primes only to state variables
Design Documents
24.
ADR-002: types and type annotations
25.
ADR-003: transition executor (TRex)
26.
ADR-004: code annotations
27.
ADR-005: JSON Serialization Format
28.
RFC-006: unit tests and property-based tests
Light (default)
Rust
Coal
Navy
Ayu
Apalache Documentation
Anonymous operator definitions
work in progress...
[Back to user operators]