Fix bug in memory protocol implementation. Add example 13 from Day & Atlee. More efficient implementation when enabledness and assignment memory protocol options are the same.

src/sccd/statechart/dynamic/memory_snapshot.py

@@ -1,13 +1,13 @@
 from sccd.action_lang.dynamic.memory import *
-from sccd.util import timer
+from sccd.util import timer  
 
 class MemoryPartialSnapshot(MemoryInterface):
   __slots__ = ["description", "memory", "read_only", "frame", "actual", "snapshot", "trans_dirty", "round_dirty"]
 
-  def __init__(self, description: str, memory: Memory, read_only: bool = False):
+  def __init__(self, description: str, memory: Memory):
     self.description = description
     self.memory = memory
-    self.read_only = read_only
+    self.read_only = False
 
     self.frame = memory.current_frame()
 
@@ -20,6 +20,9 @@ class MemoryPartialSnapshot(MemoryInterface):
     # Positions in stack frame written to during current big, combo or small step (depending on semantic option chosen)
     self.round_dirty = Bitmap()
 
+  def set_read_only(self, read_only: bool):
+    self.read_only = read_only
+
   def current_frame(self) -> StackFrame:
     return self.memory.current_frame()
 
@@ -50,9 +53,9 @@ class MemoryPartialSnapshot(MemoryInterface):
   def store(self, offset: int, value: Any):
     frame, offset = self.memory._get_frame(offset)
     if frame is self.frame:
+      # "our" frame! :)
       if self.read_only:
         raise SCCDRuntimeException("Attempt to write to read-only %s memory." % self.description)
-      # "our" frame! :)
       # Remember that we wrote, such that next read during same transition will be the value we wrote.
       self.trans_dirty |= bit(offset)
 
@@ -60,7 +63,7 @@ class MemoryPartialSnapshot(MemoryInterface):
     frame.storage[offset] = value
 
 
-  def flush_transition(self, read_only: bool = False):
+  def flush_transition(self):
     race_conditions = self.trans_dirty & self.round_dirty
     if race_conditions:
       variables = self.frame.scope.variables

src/sccd/statechart/dynamic/statechart_execution.py

@@ -65,6 +65,7 @@ class StatechartExecution:
                         enter_ids |= self.history_values[t.opt.target_history_id]
                     enter_set = self._ids_to_states(bm_items(enter_ids))
 
+                self.rhs_memory.set_read_only(False)
                 ctx = EvalContext(execution=self, events=events, memory=self.rhs_memory)
 
                 print_debug("fire " + str(t))
@@ -89,7 +90,7 @@ class StatechartExecution:
                 with timer.Context("actions"):
                     self.rhs_memory.push_frame(t.scope) # make room for event parameters on stack
                     if t.trigger:
-                        t.trigger.copy_params_to_stack(ctx)
+                        t.trigger.copy_params_to_stack(events, self.rhs_memory)
                     _perform_actions(ctx, t.actions)
                     self.rhs_memory.pop_frame()
 
@@ -113,16 +114,16 @@ class StatechartExecution:
             if t.guard is None:
                 return True
             else:
-                ctx = EvalContext(execution=self, events=events, memory=self.gc_memory)
+                self.gc_memory.set_read_only(True)
                 self.gc_memory.push_frame(t.scope)
                 # Guard conditions can also refer to event parameters
                 if t.trigger:
-                    t.trigger.copy_params_to_stack(ctx)
+                    t.trigger.copy_params_to_stack(events, self.gc_memory)
                 result = t.guard.eval(self.gc_memory)
                 self.gc_memory.pop_frame()
                 return result
         except Exception as e:
-            e.args = ("While checking guard of transition %s:\n" % str(t) +str(e),)
+            e.args = ("While checking guard of transition %s:\n" % str(t) + str(e),)
             raise
 
     def _start_timers(self, triggers: List[AfterTrigger]):
