Add example 3 from Day & Atlee.

test/test_files/day_atlee/statechart_fig9_trafficlight.svg

@@ -0,0 +1,163 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
+ "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
+<!-- Generated by graphviz version 2.40.1 (20161225.0304)
+ -->
+<!-- Title: state transitions Pages: 1 -->
+<svg width="514pt" height="542pt"
+ viewBox="0.00 0.00 514.00 542.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
+<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 538)">
+<title>state transitions</title>
+<polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-538 510,-538 510,4 -4,4"/>
+<g id="clust1" class="cluster">
+<title>cluster__TrafficLight</title>
+<path fill="none" stroke="#000000" stroke-width="2" d="M20,-8C20,-8 486,-8 486,-8 492,-8 498,-14 498,-20 498,-20 498,-483 498,-483 498,-489 492,-495 486,-495 486,-495 20,-495 20,-495 14,-495 8,-489 8,-483 8,-483 8,-20 8,-20 8,-14 14,-8 20,-8"/>
+<text text-anchor="start" x="223.8306" y="-476.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">TrafficLight</text>
+</g>
+<g id="clust2" class="cluster">
+<title>cluster__TrafficLight_EastWest</title>
+<polygon fill="none" stroke="#000000" stroke-dasharray="5,2" points="261,-16 261,-457 490,-457 490,-16 261,-16"/>
+<text text-anchor="start" x="350.3296" y="-438.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">EastWest</text>
+</g>
+<g id="clust3" class="cluster">
+<title>cluster__TrafficLight_NorthSouth</title>
+<polygon fill="none" stroke="#000000" stroke-dasharray="5,2" points="24,-16 24,-457 253,-457 253,-16 24,-16"/>
+<text text-anchor="start" x="108.158" y="-438.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">NorthSouth</text>
+</g>
+<!-- __initial -->
+<g id="node1" class="node">
+<title>__initial</title>
+<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="16" cy="-528.5" rx="5.5" ry="5.5"/>
+</g>
+<!-- _TrafficLight -->
+<!-- __initial&#45;&gt;_TrafficLight -->
+<g id="edge1" class="edge">
+<title>__initial&#45;&gt;_TrafficLight</title>
+<path fill="none" stroke="#000000" d="M16,-522.9533C16,-518.7779 16,-512.5043 16,-505.0332"/>
+<polygon fill="#000000" stroke="#000000" points="19.5001,-504.9971 16,-494.9971 12.5001,-504.9972 19.5001,-504.9971"/>
+<text text-anchor="middle" x="17.3895" y="-506" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
+</g>
+<!-- _TrafficLight_EastWest -->
+<!-- _TrafficLight_EastWest_initial -->
+<g id="node4" class="node">
+<title>_TrafficLight_EastWest_initial</title>
+<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="334" cy="-413.5" rx="5.5" ry="5.5"/>
+</g>
+<!-- _TrafficLight_EastWest_EW_Red -->
+<g id="node7" class="node">
+<title>_TrafficLight_EastWest_EW_Red</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="398,-326 270,-326 270,-280 398,-280 398,-326"/>
+<text text-anchor="start" x="309.9976" y="-309.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">EW_Red</text>
+<text text-anchor="start" x="275.5006" y="-289.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">onentry/ ^out.set_light</text>
+<polygon fill="#000000" stroke="#000000" points="270,-303 270,-303 398,-303 398,-303 270,-303"/>
+<path fill="none" stroke="#000000" stroke-width="2" d="M283,-281C283,-281 385,-281 385,-281 391,-281 397,-287 397,-293 397,-293 397,-313 397,-313 397,-319 391,-325 385,-325 385,-325 283,-325 283,-325 277,-325 271,-319 271,-313 271,-313 271,-293 271,-293 271,-287 277,-281 283,-281"/>
+</g>
+<!-- _TrafficLight_EastWest_initial&#45;&gt;_TrafficLight_EastWest_EW_Red -->
+<g id="edge2" class="edge">
+<title>_TrafficLight_EastWest_initial&#45;&gt;_TrafficLight_EastWest_EW_Red</title>
+<path fill="none" stroke="#000000" d="M334,-407.8288C334,-403.1736 334,-396.4097 334,-390.5 334,-390.5 334,-390.5 334,-343.5 334,-341.127 334,-338.6757 334,-336.2081"/>
+<polygon fill="#000000" stroke="#000000" points="337.5001,-336.1306 334,-326.1306 330.5001,-336.1306 337.5001,-336.1306"/>
+<text text-anchor="middle" x="335.3895" y="-364" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
+</g>
+<!-- _TrafficLight_EastWest_EW_Yellow -->
+<g id="node5" class="node">
+<title>_TrafficLight_EastWest_EW_Yellow</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="419,-70 291,-70 291,-24 419,-24 419,-70"/>
+<text text-anchor="start" x="324.3334" y="-53.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">EW_Yellow</text>
+<text text-anchor="start" x="296.5006" y="-33.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">onentry/ ^out.set_light</text>
+<polygon fill="#000000" stroke="#000000" points="291,-47 291,-47 419,-47 419,-47 291,-47"/>
+<path fill="none" stroke="#000000" stroke-width="2" d="M304,-25C304,-25 406,-25 406,-25 412,-25 418,-31 418,-37 418,-37 418,-57 418,-57 418,-63 412,-69 406,-69 406,-69 304,-69 304,-69 298,-69 292,-63 292,-57 292,-57 292,-37 292,-37 292,-31 298,-25 304,-25"/>
+</g>
+<!-- _TrafficLight_EastWest_EW_Yellow&#45;&gt;_TrafficLight_EastWest_EW_Red -->
+<g id="edge3" class="edge">
+<title>_TrafficLight_EastWest_EW_Yellow&#45;&gt;_TrafficLight_EastWest_EW_Red</title>
+<path fill="none" stroke="#000000" d="M297.8491,-70.1402C293.6406,-74.9318 291,-80.6625 291,-87.5 291,-262.5 291,-262.5 291,-262.5 291,-265.5766 291.5905,-268.4882 292.6331,-271.2314"/>
+<polygon fill="#000000" stroke="#000000" points="289.641,-273.048 297.7188,-279.9037 295.6793,-269.507 289.641,-273.048"/>
+<text text-anchor="start" x="291" y="-172" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">change &#160;&#160;</text>
+</g>
+<!-- _TrafficLight_EastWest_EW_Green -->
+<g id="node6" class="node">
+<title>_TrafficLight_EastWest_EW_Green</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="482,-198 354,-198 354,-152 482,-152 482,-198"/>
+<text text-anchor="start" x="388.3288" y="-181.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">EW_Green</text>
+<text text-anchor="start" x="359.5006" y="-161.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">onentry/ ^out.set_light</text>
+<polygon fill="#000000" stroke="#000000" points="354,-175 354,-175 482,-175 482,-175 354,-175"/>
+<path fill="none" stroke="#000000" stroke-width="2" d="M367,-153C367,-153 469,-153 469,-153 475,-153 481,-159 481,-165 481,-165 481,-185 481,-185 481,-191 475,-197 469,-197 469,-197 367,-197 367,-197 361,-197 355,-191 355,-185 355,-185 355,-165 355,-165 355,-159 361,-153 367,-153"/>
+</g>
+<!-- _TrafficLight_EastWest_EW_Green&#45;&gt;_TrafficLight_EastWest_EW_Yellow -->
+<g id="edge4" class="edge">
+<title>_TrafficLight_EastWest_EW_Green&#45;&gt;_TrafficLight_EastWest_EW_Yellow</title>
+<path fill="none" stroke="#000000" d="M383.4063,-151.6338C379.5625,-146.6363 377,-140.9034 377,-134.5 377,-134.5 377,-134.5 377,-87.5 377,-84.9095 376.6481,-82.3264 376.0334,-79.7904"/>
+<polygon fill="#000000" stroke="#000000" points="379.2882,-78.5002 372.548,-70.3259 372.7194,-80.9193 379.2882,-78.5002"/>
+<text text-anchor="start" x="377" y="-108" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">end &#160;&#160;</text>
+</g>
+<!-- _TrafficLight_EastWest_EW_Red&#45;&gt;_TrafficLight_EastWest_EW_Green -->
+<g id="edge5" class="edge">
+<title>_TrafficLight_EastWest_EW_Red&#45;&gt;_TrafficLight_EastWest_EW_Green</title>
+<path fill="none" stroke="#000000" d="M370.2813,-279.9037C374.3125,-274.8762 377,-269.0633 377,-262.5 377,-262.5 377,-262.5 377,-215.5 377,-212.5985 377.5261,-209.8346 378.4592,-207.2144"/>
+<polygon fill="#000000" stroke="#000000" points="381.5811,-208.8027 383.4063,-198.3662 375.4712,-205.3866 381.5811,-208.8027"/>
+<text text-anchor="start" x="377" y="-236" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">change &#160;&#160;</text>
+</g>
+<!-- _TrafficLight_NorthSouth -->
+<!-- _TrafficLight_NorthSouth_initial -->
+<g id="node9" class="node">
+<title>_TrafficLight_NorthSouth_initial</title>
+<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="97" cy="-413.5" rx="5.5" ry="5.5"/>
+</g>
+<!-- _TrafficLight_NorthSouth_NS_Green -->
+<g id="node12" class="node">
+<title>_TrafficLight_NorthSouth_NS_Green</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="161,-326 33,-326 33,-280 161,-280 161,-326"/>
+<text text-anchor="start" x="68.6608" y="-309.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">NS_Green</text>
+<text text-anchor="start" x="38.5006" y="-289.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">onentry/ ^out.set_light</text>
+<polygon fill="#000000" stroke="#000000" points="33,-303 33,-303 161,-303 161,-303 33,-303"/>
+<path fill="none" stroke="#000000" stroke-width="2" d="M46,-281C46,-281 148,-281 148,-281 154,-281 160,-287 160,-293 160,-293 160,-313 160,-313 160,-319 154,-325 148,-325 148,-325 46,-325 46,-325 40,-325 34,-319 34,-313 34,-313 34,-293 34,-293 34,-287 40,-281 46,-281"/>
+</g>
+<!-- _TrafficLight_NorthSouth_initial&#45;&gt;_TrafficLight_NorthSouth_NS_Green -->
+<g id="edge6" class="edge">
+<title>_TrafficLight_NorthSouth_initial&#45;&gt;_TrafficLight_NorthSouth_NS_Green</title>
+<path fill="none" stroke="#000000" d="M97,-407.8288C97,-403.1736 97,-396.4097 97,-390.5 97,-390.5 97,-390.5 97,-343.5 97,-341.127 97,-338.6757 97,-336.2081"/>
+<polygon fill="#000000" stroke="#000000" points="100.5001,-336.1306 97,-326.1306 93.5001,-336.1306 100.5001,-336.1306"/>
+<text text-anchor="middle" x="98.3895" y="-364" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
+</g>
+<!-- _TrafficLight_NorthSouth_NS_Red -->
+<g id="node10" class="node">
+<title>_TrafficLight_NorthSouth_NS_Red</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="182,-70 54,-70 54,-24 182,-24 182,-70"/>
+<text text-anchor="start" x="95.3296" y="-53.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">NS_Red</text>
+<text text-anchor="start" x="59.5006" y="-33.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">onentry/ ^out.set_light</text>
+<polygon fill="#000000" stroke="#000000" points="54,-47 54,-47 182,-47 182,-47 54,-47"/>
+<path fill="none" stroke="#000000" stroke-width="2" d="M67,-25C67,-25 169,-25 169,-25 175,-25 181,-31 181,-37 181,-37 181,-57 181,-57 181,-63 175,-69 169,-69 169,-69 67,-69 67,-69 61,-69 55,-63 55,-57 55,-57 55,-37 55,-37 55,-31 61,-25 67,-25"/>
+</g>
+<!-- _TrafficLight_NorthSouth_NS_Red&#45;&gt;_TrafficLight_NorthSouth_NS_Green -->
+<g id="edge7" class="edge">
+<title>_TrafficLight_NorthSouth_NS_Red&#45;&gt;_TrafficLight_NorthSouth_NS_Green</title>
+<path fill="none" stroke="#000000" d="M60.8491,-70.1402C56.6406,-74.9318 54,-80.6625 54,-87.5 54,-262.5 54,-262.5 54,-262.5 54,-265.5766 54.5905,-268.4882 55.6331,-271.2314"/>
+<polygon fill="#000000" stroke="#000000" points="52.641,-273.048 60.7188,-279.9037 58.6793,-269.507 52.641,-273.048"/>
+<text text-anchor="start" x="54" y="-172" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">change &#160;&#160;</text>
+</g>
+<!-- _TrafficLight_NorthSouth_NS_Yellow -->
+<g id="node11" class="node">
+<title>_TrafficLight_NorthSouth_NS_Yellow</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="245,-198 117,-198 117,-152 245,-152 245,-198"/>
+<text text-anchor="start" x="151.6654" y="-181.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">NS_Yellow</text>
+<text text-anchor="start" x="122.5006" y="-161.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">onentry/ ^out.set_light</text>
+<polygon fill="#000000" stroke="#000000" points="117,-175 117,-175 245,-175 245,-175 117,-175"/>
+<path fill="none" stroke="#000000" stroke-width="2" d="M130,-153C130,-153 232,-153 232,-153 238,-153 244,-159 244,-165 244,-165 244,-185 244,-185 244,-191 238,-197 232,-197 232,-197 130,-197 130,-197 124,-197 118,-191 118,-185 118,-185 118,-165 118,-165 118,-159 124,-153 130,-153"/>
+</g>
+<!-- _TrafficLight_NorthSouth_NS_Yellow&#45;&gt;_TrafficLight_NorthSouth_NS_Red -->
+<g id="edge8" class="edge">
+<title>_TrafficLight_NorthSouth_NS_Yellow&#45;&gt;_TrafficLight_NorthSouth_NS_Red</title>
+<path fill="none" stroke="#000000" d="M146.4063,-151.6338C142.5625,-146.6363 140,-140.9034 140,-134.5 140,-134.5 140,-134.5 140,-87.5 140,-84.9095 139.6481,-82.3264 139.0334,-79.7904"/>
+<polygon fill="#000000" stroke="#000000" points="142.2882,-78.5002 135.548,-70.3259 135.7194,-80.9193 142.2882,-78.5002"/>
+<text text-anchor="start" x="140" y="-108" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">change &#160;&#160;</text>
+</g>
+<!-- _TrafficLight_NorthSouth_NS_Green&#45;&gt;_TrafficLight_NorthSouth_NS_Yellow -->
+<g id="edge9" class="edge">
+<title>_TrafficLight_NorthSouth_NS_Green&#45;&gt;_TrafficLight_NorthSouth_NS_Yellow</title>
+<path fill="none" stroke="#000000" d="M133.2813,-279.9037C137.3125,-274.8762 140,-269.0633 140,-262.5 140,-262.5 140,-262.5 140,-215.5 140,-212.5985 140.5261,-209.8346 141.4592,-207.2144"/>
+<polygon fill="#000000" stroke="#000000" points="144.5811,-208.8027 146.4063,-198.3662 138.4712,-205.3866 144.5811,-208.8027"/>
+<text text-anchor="start" x="140" y="-236" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">end &#160;&#160;</text>
+</g>
+</g>
+</svg>

