Parallele_Verteilte_Systeme/mCRL2/TrafficLights/v3/v3_spec.mcrl2

115 lines
2.3 KiB
Plaintext

%-----------------------------------------------------------------------
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;
%------------------------------------------------------------------------
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 # Colour -> Bool;
var
status: Map;
direction: CardinalDirection;
colour: Colour;
eqn
unsafe(status, direction, colour) = (colour 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;
%------------------------------------------------------------------------
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 .
(unsafe(status, direction, c))
-> delta
<> 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
;