@@ -139,7 +140,10 @@ class StatechartExecution:
 
     # Return whether the current configuration includes ALL the states given.
     def in_state(self, state_strings: List[str]) -> bool:
-        state_ids_bitmap = bm_union(self.statechart.tree.state_dict[state_string].opt.state_id_bitmap for state_string in state_strings)
+        try:
+            state_ids_bitmap = bm_union(self.statechart.tree.state_dict[state_string].opt.state_id_bitmap for state_string in state_strings)
+        except KeyError as e:
+            raise SCCDRuntimeException("INSTATE argument %s: invalid state" % str(e)) from e
         in_state = bm_has_all(self.configuration, state_ids_bitmap)
         # if in_state:
         #     print_debug("in state"+str(state_strings))

src/sccd/statechart/dynamic/statechart_instance.py

@@ -130,19 +130,22 @@ class StatechartInstance(Instance):
 
         if semantics.assignment_memory_protocol == MemoryProtocol.BIG_STEP:
             self._big_step.when_done(rhs_memory.flush_round)
-        elif semantics.enabledness_memory_protocol == MemoryProtocol.COMBO_STEP:
+        elif semantics.assignment_memory_protocol == MemoryProtocol.COMBO_STEP:
             combo_step.when_done(rhs_memory.flush_round)
-        elif semantics.enabledness_memory_protocol == MemoryProtocol.SMALL_STEP:
+        elif semantics.assignment_memory_protocol == MemoryProtocol.SMALL_STEP:
             small_step.when_done(rhs_memory.flush_round)
 
-        gc_memory = MemoryPartialSnapshot("GC", memory, read_only=True)
-
-        if semantics.assignment_memory_protocol == MemoryProtocol.BIG_STEP:
-            self._big_step.when_done(gc_memory.flush_round)
-        elif semantics.assignment_memory_protocol == MemoryProtocol.COMBO_STEP:
-            combo_step.when_done(gc_memory.flush_round)
-        elif semantics.assignment_memory_protocol == MemoryProtocol.SMALL_STEP:
-            small_step.when_done(gc_memory.flush_round)
+        if semantics.enabledness_memory_protocol == semantics.assignment_memory_protocol:
+            gc_memory = rhs_memory
+            gc_memory.description = "RHS/GC"
+        else:
+            gc_memory = MemoryPartialSnapshot("GC", memory)
+            if semantics.enabledness_memory_protocol == MemoryProtocol.BIG_STEP:
+                self._big_step.when_done(gc_memory.flush_round)
+            elif semantics.enabledness_memory_protocol == MemoryProtocol.COMBO_STEP:
+                combo_step.when_done(gc_memory.flush_round)
+            elif semantics.enabledness_memory_protocol == MemoryProtocol.SMALL_STEP:
+                small_step.when_done(gc_memory.flush_round)
 
         print_debug("\nRound hierarchy: " + str(self._big_step) + '\n')
 

src/sccd/statechart/static/tree.py

@@ -129,21 +129,21 @@ class Trigger:
     def render(self) -> str:
         return ' ∧ '.join(e.render() for e in self.enabling)
 
-    def copy_params_to_stack(self, ctx: EvalContext):
-        # Both 'ctx.events' and 'self.enabling' are sorted by event ID,
+    def copy_params_to_stack(self, events: List[InternalEvent], memory: MemoryInterface):
+        # Both 'events' and 'self.enabling' are sorted by event ID,
         # this way we have to iterate over each of both lists at most once.
         iterator = iter(self.enabling)
         try:
             event_decl = next(iterator)
             offset = 0
-            for e in ctx.events:
+            for e in events:
                 if e.id < event_decl.id:
                     continue
                 else:
                     while e.id > event_decl.id:
                         event_decl = next(iterator)
                     for p in e.params:
-                        ctx.memory.store(offset, p)
+                        memory.store(offset, p)
                         offset += 1
         except StopIteration:
             pass
