-
Notifications
You must be signed in to change notification settings - Fork 1
/
rutschblock.tla
69 lines (52 loc) · 2.28 KB
/
rutschblock.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
---------------------------- MODULE rutschblock ----------------------------
(***************************************************************************)
(* TLA+ utilities for the Avalanche consensus protocols *)
(***************************************************************************)
EXTENDS Naturals, Sequences, Integers, Reals
\* the K constant as specified in the paper
CONSTANT K
\* the M constant as specified in the paper
CONSTANT M
\* the α constant as specified in the paper
CONSTANT Alpha
\* the sum of nodes participating in consensus
CONSTANT N
\* Server states
CONSTANTS Red, Blue, Uncolored
\* the nodes state
VARIABLE state
\* the responses a node receives
VARIABLE responses
\* the queries for a specific node
VARIABLE queries
\* the set of colors
Colors == { Red, Blue }
\* the sef of all possible nodes
Node == 1 .. N
(***************************************************************************)
(* Respond to `r` with a color `c` *)
(***************************************************************************)
Respond(r, c) ==
/\ responses' = [responses EXCEPT ![r][c] = responses[r][c] + 1]
(***************************************************************************)
(* Node `n` receives a query from `s` with color `c` *)
(***************************************************************************)
OnQuery(n, s, c) ==
/\ state' =
IF state[n] = Uncolored
THEN [state EXCEPT ![n] = c]
ELSE state
/\ Respond(s, state[n])
(***************************************************************************)
(* Node `n` sends a query to `r` with color `c` *)
(***************************************************************************)
Query(n, r, c) ==
/\ queries' = [queries EXCEPT ![r] = Append(@, [node |-> n, color |-> c])]
(***************************************************************************)
(* Node `n` processes its current queries *)
(***************************************************************************)
ProcessQueries(n) ==
/\ \E q \in queries[n]:
OnQuery(n, q.node, q.color)
/\ queries' = [queries EXCEPT ![n] = {}]
=============================================================================