Implemented 'Syntactic' big step maximality option (not yet fully tested)

src/sccd/execution/round.py

@@ -10,16 +10,16 @@ class CandidatesGenerator:
         self.cache = {}
 
 class CandidatesGeneratorCurrentConfigBased(CandidatesGenerator):
-    def generate(self, state, enabled_events: List[Event], arenas_changed: Bitmap) -> Iterable[Transition]:
+    def generate(self, state, enabled_events: List[Event], forbidden_arenas: Bitmap) -> Iterable[Transition]:
         events_bitmap = Bitmap.from_list(e.id for e in enabled_events)
-        key = (state.configuration_bitmap, arenas_changed)
+        key = (state.configuration_bitmap, forbidden_arenas)
 
         try:
             candidates = self.cache[key]
         except KeyError:
             candidates = self.cache[key] = [
                 t for s in state.configuration
-                    if (not arenas_changed & s.gen.state_id_bitmap)
+                    if (not forbidden_arenas & s.gen.state_id_bitmap)
                     for t in s.transitions
                 ]
             if self.reverse:
@@ -30,9 +30,9 @@ class CandidatesGeneratorCurrentConfigBased(CandidatesGenerator):
         return filter(filter_f, candidates)
 
 class CandidatesGeneratorEventBased(CandidatesGenerator):
-    def generate(self, state, enabled_events: List[Event], arenas_changed: Bitmap) -> Iterable[Transition]:
+    def generate(self, state, enabled_events: List[Event], forbidden_arenas: Bitmap) -> Iterable[Transition]:
         events_bitmap = Bitmap.from_list(e.id for e in enabled_events)
-        key = (events_bitmap, arenas_changed)
+        key = (events_bitmap, forbidden_arenas)
 
         try:
             candidates = self.cache[key]
@@ -40,7 +40,7 @@ class CandidatesGeneratorEventBased(CandidatesGenerator):
             candidates = self.cache[key] = [
                 t for t in state.model.tree.transition_list
                     if (not t.trigger or t.trigger.check(events_bitmap)) # todo: check port?
-                    and (not arenas_changed & t.source.gen.state_id_bitmap)
+                    and (not forbidden_arenas & t.source.gen.state_id_bitmap)
                 ]
             if self.reverse:
                 candidates.reverse()
@@ -49,6 +49,10 @@ class CandidatesGeneratorEventBased(CandidatesGenerator):
             return state.check_source(t) and state.check_guard(t, enabled_events)
         return filter(filter_f, candidates)
 
+# 1st bitmap: arenas covered by transitions fired
+# 2nd bitmap: arenas covered by transitions that had a stable target state
+RoundResult = Tuple[Bitmap, Bitmap]
+
 class Round(ABC):
     def __init__(self, name):
         self.name = name
@@ -62,18 +66,20 @@ class Round(ABC):
     def when_done(self, callback):
         self.callbacks.append(callback)
 
-    def run(self, arenas_changed: Bitmap = Bitmap()) -> Bitmap:
-        changed = self._internal_run(arenas_changed)
+    def run(self, forbidden_arenas: Bitmap = Bitmap()) -> RoundResult:
+        changed, stable = self._internal_run(forbidden_arenas)
         if changed:
+            # notify round observers
             for callback in self.callbacks:
                 callback()
+            # rotate enabled events
             self.remainder_events = self.next_events
             self.next_events = []
             print_debug("completed "+self.name)
-        return changed
+        return (changed, stable)
 
     @abstractmethod
-    def _internal_run(self, arenas_changed: Bitmap) -> Bitmap:
+    def _internal_run(self, forbidden_arenas: Bitmap) -> RoundResult:
         pass
 
     def add_remainder_event(self, event: Event):
@@ -91,32 +97,80 @@ class Round(ABC):
     def __repr__(self):
         return self.name
 
