Echo algorithm in electrum

1

This is an attempt to specify the echo algorithm in electrum.

Do you think, the spec is correct?

Any hints for improving the spec?

/* Echo algorithm for constructing a spanning tree in an undirected   
   graph starting from a single initiator.
*/

open util/graph[Node]

enum Color {Red, Green}

abstract sig Node {
	neighbors: set Node,   -- Graph
	var parent: lone Node, -- relation for tree
	var inbox: set Node,   -- inbox for messages from other nodes
	var received: set Node,-- already received messages
	var color: one Color   -- ready = returns message to parent = green 
}

one sig INode extends Node {} -- initiator
sig PNode extends Node {}     -- paricipants

fact {
	noSelfLoops[neighbors]     -- irreflexive
	undirected[neighbors]      -- undirected
	rootedAt[neighbors, INode] -- connected with initiator
}

// skip state' = state
pred skip {
	parent' = parent
	inbox' = inbox
	received' = received
	color' = color
}
	
// initial state
pred init {
	no parent and no inbox and no received
	color = Node -> Red
}

pred broadcast[n: Node, to: set Node] {
	all q: to | q.inbox' = q.inbox + n
	all unchanged: Node - to | unchanged.inbox' = unchanged.inbox  
}

// initial state and broadcast from initiator to all his neighbors
pred initiate {
	init
	broadcast[INode, INode.neighbors]
	parent' = parent
	received' = received
	color' = color
}

pred broadcast2[n: Node, to: set Node] {
	all q: to | q.inbox' = q.inbox + n
	all u: (Node - to) | u != n implies u.inbox' = u.inbox else no u.inbox'   
}

// forward: msg from future parent forwarded to all other neighbors
pred forward {
	some n: PNode, msg: Node | {
			no n.parent and msg in n.inbox 
			parent' = parent ++ n->msg
			broadcast2[n, (n.neighbors - msg)]
			received' = received ++ n->(n.received + msg)
			color' = color
	}
}

// received: msg from other neighbor returned
pred received {
	some n: Node, msg: Node | {
			(one n.parent or n = INode) and msg in n.inbox 
			parent' = parent
			all u: Node | u != n implies u.inbox' = u.inbox else no u.inbox'
			received' = received ++ n->(n.received + msg)
			color' = color
	}
}

// ready: alle msg from other neighbors returned, msg to parent
pred ready {
	some n: PNode | {
		n.received = n.neighbors and n.color = Red // Ausgangslage
		parent' = parent
		inbox' = inbox ++ (n.parent->n)
		received' = received
		color' = color ++ (n->Green)
	}
} 

// rerminate: initiator got all return msgs
pred terminate {
	no PNode or (some INode.neighbors and INode.neighbors = INode.received) // Ausgangslage
	parent' = parent
	inbox' = inbox
	received' = received
	color' = color ++ (INode->Green)
}

// echo algorithm with end criteria
fact { 
	init
	always {
		initiate or
		forward or
		received or
		ready or
		terminate or
    skip
	}
	eventually INode.color = Green
} 

run {} for 1 Node
run {} for exactly 2 Node
run {} for exactly 3 Node
run {} for exactly 4 Node, 12 steps
run {} for exactly 5 Node, 15 steps // 200 sec or so on my machine

// check Spannbaum gefunden?
check {eventually tree[~parent]} for 4 Node, 12 steps
2

Hi
I won’t comment on the correctness as I don’t know the algorithm and I don’t really have time to delve into the model. But, overall, it seems absolutely fine (I’m just surprised by the last fact which contains eventually INode.color = Green: is it normal that you impose an outcome rather than verifying it?).

