-
Notifications
You must be signed in to change notification settings - Fork 0
/
message.maude
69 lines (47 loc) · 1.86 KB
/
message.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
mod MESSAGE is
ex CONFIGURATION .
pr LOG .
sort MsgCont .
--- for leader
op Request : Command -> MsgCont [ctor] .
--- the nat of the next three commands is the current term
--- send the Log to followers
op AppendEntry : Nat Log -> MsgCont [ctor] .
--- vote yes if log updated, no otherwise (if node is down or AppendEntry came from dead leader)
op AppendEntryResponse : Nat Bool -> MsgCont [ctor] .
--- tell nodes to commit up to the designated entry (if entry doesn't exist, do nothing)
op Commit : Nat Entry -> MsgCont [ctor] .
--- tell a node to die
op Die : -> MsgCont [ctor] .
--- tell a node to come online
op Live : -> MsgCont [ctor] .
--- tell a node to try to become leader for specified term
op BecomeLeader : Nat -> MsgCont [ctor] .
--- request a vote from a node, giving the term and Log of the candidate
op RequestVote : Nat Entry -> MsgCont [ctor] .
--- if the logs have latest entries with different terms, the higher term is more up-to-date.
--- otherwise, the higher index is more up-to-date
--- Vote yes (true) if candidate is at least as up-to-date and not offline, no otherwise
op Vote : Nat Bool -> MsgCont [ctor] .
op msg_from_to_ : MsgCont Oid Oid -> Msg [ctor] .
var C : MsgCont .
vars O O2 : Oid .
op dest : Msg -> Oid .
eq dest(msg C from O to O2) = O2 .
op cont : Msg -> MsgCont .
eq cont(msg C from O to O2) = C .
endm
mod MULTICAST is
pr MESSAGE .
--- send message to multiple nodes at once
sort OidSet .
subsort Oid < OidSet .
op none : -> OidSet [ctor] .
op _,_ : OidSet OidSet -> OidSet [ctor assoc comm id: none] .
var M : MsgCont .
vars O O2 : Oid .
var OS : OidSet .
op multicast_from_to_ : MsgCont Oid OidSet -> Msg [ctor] .
eq multicast M from O to none = none .
eq multicast M from O to (O2 , OS) = (msg M from O to O2) multicast M from O to OS .
endm