+class SuperRoundMaximality(ABC):
+    @staticmethod
+    @abstractmethod
+    def forbidden_arenas(forbidden_arenas: Bitmap, arenas_changed: Bitmap, arenas_stabilized: Bitmap) -> Bitmap:
+        pass
+
+class TakeOne(SuperRoundMaximality):
+    @staticmethod
+    def forbidden_arenas(forbidden_arenas: Bitmap, arenas_changed: Bitmap, arenas_stabilized: Bitmap) -> Bitmap:
+        return forbidden_arenas | arenas_changed
+
+class TakeMany(SuperRoundMaximality):
+    @staticmethod
+    def forbidden_arenas(forbidden_arenas: Bitmap, arenas_changed: Bitmap, arenas_stabilized: Bitmap) -> Bitmap:
+        return Bitmap()
+
+class Syntactic(SuperRoundMaximality):
+    @staticmethod
+    def forbidden_arenas(forbidden_arenas: Bitmap, arenas_changed: Bitmap, arenas_stabilized: Bitmap) -> Bitmap:
+        return forbidden_arenas | arenas_stabilized
+
 # Examples: Big step, combo step
 class SuperRound(Round):
-    def __init__(self, name, subround: Round, take_one: bool, limit: Optional[int] = None):
+    def __init__(self, name, subround: Round, maximality: SuperRoundMaximality):
         super().__init__(name)
         self.subround = subround
         subround.parent = self
-        self.take_one = take_one
+        self.maximality = maximality
+
+    def __repr__(self):
+        return self.name + " > " + self.subround.__repr__()
+
+    def _internal_run(self, forbidden_arenas: Bitmap) -> RoundResult:
+        arenas_changed = Bitmap()
+        arenas_stabilized = Bitmap()
+
+        while True:
+            forbidden = self.maximality.forbidden_arenas(forbidden_arenas, arenas_changed, arenas_stabilized)
+            changed, stabilized = self.subround.run(forbidden) # no forbidden arenas in subround
+            if not changed:
+                break # no more transitions could be executed, done!
+
+            arenas_changed |= changed
+            arenas_stabilized |= stabilized
+
+        return (arenas_changed, arenas_stabilized)
+
+# Almost identical to SuperRound, but counts subrounds and raises exception if limit exceeded.
+# Useful for maximality options possibly causing infinite big steps like TakeMany and Syntactic.
+class SuperRoundWithLimit(SuperRound):
+    def __init__(self, name, subround: Round, maximality: SuperRoundMaximality, limit: int):
+        super().__init__(name, subround, maximality)
         self.limit = limit
-    
-    def _internal_run(self, arenas_changed: Bitmap) -> Bitmap:
+
+    def _internal_run(self, forbidden_arenas: Bitmap) -> RoundResult:
+        arenas_changed = Bitmap()
+        arenas_stabilized = Bitmap()
+
         subrounds = 0
         while True:
-            if self.take_one:
-                changed = self.subround.run(arenas_changed)
-            else:
-                if self.limit and subrounds == self.limit:
-                    raise Exception("%s: Limit reached! (%d×%s) Possibly a never-ending big step." % (self.name, self.limit, self.subround.name))
-                changed = self.subround.run()
-                subrounds += 1
+            forbidden = self.maximality.forbidden_arenas(forbidden_arenas, arenas_changed, arenas_stabilized)
+            changed, stabilized = self.subround.run(forbidden) # no forbidden arenas in subround
             if not changed:
-                break
+                break # no more transitions could be executed, done!
+
+            subrounds += 1
+            if subrounds >= self.limit:
+                raise Exception("%s: Limit reached! (%d×%s) Possibly a never-ending big step." % (self.name, subrounds, self.subround.name))
+
             arenas_changed |= changed
-        return arenas_changed
+            arenas_stabilized |= stabilized
+
+        return (arenas_changed, arenas_stabilized)
 
-    def __repr__(self):
-        return self.name + " > " + self.subround.__repr__()
 
 class SmallStep(Round):
     def __init__(self, name, state, generator: CandidatesGenerator):
@@ -124,9 +178,9 @@ class SmallStep(Round):
         self.state = state
         self.generator = generator
 