Then, if I were you, I would just perform a few improvements (in this order):

  1. Introduce an unchanged (let unchanged[r] { (r) = (r)' }) macro and use it to show more explicitly unchanging relations.
  2. Instead of using existential quantifications in events, I’d rather move the quantified variables to pred parameters.
  3. Then I would apply the event reification idiom for a nice visualization. Having done the previous step, you will be able to see clearly the value given to the quantified variables that were moved to parameters.
3

Hi,

The echo algorithm constructs a spanning tree in an undirected connected graph.

The initiator sends his id to all its neighbors. Each node marks the first sender as his parent and forwards the message to all its neighbors. Messages from later senders are just noted until the node got messages from all its neighbors. It then changes its color to green and sends its id to its parent. Eventually the initiator gets the echos all back on the parent relation and changes his color to green.

The assertion to check is then that the parent relation is a spanning tree of the graph.

In my model I want to ensure that i get just models where the echo is back to the initiator, therefore the constraint eventually INode.color = Green. The actual check of the desired property is eventually tree[~parent].

Thank you for the hint to the event reification idiom, I will try it.

When running (a slightly changed) model with SAT4J I get the results I expect. But with Electrod/NuSMV I run into a problem.

The code snippet in Alloy:

pred broadcast[n, fp: Node] {
	let to = n.neighbors - fp {
		all q: to | q.inbox' = q.inbox + n
		all u: (Node - to) - n | u.inbox' = u.inbox
		n.inbox' = n.inbox - fp 
	} 
}

This predicate is used in predicate forward in the following situation:

n = PNode$1
fp = INode$0
n.neighbors = {PNode$0, INode$0}

In this situation the Alloy evaluator evaluates:

all q from to = PNode$1.neighbors - INode$0 = PNode$0
all u from (Node - to) - n = INode$0

The generated code for Electrod at the corresponding point is

 (all broadcast_q: (forward_n . this##Node#neighbors) - forward_msg { 
     (broadcast_q . (this##Node#inbox)' ) = ((broadcast_q . this##Node#inbox) + 
     forward_n)
     }) and 
   (all broadcast_u: (this##INode + this##PNode) - (forward_n . 
    this##Node#neighbors) - forward_msg - forward_n { 
     (broadcast_u . (this##Node#inbox)' ) = (broadcast_u . this##Node#inbox)
     }) and 
   (forward_n . (this##Node#inbox)' ) = ((forward_n . this##Node#inbox) - 
   forward_msg)

and this corresponds to

all q from  PNode$1.neighbors - INode$0 = PNode$0 
all u from Node - PNode$1.neighbors - INode$0 - PNode$1 = {}

It looks like this is a bug in the translation from Alloy to Electrod. ???

4

OK, this is what I had suspected.

IIUC, the translation yields:

all broadcast_u: (this##INode + this##PNode) 
    - (forward_n . this##Node#neighbors) - forward_msg 
    - forward_n

instead of:

all broadcast_u: (this##INode + this##PNode) 
    - ((forward_n . this##Node#neighbors)) - forward_msg 
    - forward_n

(bad parenthesizing)?

Would you please report an issue on the Electrum2 repo with a short example if possible? Thanks.

5

The specification of the echo algorithm that I posted here the other day has significant flaws. In particular, it is not a good idea to formulate a desired result as a fact, such as the echo coming back to the initiator.

Because then you don’t see the scenarios in which errors in the specification become visible. It is much better to formulate conditions that ensure that not the stutter transitions are carried out all the time, but those transitions, that make progress in the unfolding of the algorithm. The predicate fairness does ensure that progress is made.

David Chemouil’s hints helped me a lot to improve the specification.

Here the improved and simplified version:

open util/graph[Node]

let unchanged[r] { (r)' = (r) } 

enum Color {Red, Green}

abstract sig Node {
	neighbors: set Node,
	var parent: lone Node,
	var inbox: set Node,
	var color: Color
}	

one sig INode extends Node{}
sig PNode extends Node{}

fact {
	noSelfLoops[neighbors]
	undirected[neighbors]
	rootedAt[neighbors, INode]
}

pred init {
	parent = INode -> INode
	no inbox
	color = Node -> Red
}

pred stutter {
	unchanged[parent]
	unchanged[inbox]
	unchanged[color]
}

pred broadcast[n, fp: Node] {
	let to = n.neighbors - fp {
		all q: to | q.inbox' = q.inbox + n
		all u: (Node - to) | u.inbox' = u.inbox	
	} 
}

pred initiate {
		init
		broadcast[INode, INode]
		unchanged[parent]
		unchanged[color]
}

pred forward [n: Node, msg: Node] {
	no n.parent and msg in n.inbox
	parent' = parent + n->msg
	broadcast[n, msg]
	unchanged[color]
}

pred echo [n: Node] {
	one n.parent and n.inbox = n.neighbors and n.color = Red
	unchanged[parent]
	n = INode implies
		inbox' = inbox
	else
		inbox' = inbox ++ n.parent->(n.parent.inbox + n)
	color' = color ++ (n->Green)
}

fact trans {
	init
	always { 
		initiate or
		some n, msg: Node | forward[n, msg] or
		some n: Node | echo[n] or
		stutter }
}

pred fairness {
	all n, msg: Node {
		(eventually always init) 
				implies (always eventually initiate)
		(eventually always (no n.parent and msg in n.inbox))
				implies (always eventually forward[n, msg])
		(eventually always (one n.parent and n.inbox = n.neighbors and n.color = Red))
				implies (always eventually echo[n])
	}
}
		
run examples {}
						
run withProgress {fairness}

assert EchoComesBack {
	fairness implies eventually INode.color = Green
}

check EchoComesBack

assert SpanningTree {
	let pt = parent - INode->INode |
	(eventually INode.color = Green) implies (eventually tree[~pt])
}

check SpanningTree

Another remark: Because the analysis is limited to 10 steps, certain graphs may not be analyzed because it would take more steps for the echo to return to the initiator. You can then do unbounded model checking with NuSMV as a solver. In our example, however, we can specify complete graphs. They have the maximum possible number of edges and therefore need the maximal number of steps to execute the algorithm and echoing back to the initiator.

Now you can set the bound to let’s say 20 steps and then generate a scenario to see how many steps are actually needed.

pred complete {
	neighbors = (Node->Node) - iden
}

run completeGraph {
	complete
  eventually INode.color = Green
} for exactly 5 Node, 20 steps

Doing so, we see that for graphs with 5 nodes 11 steps suffice to include all possible graphs with up to 5 nodes.