Wei-jupiter-tla: formatting, overall slight refactor

tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AJupiterImplXJupiter.toolbox/AJupiterImplXJupiter/CSComm.tla

@@ -5,9 +5,9 @@ Specification of communication in a Client-Server system model.
 EXTENDS SequenceUtils
 -----------------------------------------------------------------------------
 CONSTANTS
- Client,  \* the set of clients
- Server,  \* the (unique) server
- Msg  \* the set of possible messages
+ Client, \* the set of clients
+ Server, \* the (unique) server
+ Msg \* the set of messages
 -----------------------------------------------------------------------------
 VARIABLES
  cincoming, \* cincoming[c]: incoming channel at client c \in Client
@@ -23,44 +23,32 @@ Init ==
 
 EmptyChannel == Init
 -----------------------------------------------------------------------------
-(* 
-A client sends a message msg to the Server.
-*)
-CSend(msg) == 
+CSend(msg) == \* A client sends a message msg to the Server.
  /\ sincoming' = Append(sincoming, msg)
  /\ UNCHANGED cincoming
-(* 
-Client c receives a message from the Server. 
-*)
-CRev(c) ==
+
+CRev(c) == \* Client c receives and consumes a message from the Server. 
  /\ cincoming[c] # <<>>
- /\ cincoming' = [cincoming EXCEPT ![c] = Tail(@)] \* consume a message
+ /\ cincoming' = [cincoming EXCEPT ![c] = Tail(@)]
  /\ UNCHANGED sincoming
 -----------------------------------------------------------------------------
 (* 
 SRev/SSend below is often used as a subaction. 
 No UNCHANGED in their definitions. 
 *)
-(*
-The Server receives a message. 
-*)
-SRev == 
+SRev == \* The Server receives and consumes a message. 
  /\ sincoming # <<>>
- /\ sincoming' = Tail(sincoming) \* consume a message
-(* 
-The Server sents a message cmsg to each client other than c \in Client.
-*)
-SSend(c, cmsg) ==
+ /\ sincoming' = Tail(sincoming)
+
+SSend(c, cmsg) == \* The Server sents a message cmsg to each client other than c \in Client.
  /\ cincoming' = [cl \in Client |->
  IF cl = c
  THEN cincoming[cl]
  ELSE Append(cincoming[cl], cmsg[cl])]
-(* 
-The Server broadcasts the same message msg to all Clients other than c \in Client. 
-*)
-SSendSame(c, msg) ==
+
+SSendSame(c, msg) == \* The Server broadcasts the message msg to all clients other than c \in Client.
  /\ SSend(c, [cl \in Client |-> msg])
 =============================================================================
 \* Modification History
-\* Last modified Tue Dec 04 20:49:02 CST 2018 by hengxin
+\* Last modified Mon Dec 31 19:04:29 CST 2018 by hengxin
 \* Created Sun Jun 24 10:25:34 CST 2018 by hengxin

tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AJupiterImplXJupiter.toolbox/AJupiterImplXJupiter/GraphsUtil.tla