-    def _internal_run(self, arenas_changed: Bitmap) -> Bitmap:
+    def _internal_run(self, forbidden_arenas: Bitmap) -> RoundResult:
         enabled_events = self.enabled_events()
-        candidates = self.generator.generate(self.state, enabled_events, arenas_changed)
+        candidates = self.generator.generate(self.state, enabled_events, forbidden_arenas)
 
         if is_debug():
             candidates = list(candidates) # convert generator to list (gotta do this, otherwise the generator will be all used up by our debug printing
@@ -137,5 +191,13 @@ class SmallStep(Round):
                 print_debug("candidates: " + str(candidates))
 
         for t in candidates:
-            arenas_changed |= self.state.fire_transition(enabled_events, t)
-            return arenas_changed
+            arena = self.state.fire_transition(enabled_events, t)
+
+            # Return after first transition execution
+            if t.targets[0].stable:
+                return (arena, arena)
+            else:
+                return (arena, Bitmap())
+
+        # There were no transition candidates
+        return (Bitmap(), Bitmap())

src/sccd/execution/statechart_instance.py

@@ -9,6 +9,10 @@ from sccd.execution.round import *
 from sccd.execution.statechart_state import *
 from sccd.execution.memory import *
 
+# Hardcoded limit on number of sub-rounds of combo and big step to detect never-ending superrounds.
+# TODO: make this configurable
+LIMIT = 1000
+
 class StatechartInstance(Instance):
     def __init__(self, statechart: Statechart, object_manager):
         self.object_manager = object_manager
@@ -24,12 +28,12 @@ class StatechartInstance(Instance):
 
 
         if semantics.big_step_maximality == BigStepMaximality.TAKE_ONE:
-            self._big_step = combo_step = SuperRound(termcolor.colored("big_one", 'red'), small_step, take_one=True) # No combo steps
+            self._big_step = combo_step = SuperRound(termcolor.colored("big_one", 'red'), small_step, maximality=TakeOne()) # No combo steps
 
-        elif semantics.big_step_maximality == BigStepMaximality.TAKE_MANY:
+        elif semantics.big_step_maximality == BigStepMaximality.TAKE_MANY or semantics.big_step_maximality == BigStepMaximality.SYNTACTIC:
             # Always add a layer of 'fairness' above our small steps, so
             # orthogonal transitions take turns fairly.
-            combo_one = SuperRound(termcolor.colored("combo_one", 'magenta'), small_step, take_one=True)
+            combo_one = SuperRound(termcolor.colored("combo_one", 'magenta'), small_step, maximality=TakeOne())
 
             if semantics.combo_step_maximality == ComboStepMaximality.COMBO_TAKE_ONE:
                 # Fairness round becomes our combo step round
@@ -37,12 +41,16 @@ class StatechartInstance(Instance):
 
             elif semantics.combo_step_maximality == ComboStepMaximality.COMBO_TAKE_MANY:
                 # Add even more layers, basically an onion at this point.
-                combo_step = SuperRound(termcolor.colored("combo_many", 'cyan'), combo_one, take_one=False, limit=1000)
+                combo_step = SuperRoundWithLimit(termcolor.colored("combo_many", 'cyan'), combo_one, maximality=TakeMany(), limit=LIMIT)
 
             else:
                 raise Exception("Unsupported option: %s" % semantics.combo_step_maximality)
 
-            self._big_step = SuperRound(termcolor.colored("big_many", 'red'), combo_step, take_one=False, limit=1000)
+            if semantics.big_step_maximality == BigStepMaximality.TAKE_MANY:
+                self._big_step = SuperRoundWithLimit(termcolor.colored("big_many", 'red'), combo_step, maximality=TakeMany(), limit=LIMIT)
+            else:
+                self._big_step = SuperRoundWithLimit(termcolor.colored("big_syntactic", 'red'), combo_step, maximality=Syntactic(), limit=LIMIT)
+
         else:
             raise Exception("Unsupported option: %s" % semantics.big_step_maximality)
 
