-
Notifications
You must be signed in to change notification settings - Fork 0
/
AJupiter.tla
85 lines (76 loc) · 3.39 KB
/
AJupiter.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
------------------------------ MODULE AJupiter ------------------------------
(*
Specification of the Jupiter protocol presented by Attiya et al.
*)
EXTENDS JupiterInterface, OT, BufferStateSpace
-----------------------------------------------------------------------------
VARIABLES
cbuf, \* cbuf[c]: buffer for locally generated operations at client c \in Client
crec, \* crec[c]: number of remote operations received by client c \in Client
\* since the last time a local operation was generated
sbuf, \* sbuf[c]: buffer for transformed remote operations w.r.t client c \in Client
srec \* srec[c]: number of locally generated operations by client c \in Client
\* since the last time a remote operation was transformed at the Server
vars == <<intVars, cbuf, crec, sbuf, srec>>
AJMsg ==
[c: Client, ack: Nat, op: Op \cup {Nop}] \cup \* messages sent to the Server from client c \in Client
[ack: Nat, op: Op \cup {Nop}] \* messages broadcast to Clients from the Server
-----------------------------------------------------------------------------
TypeOK ==
/\ TypeOKInt
/\ cbuf \in [Client -> Seq(Op \cup {Nop})]
/\ crec \in [Client -> Nat]
/\ sbuf \in [Client -> Seq(Op \cup {Nop})]
/\ srec \in [Client -> Nat]
-----------------------------------------------------------------------------
Init ==
/\ InitInt
/\ cbuf = [c \in Client |-> <<>>]
/\ crec = [c \in Client |-> 0]
/\ sbuf = [c \in Client |-> <<>>]
/\ srec = [c \in Client |-> 0]
-----------------------------------------------------------------------------
ClientPerform(c, m) ==
LET xform == xFormShift(OT, m.op, cbuf[c], m.ack) \* [xop, xops]
IN /\ cbuf' = [cbuf EXCEPT ![c] = xform.xops]
/\ crec' = [crec EXCEPT ![c] = @ + 1]
/\ SetNewAop(c, xform.xop)
ServerPerform(m) ==
LET c == m.c
xform == xFormShift(OT, m.op, sbuf[c], m.ack) \* [xop, xops]
xop == xform.xop
IN /\ srec' = [cl \in Client |-> IF cl = c THEN srec[cl] + 1 ELSE 0]
/\ sbuf' = [cl \in Client |-> IF cl = c THEN xform.xops
ELSE Append(sbuf[cl], xop)]
/\ SetNewAop(Server, xop)
/\ Comm!SSend(c, [cl \in Client |-> [ack |-> srec[cl], op |-> xop]])
-----------------------------------------------------------------------------
DoOp(c, op) ==
/\ SetNewAop(c, op)
/\ cbuf' = [cbuf EXCEPT ![c] = Append(@, op)]
/\ crec' = [crec EXCEPT ![c] = 0]
/\ Comm!CSend([c |-> c, ack |-> crec[c], op |-> op])
Do(c) ==
/\ DoInt(DoOp, c)
/\ UNCHANGED <<sbuf, srec>>
Rev(c) ==
/\ RevInt(ClientPerform, c)
/\ UNCHANGED <<sbuf, srec>>
SRev ==
/\ SRevInt(ServerPerform)
/\ UNCHANGED <<cbuf, crec>>
-----------------------------------------------------------------------------
Next ==
\/ \E c \in Client: Do(c) \/ Rev(c)
\/ SRev
Fairness ==
WF_vars(SRev \/ \E c \in Client: Rev(c))
Spec == Init /\ [][Next]_vars \* /\ Fairness
-----------------------------------------------------------------------------
QC == \* Quiescent Consistency
Comm!EmptyChannel => Cardinality(Range(state)) = 1
THEOREM Spec => []QC
=============================================================================
\* Modification History
\* Last modified Thu Jan 17 10:30:39 CST 2019 by hengxin
\* Created Satchins, Jun 23 17:14:18 CST 2018 by hengxin