Browse Source

Add another example from Day & Atlee + correction in fire_transition: must exit all descendants of arena (not LCA!) + performance improvement in fire_transition.

Joeri Exelmans 5 years ago
parent
commit
f57b8feee2

+ 9 - 12
src/sccd/statechart/dynamic/statechart_execution.py

@@ -59,10 +59,7 @@ class StatechartExecution:
 
     # events: list SORTED by event id
     def fire_transition(self, events: List[Event], t: Transition):
-        try:
-            def __exitSet():
-                return [s for s in reversed(t.gen.lca.gen.descendants) if (s in self.configuration)]
-            
+        try:            
             def __enterSet(targets):
                 target = targets[0]
                 for a in reversed(target.gen.ancestors):
@@ -81,8 +78,12 @@ class StatechartExecution:
                             targets.append(e_t)
                 return targets
 
+            ctx = EvalContext(current_state=self, events=events, memory=self.rhs_memory)
+
+            print_debug("fire " + str(t))
+
             # exit states...
-            exit_set = __exitSet()
+            exit_set = (s for s in reversed(self.configuration) if s.gen.state_id_bitmap & t.gen.arena.gen.descendant_bitmap)
             for s in exit_set:
                 # remember which state(s) we were in if a history state is present
                 for h in s.gen.history:
@@ -91,16 +92,14 @@ class StatechartExecution:
                         f = lambda s0: not s0.gen.descendants and s0 in s.gen.descendants
                     self.history_values[h.gen.state_id] = list(filter(f, self.configuration))
 
-            ctx = EvalContext(current_state=self, events=events, memory=self.rhs_memory)
-
-            print_debug("fire " + str(t))
-            for s in exit_set:
                 print_debug(termcolor.colored('  EXIT %s' % s.gen.full_name, 'green'))
                 self.eventless_states -= s.gen.has_eventless_transitions
                 # execute exit action(s)
                 self._perform_actions(ctx, s.exit)
                 # self.rhs_memory.pop_local_scope(s.scope)
                 self.configuration_bitmap &= ~s.gen.state_id_bitmap
+
+            # print("arena was: ", t.gen.arena.gen.full_name)
                     
             # execute transition action(s)
             self.rhs_memory.push_frame(t.scope) # make room for event parameters on stack
@@ -110,9 +109,7 @@ class StatechartExecution:
             self.rhs_memory.pop_frame()
                 
             # enter states...
-            targets = __getEffectiveTargetStates()
-            enter_set = __enterSet(targets)
-            for s in enter_set:
+            for s in __enterSet(__getEffectiveTargetStates()):
                 print_debug(termcolor.colored('  ENTER %s' % s.gen.full_name, 'green'))
                 self.eventless_states += s.gen.has_eventless_transitions
                 self.configuration_bitmap |= s.gen.state_id_bitmap

+ 9 - 1
src/sccd/statechart/static/tree.py

@@ -184,6 +184,8 @@ class Transition:
 @dataclass(frozen=True)
 class TransitionOptimization:
     lca: State
+    lca_bitmap: Bitmap
+    arena: State
     arena_bitmap: Bitmap
 
 # @dataclass
@@ -271,6 +273,12 @@ class StateTree:
                             lca = a
                             break
 
+            arena = lca
+            while isinstance(arena, ParallelState):
+                arena = arena.parent
+
             t.gen = TransitionOptimization(
                 lca=lca,
-                arena_bitmap=lca.gen.descendant_bitmap | lca.gen.state_id_bitmap)
+                lca_bitmap=lca.gen.descendant_bitmap | lca.gen.state_id_bitmap,
+                arena=arena,
+                arena_bitmap=arena.gen.descendant_bitmap | arena.gen.state_id_bitmap)

+ 162 - 0
test/test_files/day_atlee/statechart_fig10_counter.svg

