Parallele_Verteilte_Systeme/mCRL2/TrafficLights/v1/v1_spec.mcrl2

35 lines
929 B
Plaintext

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)
;