@@ -180,7 +180,7 @@ class AfterTrigger(Trigger):
     # Override.
     # An 'after'-event also has 1 parameter, but it is not accessible to the user,
     # hence the override.
-    def copy_params_to_stack(self, ctx: EvalContext):
+    def copy_params_to_stack(self, events: List[InternalEvent], memory: MemoryInterface):
         pass
 
 _empty_trigger = Trigger(enabling=[])

test/test_files/day_atlee/fail_13_invar_rhs_bigstep.xml

@@ -0,0 +1,22 @@
+<?xml version="1.0" ?>
+<test>
+  <!-- Example 13 in BSML paper with RHS Big Step semantics contains multiple assignments to variables 'a' and 'b' during the big-step, which we (correctly) detect as a race condition, making the example invalid -->
+  
+  <statechart src="statechart_fig20_invar.xml">
+    <override_semantics
+      assignment_memory_protocol="big_step"/>
+  </statechart>
+
+  <input>
+    <event port="in" name="start" time="0 d"/>
+  </input>
+
+  <output>
+    <big_step>
+      <event port="out" name="done">
+        <param val="21"/>
+        <param val="16"/>
+      </event>
+    </big_step>
+  </output>
+</test>

test/test_files/day_atlee/statechart_fig20_invar.svg

