--- Leader election algorithm. Only One leader election. --- Extending it to multiple leader elections should be an exercise. --- Usual spanning tree algorithm: --- a. each node has a set of neighbors --- b. send election messages to nbs --- c. recvr election first time: --- i. remember parent, and ii. send election to all other nbs --- d. rcv election message for not-first time: ack sender --- e. rcvd ack from everybody except parent: --- ack parent, with highest value in subtree --- f. when initiator/root has gotten all acks: find largest number --- and start propagating it to children. load full-maude26 load messages (omod MULTICAST is --- this one was on another machine ... including MESSAGE-WRAPPER . sort OidSet . subsort Oid < OidSet . op none : -> OidSet [ctor] . op _;_ : OidSet OidSet -> OidSet [ctor assoc comm id: none] . op multicast_from_to_ : MsgContent Oid OidSet -> Msg [ctor] . var M : MsgContent . vars SENDER ARECEIVER : Oid . var OTHER-RECEIVERS : OidSet . eq multicast M from SENDER to none = none . eq multicast M from SENDER to ARECEIVER ; OTHER-RECEIVERS = (msg M from SENDER to ARECEIVER) (multicast M from SENDER to OTHER-RECEIVERS) . endom) --- Assume that all Oids are numbers, and that all nodes have numbers/oid > 0. --- The number 0 is the default value for "no parent" etc. (omod ST-LEADER-ELECTION is including MULTICAST . protecting NAT . --- Each node has a number oid, which is also its value: subsort Nat < Oid . class Node | parent : Oid, --- originally 0 max : Oid, --- originally the node's own id state : STstate, --- idle, waitForAck leader : Oid, --- initially 0 neighbors : OidSet . --- neighbors sort STstate . ops idle waitForLeader : -> STstate [ctor] . op waitForAck : OidSet -> STstate [ctor] . --- Messages: msg electLeader : Oid -> Msg . *** kicks off a round of the protocol op election : -> MsgContent [ctor] . ops ack leader : Oid -> MsgContent [ctor] . vars NZN MAX PARENT : NzNat . var N : Nat . vars O O1 : Oid . var OS : OidSet . var S : STstate . --- Kick off a round of the protocol: rl [startLeaderElection] : electLeader(O) < O : Node | neighbors : OS > => < O : Node | state : waitForAck(OS), parent : O > (multicast election from O to OS) . --- Receive a message for the first time: rl [rcvElection1] : (msg election from O1 to O) < O : Node | state : idle, neighbors : O1 ; OS > => < O : Node | parent : O1, state : waitForAck(OS) > (multicast election from O to OS) . --- Receive election message when already in an election: crl [rcvElection2] : (msg election from O1 to O) < O : Node | state : S > => < O : Node | > (msg ack(0) from O to O1) if S =/= idle . --- Receive an ack, either from sibling, with value 0, or from child: rl [rcvAck1] : (msg ack(N) from O1 to O) < O : Node | state : waitForAck(O1 ; OS), max : MAX > => < O : Node | state : waitForAck(OS), max : max(MAX, N) > . --- No longer waiting for an ack from children/siblings: send ack upstream, --- unless you are the root: crl [ackParent] : < O : Node | state : waitForAck(none), max : MAX, parent : PARENT > => < O : Node | state : waitForLeader > (msg ack(MAX) from O to PARENT) if PARENT =/= O . --- You are the parent, and must start a new round: rl [sendLeader] : < O : Node | state : waitForAck(none), neighbors : OS, max : MAX, parent : O > => < O : Node | state : idle, leader : MAX > (multicast leader(MAX) from O to OS) . --- Receive leader message; if for the first time, send to other neighbors: rl [rcvLeader1] : (msg leader(NZN) from O1 to O) < O : Node | state : waitForLeader, neighbors : O1 ; OS > => < O : Node | state : idle, leader : NZN > (multicast leader(NZN) from O to OS) . --- Receive leader message, but have already received leader message: rl [rcvLeader] : (msg leader(NZN) from O1 to O) < O : Node | state : idle > => < O : Node | > . endom) (omod ST-LEADER-STATES is protecting ST-LEADER-ELECTION . ops init1 init2 init3 : -> Configuration . eq init1 = electLeader(1) < 1 : Node | state : idle, max : 1, parent : 0, leader : 0, neighbors : 2 ; 3 > < 2 : Node | state : idle, max : 2, parent : 0, leader : 0, neighbors : 1 ; 3 > < 3 : Node | state : idle, max : 3, parent : 0, leader : 0, neighbors : 1 ; 2 > . eq init2 = electLeader(1) < 1 : Node | state : idle, max : 1, parent : 0, leader : 0, neighbors : 2 ; 3 ; 4 > < 2 : Node | state : idle, max : 2, parent : 0, leader : 0, neighbors : 1 ; 3 ; 4 > < 3 : Node | state : idle, max : 3, parent : 0, leader : 0, neighbors : 1 ; 2 ; 4 > < 4 : Node | state : idle, max : 4, parent : 0, leader : 0, neighbors : 1 ; 2 ; 3 > . eq init3 = electLeader(3) < 1 : Node | state : idle, max : 1, parent : 0, leader : 0, neighbors : 2 ; 3 > < 2 : Node | state : idle, max : 2, parent : 0, leader : 0, neighbors : 1 ; 3 ; 5 > < 3 : Node | state : idle, max : 3, parent : 0, leader : 0, neighbors : 1 ; 2 ; 4 > < 4 : Node | state : idle, max : 4, parent : 0, leader : 0, neighbors : 3 ; 5 > < 5 : Node | state : idle, max : 5, parent : 0, leader : 0, neighbors : 2 ; 4 > . endom) (rew init2 .) (search init1 =>! C:Configuration .) (search init1 =>! C:Configuration < O:Oid : Node | leader : N:Nat > such that N:Nat =/= 3 .) (search init2 =>! C:Configuration .) (search init2 =>! C:Configuration < O:Oid : Node | leader : N:Nat > such that N:Nat =/= 4 .) eof (search init3 =>! C:Configuration .) (search init3 =>! C:Configuration < O:Oid : Node | leader : N:Nat > such that N:Nat =/= 5 .)