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.
Folding Operators
3.13.
Profiling Your Specification
3.14.
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.
Apalache operators
20.
Modules, Extends, and Instances
Idiomatic TLA+
21.
Introduction
22.
Keep state variables to the minimum
23.
Update state variables with assignments
24.
Apply primes only to state variables
25.
Avoid sets of mixed records
Design Documents
26.
ADR-002: types and type annotations
27.
ADR-003: transition executor (TRex)
28.
ADR-004: code annotations
29.
ADR-005: JSON Serialization Format
30.
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]