-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathRGA.tla
113 lines (102 loc) · 4.86 KB
/
RGA.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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
-------------------------------- MODULE RGA --------------------------------
EXTENDS Integers, Sequences, Naturals, TLC, InsertTree
CONSTANTS Read(_), InitMsg
-----------------------------------------------------------------------------
VARIABLES
tree,
tomb,
insbuf,
tombbuf,
chins, \* varialble for checking list specification
(* variables for network: *)
incoming, \* incoming[r]: incoming channel at replica r \in Replica
lmsg, \* lmsg[r]: the last message delivered at r \in Replica to the upper-layer protocol
vc, \* vc[r][s] denotes the latest message from s \in Replica observed by r \in Replica
(* variables for correctness: *)
doset, \* doset[r]: the set of updates generated by replica r \in Replica
delset, \* uset[r]: the set of updates delivered by replica r \in Replica
uincoming, \* uincoming[r]: incoming channel for broadcasting/delivering updates at r \in Replica
buset \* buset[r]: the buffer of local updates made by r \in Replica since the last broadcast
nVars == <<incoming, lmsg, vc>>
cVars == <<doset, delset, uincoming, buset>>
vars == <<tree, tomb, insbuf, tombbuf, chins, seq, nVars, cVars>>
-----------------------------------------------------------------------------
Msg == [r : Replica, tombbuf : SUBSET node, insbuf : SUBSET Char]
List == Seq(Char)
RECURSIVE maxtime(_, _)
maxtime(tr, curmax) == IF tr = {} THEN curmax
ELSE LET t == CHOOSE x \in tr: TRUE
IN maxtime(tr\{t}, Nummax((t.ts).time, curmax))
Network == INSTANCE ReliableCausalNetwork \* WITH incoming <- incoming, lmsg <- lmsg, vc <- vc
ReadRGA(r) == Readtree2list(tree[r],"o",tomb[r],{}) \* read the state of r\in Replica
Correctness == INSTANCE OpCorrectness
\* WITH doset <- doset, delset <- delset, uincoming <- uincoming, buset <- buset
-----------------------------------------------------------------------------
TypeOK ==
/\ tree \in [Replica -> SUBSET node]
/\ tomb \in [Replica -> SUBSET Char]
/\ insbuf \in [Replica -> SUBSET node]
/\ tombbuf \in [Replica -> SUBSET Char]
/\ chins \in SUBSET Char
-----------------------------------------------------------------------------
Init ==
/\ tree = [r \in Replica |-> {}]
/\ tomb = [r \in Replica |-> {}]
/\ insbuf = [r \in Replica |-> {}]
/\ tombbuf = [r \in Replica |-> {}]
/\ chins = Char
/\ IntInit
/\ Network!RCNInit
/\ Correctness!OpCInit
DoIns(r) == \* r\in Replica generates an insert operation
\E ins \in node:
/\ ins.parent \in Readtree2set(tree[r]) \cup {"o"}
/\ ins.ts = [r |-> r, time |-> maxtime(tree[r], 1)]
/\ ins.ch \in chins
/\ chins' = chins \ {ins.ch}
/\ tree' = [tree EXCEPT![r] = @ \cup {ins}]
/\ insbuf' = [insbuf EXCEPT![r] = @ \cup {ins}]
/\ IntDo(r)
/\ Correctness!OpCDo(r)
/\ UNCHANGED <<tomb, tombbuf, nVars>>
DoDel(r) == \* r\in Replica generates a delete operation
\E del \in Char:
/\ del \in Readtree2set(tree[r])
/\ ~ del \in tomb[r]
/\ tomb' = [tomb EXCEPT ![r] = @ \cup {del}]
/\ tombbuf' = [tombbuf EXCEPT ![r] = @ \cup {del}]
/\ IntDo(r)
/\ Correctness!OpCDo(r)
/\ UNCHANGED <<tree, insbuf, chins, nVars>>
Do(r) ==
\/ DoIns(r)
\/ DoDel(r)
-----------------------------------------------------------------------------
Send(r) ==
/\ \/ tombbuf[r] # {}
\/ insbuf[r] # {}
/\ Network!RCNBroadcast(r, [aid |-> [r |-> r, seq |-> seq[r]],
tombbuf |-> tombbuf[r], insbuf |-> insbuf[r]])
/\ IntSend(r)
/\ Correctness!OpCSend(r)
/\ tombbuf' = [tombbuf EXCEPT ![r] = {}]
/\ insbuf' = [insbuf EXCEPT![r] = {}]
/\ UNCHANGED <<chins, tree, tomb>>
Deliver(r) ==
/\IntDeliver(r)
/\Network!RCNDeliver(r)
/\Correctness!OpCDeliver(r, lmsg'[r].aid)
/\ tree' = [tree EXCEPT![r] = @ \cup lmsg'[r].insbuf]
/\ tomb' = [tomb EXCEPT ![r] = @ \cup lmsg'[r].tombbuf]
/\ UNCHANGED <<chins, seq, tombbuf, insbuf>>
-----------------------------------------------------------------------------
Next == \E r \in Replica: Do(r) \/ Send(r) \/ Deliver(r)
Fairness == \A r \in Replica: WF_vars(Send(r)) /\ WF_vars(Deliver(r))
Spec == Init /\ [][Next]_vars /\ Fairness
=============================================================================
\* Modification History
\* Last modified Wed Oct 23 22:53:25 CST 2019 by JYwellin
\* Last modified Fri May 31 21:33:29 CST 2019 by xhdn
\* Last modified Mon May 06 16:52:19 CST 2019 by jywellin
\* Last modified Thu Jan 10 15:34:04 CST 2019 by jywellins
\* Created Tue Nov 06 15:55:23 CST 2018 by xhdn