ExtremaFinding.casm // (by Jacopo Soldani, Pisa 2014)
//parallel synchronous version

use Standard
use TabBlocks
use SchedulingPolicies

//All processes are synchronized
option SchedulingPolicies.policy allfirst

enum STATES = {ACTIVE, INACTIVE}


function mode : Agents -> STATES
function rightMsg : Agents -> NUMBER
function leftMsg : Agents -> NUMBER
function id : Agents -> NUMBER
function isLargest: Agents -> BOOLEAN
function notified : Agents -> BOOLEAN

function pos : Agents -> NUMBER

derived N = 4
derived processes = {a | a in Agents with pos(a) != undef}
derived l(p) = pick proc in processes with pos(proc) = (pos(p)-1+N) % N
derived r(p) = pick proc in processes with pos(proc) = (pos(p)+1) % N
derived largerMsgReceived = rightMsg(self) > id(self) or leftMsg(self) > id(self)
derived myMsgReceived  = rightMsg(self) = id(self) or leftMsg(self) = id(self)

init InitiateState

rule ExtremaFinding = 

	//Each process p will execute this rule with p=self. 
	//The forall synchronization will be implemented by 
	//the CoreASM scheduling policy "allfirst".
	
	if mode(self) = ACTIVE then
		if not isLargest(self) then
			rightMsg(l(self)) := id(self)
			leftMsg(r(self)) := id(self)
		if largerMsgReceived then
			mode(self) := INACTIVE
		if myMsgReceived  then
			isLargest(self):=true
			notified(r(self)) := true

	if mode(self) = INACTIVE then
		if notified(self) then
			notified(r(self)) := true 
		else
			PassMsgs

	if isLargest(self) and notified(self) then
		print "Extrema found!!!"
		StopASM

rule PassMsgs = 
		rightMsg(l(self)) := rightMsg(self)
		leftMsg(r(self)) := leftMsg(self)

rule StopASM =
	forall m in Agents do
		program(m) := undef
		
rule InitiateState =
	//We will employ n,m to generate pairwise different integer numbers used 
	//as ids (for each process p) to implement the < relation.
	choose n in {11*N,13*N,17*N}  do
		choose m in {11*N,13*N,17*N} do 
			forall i in [0..(N-1)] do
				extend Agents with p do	
					program(p) := @ExtremaFinding
					pos(p) := i
					id(p) := (i+n+m) % N + 1
					mode(p) := ACTIVE
					notified(p) := false
					isLargest(p) :=false
					rightMsg(p) := (i+n+m) % N + 1
					leftMsg(p) := (i+n+m) % N + 1
		program(self):=undef