@@ -68,6 +76,7 @@ class StatechartInstance(Instance):
             InternalEventLifeline.NEXT_SMALL_STEP: small_step.add_next_event,
 
             InternalEventLifeline.REMAINDER: self._big_step.add_remainder_event,
+            InternalEventLifeline.SAME: small_step.add_remainder_event,
         }[semantics.internal_event_lifeline]
 
         memory = Memory(statechart.scope)

src/sccd/parser/statechart_parser.py

@@ -188,6 +188,9 @@ class StateParser(ActionParser):
       else:
         raise Exception("Only 1 root <state> allowed.")
 
+    if el.get("stable", "") == "true":
+      state.stable = True
+
     self.state.push(state)
     self.state_children.push({})
 

src/sccd/syntax/tree.py

@@ -9,8 +9,10 @@ class State:
     short_name: str # value of 'id' attribute in XML
     parent: Optional['State'] # only None if root state
 
+    stable: bool = False # whether this is a stable stabe. this field is ignored if maximality semantics is not set to SYNTACTIC
+
     children: List['State'] = field(default_factory=list)
-    default_state = None
+    default_state = None # child state pointed to by 'initial' attribute
 
     transitions: List['Transition'] = field(default_factory=list)
 
@@ -170,6 +172,7 @@ class StateTree:
         self.state_list = [] # depth-first list of states
         self.transition_list = [] # all transitions in the tree, sorted by source state, depth-first
         self.after_triggers = []
+        self.stable_bitmap = Bitmap() # bitmap of state IDs of states that are stable. Only used for SYNTACTIC-maximality semantics.
 
         next_id = 0
 
@@ -222,6 +225,9 @@ class StateTree:
                 has_eventless_transitions=has_eventless_transitions,
                 after_triggers=after_triggers)
 
+            if state.stable:
+                self.stable_bitmap |= bit(state_id)
+
             # print("state:", full_name)
             # print("ancestors:", len(ancestors))
 
@@ -243,4 +249,4 @@ class StateTree:
 
             t.gen = TransitionOptimization(
                 lca=lca,
-                arena_bitmap=lca.gen.descendant_bitmap.set(lca.gen.state_id))
+                arena_bitmap=lca.gen.descendant_bitmap | lca.gen.state_id_bitmap)

src/sccd/util/bitmap.py

@@ -6,6 +6,7 @@ import math
 # Methods that return a Bitmap return a new bitmap and leave the arguments untouched.
 # To change a bitmap, use an assignment operator ('=', '|=', '&=', ...)
 class Bitmap(int):
+  # Create from int
   def __new__(cls, value=0, *args, **kwargs):
     return super(cls, cls).__new__(cls, value)
 
@@ -30,12 +31,6 @@ class Bitmap(int):
   def __invert__(self):
     return self.__class__(super().__invert__())
 
-  def set(self, pos):
-    return self.__or__(2**pos)
-
-  def unset(self, pos):
-    return self.__and__(~2**pos)
-
   def has(self, pos):
     return self & 2**pos
 
@@ -53,5 +48,6 @@ class Bitmap(int):
         yield pos
       pos += 1
 
+# Create a bitmap with a single bit set.
 def bit(pos):
   return Bitmap(2 ** pos)

test/render.py

@@ -56,8 +56,10 @@ if __name__ == '__main__':
         f = open(smcat_target, 'w')
         w = IndentingWriter(f)
 
-        def name_to_label(name):
-          label = name.split('/')[-1]
+        def name_to_label(state):
+          label = state.gen.full_name.split('/')[-1]
+          if state.stable:
+            label += " ✓"
           return label if len(label) else "root"
         def name_to_name(name):
           return name.replace('/','_')
@@ -68,6 +70,7 @@ if __name__ == '__main__':
           class Gen:
             full_name: str
           def __init__(self, name):
+            self.stable = False
             self.gen = PseudoState.Gen(name)
         # Used for drawing initial state
         class PseudoTransition:
@@ -84,7 +87,7 @@ if __name__ == '__main__':
           if not hide:
             w.write(name_to_name(s.gen.full_name))
             w.extendWrite(' [label="')
