-
Notifications
You must be signed in to change notification settings - Fork 7
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Wei-jupiter-tla: code formatting, see Issue #49; TypeOK models fixed …
…for CONSTANT Msg
- Loading branch information
hengxin
committed
Jan 3, 2019
1 parent
6ebfd3a
commit 47a7bb8
Showing
97 changed files
with
2,467 additions
and
1,722 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
126 changes: 49 additions & 77 deletions
126
tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AJupiter.toolbox/TypeOK/AJupiter.tla
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,119 +1,91 @@ | ||
| ------------------------------ MODULE AJupiter ------------------------------ | ||
| (* | ||
| Specification of the Jupiter protocol presented by Hagit Attiya and others. | ||
| Specification of the Jupiter protocol presented by Attiya et al. | ||
| *) | ||
| EXTENDS JupiterInterface | ||
| ----------------------------------------------------------------------------- | ||
| (* | ||
| Messages between the Server and the Clients. | ||
| *) | ||
| Msg == [c: Client, ack: Int, op: Op \cup {Nop}] \cup \* messages sent to the Server from a client c \in Client | ||
| [ack: Int, op: Op \cup {Nop}] \* messages broadcast to Clients from the Server | ||
| ----------------------------------------------------------------------------- | ||
| VARIABLES | ||
| cbuf, \* cbuf[c]: buffer (of operations) at the client c \in Client | ||
| crec, \* crec[c]: the number of new messages have been received by the client c \in Client | ||
| \* since the last time a message was sent | ||
| sbuf, \* sbuf[c]: buffer (of operations) at the Server, one per client c \in Client | ||
| srec \* srec[c]: the number of new messages have been ..., one per client c \in Client | ||
| 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 | ||
| /\ Comm(Msg)!TypeOK | ||
| /\ cbuf \in [Client -> Seq(Op \cup {Nop})] | ||
| /\ crec \in [Client -> Int] | ||
| /\ crec \in [Client -> Nat] | ||
| /\ sbuf \in [Client -> Seq(Op \cup {Nop})] | ||
| /\ srec \in [Client -> Int] | ||
| /\ srec \in [Client -> Nat] | ||
| ----------------------------------------------------------------------------- | ||
| Init == | ||
| /\ InitInt | ||
| /\ Comm(Msg)!Init | ||
| /\ cbuf = [c \in Client |-> <<>>] | ||
| /\ crec = [c \in Client |-> 0] | ||
| /\ sbuf = [c \in Client |-> <<>>] | ||
| /\ srec = [c \in Client |-> 0] | ||
| ----------------------------------------------------------------------------- | ||
| (* | ||
| Client c \in Client issues an operation op. | ||
| *) | ||
| ClientPerform(c, m) == | ||
| LET cBuf == cbuf[c] | ||
| cShiftedBuf == SubSeq(cBuf, m.ack + 1, Len(cBuf)) | ||
| xop == XformOpOps(Xform, m.op, cShiftedBuf) | ||
| xcBuf == XformOpsOp(Xform, cShiftedBuf, m.op) | ||
| IN /\ cbuf' = [cbuf EXCEPT ![c] = xcBuf] | ||
| /\ crec' = [crec EXCEPT ![c] = @ + 1] | ||
| /\ SetNewAop(c, xop) | ||
|
|
||
| ServerPerform(m) == | ||
| LET c == m.c | ||
| cBuf == sbuf[c] | ||
| cShiftedBuf == SubSeq(cBuf, m.ack + 1, Len(cBuf)) | ||
| xop == XformOpOps(Xform, m.op, cShiftedBuf) | ||
| xcBuf == XformOpsOp(Xform, cShiftedBuf, m.op) | ||
| IN /\ srec' = [cl \in Client |-> | ||
| IF cl = c THEN srec[cl] + 1 ELSE 0] | ||
| /\ sbuf' = [cl \in Client |-> | ||
| IF cl = c THEN xcBuf ELSE Append(sbuf[cl], xop)] | ||
| /\ SetNewAop(Server, xop) | ||
| /\ Comm!SSend(c, [cl \in Client |-> [ack |-> srec[cl], op |-> xop]]) | ||
| ----------------------------------------------------------------------------- | ||
| DoOp(c, op) == | ||
| /\ state' = [state EXCEPT ![c] = Apply(op, @)] | ||
| /\ SetNewAop(c, op) | ||
| /\ cbuf' = [cbuf EXCEPT ![c] = Append(@, op)] | ||
| /\ crec' = [crec EXCEPT ![c] = 0] | ||
| /\ Comm(Msg)!CSend([c |-> c, ack |-> crec[c], op |-> op]) | ||
|
|
||
| DoIns(c) == | ||
| \E ins \in {op \in Ins: op.pos \in 1 .. (Len(state[c]) + 1) /\ op.ch \in chins /\ op.pr = Priority[c]}: | ||
| /\ DoOp(c, ins) | ||
| /\ chins' = chins \ {ins.ch} \* We assume that all inserted elements are unique. | ||
|
|
||
| DoDel(c) == | ||
| \E del \in {op \in Del: op.pos \in 1 .. Len(state[c])}: | ||
| /\ DoOp(c, del) | ||
| /\ UNCHANGED chins | ||
| /\ Comm!CSend([c |-> c, ack |-> crec[c], op |-> op]) | ||
|
|
||
| Do(c) == | ||
| /\ \/ DoIns(c) | ||
| \/ DoDel(c) | ||
| /\ DoInt(DoOp, c) | ||
| /\ UNCHANGED <<sbuf, srec>> | ||
| (* | ||
| Client c \in Client receives a message from the Server. | ||
| *) | ||
|
|
||
| Rev(c) == | ||
| /\ Comm(Msg)!CRev(c) | ||
| /\ crec' = [crec EXCEPT ![c] = @ + 1] | ||
| /\ LET m == Head(cincoming[c]) | ||
| cBuf == cbuf[c] \* the buffer at client c \in Client | ||
| cShiftedBuf == SubSeq(cBuf, m.ack + 1, Len(cBuf)) \* buffer shifted | ||
| xop == XformOpOps(Xform, m.op, cShiftedBuf) \* transform op vs. shifted buffer | ||
| xcBuf == XformOpsOp(Xform, cShiftedBuf, m.op) \* transform shifted buffer vs. op | ||
| IN /\ cbuf' = [cbuf EXCEPT ![c] = xcBuf] | ||
| /\ state' = [state EXCEPT ![c] = Apply(xop, @)] \* apply the transformed operation xop | ||
| /\ UNCHANGED <<chins, sbuf, srec>> | ||
| (* | ||
| The Server receives a message. | ||
| *) | ||
| /\ RevInt(ClientPerform, c) | ||
| /\ UNCHANGED <<sbuf, srec>> | ||
|
|
||
| SRev == | ||
| /\ Comm(Msg)!SRev | ||
| /\ LET m == Head(sincoming) \* the message to handle with | ||
| c == m.c \* the client c \in Client that sends this message | ||
| cBuf == sbuf[c] \* the buffer at the Server for client c \in Client | ||
| cShiftedBuf == SubSeq(cBuf, m.ack + 1, Len(cBuf)) \* buffer shifted | ||
| xop == XformOpOps(Xform, m.op, cShiftedBuf) \* transform op vs. shifted buffer | ||
| xcBuf == XformOpsOp(Xform, cShiftedBuf, m.op) \* transform shifted buffer vs. op | ||
| IN /\ srec' = [cl \in Client |-> | ||
| IF cl = c | ||
| THEN srec[cl] + 1 \* receive one more operation from client c \in Client | ||
| ELSE 0] \* reset srec for other clients than c \in Client | ||
| /\ sbuf' = [cl \in Client |-> | ||
| IF cl = c | ||
| THEN xcBuf \* transformed buffer for client c \in Client | ||
| ELSE Append(sbuf[cl], xop)] \* store transformed xop into other clients' bufs | ||
| /\ state' = [state EXCEPT ![Server] = Apply(xop, @)] \* apply the transformed operation | ||
| /\ Comm(Msg)!SSend(c, [cl \in Client |-> [ack |-> srec[cl], op |-> xop]]) | ||
| /\ UNCHANGED <<chins, cbuf, crec>> | ||
| /\ SRevInt(ServerPerform) | ||
| /\ UNCHANGED <<cbuf, crec>> | ||
| ----------------------------------------------------------------------------- | ||
| Next == | ||
| \/ \E c \in Client: Do(c) \/ Rev(c) | ||
| \/ SRev | ||
| (* | ||
| Fairness: There is no requirement that the clients ever generate operations. | ||
| *) | ||
|
|
||
| Fairness == | ||
| WF_vars(SRev \/ \E c \in Client: Rev(c)) | ||
|
|
||
| Spec == Init /\ [][Next]_vars \* /\ Fairness | ||
| ----------------------------------------------------------------------------- | ||
| (* | ||
| Quiescent Consistency (QC) | ||
| *) | ||
| QC == | ||
| Comm(Msg)!EmptyChannel => Cardinality(Range(state)) = 1 | ||
| QC == \* Quiescent Consistency | ||
| Comm!EmptyChannel => Cardinality(Range(state)) = 1 | ||
|
|
||
| THEOREM Spec => []QC | ||
| ============================================================================= | ||
| \* Modification History | ||
| \* Last modified Fri Dec 28 18:06:40 CST 2018 by hengxin | ||
| \* Created Sat Jun 23 17:14:18 CST 2018 by hengxin | ||
| \* Last modified Wed Jan 02 21:37:02 CST 2019 by hengxin | ||
| \* Created Satchins, Jun 23 17:14:18 CST 2018 by hengxin |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.