TLA+ wiki

Modules:

• Integers
• Naturals
• Reals
• Sequences
• TLC -- print
• Bags -- (+) (-)
• FiniteSets
• RealTime -- RTBound RTnow now

Definition:
$<A>_v$ == $A \land (v' \neq v)$
$[A]_v$ == $A \lor (v'=v)$

Operators:

Divides (p, n) == $\exists q \in Int : n = q * p$

DivisorsOf (n) == {$p \in Int$ : Divides(p, n)}

SetMax (S) == CHOOSE $i \in S$ : $\forall j \in S$ : $i \geq j$

GCD (m, n) == SetMax(DivisorsOf(m) $\cap$ DivisorsOf(n))

SetGCD(T) == SetMax( {$d \in Int$ : $\forall t \in T$ : Divides(d, t)} )

max(x, y) == IF x>y THEN x ELSE y
min(x, y) == IF x<y THEN x ELSE y

maxv(x, y) == [$i \in$ DOMAIN x |-> max(x[i], y[i])]

Cardinality(set)

SortSeq(s, <)

Len(s)

Head(s)

Tail(s)

Append(s,e)

Seq(s)

SubSeq(s, m, n)

SelectSeq(s, op)

successor[$i \in Nat$] == i+1

successor == [$i \in Nat$ |-> i+1]

factorial[$n \in Nat$] == IF n = 0 THEN 1 ELSE n * factorial[n-1]

RECURSIVE FactorialOp(_)

FactorialOp(n) == IF n=0 THEN 1 ELSE n * Factorial(n-1)

RECURSIVE Cardinality(_)

Cardinality(S) == IF S={} THEN 0 ELSE 1+Cardinality(S \ {CHOOSE $x \in S$ : TRUE})

Sortings(S) == LET D == 1..Cardinality(S) 
IN {$seq \in [D \to S] : $
$\land S \subseteq \{seq[i] : i \in D\}$
$\land \forall i,j \in D : (i<j) \implies (seq[i].key \leq seq[j].key)$}

RECURSIVE SetSum(_)
SetSum(S) == IF S={} THEN 0 ELSE LET s==CHOOSE $x \in S$ : TRUE IN s + SetSum(S \ {s})

RECURSIVE SeqSum(_)
SeqSum(s) == IF s=<<>> THEN 0 ELSE Head(s) + SeqSum(Tail(s))

Network:

variable network = [from $\in 1..N$ |-> [to $\in 1..N$ |-> <<>>]];

define

{

    send(from, to, msg) == [network EXCEPT ![from][to] = Append(@, msg)]

    bcast(from, msg) == [network EXCEPT ![from] = [to $\in 1..N$ |-> Append(network[from][to], msg)]]

}

macro rcv()

{

    with (from $\in$ {$j \in 1..N$ : Len(network[j][self]) > 0}) {

        msg := Head(network[from][self]);

        network[from][self] := Tail(@)

    };

}