-            w.extendWrite(name_to_label(s.gen.full_name))
+            w.extendWrite(name_to_label(s))
             w.extendWrite('"')
             if isinstance(s, ParallelState):
               w.extendWrite(' type=parallel')

test/test_files/day_atlee/statechart_fig1_redialer.svg

@@ -0,0 +1,144 @@
+<?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="812pt" height="394pt"
+ viewBox="0.00 0.00 812.00 394.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 390)">
+<title>state transitions</title>
+<polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-390 808,-390 808,4 -4,4"/>
+<g id="clust1" class="cluster">
+<title>cluster__Dialing</title>
+<path fill="none" stroke="#000000" stroke-width="2" d="M20,-8C20,-8 784,-8 784,-8 790,-8 796,-14 796,-20 796,-20 796,-335 796,-335 796,-341 790,-347 784,-347 784,-347 20,-347 20,-347 14,-347 8,-341 8,-335 8,-335 8,-20 8,-20 8,-14 14,-8 20,-8"/>
+<text text-anchor="start" x="383.6682" y="-328.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Dialing</text>
+</g>
+<g id="clust2" class="cluster">
+<title>cluster__Dialing_Redialer</title>
+<polygon fill="none" stroke="#000000" stroke-dasharray="5,2" points="445,-16 445,-309 788,-309 788,-16 445,-16"/>
+<text text-anchor="start" x="594.1668" y="-290.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Redialer</text>
+</g>
+<g id="clust3" class="cluster">
+<title>cluster__Dialing_Dialer</title>
+<polygon fill="none" stroke="#000000" stroke-dasharray="5,2" points="24,-16 24,-309 437,-309 437,-16 24,-16"/>
+<text text-anchor="start" x="215.3376" y="-290.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Dialer</text>
+</g>
+<!-- __initial -->
+<g id="node1" class="node">
+<title>__initial</title>
+<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="16" cy="-380.5" rx="5.5" ry="5.5"/>
+</g>
+<!-- _Dialing -->
+<!-- __initial&#45;&gt;_Dialing -->
+<g id="edge1" class="edge">
+<title>__initial&#45;&gt;_Dialing</title>
+<path fill="none" stroke="#000000" d="M16,-374.9533C16,-370.7779 16,-364.5043 16,-357.0332"/>
+<polygon fill="#000000" stroke="#000000" points="19.5001,-356.9971 16,-346.9971 12.5001,-356.9972 19.5001,-356.9971"/>
+<text text-anchor="middle" x="17.3895" y="-358" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
+</g>
+<!-- _Dialing_Redialer -->
+<!-- _Dialing_Redialer_initial -->
+<g id="node4" class="node">
+<title>_Dialing_Redialer_initial</title>
+<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="559" cy="-265.5" rx="5.5" ry="5.5"/>
+</g>
+<!-- _Dialing_Redialer_WaitForRedial -->
+<g id="node6" class="node">
+<title>_Dialing_Redialer_WaitForRedial</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="614.5,-178 503.5,-178 503.5,-142 614.5,-142 614.5,-178"/>
+<text text-anchor="start" x="514.8342" y="-156.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">WaitForRedial ✓</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M515.8333,-143C515.8333,-143 602.1667,-143 602.1667,-143 607.8333,-143 613.5,-148.6667 613.5,-154.3333 613.5,-154.3333 613.5,-165.6667 613.5,-165.6667 613.5,-171.3333 607.8333,-177 602.1667,-177 602.1667,-177 515.8333,-177 515.8333,-177 510.1667,-177 504.5,-171.3333 504.5,-165.6667 504.5,-165.6667 504.5,-154.3333 504.5,-154.3333 504.5,-148.6667 510.1667,-143 515.8333,-143"/>
+</g>
+<!-- _Dialing_Redialer_initial&#45;&gt;_Dialing_Redialer_WaitForRedial -->
+<g id="edge2" class="edge">
+<title>_Dialing_Redialer_initial&#45;&gt;_Dialing_Redialer_WaitForRedial</title>
+<path fill="none" stroke="#000000" d="M559,-259.8288C559,-255.1736 559,-248.4097 559,-242.5 559,-242.5 559,-242.5 559,-195.5 559,-193.1079 559,-190.6252 559,-188.1342"/>
+<polygon fill="#000000" stroke="#000000" points="562.5001,-188.0597 559,-178.0598 555.5001,-188.0598 562.5001,-188.0597"/>
+<text text-anchor="middle" x="560.3895" y="-216" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
+</g>
+<!-- _Dialing_Redialer_RedialDigits -->
+<g id="node5" class="node">
+<title>_Dialing_Redialer_RedialDigits</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="568.5,-60 483.5,-60 483.5,-24 568.5,-24 568.5,-60"/>
+<text text-anchor="start" x="494.5026" y="-38.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">RedialDigits</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M495.8333,-25C495.8333,-25 556.1667,-25 556.1667,-25 561.8333,-25 567.5,-30.6667 567.5,-36.3333 567.5,-36.3333 567.5,-47.6667 567.5,-47.6667 567.5,-53.3333 561.8333,-59 556.1667,-59 556.1667,-59 495.8333,-59 495.8333,-59 490.1667,-59 484.5,-53.3333 484.5,-47.6667 484.5,-47.6667 484.5,-36.3333 484.5,-36.3333 484.5,-30.6667 490.1667,-25 495.8333,-25"/>
+</g>
+<!-- _Dialing_Redialer_RedialDigits&#45;&gt;_Dialing_Redialer_RedialDigits -->
+<g id="edge3" class="edge">
+<title>_Dialing_Redialer_RedialDigits&#45;&gt;_Dialing_Redialer_RedialDigits</title>
+<path fill="none" stroke="#000000" d="M568.7986,-46.856C581.0518,-46.6655 590.5,-45.0469 590.5,-42 590.5,-39.8577 585.8289,-38.4214 578.7961,-37.6913"/>
+<polygon fill="#000000" stroke="#000000" points="578.9749,-34.1959 568.7986,-37.144 578.5923,-41.1855 578.9749,-34.1959"/>
+<text text-anchor="start" x="590.5" y="-39" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">[c &lt; numdigits(p)]^dial(digit(p, c+1)) &#160;&#160;</text>
+</g>
+<!-- _Dialing_Redialer_RedialDigits&#45;&gt;_Dialing_Redialer_WaitForRedial -->
+<g id="edge4" class="edge">
+<title>_Dialing_Redialer_RedialDigits&#45;&gt;_Dialing_Redialer_WaitForRedial</title>
+<path fill="none" stroke="#000000" d="M483.4216,-59.8718C478.3898,-64.5715 475,-70.3799 475,-77.5 475,-124.5 475,-124.5 475,-124.5 475,-130.7463 482.9804,-136.5147 494.0215,-141.5063"/>
+<polygon fill="#000000" stroke="#000000" points="492.8568,-144.811 503.4386,-145.3373 495.4946,-138.327 492.8568,-144.811"/>
+<text text-anchor="start" x="475" y="-98" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">[c == numdigits(p)] &#160;&#160;</text>
+</g>
+<!-- _Dialing_Redialer_WaitForRedial&#45;&gt;_Dialing_Redialer_RedialDigits -->
+<g id="edge5" class="edge">
+<title>_Dialing_Redialer_WaitForRedial&#45;&gt;_Dialing_Redialer_RedialDigits</title>
+<path fill="none" stroke="#000000" d="M602.0313,-141.6979C606.8125,-137.0752 610,-131.4043 610,-124.5 610,-124.5 610,-124.5 610,-77.5 610,-69.0842 595.5133,-61.5359 578.5722,-55.5861"/>
+<polygon fill="#000000" stroke="#000000" points="579.5769,-52.2323 568.9843,-52.4497 577.4005,-58.8854 579.5769,-52.2323"/>
+<text text-anchor="start" x="610" y="-98" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">redial [c == 0]/p = lp ^dial(digit(lp, 1)) &#160;&#160;</text>
+</g>
+<!-- _Dialing_Dialer -->
+<!-- _Dialing_Dialer_initial -->
+<g id="node8" class="node">
+<title>_Dialing_Dialer_initial</title>
+<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="80" cy="-265.5" rx="5.5" ry="5.5"/>
+</g>
+<!-- _Dialing_Dialer_WaitForDial -->
+<g id="node10" class="node">
+<title>_Dialing_Dialer_WaitForDial</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="128.5,-178 31.5,-178 31.5,-142 128.5,-142 128.5,-178"/>
+<text text-anchor="start" x="42.505" y="-156.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">WaitForDial ✓</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M43.8333,-143C43.8333,-143 116.1667,-143 116.1667,-143 121.8333,-143 127.5,-148.6667 127.5,-154.3333 127.5,-154.3333 127.5,-165.6667 127.5,-165.6667 127.5,-171.3333 121.8333,-177 116.1667,-177 116.1667,-177 43.8333,-177 43.8333,-177 38.1667,-177 32.5,-171.3333 32.5,-165.6667 32.5,-165.6667 32.5,-154.3333 32.5,-154.3333 32.5,-148.6667 38.1667,-143 43.8333,-143"/>
+</g>
+<!-- _Dialing_Dialer_initial&#45;&gt;_Dialing_Dialer_WaitForDial -->
+<g id="edge6" class="edge">
+<title>_Dialing_Dialer_initial&#45;&gt;_Dialing_Dialer_WaitForDial</title>
+<path fill="none" stroke="#000000" d="M80,-259.8288C80,-255.1736 80,-248.4097 80,-242.5 80,-242.5 80,-242.5 80,-195.5 80,-193.1079 80,-190.6252 80,-188.1342"/>
+<polygon fill="#000000" stroke="#000000" points="83.5001,-188.0597 80,-178.0598 76.5001,-188.0598 83.5001,-188.0597"/>
+<text text-anchor="middle" x="81.3895" y="-216" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
+</g>
+<!-- _Dialing_Dialer_DialDigits -->
+<g id="node9" class="node">
+<title>_Dialing_Dialer_DialDigits</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="140,-60 68,-60 68,-24 140,-24 140,-60"/>
+<text text-anchor="start" x="78.6734" y="-38.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">DialDigits</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M80.3333,-25C80.3333,-25 127.6667,-25 127.6667,-25 133.3333,-25 139,-30.6667 139,-36.3333 139,-36.3333 139,-47.6667 139,-47.6667 139,-53.3333 133.3333,-59 127.6667,-59 127.6667,-59 80.3333,-59 80.3333,-59 74.6667,-59 69,-53.3333 69,-47.6667 69,-47.6667 69,-36.3333 69,-36.3333 69,-30.6667 74.6667,-25 80.3333,-25"/>
+</g>
+<!-- _Dialing_Dialer_DialDigits&#45;&gt;_Dialing_Dialer_DialDigits -->
+<g id="edge7" class="edge">
+<title>_Dialing_Dialer_DialDigits&#45;&gt;_Dialing_Dialer_DialDigits</title>
+<path fill="none" stroke="#000000" d="M140.25,-46.875C152.3333,-46.875 162,-45.25 162,-42 162,-39.7656 157.431,-38.2993 150.6489,-37.6011"/>
+<polygon fill="#000000" stroke="#000000" points="150.3996,-34.0861 140.25,-37.125 150.0794,-41.0788 150.3996,-34.0861"/>
+<text text-anchor="start" x="162" y="-39" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">dial(d:int) [c &lt; 10]/lp = lp * 10 + d c += 1 &#160;^out.out(d) &#160;&#160;</text>
+</g>
+<!-- _Dialing_Dialer_DialDigits&#45;&gt;_Dialing_Dialer_WaitForDial -->
+<g id="edge8" class="edge">
+<title>_Dialing_Dialer_DialDigits&#45;&gt;_Dialing_Dialer_WaitForDial</title>
+<path fill="none" stroke="#000000" d="M74.4875,-60.3273C70.0916,-65.167 67,-70.9124 67,-77.5 67,-124.5 67,-124.5 67,-124.5 67,-126.9367 67.2734,-129.4132 67.7409,-131.8668"/>
+<polygon fill="#000000" stroke="#000000" points="64.4295,-133.0164 70.5523,-141.6629 71.1579,-131.0853 64.4295,-133.0164"/>
+<text text-anchor="start" x="67" y="-98" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">[c == 10] &#160;&#160;</text>
+</g>
+<!-- _Dialing_Dialer_WaitForDial&#45;&gt;_Dialing_Dialer_DialDigits -->
+<g id="edge10" class="edge">
+<title>_Dialing_Dialer_WaitForDial&#45;&gt;_Dialing_Dialer_DialDigits</title>
+<path fill="none" stroke="#000000" d="M128.5115,-146.0105C144.3736,-139.9675 158,-132.4599 158,-124.5 158,-124.5 158,-124.5 158,-77.5 158,-69.8638 154.1829,-63.7787 148.5785,-58.9596"/>
+<polygon fill="#000000" stroke="#000000" points="150.2577,-55.8692 140.0188,-53.1463 146.3249,-61.66 150.2577,-55.8692"/>
+<text text-anchor="start" x="158" y="-98" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">dial(d:int), redial [c == 0]/lp = d c = 1 &#160;^out.out(d) &#160;&#160;</text>
+</g>
+<!-- _Dialing_Dialer_WaitForDial&#45;&gt;_Dialing_Dialer_WaitForDial -->
+<g id="edge9" class="edge">
+<title>_Dialing_Dialer_WaitForDial&#45;&gt;_Dialing_Dialer_WaitForDial</title>
+<path fill="none" stroke="#000000" d="M128.7649,-164.8167C141.1797,-164.5001 150.5,-162.8945 150.5,-160 150.5,-157.9648 145.8922,-156.5668 138.8407,-155.8061"/>
+<polygon fill="#000000" stroke="#000000" points="138.9618,-152.307 128.7649,-155.1833 138.5299,-159.2937 138.9618,-152.307"/>
+<text text-anchor="start" x="150.5" y="-157" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">dial(d:int), not redial [c &lt; 10]/c += 1 lp = lp * 10 + d &#160;^out.out(d) &#160;&#160;</text>
+</g>
+</g>
+</svg>

