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 : pNEVERUse the versions above
CHOOSE x : pNEVERUse 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 eAll 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.
EXCEPTIf 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