@@ -0,0 +1,153 @@
+<?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="295pt" height="578pt"
+ viewBox="0.00 0.00 295.44 578.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 574)">
+<title>state transitions</title>
+<polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-574 291.444,-574 291.444,4 -4,4"/>
+<g id="clust1" class="cluster">
+<title>cluster__Invar</title>
+<path fill="none" stroke="#000000" stroke-width="2" d="M20,-74C20,-74 221,-74 221,-74 227,-74 233,-80 233,-86 233,-86 233,-519 233,-519 233,-525 227,-531 221,-531 221,-531 20,-531 20,-531 14,-531 8,-525 8,-519 8,-519 8,-86 8,-86 8,-80 14,-74 20,-74"/>
+<text text-anchor="start" x="107.1644" y="-512.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Invar</text>
+</g>
+<g id="clust2" class="cluster">
+<title>cluster__Invar_I2</title>
+<polygon fill="none" stroke="#000000" stroke-dasharray="5,2" points="136,-82 136,-493 225,-493 225,-82 136,-82"/>
+<text text-anchor="start" x="175.4972" y="-474.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">I2</text>
+</g>
+<g id="clust3" class="cluster">
+<title>cluster__Invar_I1</title>
+<polygon fill="none" stroke="#000000" stroke-dasharray="5,2" points="24,-82 24,-493 128,-493 128,-82 24,-82"/>
+<text text-anchor="start" x="70.9972" y="-474.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">I1</text>
+</g>
+<!-- __initial -->
+<g id="node1" class="node">
+<title>__initial</title>
+<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="16" cy="-564.5" rx="5.5" ry="5.5"/>
+</g>
+<!-- _Invar -->
+<!-- __initial&#45;&gt;_Invar -->
+<g id="edge1" class="edge">
+<title>__initial&#45;&gt;_Invar</title>
+<path fill="none" stroke="#000000" d="M16,-558.9533C16,-554.7779 16,-548.5043 16,-541.0332"/>
+<polygon fill="#000000" stroke="#000000" points="19.5001,-540.9971 16,-530.9971 12.5001,-540.9972 19.5001,-540.9971"/>
+<text text-anchor="middle" x="17.3895" y="-542" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
+</g>
+<!-- _Done -->
+<g id="node2" class="node">
+<title>_Done</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="219,-46 125,-46 125,0 219,0 219,-46"/>
+<text text-anchor="start" x="157.6624" y="-29.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Done</text>
+<text text-anchor="start" x="130.501" y="-9.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">enter ^out.done</text>
+<polygon fill="#000000" stroke="#000000" points="125,-23 125,-23 219,-23 219,-23 125,-23"/>
+<path fill="none" stroke="#000000" stroke-width="2" d="M138,-1C138,-1 206,-1 206,-1 212,-1 218,-7 218,-13 218,-13 218,-33 218,-33 218,-39 212,-45 206,-45 206,-45 138,-45 138,-45 132,-45 126,-39 126,-33 126,-33 126,-13 126,-13 126,-7 132,-1 138,-1"/>
+</g>
+<!-- _Invar_I2 -->
+<!-- _Invar_I2_initial -->
+<g id="node5" class="node">
+<title>_Invar_I2_initial</title>
+<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="172" cy="-449.5" rx="5.5" ry="5.5"/>
+</g>
+<!-- _Invar_I2_S4 -->
+<g id="node8" class="node">
+<title>_Invar_I2_S4</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="200,-362 144,-362 144,-326 200,-326 200,-362"/>
+<text text-anchor="start" x="164.6632" y="-340.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">S4</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M156.3333,-327C156.3333,-327 187.6667,-327 187.6667,-327 193.3333,-327 199,-332.6667 199,-338.3333 199,-338.3333 199,-349.6667 199,-349.6667 199,-355.3333 193.3333,-361 187.6667,-361 187.6667,-361 156.3333,-361 156.3333,-361 150.6667,-361 145,-355.3333 145,-349.6667 145,-349.6667 145,-338.3333 145,-338.3333 145,-332.6667 150.6667,-327 156.3333,-327"/>
+</g>
+<!-- _Invar_I2_initial&#45;&gt;_Invar_I2_S4 -->
+<g id="edge2" class="edge">
+<title>_Invar_I2_initial&#45;&gt;_Invar_I2_S4</title>
+<path fill="none" stroke="#000000" d="M172,-443.8288C172,-439.1736 172,-432.4097 172,-426.5 172,-426.5 172,-426.5 172,-379.5 172,-377.1079 172,-374.6252 172,-372.1342"/>
+<polygon fill="#000000" stroke="#000000" points="175.5001,-372.0597 172,-362.0598 168.5001,-372.0598 175.5001,-372.0597"/>
+<text text-anchor="middle" x="173.3895" y="-400" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
+</g>
+<!-- _Invar_I2_S6 -->
+<g id="node6" class="node">
+<title>_Invar_I2_S6</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="200,-126 144,-126 144,-90 200,-90 200,-126"/>
+<text text-anchor="start" x="164.6632" y="-104.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">S6</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M156.3333,-91C156.3333,-91 187.6667,-91 187.6667,-91 193.3333,-91 199,-96.6667 199,-102.3333 199,-102.3333 199,-113.6667 199,-113.6667 199,-119.3333 193.3333,-125 187.6667,-125 187.6667,-125 156.3333,-125 156.3333,-125 150.6667,-125 145,-119.3333 145,-113.6667 145,-113.6667 145,-102.3333 145,-102.3333 145,-96.6667 150.6667,-91 156.3333,-91"/>
+</g>
+<!-- _Invar_I2_S6&#45;&gt;_Done -->
+<g id="edge3" class="edge">
+<title>_Invar_I2_S6&#45;&gt;_Done</title>
+<path fill="none" stroke="#000000" d="M172,-89.9737C172,-80.1983 172,-67.8024 172,-56.3399"/>
+<polygon fill="#000000" stroke="#000000" points="175.5001,-56.1774 172,-46.1775 168.5001,-56.1775 175.5001,-56.1774"/>
+<text text-anchor="start" x="172" y="-57" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">[INSTATE([&quot;/Invar/S3&quot;])] &#160;&#160;</text>
+</g>
+<!-- _Invar_I2_S5 -->
+<g id="node7" class="node">
+<title>_Invar_I2_S5</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="200,-244 144,-244 144,-208 200,-208 200,-244"/>
+<text text-anchor="start" x="164.6632" y="-222.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">S5</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M156.3333,-209C156.3333,-209 187.6667,-209 187.6667,-209 193.3333,-209 199,-214.6667 199,-220.3333 199,-220.3333 199,-231.6667 199,-231.6667 199,-237.3333 193.3333,-243 187.6667,-243 187.6667,-243 156.3333,-243 156.3333,-243 150.6667,-243 145,-237.3333 145,-231.6667 145,-231.6667 145,-220.3333 145,-220.3333 145,-214.6667 150.6667,-209 156.3333,-209"/>
+</g>
+<!-- _Invar_I2_S5&#45;&gt;_Invar_I2_S6 -->
+<g id="edge4" class="edge">
+<title>_Invar_I2_S5&#45;&gt;_Invar_I2_S6</title>
+<path fill="none" stroke="#000000" d="M169.1785,-207.9844C168.5166,-202.3957 168,-196.206 168,-190.5 168,-190.5 168,-190.5 168,-143.5 168,-141.0928 168.0919,-138.5995 168.248,-136.1015"/>
+<polygon fill="#000000" stroke="#000000" points="171.7449,-136.2949 169.1785,-126.0156 164.7745,-135.6517 171.7449,-136.2949"/>
+<text text-anchor="start" x="168" y="-164" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">/a = 3 * a &#160;&#160;</text>
+</g>
+<!-- _Invar_I2_S4&#45;&gt;_Invar_I2_S5 -->
+<g id="edge5" class="edge">
+<title>_Invar_I2_S4&#45;&gt;_Invar_I2_S5</title>
+<path fill="none" stroke="#000000" d="M167.7033,-325.6741C166.7416,-320.1833 166,-314.1255 166,-308.5 166,-308.5 166,-308.5 166,-261.5 166,-259.2146 166.1224,-256.8579 166.3322,-254.4969"/>
+<polygon fill="#000000" stroke="#000000" points="169.8359,-254.7039 167.7033,-244.3259 162.8986,-253.7687 169.8359,-254.7039"/>
+<text text-anchor="start" x="166" y="-282" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">/a = a + b &#160;&#160;</text>
+</g>
+<!-- _Invar_I1 -->
+<!-- _Invar_I1_initial -->
+<g id="node10" class="node">
+<title>_Invar_I1_initial</title>
+<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="60" cy="-449.5" rx="5.5" ry="5.5"/>
+</g>
+<!-- _Invar_I1_S1 -->
+<g id="node13" class="node">
+<title>_Invar_I1_S1</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="88,-362 32,-362 32,-326 88,-326 88,-362"/>
+<text text-anchor="start" x="52.6632" y="-340.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">S1</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M44.3333,-327C44.3333,-327 75.6667,-327 75.6667,-327 81.3333,-327 87,-332.6667 87,-338.3333 87,-338.3333 87,-349.6667 87,-349.6667 87,-355.3333 81.3333,-361 75.6667,-361 75.6667,-361 44.3333,-361 44.3333,-361 38.6667,-361 33,-355.3333 33,-349.6667 33,-349.6667 33,-338.3333 33,-338.3333 33,-332.6667 38.6667,-327 44.3333,-327"/>
+</g>
+<!-- _Invar_I1_initial&#45;&gt;_Invar_I1_S1 -->
+<g id="edge6" class="edge">
+<title>_Invar_I1_initial&#45;&gt;_Invar_I1_S1</title>
+<path fill="none" stroke="#000000" d="M60,-443.8288C60,-439.1736 60,-432.4097 60,-426.5 60,-426.5 60,-426.5 60,-379.5 60,-377.1079 60,-374.6252 60,-372.1342"/>
+<polygon fill="#000000" stroke="#000000" points="63.5001,-372.0597 60,-362.0598 56.5001,-372.0598 63.5001,-372.0597"/>
+<text text-anchor="middle" x="61.3895" y="-400" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
+</g>
+<!-- _Invar_I1_S3 -->
+<g id="node11" class="node">
+<title>_Invar_I1_S3</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="88,-126 32,-126 32,-90 88,-90 88,-126"/>
+<text text-anchor="start" x="52.6632" y="-104.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">S3</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M44.3333,-91C44.3333,-91 75.6667,-91 75.6667,-91 81.3333,-91 87,-96.6667 87,-102.3333 87,-102.3333 87,-113.6667 87,-113.6667 87,-119.3333 81.3333,-125 75.6667,-125 75.6667,-125 44.3333,-125 44.3333,-125 38.6667,-125 33,-119.3333 33,-113.6667 33,-113.6667 33,-102.3333 33,-102.3333 33,-96.6667 38.6667,-91 44.3333,-91"/>
+</g>
+<!-- _Invar_I1_S2 -->
+<g id="node12" class="node">
+<title>_Invar_I1_S2</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="88,-244 32,-244 32,-208 88,-208 88,-244"/>
+<text text-anchor="start" x="52.6632" y="-222.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">S2</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M44.3333,-209C44.3333,-209 75.6667,-209 75.6667,-209 81.3333,-209 87,-214.6667 87,-220.3333 87,-220.3333 87,-231.6667 87,-231.6667 87,-237.3333 81.3333,-243 75.6667,-243 75.6667,-243 44.3333,-243 44.3333,-243 38.6667,-243 33,-237.3333 33,-231.6667 33,-231.6667 33,-220.3333 33,-220.3333 33,-214.6667 38.6667,-209 44.3333,-209"/>
+</g>
+<!-- _Invar_I1_S2&#45;&gt;_Invar_I1_S3 -->
+<g id="edge7" class="edge">
+<title>_Invar_I1_S2&#45;&gt;_Invar_I1_S3</title>
+<path fill="none" stroke="#000000" d="M55.7033,-207.6741C54.7416,-202.1833 54,-196.1255 54,-190.5 54,-190.5 54,-190.5 54,-143.5 54,-141.2146 54.1224,-138.8579 54.3322,-136.4969"/>
+<polygon fill="#000000" stroke="#000000" points="57.8359,-136.7039 55.7033,-126.3259 50.8986,-135.7687 57.8359,-136.7039"/>
+<text text-anchor="start" x="54" y="-164" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">/b = 2 * a + b &#160;&#160;</text>
+</g>
+<!-- _Invar_I1_S1&#45;&gt;_Invar_I1_S2 -->
+<g id="edge8" class="edge">
+<title>_Invar_I1_S1&#45;&gt;_Invar_I1_S2</title>
+<path fill="none" stroke="#000000" d="M60,-325.9402C60,-320.3497 60,-314.1701 60,-308.5 60,-308.5 60,-308.5 60,-261.5 60,-259.1079 60,-256.6252 60,-254.1342"/>
+<polygon fill="#000000" stroke="#000000" points="63.5001,-254.0597 60,-244.0598 56.5001,-254.0598 63.5001,-254.0597"/>
+<text text-anchor="start" x="60" y="-282" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">/b = 2 * b &#160;&#160;</text>
+</g>
+</g>
+</svg>

