% Breadth-first search
% The simulation just exercises this node.
% The error messages relating to "reason: actual parameter not initialized" are bogus 
%
% More or less what was given in class.  Note that "newMark" has been changed to "sendToNode". 
%
% A search is started when the environment sends a message of type "init" to a node.
% The environment should not send any more messages after that.  As nodes get messages,
% they start declaring "myparentis" over and over.

vocabulary Messages
	types
		Types enumeration [search, parent, notparent],
		Message tuple [msgtype:Types, distance:Int]
end

imports Messages
automaton BFS (p:Int, size:Int)
signature
input receive(m:Message, n:Int, const p:Int)
output send(m:Message, const p:Int, n:Int),
	myparentis(n:Int)

states
sendToNode:Array[Int, Bool] := constant(false),	% nodes to send message to
myparent:Int := -1,								% if > 0, this is my parent
newm:Message := [search, 0],					% standard message
distance: Int := 0,								% distance from root
neighbors: Set[Nat] := { 1,  3 }				% neighbors, can't be initialized in formals

transitions
	
input receive(m, n, i)
eff
	if (m.msgtype = init \/ myparent = -1) then
		for i:Nat in neighbors do
			sendToNode[i] := true
		od;
		if (m.msgtype = search) then
			newm := [m.msgtype, m.distance+1];
			myparent := n
		fi
	fi

output send(m, n, i)
pre
	sendToNode[i] /\ m = newm
eff
	sendToNode[i] := false

output myparentis(n)
pre
	myparent = n
	
schedule 
states root:Nat:=1,
msgInit:Message:=[init,0],
msgSearch:Message:=[search,1],
distance:Nat:=0,
parent:Nat:=0,
i:Int := 1,
action:Nat := 0
do
	root := choose i:Nat where i>=1 /\ i<=5;
	if (root = p) then
		fire input receive(msgInit, 6, p);
		i := 1;
		while i<=5 do	
			if sendToNode[i] then	
				fire output send(newm, p, i)
			fi;
			i := i+1
		od
	else
		distance := choose i:Nat where i>=1 /\ i<=10;
		% start workaround
		% the following four statements are equivalent to:
		% parent := choose i:Nat where i~= 1 /\ i>=1 /\ i<=5
		parent := choose i:Nat where i>=1 /\ i<=5;
		while (parent=p) do
			parent := choose i:Nat where i>=1 /\ i<=5
		od;
		% end workaround
		msgSearch.distance := distance;
		fire input receive(msgSearch, parent, p);
		i := 1;
		while i<=5 do
			action := choose i:Nat where i>=1 /\ i<=2;
			if (action = 1) then
				if (parent > 0) then
					fire output myparentis(parent)
				fi
			else
				if sendToNode[i] then
					fire output send(newm, p, i)
				fi;
				i := i+1
			fi
		od
	fi
od