test/test_files/day_atlee/statechart_fig7_dialer.svg

@@ -4,11 +4,11 @@
 <!-- Generated by graphviz version 2.40.1 (20161225.0304)
  -->
 <!-- Title: state transitions Pages: 1 -->
-<svg width="228pt" height="83pt"
- viewBox="0.00 0.00 227.70 83.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
+<svg width="225pt" height="83pt"
+ viewBox="0.00 0.00 224.92 83.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 79)">
 <title>state transitions</title>
-<polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-79 223.696,-79 223.696,4 -4,4"/>
+<polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-79 220.917,-79 220.917,4 -4,4"/>
 <!-- __initial -->
 <g id="node1" class="node">
 <title>__initial</title>
@@ -33,7 +33,7 @@
 <title>_D&#45;&gt;_D</title>
 <path fill="none" stroke="#000000" d="M56.0183,-23.9381C67.888,-24.3856 78,-22.4063 78,-18 78,-14.9707 73.2205,-13.0885 66.3762,-12.3533"/>
 <polygon fill="#000000" stroke="#000000" points="66.1128,-8.8446 56.0183,-12.0619 65.9158,-15.8419 66.1128,-8.8446"/>
-<text text-anchor="start" x="78" y="-15" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">in.dial [c &lt; 10]/c += 1 &#160;^out.out &#160;&#160;</text>
+<text text-anchor="start" x="78" y="-15" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">in.dial [c &lt; 10]/c += 1 ^out.out &#160;&#160;</text>
 </g>
 </g>
 </svg>