diff --git a/mCRL2/TrafficLights/v4/v4_spec.lps b/mCRL2/TrafficLights/v4/v4_spec.lps index cfc93b3..a184cb0 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 ee795b2..a3fd64c 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 3794ae5..00e0a77 100644 --- a/mCRL2/TrafficLights/v4/v4_spec.mcrl2 +++ b/mCRL2/TrafficLights/v4/v4_spec.mcrl2 @@ -39,7 +39,8 @@ act changedLight: Colour; changeDirection: CardinalDirection; changedDirection: CardinalDirection; - emptyAct; + wait; + proceed; %------------------------------------------------------------------------ @@ -52,7 +53,7 @@ proc <> %ansonsten show(direction, colour) . %aktuellen Zustand zeigen (colour == red) %wenn rot - -> ChangeDirection(direction) %Richtungswechsel, wenn wieder zurück + -> wait . ChangeDirection(direction) %Richtungswechsel, wenn wieder zurück . ChangeLight(direction, colour) % -> zur nächsten Farbe wechseln. <> ChangeLight(direction, colour) %ansonsten zum nächsten Zustand wechseln. @@ -69,22 +70,27 @@ proc ; System = + hide({%unnötige Informationen verstecken + proceed, + changedDirection, + changedLight + }, allow({ show, - %changeLight, changedLight, - %changeDirection, changedDirection, - emptyAct + proceed }, comm({ changeDirection | changeDirection -> changedDirection, - changeLight | changeLight -> changedLight + changeLight | changeLight -> changedLight, + wait | wait -> proceed }, + TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) || changeDirection(north) || changeDirection(south) %starten der Prozesse und auslösen des ersten Richtungswechsels - )); + ))); init System