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

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

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

sort
	Colour = struct red | green | yellow;

map
	nextColour: Colour -> Colour;

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

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

sort
	Map = K -> V;

map
	_Map: V -> Map;

var
	k: K;
	v: V;

eqn
	_Map(v)(k) = v;

sort
	K = CardinalDirection;
	V = Colour;

map
	combinations: Map;



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

act
	show : CardinalDirection # Colour;
	seeColour : CardinalDirection # Colour;
	colourSeen : CardinalDirection # Colour;

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

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

	TL(direction : CardinalDirection, colour : Colour) =
		show(direction, colour) . TL(direction, nextColour(colour))
	;

	Monitor(status : Map) = 
		sum direction : CardinalDirection.(
			sum c : Colour .
				(c == green) ->
					(direction == north || direction == south) ->
						((status(east) == red && status(west) == red) ->  % sind die anderen Ampeln rot ?
							seeColour(direction, c) . Monitor(status= status[direction -> c])) % dann darf fortgefahren werden
					<>
						((status(north) == red && status(south) == red) ->
							seeColour(direction, c) . Monitor(status= status[direction -> c]))
				<> %soll nicht grün gezeigt werden kann einfach fortgefahren werden, es wurde ja bereits überprüft
				seeColour(direction, c) .
						Monitor(status= status[direction -> c])
				 	
	);


	System =
		allow({
			colourSeen
		},
		comm({
			show | seeColour -> colourSeen
			
		},

		TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) || Monitor(_Map(red))
	));
		

	
		

init
	  System
;