@@ -0,0 +1,162 @@
+<?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="272pt" height="640pt"
+ viewBox="0.00 0.00 272.00 640.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 636)">
+<title>state transitions</title>
+<polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-636 268,-636 268,4 -4,4"/>
+<g id="clust1" class="cluster">
+<title>cluster__Counter</title>
+<path fill="none" stroke="#000000" stroke-width="2" d="M20,-8C20,-8 244,-8 244,-8 250,-8 256,-14 256,-20 256,-20 256,-581 256,-581 256,-587 250,-593 244,-593 244,-593 20,-593 20,-593 14,-593 8,-587 8,-581 8,-581 8,-20 8,-20 8,-14 14,-8 20,-8"/>
+<text text-anchor="start" x="110.6622" y="-574.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Counter</text>
+</g>
+<g id="clust2" class="cluster">
+<title>cluster__Counter_Status</title>
+<polygon fill="none" stroke="#000000" stroke-dasharray="5,2" points="120,-16 120,-216 248,-216 248,-16 120,-16"/>
+<text text-anchor="start" x="166.993" y="-197.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Status</text>
+</g>
+<g id="clust3" class="cluster">
+<title>cluster__Counter_Bit_2</title>
+<polygon fill="none" stroke="#000000" stroke-dasharray="5,2" points="176,-262 176,-555 248,-555 248,-262 176,-262"/>
+<text text-anchor="start" x="198.829" y="-536.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Bit_2</text>
+</g>
+<g id="clust4" class="cluster">
+<title>cluster__Counter_Bit_1</title>
+<polygon fill="none" stroke="#000000" stroke-dasharray="5,2" points="24,-262 24,-555 168,-555 168,-262 24,-262"/>
+<text text-anchor="start" x="82.829" y="-536.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Bit_1</text>
+</g>
+<!-- __initial -->
+<g id="node1" class="node">
+<title>__initial</title>
+<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="16" cy="-626.5" rx="5.5" ry="5.5"/>
+</g>
+<!-- _Counter -->
+<!-- __initial&#45;&gt;_Counter -->
+<g id="edge1" class="edge">
+<title>__initial&#45;&gt;_Counter</title>
+<path fill="none" stroke="#000000" d="M16,-620.9533C16,-616.7779 16,-610.5043 16,-603.0332"/>
+<polygon fill="#000000" stroke="#000000" points="19.5001,-602.9971 16,-592.9971 12.5001,-602.9972 19.5001,-602.9971"/>
+<text text-anchor="middle" x="17.3895" y="-604" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
+</g>
+<!-- _Counter_Status -->
+<!-- _Counter_Status_initial -->
+<g id="node4" class="node">
+<title>_Counter_Status_initial</title>
+<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="212" cy="-160" rx="5.5" ry="5.5"/>
+</g>
+<!-- _Counter_Status_Counting -->
+<g id="node6" class="node">
+<title>_Counter_Status_Counting</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="219,-60 149,-60 149,-24 219,-24 219,-60"/>
+<text text-anchor="start" x="159.9928" y="-38.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Counting</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M161.3333,-25C161.3333,-25 206.6667,-25 206.6667,-25 212.3333,-25 218,-30.6667 218,-36.3333 218,-36.3333 218,-47.6667 218,-47.6667 218,-53.3333 212.3333,-59 206.6667,-59 206.6667,-59 161.3333,-59 161.3333,-59 155.6667,-59 150,-53.3333 150,-47.6667 150,-47.6667 150,-36.3333 150,-36.3333 150,-30.6667 155.6667,-25 161.3333,-25"/>
+</g>
+<!-- _Counter_Status_initial&#45;&gt;_Counter_Status_Counting -->
+<g id="edge2" class="edge">
+<title>_Counter_Status_initial&#45;&gt;_Counter_Status_Counting</title>
+<path fill="none" stroke="#000000" d="M215.7109,-155.2521C220.4375,-148.7156 228,-136.398 228,-124.5 228,-124.5 228,-124.5 228,-77.5 228,-73.7549 227.0225,-70.3376 225.359,-67.2335"/>
+<polygon fill="#000000" stroke="#000000" points="228.0404,-64.9815 219.0959,-59.3028 222.5469,-69.3199 228.0404,-64.9815"/>
+<text text-anchor="middle" x="229.3895" y="-98" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
+</g>
+<!-- _Counter_Status_Max -->
+<g id="node5" class="node">
+<title>_Counter_Status_Max</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="184,-178 128,-178 128,-142 184,-142 184,-178"/>
+<text text-anchor="start" x="144.6672" y="-156.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Max</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M140.3333,-143C140.3333,-143 171.6667,-143 171.6667,-143 177.3333,-143 183,-148.6667 183,-154.3333 183,-154.3333 183,-165.6667 183,-165.6667 183,-171.3333 177.3333,-177 171.6667,-177 171.6667,-177 140.3333,-177 140.3333,-177 134.6667,-177 129,-171.3333 129,-165.6667 129,-165.6667 129,-154.3333 129,-154.3333 129,-148.6667 134.6667,-143 140.3333,-143"/>
+</g>
+<!-- _Counter_Status_Max&#45;&gt;_Counter_Status_Counting -->
+<g id="edge3" class="edge">
+<title>_Counter_Status_Max&#45;&gt;_Counter_Status_Counting</title>
+<path fill="none" stroke="#000000" d="M153.8839,-141.9651C153.3875,-136.3756 153,-130.1903 153,-124.5 153,-124.5 153,-124.5 153,-77.5 153,-74.5083 153.6323,-71.6471 154.7164,-68.94"/>
+<polygon fill="#000000" stroke="#000000" points="157.7198,-70.7371 159.8799,-60.3648 151.723,-67.1262 157.7198,-70.7371"/>
+<text text-anchor="start" x="153" y="-98" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">reset &#160;&#160;</text>
+</g>
+<!-- _Counter_Bit_2 -->
+<!-- _Counter_Bit_2_initial -->
+<g id="node8" class="node">
+<title>_Counter_Bit_2_initial</title>
+<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="212" cy="-511.5" rx="5.5" ry="5.5"/>
+</g>
+<!-- _Counter_Bit_2_Bit_21 -->
+<g id="node10" class="node">
+<title>_Counter_Bit_2_Bit_21</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="240,-424 184,-424 184,-388 240,-388 240,-424"/>
+<text text-anchor="start" x="194.9936" y="-402.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Bit_21</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M196.3333,-389C196.3333,-389 227.6667,-389 227.6667,-389 233.3333,-389 239,-394.6667 239,-400.3333 239,-400.3333 239,-411.6667 239,-411.6667 239,-417.3333 233.3333,-423 227.6667,-423 227.6667,-423 196.3333,-423 196.3333,-423 190.6667,-423 185,-417.3333 185,-411.6667 185,-411.6667 185,-400.3333 185,-400.3333 185,-394.6667 190.6667,-389 196.3333,-389"/>
+</g>
+<!-- _Counter_Bit_2_initial&#45;&gt;_Counter_Bit_2_Bit_21 -->
+<g id="edge4" class="edge">
+<title>_Counter_Bit_2_initial&#45;&gt;_Counter_Bit_2_Bit_21</title>
+<path fill="none" stroke="#000000" d="M212,-505.8288C212,-501.1736 212,-494.4097 212,-488.5 212,-488.5 212,-488.5 212,-441.5 212,-439.1079 212,-436.6252 212,-434.1342"/>
+<polygon fill="#000000" stroke="#000000" points="215.5001,-434.0597 212,-424.0598 208.5001,-434.0598 215.5001,-434.0597"/>
+<text text-anchor="middle" x="213.3895" y="-462" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
+</g>
+<!-- _Counter_Bit_2_Bit_22 -->
+<g id="node9" class="node">
+<title>_Counter_Bit_2_Bit_22</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="240,-306 184,-306 184,-270 240,-270 240,-306"/>
+<text text-anchor="start" x="194.9936" y="-284.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Bit_22</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M196.3333,-271C196.3333,-271 227.6667,-271 227.6667,-271 233.3333,-271 239,-276.6667 239,-282.3333 239,-282.3333 239,-293.6667 239,-293.6667 239,-299.3333 233.3333,-305 227.6667,-305 227.6667,-305 196.3333,-305 196.3333,-305 190.6667,-305 185,-299.3333 185,-293.6667 185,-293.6667 185,-282.3333 185,-282.3333 185,-276.6667 190.6667,-271 196.3333,-271"/>
+</g>
+<!-- _Counter_Bit_2_Bit_22&#45;&gt;_Counter_Status_Max -->
+<g id="edge5" class="edge">
+<title>_Counter_Bit_2_Bit_22&#45;&gt;_Counter_Status_Max</title>
+<path fill="none" stroke="#000000" d="M204.0953,-269.9322C194.7264,-248.5176 179.0133,-212.6019 168.1083,-187.676"/>
+<polygon fill="#000000" stroke="#000000" points="171.2606,-186.149 164.0458,-178.3904 164.8475,-188.9548 171.2606,-186.149"/>
+<text text-anchor="start" x="193" y="-236" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">tk1^out.done &#160;&#160;</text>
+</g>
+<!-- _Counter_Bit_2_Bit_21&#45;&gt;_Counter_Bit_2_Bit_22 -->
+<g id="edge6" class="edge">
+<title>_Counter_Bit_2_Bit_21&#45;&gt;_Counter_Bit_2_Bit_22</title>
+<path fill="none" stroke="#000000" d="M212,-387.9402C212,-382.3497 212,-376.1701 212,-370.5 212,-370.5 212,-370.5 212,-323.5 212,-321.1079 212,-318.6252 212,-316.1342"/>
+<polygon fill="#000000" stroke="#000000" points="215.5001,-316.0597 212,-306.0598 208.5001,-316.0598 215.5001,-316.0597"/>
+<text text-anchor="start" x="212" y="-344" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">tk1 &#160;&#160;</text>
+</g>
+<!-- _Counter_Bit_1 -->
+<!-- _Counter_Bit_1_initial -->
+<g id="node12" class="node">
+<title>_Counter_Bit_1_initial</title>
+<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="78" cy="-511.5" rx="5.5" ry="5.5"/>
+</g>
+<!-- _Counter_Bit_1_Bit_11 -->
+<g id="node14" class="node">
+<title>_Counter_Bit_1_Bit_11</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="106,-424 50,-424 50,-388 106,-388 106,-424"/>
+<text text-anchor="start" x="60.9936" y="-402.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Bit_11</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M62.3333,-389C62.3333,-389 93.6667,-389 93.6667,-389 99.3333,-389 105,-394.6667 105,-400.3333 105,-400.3333 105,-411.6667 105,-411.6667 105,-417.3333 99.3333,-423 93.6667,-423 93.6667,-423 62.3333,-423 62.3333,-423 56.6667,-423 51,-417.3333 51,-411.6667 51,-411.6667 51,-400.3333 51,-400.3333 51,-394.6667 56.6667,-389 62.3333,-389"/>
+</g>
+<!-- _Counter_Bit_1_initial&#45;&gt;_Counter_Bit_1_Bit_11 -->
+<g id="edge7" class="edge">
+<title>_Counter_Bit_1_initial&#45;&gt;_Counter_Bit_1_Bit_11</title>
+<path fill="none" stroke="#000000" d="M78,-505.8288C78,-501.1736 78,-494.4097 78,-488.5 78,-488.5 78,-488.5 78,-441.5 78,-439.1079 78,-436.6252 78,-434.1342"/>
+<polygon fill="#000000" stroke="#000000" points="81.5001,-434.0597 78,-424.0598 74.5001,-434.0598 81.5001,-434.0597"/>
+<text text-anchor="middle" x="79.3895" y="-462" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
+</g>
+<!-- _Counter_Bit_1_Bit_12 -->
+<g id="node13" class="node">
+<title>_Counter_Bit_1_Bit_12</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="124,-306 68,-306 68,-270 124,-270 124,-306"/>
+<text text-anchor="start" x="78.9936" y="-284.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Bit_12</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M80.3333,-271C80.3333,-271 111.6667,-271 111.6667,-271 117.3333,-271 123,-276.6667 123,-282.3333 123,-282.3333 123,-293.6667 123,-293.6667 123,-299.3333 117.3333,-305 111.6667,-305 111.6667,-305 80.3333,-305 80.3333,-305 74.6667,-305 69,-299.3333 69,-293.6667 69,-293.6667 69,-282.3333 69,-282.3333 69,-276.6667 74.6667,-271 80.3333,-271"/>
+</g>
+<!-- _Counter_Bit_1_Bit_12&#45;&gt;_Counter_Bit_1_Bit_11 -->
+<g id="edge8" class="edge">
+<title>_Counter_Bit_1_Bit_12&#45;&gt;_Counter_Bit_1_Bit_11</title>
+<path fill="none" stroke="#000000" d="M67.7524,-301.1838C60.1549,-306.7482 54,-314.1435 54,-323.5 54,-370.5 54,-370.5 54,-370.5 54,-373.3317 54.5305,-376.1061 55.4339,-378.7776"/>
+<polygon fill="#000000" stroke="#000000" points="52.421,-380.5757 60.0562,-387.9211 58.6681,-377.4176 52.421,-380.5757"/>
+<text text-anchor="start" x="54" y="-344" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">tk0^tk1 &#160;&#160;</text>
+</g>
+<!-- _Counter_Bit_1_Bit_11&#45;&gt;_Counter_Bit_1_Bit_12 -->
+<g id="edge9" class="edge">
+<title>_Counter_Bit_1_Bit_11&#45;&gt;_Counter_Bit_1_Bit_12</title>
+<path fill="none" stroke="#000000" d="M106.2431,-400.4378C121.8052,-395.5506 138,-386.5975 138,-370.5 138,-370.5 138,-370.5 138,-323.5 138,-317.506 135.474,-312.3169 131.661,-307.8984"/>
+<polygon fill="#000000" stroke="#000000" points="134.009,-305.3028 124.2476,-301.1838 129.3098,-310.491 134.009,-305.3028"/>
+<text text-anchor="start" x="138" y="-344" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">tk0 &#160;&#160;</text>
+</g>
+</g>
+</svg>

