diff --git a/mCRL2/TrafficLights/v4/v4_spec.lps b/mCRL2/TrafficLights/v4/v4_spec.lps index 13c7fda..cfc93b3 100644 Binary files a/mCRL2/TrafficLights/v4/v4_spec.lps and b/mCRL2/TrafficLights/v4/v4_spec.lps differ diff --git a/mCRL2/TrafficLights/v4/v4_spec.lts b/mCRL2/TrafficLights/v4/v4_spec.lts index 42ebf1c..ee795b2 100644 Binary files a/mCRL2/TrafficLights/v4/v4_spec.lts and b/mCRL2/TrafficLights/v4/v4_spec.lts differ diff --git a/mCRL2/TrafficLights/v4/v4_spec.mcrl2 b/mCRL2/TrafficLights/v4/v4_spec.mcrl2 index f961434..3794ae5 100644 --- a/mCRL2/TrafficLights/v4/v4_spec.mcrl2 +++ b/mCRL2/TrafficLights/v4/v4_spec.mcrl2 @@ -47,27 +47,30 @@ proc TrafficLight(direction : CardinalDirection) = TL(direction, red, true); TL(direction : CardinalDirection, colour : Colour, firstStart : Bool) = - (firstStart) - -> changeDirection(direction) . ChangeLight(direction, colour) - <> - show(direction, colour) . - (colour == red) - -> ChangeDirection(direction) . ChangeLight(direction, colour) - <> ChangeLight(direction, colour) + (firstStart) %beim ersten Start nur das Licht umschalten + -> changeDirection(direction) . TL(direction, colour, false) + <> %ansonsten + show(direction, colour) . %aktuellen Zustand zeigen + (colour == red) %wenn rot + -> ChangeDirection(direction) %Richtungswechsel, wenn wieder zurück + . ChangeLight(direction, colour) % -> zur nächsten Farbe wechseln. + <> ChangeLight(direction, colour) %ansonsten zum nächsten Zustand wechseln. ; ChangeDirection(direction : CardinalDirection) = - changeDirection(nextDirection(direction)) . changeDirection(direction) + changeDirection(nextDirection(direction)) %nächste Richtung freigeben + . changeDirection(direction) % -> warten bis eigene Richtung wieder freigegeben. ; ChangeLight(direction : CardinalDirection, colour : Colour) = - changeLight(nextColour(colour)) . TL(direction, nextColour(colour), false) + changeLight(nextColour(colour)) %zur nächsten Farbe wechseln, wenn beide Richtungen dies autorisieren + . TL(direction, nextColour(colour), false) %fortfahren ; System = allow({ - show, + show, %changeLight, changedLight, %changeDirection, @@ -77,10 +80,10 @@ proc comm({ changeDirection | changeDirection -> changedDirection, changeLight | changeLight -> changedLight - }, TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) || changeDirection(north) || changeDirection(south) + %starten der Prozesse und auslösen des ersten Richtungswechsels )); init