/*
* Leader election algorithm with minimal path to leader
* computation over next hop in CoreASM.
* by Julian Lettner (FH Hagenberg, May 2011).
*/ downloaded from https://github.com/CoreASM/coreasm.core/wiki/Examples
CoreASM LeaderElection
use Standard
// for max(..)
use Math
// for treating a list like a queue (enqueue .. into ..), we need a queue because of concurrency
use Queue
// Strict options
option Signature.NoUndefinedId strict
option Signature.TypeChecking strict
// Universe and enums
enum AgentState = {proposeToNeighbors, checkProposals}
// Functions
function state: Agents -> AgentState // agent states
function cand: Agents -> Agents // current leader candidates
function proposals: Agents -> LIST // received proposals for specific agent
// Function type of proposals is a list (queue) because of concurrency (need to use enqueue)
// Proposals elemnts are a list with 3 elements: [cand, nearNeighbor, distance]
function nearNeighbor: Agents -> Agents // next hop on shortest path to leader
function distance: Agents -> NUMBER // total (summed up) distance to leader
function distanceBetween: Agents * Agents -> NUMBER // distance between two neighbors
// Example (derived) functions
// Edit the following for changing the example scenario
derived neighborMap = {
1 -> {2, 4},
2 -> {1, 3, 4, 5},
3 -> {2, 6},
4 -> {1, 2, 5},
5 -> {2, 4, 6},
6 -> {5, 3}
}
rule InitDistances =
par
InitBidirDistance(1, 2, 5)
InitBidirDistance(1, 4, 1)
InitBidirDistance(2, 3, 5)
InitBidirDistance(2, 4, 2)
InitBidirDistance(2, 5, 2)
InitBidirDistance(3, 6, 12)
InitBidirDistance(4, 5, 5)
InitBidirDistance(5, 6, 3)
endpar
rule InitBidirDistance(a1, a2, distance) =
par
distanceBetween(a1, a2) := distance
distanceBetween(a2, a1) := distance
endpar
// Derived functions
// Number of connected nodes (agents), neighbor relationship and 'self' functions
derived agentCount = size(neighborMap)
// 'self' functions
derived myNeighbors = neighborMap()(self)
derived myState = state(self)
derived myCandidate= cand(self)
derived myNearNeighbor = nearNeighbor(self)
derived myDistance = distance(self)
derived myProposals = {x | x in proposals(self)}
derived myName = "Agent " + self
// 'ground model' functions
derived thereAreProposals = size(myProposals) > 0
// Proposals are lists with 3 elements: [cand, nearNeighbor, distance]
derived bestProposal =
pick x in myProposals with (forall y in myProposals holds
nth(x,1) >= nth(y,1) and // correct leader
(nth(x,1) = nth(y,1) implies nth(x,3) <= nth(y,3)) // minimal distance if same leader
)
derived bestCand = nth(bestProposal, 1)
derived bestNearNeighbor = nth(bestProposal, 2)
derived bestDistance = nth(bestProposal, 3)
// Proposal improved current status if better leader or shorter path to same leader
derived proposalsImprove = bestCand > myCandidate or (bestCand = myCandidate and bestDistance < myDistance)
derived networkConverged =
forall x in [1..agentCount] holds
cand(x) = agentCount and state(x) = checkProposals and size(proposals(x)) = 0
// Every agent knows correct leader and minimal path, is in state 'check proposals' and it's proposal set is empty
init InitRule
// --- Initial rule ---
rule InitRule =
seq
par
// Intialize distance between neighbors
InitDistances
// Initialize agents
forall i in [1..agentCount] do par
Agents(i) := true
program(i) := @AgentProgram
// Initial values for agents
state(i) := proposeToNeighbors // agent state
cand(i) := i // leader candidate -> self
proposals(i) := [] // no proposals
distance(i) := 0 // distance to leader
nearNeighbor(i) := i // Next hop -> self (initial candidate)
endpar endforall
endpar
next
program(self) := undef
// --- Program for every agent ---
rule AgentProgram =
par
// Standard algorithm
case myState of
proposeToNeighbors: ProposeToNeighbors
checkProposals: CheckProposals
endcase
// Termination condition
// This is a bit like cheating (single agent does not know global state), but
// we only use it to shutdown the ASM execution engine.
// Only terminate agent if agent already knows the correct leader and there are
// no more proposals circulating in the network (= converged state).
if networkConverged then par
print myName + ": elected leader " + myCandidate+ "/" + myDistance + ", next hop is " + myNearNeighbor
program(self) := undef
endpar endif
endpar
rule ProposeToNeighbors =
par
// Propose candidate to neighbors
forall a in myNeighbors do par
// We need enqueue because of concurrency
enqueue [myCandidate, self, myDistance + distanceBetween(self, a)] into proposals(a)
endpar endforall
print myName + ": proposing " + myCandidate+ "/" + myDistance + " to " + myNeighbors
// Update state
state(self) := checkProposals
endpar
rule CheckProposals =
if thereAreProposals then par
// Update canditate if proposal provides better candidate
if proposalsImprove then par
cand(self) := bestCand
nearNeighbor(self) := bestNearNeighbor
distance(self) := bestDistance
print myName + ": updating best candidate " + myCandidate+ "/" + myDistance + " to " + bestCand + "/" + bestDistance
// Propose to neighbors only if there is a new candidate
state(self) := proposeToNeighbors
endpar else
// Set state
state(self) := checkProposals
endif
// Remove proposals from set
proposals(self) := []
print myName + ": clearing proposals " + myProposals
endpar endif