+ 45 - 0
test/test_files/day_atlee/statechart_fig10_counter.xml

@@ -0,0 +1,45 @@
+<?xml version="1.0" ?>
+<statechart>
+  <inport name="in">
+    <event name="tk0"/>
+  </inport>
+
+  <outport name="out">
+    <event name="done"/>
+  </outport>
+
+  <root>
+    <parallel id="Counter">
+      <state id="Bit_1" initial="Bit_11">
+        <state id="Bit_11">
+          <transition event="tk0" target="../Bit_12"/>
+        </state>
+
+        <state id="Bit_12">
+          <transition event="tk0" target="../Bit_11">
+            <raise event="tk1"/>
+          </transition>
+        </state>
+      </state>
+
+      <state id="Bit_2" initial="Bit_21">
+        <state id="Bit_21">
+          <transition event="tk1" target="../Bit_22"/>
+        </state>
+
+        <state id="Bit_22">
+          <transition event="tk1" target="/Counter/Status/Max">
+            <raise event="done"/>
+          </transition>
+        </state>
+      </state>
+
+      <state id="Status" initial="Counting">
+        <state id="Counting"/>
+        <state id="Max">
+          <transition event="reset" target="../Counting"/>
+        </state>
+      </state>
+    </parallel>
+  </root>
+</statechart>