test/test_files/day_atlee/statechart_fig20_invar.xml

@@ -0,0 +1,62 @@
+<?xml version="1.0" ?>
+<statechart>
+  <semantics
+    big_step_maximality="take_many"/>
+
+  <datamodel>
+    a = 7;
+    b = 2;
+  </datamodel>
+
+  <inport name="in">
+    <event name="start"/>
+  </inport>
+
+  <outport name="out">
+    <event name="done"/>
+  </outport>
+
+  <root initial="Invar">
+    <parallel id="Invar">
+      <state id="I1" initial="S1">
+        <state id="S1">
+          <transition target="../S2">
+            <code> b = 2 * b; </code>
+          </transition>
+        </state>
+        <state id="S2">
+          <transition target="../S3">
+            <code> b = 2 * a + b; </code>
+          </transition>
+        </state>
+        <state id="S3"/>
+      </state>
+
+      <state id="I2" initial="S4">
+        <state id="S4">
+          <transition target="../S5">
+            <code> a = a + b; </code>
+          </transition>
+        </state>
+        <state id="S5">
+          <transition target="../S6">
+            <code> a = 3 * a; </code>
+          </transition>
+        </state>
+        <state id="S6">
+          <transition cond='INSTATE(["/Invar/I1/S3"])' target="/Done"/>
+        </state>
+      </state>
+    </parallel>
+
+    <!-- this state is not in the example, but we introduce it to allow a final transition with output event the values of a and b -->
+    <state id="Done">
+      <onentry>
+        <raise port="out" event="done">
+          <param expr="a"/>
+          <param expr="b"/>
+        </raise>
+      </onentry>
+    </state>
+  </root>
+</statechart>

