-
Notifications
You must be signed in to change notification settings - Fork 0
/
GraphStateSpace.tla
73 lines (69 loc) · 3.9 KB
/
GraphStateSpace.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
----------------------------- MODULE GraphStateSpace -----------------------------
(*
The graph representation of n-ary ordered state space and 2D state space
used in CJupiter and XJupiter, respectively.
*)
EXTENDS JupiterCtx, GraphUtils
-----------------------------------------------------------------------------
IsSS(G) == \* A state space is a digraph with labeled edges.
/\ IsGraph(G) \* It is a digraph (represented by a record).
/\ G.node \subseteq (SUBSET Oid) \* Each node represents a document state, i.e., a set of Oid.
/\ G.edge \subseteq [from: G.node, to: G.node, cop: Cop] \* Labeled with a Cop operation.
EmptySS == EmptyGraph
-----------------------------------------------------------------------------
Locate(cop, ss) == \* Locate the node in state space ss that matches the context of cop.
CHOOSE n \in ss.node : n = cop.ctx
xForm(NextEdge(_, _, _), r, cop, ss) == \* Transform cop with an operation sequence
LET u == Locate(cop, ss) \* in state space ss at replica r.
v == u \cup {cop.oid}
RECURSIVE xFormHelper(_, _, _, _)
xFormHelper(uh, vh, coph, xss) ==
IF uh = ds[r]
THEN [xcop |-> coph,
xss |-> xss, \* xss: eXtra ss created during transformation
lss |-> [node |-> {vh},
edge |-> {[from |-> uh, to |-> vh, cop |-> coph]}]]
ELSE LET e == NextEdge(r, uh, ss)
copprime == e.cop
uprime == e.to
vprime == vh \cup {copprime.oid}
coph2copprime == COT(coph, copprime)
copprime2coph == COT(copprime, coph)
IN xFormHelper(uprime, vprime, coph2copprime,
xss (+) [node |-> {vprime},
edge |-> {[from |-> vh, to |-> vprime,
cop |-> copprime2coph],
[from |-> uprime, to |-> vprime,
cop |-> coph2copprime]}])
IN xFormHelper(u, v, cop, [node |-> {v},
edge |-> {[from |-> u, to |-> v, cop |-> cop]}])
xFormCopCops(cop, cops) == \* Transform cop against cops on state space.
LET RECURSIVE xFormCopCopsSSHelper(_, _, _)
xFormCopCopsSSHelper(coph, copsh, xss) ==
LET u == coph.ctx
v == u \cup {coph.oid}
uvSS == [node |-> {u, v},
edge |-> {[from |-> u, to |-> v, cop |-> coph]}]
IN IF copsh = <<>> THEN [xcop |-> coph,
xss |-> xss (+) uvSS, lss |-> uvSS]
ELSE LET copprimeh == Head(copsh)
uprime == u \cup {copprimeh.oid}
vprime == u \cup {coph.oid, copprimeh.oid}
coph2copprimeh == COT(coph, copprimeh)
copprimeh2coph == COT(copprimeh, coph)
IN xFormCopCopsSSHelper(coph2copprimeh,
Tail(copsh),
xss (+) [node |-> {u, v},
edge |-> {[from |-> u, to |-> v, cop |-> coph],
[from |-> u, to |-> uprime,
cop |-> copprimeh],
[from |-> v, to |-> vprime,
cop |-> copprimeh2coph]}])
IN xFormCopCopsSSHelper(cop, cops, EmptySS)
xFormCopCopsShift(cop, cops, shift) ==
\* shifting the first shift elements out of cops
xFormCopCops(cop, SubSeq(cops, shift + 1, Len(cops)))
=============================================================================
\* Modification History
\* Last modified Tue Feb 05 11:52:00 CST 2019 by hengxin
\* Created Wed Dec 19 18:15:25 CST 2018 by hengxin