Parallele_Verteilte_Systeme/mCRL2/TrafficLights/v2/v2_spec.mcrl2

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

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

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

eqn

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

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


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

sort
	Colour = struct red | green | yellow;

map
	nextColour: Colour -> Colour;

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

%------------------------------------------------------------------------
%die aktuellen Werte f<>r die verschiedenen Ampeln werden in einer KeyValue Map gespeichert.

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;

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

map
	unsafe : Map # CardinalDirection -> Bool;

var
	status: Map;
	direction: CardinalDirection;

eqn
	unsafe(status, direction) = ((status(direction) in {green, yellow} || status(oppositeDirection(direction)) in {green, yellow})
				 && (status(nextDirection(direction)) in {green, yellow}
				|| status(oppositeDirection(nextDirection(direction))) in {green, yellow}));

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

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

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

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

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

	Monitor(status : Map) = 
		(unsafe(status, north)) %ist aktueller Zustand unsicher ?
			-> crossingUnsafe(status(north), status(east), status(south), status(west)) . delta %unsicherer Zustand, deadlock
			
		<>%wenn aktueller Zustand sicher:
		sum direction : CardinalDirection.(
			sum c : Colour .
				 seeColour(direction, c) . %jede m<>gliche Kombination anbieten
					Monitor(status= status[direction -> c])%und entsprechend speichern
		);

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

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

	
		

init
	  System
;