test/test_files/day_atlee/test_13_invar_rhs_smallstep.xml

@@ -0,0 +1,23 @@
+<?xml version="1.0" ?>
+<test>
+  <statechart src="statechart_fig20_invar.xml">
+    <override_semantics
+      assignment_memory_protocol="small_step"/>
+  </statechart>
+
+  <input>
+    <event port="in" name="start" time="0 d"/>
+  </input>
+
+  <output>
+    <big_step>
+      <!-- BSML paper gives example of big step t1, t2, t3, t4.
+           Due to fairness, we instead take the big step t1, t3, t2, t4,
+           giving the following values for a,b: -->
+      <event port="out" name="done">
+        <param val="33"/>
+        <param val="26"/>
+      </event>
+    </big_step>
+  </output>
+</test>

test/test_files/features/action_lang/fail_guard_readonly.xml

@@ -0,0 +1,34 @@
+<?xml version="1.0" ?>
+<test>
+  <!-- A guard condition's evaluation is not allowed to write to the statechart's variables -->
+  <statechart>
+    <semantics
+      big_step_maximality="take_many"/>
+    <datamodel>
+      x = 0;
+
+      inc_x = func {
+        x += 1;
+
+        # to make the type checker happy (expression 'inc_x()' should evaluate to boolean so it is a valid guard condition):
+        return False;
+      };
+    </datamodel>
+
+    <inport name="in">
+      <event name="start"/>
+    </inport>
+
+    <root>
+      <state id="s1">
+        <!-- Guard condition will write to the statechart's variable 'x'.
+             This results in a runtime error -->
+        <transition cond="inc_x()" target="."/>
+      </state>
+    </root>
+  </statechart>
+
+  <input>
+    <event name="start" port="in" time="0 d"/>
+  </input>
+</test>

