-
Notifications
You must be signed in to change notification settings - Fork 0
/
node.maude
75 lines (57 loc) · 1.97 KB
/
node.maude
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
mod NODE is
pr MULTICAST .
sort NodeCid .
subsort NodeCid < Cid .
op node : Nat -> Oid [ctor] .
op FollowerNode : -> NodeCid .
op LeaderNode : -> NodeCid .
op OfflineNode : -> NodeCid .
op CandidateNode : -> NodeCid .
--- AttributeSet
--- term of node. starts at 0. 1 term corresponds to 1 election
op currentTerm :_ : Nat -> Attribute [ctor gather(&)] .
--- current Log
op log :_ : Log -> Attribute [ctor gather(&)] .
--- committed commands (relfected on state machine)
op committed :_ : Log -> Attribute [ctor gather(&)] .
--- other nodes
op neighbors :_ : OidSet -> Attribute [ctor gather(&)] .
--- whether leader is waiting for nodes AppendEntry
op waiting :_ : Bool -> Attribute [ctor gather(&)] .
--- next neighbor in ring
op next-neighbor :_ : Oid -> Attribute [ctor gather(&)] .
--- value for majority of nodes
op majority :_ : Nat -> Attribute [ctor gather(&)] .
--- number of neighbors (static)
op number-neighbors :_ : Nat -> Attribute [ctor gather(&)] .
--- number of yes response (election or commit)
op yes :_ : Nat -> Attribute [ctor gather(&)] .
--- number of no responses
op number-response :_ : Nat -> Attribute [ctor gather(&)] .
op to-nat : Bool -> Nat .
eq to-nat(false) = 0 .
eq to-nat(true) = 1 .
--- cleanup for each object
var O : Oid .
var C : NodeCid .
var N : Nat .
var M : Msg .
var MC : MsgCont .
var AS : AttributeSet .
var led : Log .
var E : Entry .
var B : Bool .
--- get the term of a message content, used for cleanup
op get-term : MsgCont -> Nat .
eq get-term(AppendEntry(N, led)) = N .
eq get-term(AppendEntryResponse(N, B)) = N .
eq get-term(Commit(N, E)) = N .
eq get-term(RequestVote(N, E)) = N .
eq get-term(Vote(N, B)) = N .
--- delete a message if the term of its contents is less than the term of the object
ceq
(M)
< O : C | currentTerm : N, AS > =
< O : C | currentTerm : N, AS >
if N > get-term(cont(M)) /\ dest(M) == O .
endm