Parallele_Verteilte_Systeme/mCRL2/TrafficLights/v4/v4_spec.mcrl2

%-----------------------------------------------------------------------

sort
	CardinalDirection = struct north | east | south | west;

map
	oppositeDirection: CardinalDirection -> CardinalDirection;
	nextDirection: CardinalDirection -> CardinalDirection;

eqn
	oppositeDirection(north) = south;
	oppositeDirection(south) = north;
	oppositeDirection(east) = west;
	oppositeDirection(west) = east;

	nextDirection(north) = east;
	nextDirection(east) = south;
	nextDirection(south) = west;
	nextDirection(west) = north;

%-----------------------------------------------------------------------

sort
	Colour = struct red | green | yellow;

map
	nextColour: Colour -> Colour;

eqn
	nextColour(red) = green;
	nextColour(green) = yellow;
	nextColour(yellow) = red;

%------------------------------------------------------------------------

act
	show : CardinalDirection # Colour;
	changeLight: Colour;
	changedLight: Colour;
	changeDirection: CardinalDirection;
	changedDirection: CardinalDirection;
	emptyAct;
	
%------------------------------------------------------------------------

proc
	TrafficLight(direction : CardinalDirection) = TL(direction, red, true);

	TL(direction : CardinalDirection, colour : Colour, firstStart : Bool) =
		(firstStart)
		-> changeDirection(direction) . ChangeLight(direction, colour)
		<>
			show(direction, colour) .
			(colour == red) 
				-> ChangeDirection(direction) . ChangeLight(direction, colour)
				<> ChangeLight(direction, colour)
		
	;

	ChangeDirection(direction : CardinalDirection) =
		changeDirection(nextDirection(direction)) . changeDirection(direction)
	;
	
	ChangeLight(direction : CardinalDirection, colour : Colour) =
		changeLight(nextColour(colour)) . TL(direction, nextColour(colour), false)
	;

	System =
		allow({
			show, 
			%changeLight,
			changedLight,
			%changeDirection, 
			changedDirection,
			emptyAct
		},
		comm({
			changeDirection | changeDirection -> changedDirection,
			changeLight | changeLight -> changedLight
			
		},

		TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) || changeDirection(north) || changeDirection(south)
	));

init
	  System
;