test/test_files/features/action_lang/test_guard_readonly.xml

@@ -0,0 +1,49 @@
+<?xml version="1.0" ?>
+<test>
+  <!-- A guard condition evaluation is allowed to write to temporary (stack) variables -->
+  <statechart>
+    <semantics
+      big_step_maximality="take_many"/>
+    <datamodel>
+      inc_x = func(x: int) {
+        x += 1;
+        return False;
+      };
+    </datamodel>
+
+    <inport name="in">
+      <event name="start"/>
+    </inport>
+    <outport name="out">
+      <event name="ok"/>
+    </outport>
+
+    <root initial="s1">
+      <state id="s1">
+        <!-- 1st guard to be evaluated -->
+        <!-- increments 'x', but only locally in the function inc_x -->
+        <transition event="start(x: int)" cond="inc_x(x)" target="."/>
+
+        <!-- 2nd guard to be evaluated. x is still 42 -->
+        <transition event="start(x: int)" cond="x == 42" target="../s2"/>
+      </state>
+      <state id="s2">
+        <onentry>
+          <raise port="out" event="ok"/>
+        </onentry>
+      </state>
+    </root>
+  </statechart>
+
+  <input>
+    <event name="start" port="in" time="0 d">
+      <param name="x" expr="42"/>
+    </event>
+  </input>
+
+  <output>
+    <big_step>
+      <event port="out" name="ok"/>
+    </big_step>
+  </output>
+</test>