diff --git a/mCRL2/TrafiicLights/v1/v1.mcrl2proj b/mCRL2/TrafiicLights/v1/v1.mcrl2proj new file mode 100644 index 0000000..e9162bd --- /dev/null +++ b/mCRL2/TrafiicLights/v1/v1.mcrl2proj @@ -0,0 +1,4 @@ + + v1_spec.mcrl2 + + diff --git a/mCRL2/TrafiicLights/v1/v1_spec.lps b/mCRL2/TrafiicLights/v1/v1_spec.lps new file mode 100644 index 0000000..f00fa55 Binary files /dev/null and b/mCRL2/TrafiicLights/v1/v1_spec.lps differ diff --git a/mCRL2/TrafiicLights/v1/v1_spec.lts b/mCRL2/TrafiicLights/v1/v1_spec.lts new file mode 100644 index 0000000..005536c Binary files /dev/null and b/mCRL2/TrafiicLights/v1/v1_spec.lts differ diff --git a/mCRL2/TrafiicLights/v1/v1_spec.mcrl2 b/mCRL2/TrafiicLights/v1/v1_spec.mcrl2 new file mode 100644 index 0000000..cf47e47 --- /dev/null +++ b/mCRL2/TrafiicLights/v1/v1_spec.mcrl2 @@ -0,0 +1,32 @@ + +sort + CardinalDirection = struct north | east | south | west; + + +sort + Colour = struct red | green | yellow; + +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). + TF(direction, nextColour(colour)) + ; + + + +init + TrafficLight(north) || TrafficLight(east) || TrafficLight(south) || TrafficLight(west) +; \ No newline at end of file