TLA+ wiki

Modules #

  • Integers
  • Naturals
  • Reals
  • Sequences
  • TLC – print
  • Bags are multi-set functions, each element points to an integer as its quntity. Defines operators: (+) (-)
  • FiniteSets defines IsFiniteSet(S) and Cardinality(S).
  • RealTime – RTBound RTnow now

Definition #

<A>_v == A /\ (v' # v)

$$\langle A \rangle_v == A \land (v’ \neq v)$$

[A]_v == A \/ (v' = 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) \Rightarrow (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(@)
    };
}