@@ -1,9 +1,5 @@
 ----------------------------- MODULE GraphsUtil -----------------------------
 (*
-A module that defines graphs and the operations on them.
-*)
------------------------------------------------------------------------------
-(*
 A graph is a pair consisting of a set of nodes
 and a set of directed edges, each of which is a pair of nodes.
 It is represented by a record with node field and edge field. 
@@ -17,5 +13,5 @@ g (+) h == \* A union (in terms of set) of two graphs g and h.
  [node |-> g.node \cup h.node, edge |-> g.edge \cup h.edge]
 =============================================================================
 \* Modification History
-\* Last modified Wed Dec 19 18:22:46 CST 2018 by hengxin
+\* Last modified Mon Dec 31 19:47:39 CST 2018 by hengxin
 \* Created Wed Dec 19 11:11:25 CST 2018 by hengxin

tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AJupiterImplXJupiter.toolbox/AJupiterImplXJupiter/JupiterCtx.tla

@@ -19,7 +19,7 @@ ClientOf(cop) == cop.oid.c
 COT(lcop, rcop) == \* OT of two Cop(s). 
  [lcop EXCEPT !.op = Xform(lcop.op, rcop.op), !.ctx = @ \cup {rcop.oid}]
 
-UpdateDS(r, oid) == \* update ds to include new oid \in Oid
+UpdateDS(r, oid) == \* update ds[r] to include new oid \in Oid
  ds' = [ds EXCEPT ![r] = @ \cup {oid}]
 -----------------------------------------------------------------------------
 TypeOKCtx ==
@@ -43,5 +43,5 @@ SRevCtx ==
  /\ UNCHANGED cseq
 =============================================================================
 \* Modification History
-\* Last modified Fri Dec 28 14:38:39 CST 2018 by hengxin
+\* Last modified Mon Dec 31 18:52:44 CST 2018 by hengxin
 \* Created Wed Dec 05 20:03:50 CST 2018 by hengxin

tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AJupiterImplXJupiter.toolbox/AJupiterImplXJupiter/JupiterInterface.tla

@@ -6,9 +6,9 @@ the interface of a family of Jupiter specs.
 EXTENDS Integers, SequenceUtils, OT
 -----------------------------------------------------------------------------
 CONSTANTS
+ Char, \* the set of characters
  Client, \* the set of client replicas
  Server, \* the (unique) server replica
- Char, \* the set of characters allowed to be inserted
  InitState \* the initial state of each replica
 
 ASSUME \* We assume that all inserted elements are unique.
@@ -50,5 +50,5 @@ Ins == [type: {"Ins"}, pos: 1 .. (MaxLen + 1), ch: Char, pr: 1 .. ClientNum] \*
 Op == Ins \cup Del \* Now we don't consider Rd operations
 =============================================================================
 \* Modification History
-\* Last modified Wed Dec 12 20:20:43 CST 2018 by hengxin
+\* Last modified Mon Dec 31 18:51:58 CST 2018 by hengxin
 \* Created Tue Dec 04 19:01:01 CST 2018 by hengxin

tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AJupiterImplXJupiter.toolbox/AJupiterImplXJupiter/MC.cfg

@@ -10,22 +10,22 @@ b = b
 CONSTANT Server = Server
 \* MV CONSTANT definitions
 CONSTANT
-Client <- const_154622583969830000
+Client <- const_15462569000992000
 \* MV CONSTANT definitions
 CONSTANT
-Char <- const_154622583969831000
+Char <- const_15462569000993000
 \* SYMMETRY definition
-SYMMETRY symm_154622583969832000
+SYMMETRY symm_15462569000994000
 \* CONSTANT definitions
 CONSTANT
-InitState <- const_154622583969833000
+InitState <- const_15462569000995000
 \* CONSTANT definition
 CONSTANT
 Nop = Nop
 \* SPECIFICATION definition
 SPECIFICATION
-spec_154622583969935000
+spec_15462569001007000
 \* PROPERTY definition
 PROPERTY
-prop_154622583969936000
-\* Generated on Mon Dec 31 11:10:39 CST 2018
+prop_15462569001008000
+\* Generated on Mon Dec 31 19:48:20 CST 2018

tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AJupiterImplXJupiter.toolbox/AJupiterImplXJupiter/MC.tla

@@ -12,33 +12,33 @@ a, b
 ----
 
 \* MV CONSTANT definitions Client
-const_154622583969830000 == 
+const_15462569000992000 == 
 {c1, c2}
 ----
 
 \* MV CONSTANT definitions Char
-const_154622583969831000 == 
+const_15462569000993000 == 
 {a, b}
 ----
 
 \* SYMMETRY definition
-symm_154622583969832000 == 
-Permutations(const_154622583969831000)
+symm_15462569000994000 == 
+Permutations(const_15462569000993000)
 ----
 
 \* CONSTANT definitions @modelParameterConstants:2InitState
-const_154622583969833000 == 
+const_15462569000995000 == 
 <<>>
 ----
 
 \* SPECIFICATION definition @modelBehaviorSpec:0
-spec_154622583969935000 ==
+spec_15462569001007000 ==
 SpecImpl
 ----
 \* PROPERTY definition @modelCorrectnessProperties:0
-prop_154622583969936000 ==
+prop_15462569001008000 ==
 XJ!Spec
 ----
 =============================================================================
 \* Modification History
-\* Created Mon Dec 31 11:10:39 CST 2018 by hengxin
+\* Created Mon Dec 31 19:48:20 CST 2018 by hengxin

tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AJupiterImplXJupiter.toolbox/AJupiterImplXJupiter/OT.tla

@@ -1,21 +1,11 @@
 --------------------------------- MODULE OT ---------------------------------
-(***************************************************************************)
-(* Specification of OT (Operational Transformation) functions. *)
-(* It consists of the basic OT functions for two operations and *)
-(* more general ones involving operation sequences. *)
-(***************************************************************************)
+(*
+This module contains the basic OT (Operational Transformation) functions 
+for two operations and general ones involving operation sequences. 
+*)
 EXTENDS OpOperators, SetUtils
 -----------------------------------------------------------------------------
-(***************************************************************************)
-(* OT (Operational Transformation) functions. *)
-(* *)
-(* Naming convention: I for "Ins" and D for "Del". *)
-(***************************************************************************)
-
-(***************************************************************************)
-(* The left "Ins" lins transformed against the right "Ins" rins. *)
-(***************************************************************************)
-XformII(lins, rins) == 
+XformII(lins, rins) == \* lins is transformed against rins
  IF lins.pos < rins.pos
  THEN lins
  ELSE IF lins.pos > rins.pos
@@ -25,84 +15,59 @@ XformII(lins, rins) ==
  ELSE IF lins.pr > rins.pr
  THEN [lins EXCEPT !.pos = @+1]
  ELSE lins
-(***************************************************************************)
-(* The left "Ins" ins transformed against the right "Del" del. *)
-(***************************************************************************)
-XformID(ins, del) == 
+
+XformID(ins, del) == \* ins is transformed against del
  IF ins.pos <= del.pos
  THEN ins
  ELSE [ins EXCEPT !.pos = @-1]
-(***************************************************************************)
-(* The left "Del" del transformed against the right "Ins" ins. *)
-(***************************************************************************)
-XformDI(del, ins) == 
+
+XformDI(del, ins) == \* del is transformed against ins
  IF del.pos < ins.pos
  THEN del
  ELSE [del EXCEPT !.pos = @+1]
-(***************************************************************************)
-(* The left "Del" ldel transformed against the right "Del" rdel. *)
-(***************************************************************************)
-XformDD(ldel, rdel) == 
+
+XformDD(ldel, rdel) == \* ldel is transformed against rdel
  IF ldel.pos < rdel.pos
  THEN ldel
  ELSE IF ldel.pos > rdel.pos
  THEN [ldel EXCEPT !.pos = @-1]
  ELSE Nop
------------------------------------------------------------------------------
-(***************************************************************************)
-(* Transform the left operation lop against the right operation rop *)
-(* with appropriate OT function. *)
-(***************************************************************************)
-Xform(lop, rop) == 
+
+Xform(lop, rop) == \* lop is transformed against rop
  CASE lop = Nop \/ rop = Nop -> lop
  [] lop.type = "Ins" /\ rop.type = "Ins" -> XformII(lop, rop)
  [] lop.type = "Ins" /\ rop.type = "Del" -> XformID(lop, rop)
  [] lop.type = "Del" /\ rop.type = "Ins" -> XformDI(lop, rop)
  [] lop.type = "Del" /\ rop.type = "Del" -> XformDD(lop, rop)
 -----------------------------------------------------------------------------
-(***************************************************************************)
-(* Generalized OT functions on operation sequences. *)
-(***************************************************************************)
-
-(***************************************************************************)
-(* Iteratively/recursively transforms the operation op *)
-(* against an operation sequence ops. *)
-(***************************************************************************)
-RECURSIVE XformOpOps(_, _, _)
-XformOpOps(xform(_,_), op, ops) == 
+(*
+Generalized OT functions on operation sequences.
+*)
+RECURSIVE XformOpOps(_, _, _) 
+XformOpOps(xform(_,_), op, ops) == \* Transform an operation op against an operation sequence ops.
  IF ops = <<>> 
  THEN op 
  ELSE XformOpOps(xform, xform(op, Head(ops)), Tail(ops))
-(***************************************************************************)
-(* Iteratively/recursively transforms the operation op *)
-(* against an operation sequence ops. *)
-(* Being different from XformOpOps, *)
-(* XformOpOpsX maintains the intermediate transformed operation *)
-(***************************************************************************)
+
 RECURSIVE XformOpOpsX(_, _,_)
-XformOpOpsX(xform(_, _), op, ops) == 
+XformOpOpsX(xform(_, _), op, ops) == \* Transform an operation op against an operation sequence ops. 
  IF ops = <<>> 
- THEN <<op>> 
+ THEN <<op>> \* Maintain and return the intermediate transformed operations.
  ELSE <<op>> \o XformOpOpsX(xform, xform(op, Head(ops)), Tail(ops))
-(***************************************************************************)
-(* Iteratively/recursively transforms the operation sequence ops *)
-(* against an operation op. *)
-(***************************************************************************)
-XformOpsOp(xform(_, _), ops, op) == 
+
+XformOpsOp(xform(_, _), ops, op) == \* Transform an operation sequence ops against an operation op.
  LET opX == XformOpOpsX(xform, op, ops)
  IN [i \in 1 .. Len(ops) |-> xform(ops[i], opX[i])]
-(***************************************************************************)
-(* Iteratively/recursively transforms an operation sequence ops1 *)
-(* against another operation sequence ops2. *)
-(* *)
-(* See also Definition 2.13 of the paper "Imine @ TCS06". *)
-(***************************************************************************)
+(*
+Transforms an operation sequence ops1 against another operation sequence ops2; 
+see Definition 2.13 of the paper "Imine@TCS06".
+*)
 RECURSIVE XformOpsOps(_, _,_)
-XformOpsOps(xform(_, _), ops1, ops2) ==
+XformOpsOps(xform(_, _), ops1, ops2) == 
  IF ops2 = <<>>
  THEN ops1
  ELSE XformOpsOps(xform, XformOpsOp(xform, ops1, Head(ops2)), Tail(ops2))
 =============================================================================
 \* Modification History
-\* Last modified Fri Dec 28 14:58:58 CST 2018 by hengxin
+\* Last modified Mon Dec 31 19:45:16 CST 2018 by hengxin
 \* Created Sun Jun 24 15:57:48 CST 2018 by hengxin

tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AJupiterImplXJupiter.toolbox/AJupiterImplXJupiter/OpOperators.tla

@@ -1,39 +1,23 @@
 ---------------------------- MODULE OpOperators ----------------------------
-(***************************************************************************)
-(* Operators for Op. *)
-(***************************************************************************)
+(*
+Operators for Op.
+*)
 EXTENDS Naturals, Sequences, SequenceUtils
-
-Nop == PickNone(Nat)
 -----------------------------------------------------------------------------
-(*********************************************************************)
-(* The "Apply" operator which applies an operation op on the list l. *)
-(* *)
-(* Del: If pos > Len(l), the last element of l is deleted. *)
-(* This is realized by the DeleteElement operator. *)
-(* Ins: If pos > Len(l), the new element is appended to l. *)
-(* This is realized by the InsertElement operator. *)
-(*********************************************************************)
-Apply(op, l) == CASE op = Nop -> l
- [] op.type = "Rd" -> l
- [] op.type = "Del" -> DeleteElement(l, op.pos)
- [] op.type = "Ins" -> InsertElement(l, op.ch, op.pos)
-(*********************************************************************)
-(* The "ApplyOps" operator which applies an operation sequence ops *)
-(* on the list l. *)
-(*********************************************************************)
-RECURSIVE ApplyOps(_, _)
+Nop == PickNone(Nat)
+
+Apply(op, l) == \* Apply an operation op on the list l.
+ CASE op = Nop -> l
+ [] op.type = "Rd" -> l
+ [] op.type = "Del" -> DeleteElement(l, op.pos) \* Last(l) is deleted if pos > Len(l)
+ [] op.type = "Ins" -> InsertElement(l, op.ch, op.pos) \* Append(l, ch) if pos > Len(l)
+
+RECURSIVE ApplyOps(_, _) \* Apply an operation sequence ops on the list l.
 ApplyOps(ops, l) ==
  IF ops = <<>>
  THEN l
  ELSE Apply(Last(ops), ApplyOps(AllButLast(ops), l))
------------------------------------------------------------------------------
-(*********************************************************************)
-(* Check whether an operation op is legal with respect to the list l.*)
-(*********************************************************************)
-IsLegalOp(op, l) == CASE op.type = "Del" -> op.pos <= Len(l)
- [] op.type = "Ins" -> op.pos <= Len(l) + 1
 =============================================================================
 \* Modification History
-\* Last modified Mon Dec 03 20:14:35 CST 2018 by hengxin
+\* Last modified Mon Dec 31 19:21:16 CST 2018 by hengxin
 \* Created Tue Aug 28 14:58:54 CST 2018 by hengxin