Parallele_Verteilte_Systeme/mCRL2/TrafficLights/v1/v1_spec.mcrl2

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

%-----------------------------------------------------------------------------
sort
	Colour = struct red | green | yellow;

%Definition Farbliche Reihenfolge

map
	nextColour: Colour -> Colour;

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

%------------------------------------------------------------------------------
act
	show : CardinalDirection # Colour;

proc
	TrafficLight(direction : CardinalDirection) = TF(direction, red);

	TF(direction : CardinalDirection, colour : Colour) =
		show(direction, colour) . %zeige aktuellen Zustand
			TF(direction, nextColour(colour)) %zum n<>chsten Zustand wechseln
	;

%-----------------------------------------------------------------------------
%Initialisation der seperaten Ampeln
init
	TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west)
;