Modules:
- Integers
- Naturals
- Reals
- Sequences
- TLC -- print
- Bags -- (+) (-)
- FiniteSets
- RealTime -- RTBound RTnow now
$<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
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))
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(@)
};
}
