# Apalache operators

In addition to the standard TLA+ operators described in the previous section, Apalache defines a number of operators, which do not belong to the core language of TLA+, but which Apalache uses to provide clarity, efficiency, or special functionality. These operators belong to the module Apalache, and can be used in any specification by declaring EXTENDS Apalache.

## Assigmnent

Notation: v' := e

LaTeX notation: Arguments: Two arguments. The first is a primed variable name, the second is arbitrary.

Apalache type: (a, a) => Bool, for some type a

Effect: The expression v' := e evaluates to v' = e. At the level of Apalache static analysis, such expressions indicate parts of an action, where the value of a state-variable in a successor state is determined. See here for more details about assignments in Apalache.

Determinism: Deterministic.

Errors: If the first argument is not a primed variable name, or if the assignment operator is used where assignments are prohibited, Apalache statically reports an error.

Example in TLA+:

x' := 1                   \* x' = 1
x' := (y = z)             \* x' = (y = z)
x' := (y' := z)           \* x' = (y' = z) in TLC, assignment error in Apalache
x' := 1 \/ x' := 2        \* x' = 1 \/ x' = 2
x' := 1 /\ x' := 2        \* FALSE in TLC, assignment error in Apalache
x' := 1 \/ x' := "a"      \* Type error in Apalache
(x' + 1) := 1             \* (x' + 1) = 1 in TLC, assignment error in Apalache
IF x' := 1 THEN 1 ELSE 0  \* Assignment error in Apalache


Example in Python:

>> a = 1          # a' := 1
>> a == 1         # a' = 1
True
>> a = b = "c"    # b' := "c" /\ a' := b'
>> a = (b == "c") # a' := (b = "c")


## Sequence cast

Notation: FunAsSeq(fn, maxLen)

LaTeX notation: FunAsSeq(fn, maxLen)

Arguments: Two arguments. The first is a function, the second is an integer.

Apalache type: (Int -> a, Int) => Seq(a), for some type a

Effect: The expression FunAsSeq(fn, maxLen) evaluates to the sequence << fn, ..., fn[maxLen] >>. At the level of Apalache static analysis, FunAsSeq indicates type-casting a function type Int -> a to a sequence type Seq(a), since one cannot use function constructors to define a sequence in Apalache otherwise.

Determinism: Deterministic.

Errors: If fn is not a function of the type Int -> a or if maxLen is not an integer, Apalache statically reports a type error. Additionally, if it is not the case that 1..maxLen \subseteq DOMAIN fn, the result is undefined.

Example in TLA+:

Head( [ x \in 1..5 |-> x * x ] )                \* 1 in TLC, type error in Apalache
FunAsSeq( [ x \in 1..5 |-> x * x ], 3 )         \* <<1,4,9>>
Head( FunAsSeq( [ x \in 1..5 |-> x * x ], 3 ) ) \* 1
FunAsSeq( <<1,2,3>>, 3 )                        \* <<1,2,3>> in TLC, type error in Apalache
FunAsSeq( [ x \in {0,42} |-> x * x ], 3 )       \* UNDEFINED


Example in Python:

def funAsSeq(f,imax):
# f === { x:f(x) | x \in Dom(f) }
return[f.get(i) for i in range(1,imax+1)]
def boundedFn(f, dom):
return { x:f(x) for x in dom }
f = boundedFn( lambda x: x*x, range(1,6) ) # [ x \in 1..5 |-> x * x ]
g = boundedFn( lambda x: x*x, {0,42} )     # [ x \in {0,42} |-> x * x ]
>>> f                                   # Head( [ x \in 1..5 |-> x * x ] )
1
>>> funAsSeq(f, 3)                         # FunAsSeq( [ x \in 1..5 |-> x * x ], 3 )
[1,4,9]
>>> funAsSeq(f, 3)                      # Head( FunAsSeq( [ x \in 1..5 |-> x * x ], 3 ) )
1
>>> funAsSeq( g, 3 )                       # FunAsSeq( [ x \in {0,42} |-> x * x ], 3 )
[None, None, None]


## Skolemization Hint

Notation: Skolem(e)

LaTeX notation: Skolem(e)

Arguments: One argument. Must be an expression of the form \E x \in S: P.

Apalache type: (Bool) => Bool

Effect: The expression Skolem(\E x \in S: P) provides a hint to Apalache, that the existential quantification may be skolemized. It evaluates to the same value as \E x \in S: P.

Determinism: Deterministic.

Errors: If e is not a Boolean expression, throws a type error. If it is Boolean, but not an existentially quantified expression, throws a StaticAnalysisException.

Note: This is an operator produced internally by Apalache. You may see instances of this operator, when reading the .tla side-outputs of various passes. Manual use of this operator is discouraged and, in many cases, not supported.

Example in TLA+:

Skolem( \E x \in {1,2}: x = 1 ) \* TRUE
Skolem( 1 )                     \* 1 in TLC, type error in Apalache
Skolem( TRUE )                  \* TRUE in TLC, error in Apalache


## Set expansion

Notation: Expand(S)

LaTeX notation: Expand(S)

Arguments: One argument. Must be either SUBSET SS or [T1 -> T2].

Apalache type: (Set(a)) => Set(a), for some a.

Effect: The expression Expand(S) provides instructions to Apalache, that the large set S (powerset or set of functions) should be explicitly constructed as a finite set, overriding Apalache's optimizations for dealing with such collections. It evaluates to the same value as S.

Determinism: Deterministic.

Errors: If e is not a set, throws a type error. If the expression is a set, but is not of the form SUBSET SS or [T1 -> T2], throws a StaticAnalysisException.

Note: This is an operator produced internally by Apalache. You may see instances of this operator, when reading the .tla side-outputs of various passes. Manual use of this operator is discouraged and, in many cases, not supported.

Example in TLA+:

Expand( SUBSET {1,2} ) \* {{},{1},{2},{1,2}}
Expand( {1,2} )        \* {1,2} in TLC, error in Apalache
Expand( 1 )            \* 1 in TLC, type error in Apalache


## Cardinality Hint

Notation: ConstCardinality(e)

LaTeX notation: ConstCardinality(e)

Arguments: One argument. Must be an expression of the form Cardinality(S) >= k.

Apalache type: (Bool) => Bool

Effect: The expression ConstCardinality(Cardinality(S) >= k) provides a hint to Apalache, that Cardinality(S) is a constant, allowing Apalache to encode the constraint e without attempting to dynamically encode Cardinality(S). It evaluates to the same value as e.

Determinism: Deterministic.

Errors: If S is not a Boolean expression, throws a type error. If it is Boolean, but not an existentially quantified expression, throws a StaticAnalysisException.

Note: This is an operator produced internally by Apalache. You may see instances of this operator, when reading the .tla side-outputs of various passes. Manual use of this operator is discouraged and, in many cases, not supported.

Example in TLA+:

Skolem( \E x \in {1,2}: x = 1 ) \* TRUE
Skolem( 1 )                     \* 1 in TLC, type error in Apalache
Skolem( TRUE )                  \* TRUE in TLC, error in Apalache


## Folding

The operators FoldSet and FoldSeq` are explained in more detail in a dedicated section here.