-
Notifications
You must be signed in to change notification settings - Fork 0
/
safe_network.tla
122 lines (99 loc) · 4.1 KB
/
safe_network.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
114
115
116
117
118
119
120
121
122
---------------------------- MODULE safe_network ----------------------------
(* Naming convention:
* UpperCase: sets, modules, operators, predicates
* lowerCase: variables
*)
EXTENDS Naturals, Sequences, FiniteSets, TLC
(* --------- Utility functions -------------- *)
(* Sum of a set of natural numbers *)
(* From: https://github.com/jameshfisher/tlaplus/blob/master/examples/CarTalkPuzzle/CarTalkPuzzle.tla *)
RECURSIVE Sum(_, _)
Sum(f, S) == IF S = {} THEN 0
ELSE LET x == CHOOSE x \in S : TRUE
IN f[x] + Sum(f, S \ {x})
(* Choose n arbitrary elements of a set *)
RECURSIVE ChooseN(_, _)
ChooseN(S, n) == IF n = 0 THEN {} ELSE
LET chosen == CHOOSE x \in S : TRUE
IN UNION {{chosen}, ChooseN(S\{chosen}, n - 1)}
(* --------------- The model --------------------- *)
CONSTANT numSeedNodes, maxNodes
VARIABLE nodes, sections, nodeCount
vars == <<nodes, sections, nodeCount>>
(* Fixed values *)
MaxPrefixLen == 6 \* Maximum length of any prefix
MinSectionSize == 8 \* Minimum section size
(* Typing rules *)
(* Set of all prefixes up to a finite length *)
Prefixes == UNION {[1..n -> {0, 1}] : n \in 0..MaxPrefixLen}
IsRT(rt) == \A prefix \in DOMAIN rt:
/\ prefix \in Prefixes
/\ \A node \in rt[prefix]: node \in Nat
SectionsOK == \A prefix \in DOMAIN sections:
/\ prefix \in Prefixes
/\ IsRT(sections[prefix])
NodesOK == \A node \in DOMAIN nodes:
/\ node \in Nat
/\ nodes[node] \in Prefixes
/\ nodes[node] \in DOMAIN sections
(* Type invariant *)
TypeOK == /\ numSeedNodes \in Nat
/\ SectionsOK
/\ NodesOK
(* Next-step relations *)
(* TODO: section splitting based on XOR metric? *)
SplitThreshold == MinSectionSize * 2 + 2
CanSplit(section) == Cardinality(section) > SplitThreshold
(* Step which adds a node to a section *)
(* FIXME: re-enable this
AddNode == \E p \in prefixes :
/\ nodeCount' = nodeCount + 1
/\ sections' = [sections EXCEPT ![p] = UNION {sections[p], {nodeCount + 1}}]
/\ nodeCount < maxNodes
/\ CanSplit(sections[p]) = FALSE
/\ UNCHANGED prefixes
*)
SplitSection == \E prefix \in DOMAIN sections:
LET ourSection == sections[prefix][prefix] IN
LET leftPrefix == Append(prefix, 0) IN
LET rightPrefix == Append(prefix, 1) IN
LET newPrefixes == UNION {(DOMAIN sections)\{prefix}, {leftPrefix, rightPrefix}} IN
LET newSectionSize == MinSectionSize + 1 IN
LET leftSection == ChooseN(ourSection, newSectionSize) IN
LET rightSection == ourSection\leftSection IN
LET updatedRT == [q \in newPrefixes |->
IF q = leftPrefix THEN leftSection
ELSE IF q = rightPrefix THEN rightSection
ELSE sections[prefix][q]
] IN
/\ CanSplit(ourSection)
(* TODO: delete sections that we're now disconnected from *)
/\ sections' = [q \in newPrefixes |->
IF q = leftPrefix THEN updatedRT
ELSE IF q = rightPrefix THEN updatedRT
ELSE sections[q]]
(* TODO: send section update to neighbours *)
/\ nodes' = [n \in DOMAIN nodes |->
IF n \in leftSection THEN leftPrefix
ELSE IF n \in rightSection THEN rightPrefix
ELSE nodes[n]]
/\ UNCHANGED nodeCount
(* Initial conditions *)
Init == /\ nodeCount = numSeedNodes
/\ LET initRT == [p \in {<<>>} |-> (1..nodeCount)] IN
sections = [p \in {<<>>} |-> initRT]
/\ nodes = [n \in (1..nodeCount) |-> <<>>]
(* Step relation *)
Next == \/ SplitSection
\/ UNCHANGED vars \* Allows stuttering termination... I think.
(* ------- Invariants -------- *)
(* Network size invariant: number of nodes in all sections = total node count *)
\* NetworkSizeInv == Sum([p \in prefixes |-> Cardinality(sections[p])], prefixes) = nodeCount
(* Num sections invariant: number of sections is less than floor(nodeCount/MinSectionSize) *)
\* NumSectionsInv == Cardinality(prefixes) <= (nodeCount \div MinSectionSize)
\* FIXME: restore invariants
MainInvariant == TRUE
=============================================================================
\* Modification History
\* Last modified Tue Feb 28 17:26:45 AEDT 2017 by michael
\* Created Mon Feb 27 13:40:49 AEDT 2017 by michael