-
Notifications
You must be signed in to change notification settings - Fork 201
/
MCEcho.tla
36 lines (31 loc) · 1.01 KB
/
MCEcho.tla
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
---------- MODULE MCEcho ----------
EXTENDS Echo
\* A tiny graph with three nodes.
N1 == {"a", "b", "c"}
\* We don't care which node gets
\* picked as the initiator.
I1 == CHOOSE n \in N1 : TRUE
\* The tiny graph is fully meshed:
\* <<"a", "a">> :> FALSE @@
\* <<"a", "b">> :> TRUE @@
\* <<"b", "a">> :> TRUE @@
\* <<"b", "b">> :> FALSE @@
\* <<"a", "c">> :> TRUE @@
\* <<"c", "a">> :> TRUE @@
\* <<"b", "c">> :> TRUE @@
\* <<"c", "b">> :> TRUE @@
\* <<"c", "c">> :> FALSE
\* More concisely defined as:
R1 == [ edge \in (N1 \X N1) |-> IF edge[1] = edge[2]
THEN FALSE
ELSE TRUE ]
\* To get a graph that satisfies the
\* assumptions in Echo, we simply
\* define R to be:
R2 == CHOOSE r \in [ N1 \X N1 -> BOOLEAN ] :
/\ IsConnected(r, N1)
/\ IsSymmetric(r, N1)
/\ IsIrreflexive(r, N1)
\* Print R to stdout at startup.
TestSpec == PrintT(R) /\ Spec
===================================