test/test_files/day_atlee/statechart_fig9_trafficlight.xml

@@ -0,0 +1,81 @@
+<?xml version="1.0" ?>
+<statechart>
+  <semantics big_step_maximality="take_one"/>
+
+  <inport name="in">
+    <event name="change"/>
+    <event name="end"/>
+  </inport>
+
+  <outport name="out">
+    <event name="set_light"/>
+  </outport>
+
+  <root>
+    <parallel id="TrafficLight">
+      <state id="NorthSouth" initial="NS_Green">
+        <state id="NS_Green">
+          <onentry>
+            <raise event="set_light">
+              <param expr='"NS"'/>
+              <param expr='"Green"'/>
+            </raise>
+          </onentry>
+          <transition event="end" target="../NS_Yellow"/>
+        </state>
+
+        <state id="NS_Yellow">
+          <onentry>
+            <raise event="set_light">
+              <param expr='"NS"'/>
+              <param expr='"Yellow"'/>
+            </raise>
+          </onentry>
+          <transition event="change" target="../NS_Red"/>
+        </state>
+
+        <state id="NS_Red">
+          <onentry>
+            <raise event="set_light">
+              <param expr='"NS"'/>
+              <param expr='"Red"'/>
+            </raise>
+          </onentry>
+          <transition event="change" target="../NS_Green"/>
+        </state>
+      </state>
+
+      <state id="EastWest" initial="EW_Red">
+        <state id="EW_Red">
+          <onentry>
+            <raise event="set_light">
+              <param expr='"EW"'/>
+              <param expr='"Red"'/>
+            </raise>
+          </onentry>
+          <transition event="change" target="../EW_Green"/>
+        </state>
+
+        <state id="EW_Green">
+          <onentry>
+            <raise event="set_light">
+              <param expr='"EW"'/>
+              <param expr='"Green"'/>
+            </raise>
+          </onentry>
+          <transition event="end" target="../EW_Yellow"/>
+        </state>
+
+        <state id="EW_Yellow">
+          <onentry>
+            <raise event="set_light">
+              <param expr='"EW"'/>
+              <param expr='"Yellow"'/>
+            </raise>
+          </onentry>
+          <transition event="change" target="../EW_Red"/>
+        </state>
+      </state>
+    </parallel>
+  </root>
+</statechart>