+ 21 - 0
test/test_files/day_atlee/test_04_counter_many_arenaortho.xml

@@ -0,0 +1,21 @@
+<?xml version="1.0" ?>
+<test>
+  <statechart src="statechart_fig10_counter.xml">
+    <override_semantics
+      big_step_maximality="take_one"
+      concurrency="many"
+      internal_event_lifeline="same"/>
+  </statechart>
+
+  <input>
+    <!-- setup ... -->
+    <event port="in" name="tk0" time="10 ms"/>
+    <event port="in" name="tk0" time="20 ms"/>
+    <event port="in" name="tk0" time="30 ms"/>
+    <!-- we are now in Bit_12, Bit_22 and Counting -->
+    <event port="in" name="tk0" time="40 ms"/>
+  </input>
+
+  <output>
+  </output>
+</test>

+ 24 - 0
test/test_files/day_atlee/test_04_counter_single.xml

@@ -0,0 +1,24 @@
+<?xml version="1.0" ?>
+<test>
+  <statechart src="statechart_fig10_counter.xml">
+    <!-- these semantic configuration is not discussed in Day & Atlee, but I added it for fun -->
+    <override_semantics
+      big_step_maximality="take_one"
+      internal_event_lifeline="next_small_step"/>
+  </statechart>
+
+  <input>
+    <!-- setup ... -->
+    <event port="in" name="tk0" time="10 ms"/>
+    <event port="in" name="tk0" time="20 ms"/>
+    <event port="in" name="tk0" time="30 ms"/>
+    <!-- we are now in Bit_12, Bit_22 and Counting -->
+    <event port="in" name="tk0" time="40 ms"/>
+  </input>
+
+  <output>
+    <big_step>
+      <event port="out" name="done"/>
+    </big_step>
+  </output>
+</test>