diff --git a/mCRL2/TrafiicLights/TrafficLights v1_spec.lts b/mCRL2/TrafficLights/TrafficLights v1_spec.lts similarity index 100% rename from mCRL2/TrafiicLights/TrafficLights v1_spec.lts rename to mCRL2/TrafficLights/TrafficLights v1_spec.lts diff --git a/mCRL2/TrafiicLights/TrafficLights v2_spec.lps b/mCRL2/TrafficLights/TrafficLights v2_spec.lps similarity index 100% rename from mCRL2/TrafiicLights/TrafficLights v2_spec.lps rename to mCRL2/TrafficLights/TrafficLights v2_spec.lps diff --git a/mCRL2/TrafiicLights/TrafficLights v2_spec.lts b/mCRL2/TrafficLights/TrafficLights v2_spec.lts similarity index 100% rename from mCRL2/TrafiicLights/TrafficLights v2_spec.lts rename to mCRL2/TrafficLights/TrafficLights v2_spec.lts diff --git a/mCRL2/TrafiicLights/TrafficLights v3_spec.lps b/mCRL2/TrafficLights/TrafficLights v3_spec.lps similarity index 100% rename from mCRL2/TrafiicLights/TrafficLights v3_spec.lps rename to mCRL2/TrafficLights/TrafficLights v3_spec.lps diff --git a/mCRL2/TrafiicLights/TrafficLights v3_spec.lts b/mCRL2/TrafficLights/TrafficLights v3_spec.lts similarity index 100% rename from mCRL2/TrafiicLights/TrafficLights v3_spec.lts rename to mCRL2/TrafficLights/TrafficLights v3_spec.lts diff --git a/mCRL2/TrafiicLights/TrafficLights v4_spec.lps b/mCRL2/TrafficLights/TrafficLights v4_spec.lps similarity index 100% rename from mCRL2/TrafiicLights/TrafficLights v4_spec.lps rename to mCRL2/TrafficLights/TrafficLights v4_spec.lps diff --git a/mCRL2/TrafiicLights/TrafficLights v4_spec.lts b/mCRL2/TrafficLights/TrafficLights v4_spec.lts similarity index 100% rename from mCRL2/TrafiicLights/TrafficLights v4_spec.lts rename to mCRL2/TrafficLights/TrafficLights v4_spec.lts diff --git a/mCRL2/TrafiicLights/TrafficLights v4_spec_bb.lts b/mCRL2/TrafficLights/TrafficLights v4_spec_bb.lts similarity index 100% rename from mCRL2/TrafiicLights/TrafficLights v4_spec_bb.lts rename to mCRL2/TrafficLights/TrafficLights v4_spec_bb.lts diff --git a/mCRL2/TrafiicLights/v1/v1.mcrl2proj b/mCRL2/TrafficLights/v1/v1.mcrl2proj similarity index 100% rename from mCRL2/TrafiicLights/v1/v1.mcrl2proj rename to mCRL2/TrafficLights/v1/v1.mcrl2proj diff --git a/mCRL2/TrafiicLights/v1/v1_spec.lps b/mCRL2/TrafficLights/v1/v1_spec.lps similarity index 100% rename from mCRL2/TrafiicLights/v1/v1_spec.lps rename to mCRL2/TrafficLights/v1/v1_spec.lps diff --git a/mCRL2/TrafiicLights/v1/v1_spec.lts b/mCRL2/TrafficLights/v1/v1_spec.lts similarity index 100% rename from mCRL2/TrafiicLights/v1/v1_spec.lts rename to mCRL2/TrafficLights/v1/v1_spec.lts diff --git a/mCRL2/TrafiicLights/v1/v1_spec.mcrl2 b/mCRL2/TrafficLights/v1/v1_spec.mcrl2 similarity index 100% rename from mCRL2/TrafiicLights/v1/v1_spec.mcrl2 rename to mCRL2/TrafficLights/v1/v1_spec.mcrl2 diff --git a/mCRL2/TrafiicLights/v2/v2.mcrl2proj b/mCRL2/TrafficLights/v2/v2.mcrl2proj similarity index 100% rename from mCRL2/TrafiicLights/v2/v2.mcrl2proj rename to mCRL2/TrafficLights/v2/v2.mcrl2proj diff --git a/mCRL2/TrafiicLights/v2/v2_spec.lps b/mCRL2/TrafficLights/v2/v2_spec.lps similarity index 100% rename from mCRL2/TrafiicLights/v2/v2_spec.lps rename to mCRL2/TrafficLights/v2/v2_spec.lps diff --git a/mCRL2/TrafiicLights/v2/v2_spec.lts b/mCRL2/TrafficLights/v2/v2_spec.lts similarity index 100% rename from mCRL2/TrafiicLights/v2/v2_spec.lts rename to mCRL2/TrafficLights/v2/v2_spec.lts diff --git a/mCRL2/TrafiicLights/v2/v2_spec.mcrl2 b/mCRL2/TrafficLights/v2/v2_spec.mcrl2 similarity index 100% rename from mCRL2/TrafiicLights/v2/v2_spec.mcrl2 rename to mCRL2/TrafficLights/v2/v2_spec.mcrl2 diff --git a/mCRL2/TrafiicLights/v3/v3.mcrl2proj b/mCRL2/TrafficLights/v3/v3.mcrl2proj similarity index 100% rename from mCRL2/TrafiicLights/v3/v3.mcrl2proj rename to mCRL2/TrafficLights/v3/v3.mcrl2proj diff --git a/mCRL2/TrafiicLights/v3/v3_spec.lps b/mCRL2/TrafficLights/v3/v3_spec.lps similarity index 100% rename from mCRL2/TrafiicLights/v3/v3_spec.lps rename to mCRL2/TrafficLights/v3/v3_spec.lps diff --git a/mCRL2/TrafiicLights/v3/v3_spec.lts b/mCRL2/TrafficLights/v3/v3_spec.lts similarity index 100% rename from mCRL2/TrafiicLights/v3/v3_spec.lts rename to mCRL2/TrafficLights/v3/v3_spec.lts diff --git a/mCRL2/TrafiicLights/v3/v3_spec.mcrl2 b/mCRL2/TrafficLights/v3/v3_spec.mcrl2 similarity index 100% rename from mCRL2/TrafiicLights/v3/v3_spec.mcrl2 rename to mCRL2/TrafficLights/v3/v3_spec.mcrl2 diff --git a/mCRL2/TrafiicLights/v4/v4.mcrl2proj b/mCRL2/TrafficLights/v4/v4.mcrl2proj similarity index 100% rename from mCRL2/TrafiicLights/v4/v4.mcrl2proj rename to mCRL2/TrafficLights/v4/v4.mcrl2proj diff --git a/mCRL2/TrafiicLights/v4/v4_spec.mcrl2 b/mCRL2/TrafficLights/v4/v4_spec.mcrl2 similarity index 81% rename from mCRL2/TrafiicLights/v4/v4_spec.mcrl2 rename to mCRL2/TrafficLights/v4/v4_spec.mcrl2 index 2001644..ba4aab3 100644 --- a/mCRL2/TrafiicLights/v4/v4_spec.mcrl2 +++ b/mCRL2/TrafficLights/v4/v4_spec.mcrl2 @@ -47,13 +47,15 @@ proc TrafficLight(direction : CardinalDirection) = TL(direction, red); TL(direction : CardinalDirection, colour : Colour) = + show(direction, colour). (colour == red) - -> changeDirection(nextDirection(direction)) . TL(direction, nextColour(colour)) - <> changeLight(nextColour(colour)) . show(direction, nextColour(colour)) . TL(direction, nextColour(colour)) - + -> ChangeLight(direction, colour) + <> changeDirection(nextDirection(direction)) . ChangeLight(direction, colour) ; - + ChangeLight(direction : CardinalDirection, colour : Colour) = + changeLight(nextColour(colour)) . TL(direction, nextColour(colour)) + ; System = allow({ @@ -70,7 +72,7 @@ proc }, - TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) + TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) || changeDirection(north) || changeDirection(south) )); init