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 only able to check invariants and inductive invariants. 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 and Reals)
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.
f[x ∈ S] == expβœ” / βœ–-Recursive functions are only supported if they return integers or Booleans.
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βœ”/βœ–-Similar to TLC, we implement a non-deterministic choice. We will add a deterministic version in the future.
CHOOSE x : x \notin Sβœ–?That is a commonly used idiom
\A x : p, \E x : pβœ–NEVERUse the versions above
CHOOSE x : pβœ–NEVERUse the version above

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}βœ”-Empty sets {} require type annotations
{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 tuples 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
<<<<<<< Updated upstream
CASE p1 -> e1 [] ... [] p_n -> e_n [] OTHER -> eβœ”-See the comment above
CASE p1 -> e1 [] ... [] p_n -> e_nβœ”-
=======
CASE p1 -> e1 [] ... [] p_n -> e_n [] OTHER -> eβœ”-Provided that e1, ..., e_n have the same type
CASE p1 -> e1 [] ... [] p_n -> e_nβœ”-Provided that e1, ..., e_n have the same type
>>>>>>> Stashed changes
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)βœ–-If you need it, let us know, issue #314
SelectSeqβœ–-will not be supported in the near future

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
f @@ a :> bβœ”-Extends the function relation with the pair <<a, b>>

Reals

Not supported, not a priority