//CoreASM TerminationDetection model
// where the problems with the natural language
//specification of the algorithm have been solved,
//authored by Vincenzo Gervasi et al, Dagstuhl Seminar 13372 (2013)

use Standard
use TabBlocks

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

init InitialState

// the type information can be omitted
function hasToken: Agents -> BOOLEAN
function colorM: Agents -> COLOR
function colorT: -> COLOR
function state: Agents -> BOOLEAN  \\  control state or mode
function hasMessage: Agents -> BOOLEAN
function index: Agents -> NUMBER

rule Machine =
	// MESSAGE PASSING
	// receive a message and become active
	if hasMessage(self) then
		state(self) := ACTIVE	// A
		hasMessage(self) := false
	else// a machine only becomes passive, if it has no
		// message (removes
		// clash between A and B)
		choose spontaneous in {true, false} do
			if state(self) = ACTIVE and spontaneous then
				state(self) := PASSIVE	// B

	// TOKEN PASSING
	// Rule 0 in paper
	if hasToken(self) then
		if state(self) = ACTIVE then
			skip
		else
			if not isMaster(self) then
				PassToken

	// when active, we can spontaneous send a message
	// Rule 0 in paper - continued
	choose spontaneous in {true, false} do
		if state(self) = ACTIVE and spontaneous then
			// don't allow sending messages to yourself
			// (solves the problem with clearing messages)
			choose dest in machines with dest != self do
				SendMessage(dest)

	// Master related stuff
	// Rules 3+4 in paper
	if tokenIndicatesFinished then
		StopASM
	else
		if unsuccessful and state(self) = PASSIVE then
			PassToken

rule PassToken =
	// Rule 2 in paper
	hasToken(self) := false
	hasToken(pred(self)) := true
	if isMaster(self) then	// master always sends a white token
		colorT := WHITE
	else
		if colorM(self) = BLACK then
			colorT := BLACK

	// Rule 5 in paper
	colorM(self) := WHITE

rule SendMessage(dest) =
	hasMessage(dest) := true
	// Rule 1 in paper
	if (gt(dest,self)) then
		colorM(self) := BLACK

rule StopASM =
	forall m in Agents do
		program(m) := undef
	print "global termination detected!"

derived tokenIndicatesFinished = (colorT = WHITE) and hasToken(self)
and isMaster(self) and state(self) = PASSIVE

derived unsuccessful = (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