test/test_files/day_atlee/test_03_trafficlight_many.xml

@@ -0,0 +1,46 @@
+<?xml version="1.0" ?>
+<test>
+  <statechart src="statechart_fig9_trafficlight.xml">
+    <override_semantics concurrency="many"/>
+    <!-- No observable difference from Concurrency: 'single' -->
+  </statechart>
+
+  <input>
+    <event port="in" name="end" time="15 s"/>
+    <event port="in" name="change" time="18 s"/>
+  </input>
+
+  <output>
+    <!-- entering default states -->
+    <big_step>
+      <event port="out" name="set_light">
+        <param val='"NS"'/>
+        <param val='"Green"'/>
+      </event>
+      <event port="out" name="set_light">
+        <param val='"EW"'/>
+        <param val='"Red"'/>
+      </event>
+    </big_step>
+
+    <!-- response to input event 'end' -->
+    <big_step>
+      <event port="out" name="set_light">
+        <param val='"NS"'/>
+        <param val='"Yellow"'/>
+      </event>
+    </big_step>
+
+    <!-- response to input event 'change' -->
+    <big_step>
+      <event port="out" name="set_light">
+        <param val='"NS"'/>
+        <param val='"Red"'/>
+      </event>
+      <event port="out" name="set_light">
+        <param val='"EW"'/>
+        <param val='"Green"'/>
+      </event>
+    </big_step>
+  </output>
+</test>

