Parallele_Verteilte_Systeme/mCRL2/TrafiicLights/v1/v1_spec.mcrl2

32 lines
566 B
Plaintext

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;
act
show : CardinalDirection # Colour;
proc
TrafficLight(direction : CardinalDirection) = TF(direction, red);
TF(direction : CardinalDirection, colour : Colour) =
show(direction, colour).
TF(direction, nextColour(colour))
;
init
TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west)
;