Add Traffic Light example

TrafficLight/TrafficLight.mch

+MACHINE TrafficLight
+SETS colors = {red, redyellow, yellow, green}
+VARIABLES tl_cars, tl_peds
+INVARIANT tl_cars : colors & tl_peds : {red, green} &
+	  (tl_peds = red or tl_cars = red)
+              
+INITIALISATION  tl_cars := red; tl_peds := red
+OPERATIONS
+cars_ry = SELECT tl_cars = red & tl_peds = red THEN tl_cars := redyellow END;
+cars_y = SELECT tl_cars = green & tl_peds = red THEN tl_cars := yellow END;
+cars_g = SELECT tl_cars = redyellow & tl_peds = red THEN tl_cars := green END;
+cars_r = SELECT tl_cars = yellow & tl_peds = red THEN tl_cars := red END;
+peds_r = SELECT tl_peds = green & tl_cars = red THEN tl_peds := red END;
+peds_g = SELECT tl_peds = red & tl_cars = red THEN tl_peds := green END
+END

TrafficLight/traffic_light.json

+{
+  "svg":"traffic_light.svg",
+  "items":[
+    {
+      "id":"cars_red",
+      "attr":"fill",
+      "value":"IF tl_cars = red or tl_cars = redyellow THEN \"red\" ELSE \"black\" END"
+    },
+    {
+      "id":"cars_yellow_1",
+      "attr":"fill",
+      "value":"IF tl_cars = yellow or tl_cars = redyellow THEN \"yellow\" ELSE \"black\" END"
+    },
+    {
+      "id":"cars_yellow_1",
+      "attr":"visibility",
+      "value":"IF tl_cars /= green THEN \"visible\" ELSE \"hidden\" END"
+    },
+    {
+      "id":"cars_yellow_2",
+      "attr":"fill",
+      "value":"IF tl_cars = yellow or tl_cars = redyellow THEN \"yellow\" ELSE \"black\" END"
+    },
+    {
+      "id":"cars_yellow_2",
+      "attr":"visibility",
+      "value":"IF tl_cars /= red THEN \"visible\" ELSE \"hidden\" END"
+    },
+    {
+      "id":"cars_green",
+      "attr":"fill",
+      "value":"IF tl_cars = green THEN \"green\" ELSE \"black\" END"
+    },
+    {
+      "id":"peds_red",
+      "attr":"fill",
+      "value":"IF tl_peds = red THEN \"red\" ELSE \"black\" END"
+    },
+    {
+      "id":"peds_green",
+      "attr":"fill",
+      "value":"IF tl_peds = green THEN \"green\" ELSE \"black\" END"
+    }
+  ],
+  "events": [
+      {
+        "id":"cars_red",
+        "event":"cars_r"
+      },
+      {
+        "id":"cars_yellow_1",
+        "event":"cars_ry"
+      },
+      {
+        "id":"cars_yellow_2",
+        "event":"cars_y"
+      },
+      {
+        "id":"cars_green",
+        "event":"cars_g"
+      },
+      {
+        "id":"peds_red",
+        "event":"peds_r"
+      },
+      {
+        "id":"peds_green",
+        "event":"peds_g"
+      }
+  ]
+}

TrafficLight/traffic_light.svg

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+   xmlns:dc="http://purl.org/dc/elements/1.1/"
+   xmlns:cc="http://creativecommons.org/ns#"
+   xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+   xmlns:svg="http://www.w3.org/2000/svg"
+   xmlns="http://www.w3.org/2000/svg"
+   width="300"
+   height="300"
+   viewBox="0 0 300.0 300.0"
+   version="1.1"
+   id="traffic_light_visualsiation">
+  <defs
+     id="defs2" />
+  <metadata
+     id="metadata5">
+    <rdf:RDF>
+      <cc:Work
+         rdf:about="">
+        <dc:format>image/svg+xml</dc:format>
+        <dc:type
+           rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
+        <dc:title></dc:title>
+      </cc:Work>
+    </rdf:RDF>
+  </metadata>
+    <g id="traffic_light_cars">
+      <circle cx="50" cy="50" r="40" stroke="black" stroke-width="3" fill="red" id="cars_red"/>
+      <circle cx="50" cy="150" r="40" stroke="black" stroke-width="3" fill="yellow" visibility="visible" id="cars_yellow_1"/>
+      <circle cx="50" cy="150" r="40" stroke="black" stroke-width="3" fill="yellow" visibility="hidden" id="cars_yellow_2"/>
+      <circle cx="50" cy="250" r="40" stroke="black" stroke-width="3" fill="green" id="cars_green"/>
+    </g>
+    <g id="traffic_light_peds">
+      <circle cx="150" cy="50" r="40" stroke="black" stroke-width="3" fill="red" id="peds_red"/>
+      <circle cx="150" cy="150" r="40" stroke="black" stroke-width="3" fill="green" id="peds_green"/>
+    </g>
+</svg>