Parallele_Verteilte_Systeme/mCRL2/TrafficLights/v4/v4_spec.mcrl2

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

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

map
	nextDirection: CardinalDirection -> CardinalDirection;

eqn

	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;
	wait;
	proceed;
	
%------------------------------------------------------------------------

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

	TL(direction : CardinalDirection, colour : Colour, firstStart : Bool) =
		(firstStart) %beim ersten Start nur das Licht umschalten
		-> changeDirection(direction) . TL(direction, colour, false)
		<> %ansonsten
			show(direction, colour) . %aktuellen Zustand zeigen
			(colour == red) %wenn rot
				-> wait . ChangeDirection(direction) %Richtungswechsel, wenn wieder zur<75>ck
					. ChangeLight(direction, colour) % -> zur n<>chsten Farbe wechseln.
				<> ChangeLight(direction, colour) %ansonsten zum n<>chsten Zustand wechseln.
		
	;

	ChangeDirection(direction : CardinalDirection) =
		changeDirection(nextDirection(direction)) %n<>chste Richtung freigeben 
		. changeDirection(direction) % -> warten bis eigene Richtung wieder freigegeben.
	;
	
	ChangeLight(direction : CardinalDirection, colour : Colour) =
		changeLight(nextColour(colour)) %zur n<>chsten Farbe wechseln, wenn beide Richtungen dies autorisieren
		. TL(direction, nextColour(colour), false) %fortfahren
	;

	System =
		hide({%unn<6E>tige Informationen verstecken
			proceed,
			changedDirection,
			changedLight
		},
		allow({
			show,
			changedLight,
			changedDirection,
			proceed
		},
		comm({
			changeDirection | changeDirection -> changedDirection,
			changeLight | changeLight -> changedLight,
			wait | wait -> proceed
		},
		

		TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) || changeDirection(north) || changeDirection(south)
		%starten der Prozesse und ausl<73>sen des ersten Richtungswechsels
	)));

init
	  System
;