/* CoreASM TerminationDetection specification, 
 showing problems with the natural language
 specification of the algorithm as is,
 authored by Vincenzo Gervasi et al, Dagstuhl Seminar 13372 (2013)*/


use Standard
use TabBlocks

enum COLORS = {BLACK, WHITE}
enum STATES = {ACTIVE, PASSIVE}

init InitialState

/* 
 Problems with state(.): can become ACTIVE and PASSIVE in the same step.
 Problems with hasMessage(.): if we don't consume messages, they will
 stay forever. If we DO consume messages (say in E), we might receive
 another message in the same step (in C, from the same or another machine),
 hence inconsistent update.
*/

rule Machine = {
	if hasMessage(self) then  // E: could clear msg
		state(self) := ACTIVE	// A: clash with B
	
	choose spontaneous in {true, false} do
		if state(self) = ACTIVE and spontaneous then
			state(self) := PASSIVE	 // B: clash with A
	
	// Rule 0
	if hasToken(self) then
		if state(self) = ACTIVE then
			skip
		else
			PassToken
	
	// Rule 1
	choose spontaneous in {true, false} do
		if state(self) = ACTIVE and spontaneous then
			choose dest in machines do
				SendMessage(dest)
        // C: clash with D (more precise: ColorM := BLACK in this rule)
				
    // Rule 3 and 4				
	if isMaster(self) and unsuccessful then
		colorM(self) := WHITE
		colorT := WHITE
		PassToken								// D: clash with C (more precise: ColorM := WHITE in this rule)	
	if isMaster(self) and tokenIndicatesFinished then
		done := true
}
	

rule PassToken = {
    // Rule 2
	hasToken(self) := false
	hasToken(pred(self)) := true
	if colorM(self) = BLACK then
		colorT := BLACK
	// Rule 5
	colorM(self) := WHITE
}

rule SendMessage(dest) = {
	hasMessage(dest) := true
	if (gt(dest,self)) then
		colorM(self) := BLACK
}

derived tokenIndicatesFinished = (colorT = WHITE)
derived unsuccesful = (isMaster(self) and hasToken(self)
        and (colorT = BLACK or colorM(self) = BLACK))
derived N = 4
derived machines = {a | a in Agents with index(a) != undef}
derived pred(m) = pick p in machines with index(m) = (index(p)+1) % N
derived gt(a,b) = index(a) > index(b)
derived isMaster(m) = (index(m) = 0)

rule InitialState = {
	forall i in [0..(N-1)] do
		extend Agents with m do
			program(m) := @Machine
			index(m) := i
			choose s in {ACTIVE, PASSIVE} do			
				state(m) := s
			if i = 0 then {
				hasToken(m) := true
				colorM(m) := WHITE
			} else {
				hasToken(m) := false
				colorM(m) := BLACK
			}
	colorT := BLACK
	program(self) := undef
}