diff --git a/mCRL2/TrafficLights/v4/v4_spec.lps b/mCRL2/TrafficLights/v4/v4_spec.lps index f9c31e4..13c7fda 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 d8a302d..42ebf1c 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 e6a6eab..f961434 100644 --- a/mCRL2/TrafficLights/v4/v4_spec.mcrl2 +++ b/mCRL2/TrafficLights/v4/v4_spec.mcrl2 @@ -44,17 +44,25 @@ act %------------------------------------------------------------------------ proc - TrafficLight(direction : CardinalDirection) = TL(direction, red); + TrafficLight(direction : CardinalDirection) = TL(direction, red, true); - TL(direction : CardinalDirection, colour : Colour) = - show(direction, colour). - (colour == red) - -> (changeDirection(nextDirection(direction)) . changeDirection(direction) . ChangeLight(direction, colour)) - <> ChangeLight(direction, colour) + 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) + + ; + + ChangeDirection(direction : CardinalDirection) = + changeDirection(nextDirection(direction)) . changeDirection(direction) ; ChangeLight(direction : CardinalDirection, colour : Colour) = - changeLight(nextColour(colour)) . TL(direction, nextColour(colour)) + changeLight(nextColour(colour)) . TL(direction, nextColour(colour), false) ; System =