Here is the list of the TLA+ language features that are currently supported by Apalache, following the Summary of TLA+.

Safety vs. Liveness

At the moment, Apalache is able to check state invariants, action invariants, trace invariants as well as inductive invariants. (See the page on invariants in the manual.) Which means that you can only check safety properties with Apalache, unless you employ a liveness-to-safety transformation in your spec. In general, we do not support checking liveness properties. If you would like to see liveness implemented, upvote the liveness feature.

Language

Module-Level constructs

ConstructSupported?MilestoneComment
EXTENDS moduleβœ”-A few standard modules are not supported yet (Bags)
CONSTANTS C1, C2βœ”-Either define a ConstInit operator to initialize the constants, use a .cfg file, or declare operators instead of constants, e.g., C1 == 111
VARIABLES x, y, zβœ”-
ASSUME Pβœ” / βœ–-Parsed, but not propagated to the solver
F(x1, ..., x_n) == expβœ” / βœ–-Every application of F is replaced with its body. Recursive operators need unrolling annotations. From 0.16.1 and later, for better performance and UX, use FoldSet and FoldSeq.
f[x ∈ S] == expβœ” / βœ–-Recursive functions are only supported if they return integers or Booleans. From 0.16.1 and later, for better performance and UX, use FoldSet and FoldSeq.
INSTANCE M WITH ...βœ” / βœ–-No special treatment for ~>, \cdot, ENABLED
N(x1, ..., x_n) == INSTANCE M WITH...βœ” / βœ–-Parameterized instances are not supported
THEOREM Pβœ” / βœ–-Parsed but not used
LOCAL defβœ”-Replaced with local LET-IN definitions

The constant operators

Logic

OperatorSupported?MilestoneComment
/\, \/, ~, =>, <=>βœ”-
TRUE, FALSE, BOOLEANβœ”-
\A x \in S: p, \E x \in S : pβœ”-
CHOOSE x \in S : pβœ–-Partial support prior to version 0.16.1. From 0.16.1 and later, use Some, FoldSet, or FoldSeq. See #841.
CHOOSE x : x \notin Sβœ–-Not supported. You can use records or a default value such as -1.
\A x : p, \E x : pβœ–-Use bounded quantifiers
CHOOSE x : pβœ–-

Sets

Note: only finite sets are supported. Additionally, existential quantification over Int and Nat is supported, as soon as it can be replaced with a constant.

OperatorSupported?MilestoneComment
=, /=, \in, \notin, \intersect, \union, \subseteq, \βœ”-
{e_1, ..., e_n}βœ”-
{x \in S : p}βœ”-
{e : x \in S}βœ”-
SUBSET Sβœ”-Sometimes, the powersets are expanded
UNION Sβœ”-Provided that S is expanded

Functions

OperatorSupported?MilestoneComment
f[e]βœ”-
DOMAIN fβœ”-
[ x \in S ↦ e]βœ”-
[ S -> T ]βœ”-Supported, provided the function can be interpreted symbolically
[ f EXCEPT ![e1] = e2 ]βœ”-

Records

Use type annotations to help the model checker in finding the right types. Note that our type system distinguishes records from general functions.

OperatorSupported?MilestoneComment
e.hβœ”-
r[e]βœ”/βœ–-Provided that e is a constant expression.
[ h1 ↦ e1, ..., h_n ↦ e_n]βœ”-
[ h1 : S1, ..., h_n : S_n]βœ”-
[ r EXCEPT !.h = e]βœ”-

Tuples

Use type annotations to help the model checker in finding the right types. Note that our type system distinguishes records from general functions.

OperatorSupported?MilestoneComment
e[i]βœ” / βœ–-Provided that i is a constant expression
<< e1, ..., e_n >>βœ”-Use a type annotation to distinguish between a tuple and a sequence.
S1 \X ... \X S_nβœ”-
[ t EXCEPT ![i] = e]βœ”/βœ–-Provided that i is a constant expression

Strings and numbers

ConstructSupported?MilestoneComment
"c1...c_n"βœ”-A string is always mapped to a unique uninterpreted constant
STRINGβœ–-It is an infinite set. We cannot handle infinite sets.
d1...d_nβœ”-As long as the SMT solver (Z3) accepts that large number
d1...d_n.d_n+1...d_mβœ–-Technical issue. We will implement it upon a user request.

Miscellaneous Constructs

ConstructSupported?MilestoneComment
IF p THEN e1 ELSE e2βœ”-Provided that both e1 and e2 have the same type
CASE p1 -> e1 [] ... [] p_n -> e_n [] OTHER -> eβœ”-Provided that e1, ..., e_n, e have the same type
CASE p1 -> e1 [] ... [] p_n -> e_nβœ”-Provided that e1, ..., e_n have the same type
LET d1 == e1 ... d_n == e_n IN eβœ”All applications of d1, ..., d_n are replaced with the expressions e1, ... e_n respectively. LET-definitions without arguments are kept in place.
multi-line /\ and \/βœ”-

The Action Operators

ConstructSupported?MilestoneComment
e'βœ”-
[A]_eβœ–-It does not matter for safety
< A >_eβœ–-
ENABLED Aβœ–-
UNCHANGED <<e_1, ..., e_k>>βœ”-Always replaced with e_1' = e_1 /\ ... /\ e_k' = e_k
A βˆ™ Bβœ–-

The Temporal Operators

The model checker assumes that the specification has the form Init /\ [][Next]_e. Given an invariant candidate Inv, the tool checks, whether Inv is violated by an execution whose length is bounded by the given argument.

Except the standard form Init /\ [][Next]_e, no temporal operators are supported.

Standard modules

Integers and Naturals

For the moment, the model checker does not differentiate between integers and naturals. They are all translated as integers in SMT.

OperatorSupported?MilestoneComment
+, -, *, <=, >=, <, >βœ”-These operators are translated into integer arithmetic of the SMT solver. Linear integer arithmetic is preferred.
\div, %βœ”-Integer division and modulo
a^bβœ” / βœ–-Provided a and b are constant expressions
a..bβœ” / βœ–-Sometimes, a..b needs a constant upper bound on the range. When Apalache complains, use {x \in A..B : a <= x /\ x <= b}, provided that A and B are constant expressions.
Int, Natβœ” / βœ–-Supported in \E x \in Nat: p and \E x \in Int: p, if the expression is not located under \A and ~. We also support assignments like f' \in [S -> Int] and tests f \in [S -> Nat]
/βœ–-Real division, not supported

Sequences

OperatorSupported?MilestoneComment
<<...>>, Head, Tail, Len, SubSeq, Append, \o, f[e]βœ”-The sequence constructor <<...>> needs a type annotation.
EXCEPTβœ–If you need it, let us know, issue #324
Seq(S)βœ–-Use Gen of Apalache to produce bounded sequences
SelectSeqβœ–-Planned in #873. Till then, use FoldSeq.

FiniteSets

OperatorSupported?MilestoneComment
IsFiniteβœ”-Always returns true, as all the supported sets are finite
Cardinalityβœ”-Try to avoid it, as Cardinality(S) produces O(n^2) constraints in SMT for cardinality n

TLC

OperatorSupported?MilestoneComment
a :> bβœ”-A singleton function <<a, b>>
f @@ gβœ”-Extends function f with the domain and values of function g but keeps the values of f where domains overlap
Other operatorsDummy definitions for spec compatibility

Reals

Not supported, not a priority