test/test_files/day_atlee/test_03_trafficlight_single.xml

@@ -0,0 +1,50 @@
+<?xml version="1.0" ?>
+<test>
+  <statechart src="statechart_fig9_trafficlight.xml">
+    <override_semantics concurrency="single"/>
+    <!-- although according to Day & Atlee, this choice of semantics yields incorrect behavior
+         because between small steps, the traffic lights could be "yellow" in one direction and
+         "green" in the other at the same time, in between small steps, I would argue that this
+         doesn't matter as long as the statechart's input/output from big steps is correct (which
+         is the case), as this is the only way it can interact with the environment. -->
+  </statechart>
+
+  <input>
+    <event port="in" name="end" time="15 s"/>
+    <event port="in" name="change" time="18 s"/>
+  </input>
+
+  <output>
+    <!-- entering default states -->
+    <big_step>
+      <event port="out" name="set_light">
+        <param val='"NS"'/>
+        <param val='"Green"'/>
+      </event>
+      <event port="out" name="set_light">
+        <param val='"EW"'/>
+        <param val='"Red"'/>
+      </event>
+    </big_step>
+
+    <!-- response to input event 'end' -->
+    <big_step>
+      <event port="out" name="set_light">
+        <param val='"NS"'/>
+        <param val='"Yellow"'/>
+      </event>
+    </big_step>
+
+    <!-- response to input event 'change' -->
+    <big_step>
+      <event port="out" name="set_light">
+        <param val='"NS"'/>
+        <param val='"Red"'/>
+      </event>
+      <event port="out" name="set_light">
+        <param val='"EW"'/>
+        <param val='"Green"'/>
+      </event>
+    </big_step>
+  </output>
+</test>