add examples

examples/semantics/operational/port/models.py

@@ -98,7 +98,14 @@ port_rt_mm_cs = port_mm_cs + """
 
     BerthState:Class {
         # status == empty <=> numShips == 0
-        constraint = `(get_slot_value(this, "numShips") == 0) == (get_slot_value(this, "status") == "empty")`;
+        constraint = ```
+            errors = []
+            numShips = get_slot_value(this, "numShips")
+            status = get_slot_value(this, "status")
+            if (numShips == 0) != (status == "empty"):
+                errors.append(f"Inconsistent: numShips = {numShips}, but status = {status}")
+            errors
+        ```;
     }
     :Inheritance (BerthState -> PlaceState)
 

examples/semantics/operational/port/rulebased_runner.py

@@ -0,0 +1,62 @@
+import urllib.parse
+
+from state.devstate import DevState
+from bootstrap.scd import bootstrap_scd
+from framework.conformance import Conformance, render_conformance_check_result
+from concrete_syntax.textual_od import parser
+from concrete_syntax.plantuml.renderer import render_object_diagram, render_class_diagram
+from api.od import ODAPI
+
+from transformation.ramify import ramify
+
+from examples.semantics.operational.simulator import Simulator, RandomDecisionMaker, InteractiveDecisionMaker
+from examples.semantics.operational.port import models
+from examples.semantics.operational.port.helpers import design_to_state, state_to_design, get_time
+from examples.semantics.operational.port.renderer import render_port_textual, render_port_graphviz
+
+from examples.semantics.operational.port import rulebased_sem
+
+state = DevState()
+scd_mmm = bootstrap_scd(state) # Load meta-meta-model
+
+### Load (meta-)models ###
+
+def parse_and_check(m_cs: str, mm, descr: str):
+    m = parser.parse_od(
+        state,
+        m_text=m_cs,
+        mm=mm)
+    conf = Conformance(state, m, mm)
+    print(descr, "...", render_conformance_check_result(conf.check_nominal()))
+    return m
+
+port_mm    = parse_and_check(models.port_mm_cs,    scd_mmm,    "MM")
+port_m     = parse_and_check(models.port_m_cs,     port_mm,    "M")
+port_rt_mm = parse_and_check(models.port_rt_mm_cs, scd_mmm,    "RT-MM")
+port_rt_m  = parse_and_check(models.port_rt_m_cs,  port_rt_mm, "RT-M")
+
+print()
+
+# print(render_class_diagram(state, port_rt_mm))
+
+### Simulate ###
+
+port_rt_mm_ramified = ramify(state, port_rt_mm)
+
+rulebased_action_generator = rulebased_sem.get_action_generator(state, port_rt_mm, port_rt_mm_ramified)
+termination_condition      = rulebased_sem.TerminationCondition(state, port_rt_mm_ramified)
+
+sim = Simulator(
+    action_generator=rulebased_action_generator,
+    # decision_maker=RandomDecisionMaker(seed=2),
+    decision_maker=InteractiveDecisionMaker(),
+    termination_condition=termination_condition,
+    check_conformance=True,
+    verbose=True,
+    renderer=render_port_textual,
+    # renderer=render_port_graphviz,
+)
+
+od = ODAPI(state, port_rt_m, port_rt_mm)
+
+sim.run(od)

examples/semantics/operational/port/rulebased_sem.py

@@ -0,0 +1,67 @@
+### Operational Semantics - defined by rule-based model transformation ###
+
+from concrete_syntax.textual_od.parser import parse_od
+from transformation.rule import Rule, RuleMatcherRewriter, PriorityActionGenerator
+from transformation.matcher.mvs_adapter import match_od
+from util import loader
+
+import os
+THIS_DIR = os.path.dirname(__file__)
+
+# kind: lhs, rhs, nac
+get_filename = lambda rule_name, kind: f"{THIS_DIR}/rules/r_{rule_name}_{kind}.od"
+
+
+def get_action_generator(state, rt_mm, rt_mm_ramified):
+    matcher_rewriter = RuleMatcherRewriter(state, rt_mm, rt_mm_ramified)
+
+    #############################################################################
+    # TO IMPLEMENT: Full semantics as a set of rule-based model transformations #
+
+    rules0_dict = loader.load_rules(state, get_filename, rt_mm_ramified,
+        ["ship_sinks"] # <- list of rule_name of equal priority
+    )
+    rules1_dict = loader.load_rules(state, get_filename, rt_mm_ramified,
+        ["ship_appears_in_berth"]
+    )
+    # rules2_dict = ...
+
+    generator = PriorityActionGenerator(matcher_rewriter, [
+        rules0_dict, # highest priority
+        rules1_dict, # lower priority
+        # rules2_dict, # lowest priority
+    ])
+
+    # TO IMPLEMENT: Full semantics as a set of rule-based model transformations #
+    #############################################################################
+
+    return generator
+
+
+
+
+# The termination condition can also be specified as a pattern:
+class TerminationCondition:
+    def __init__(self, state, rt_mm_ramified):
+        self.state = state
+        self.rt_mm_ramified = rt_mm_ramified
+
+        # TO IMPLEMENT: terminate simulation when the place 'served' contains 2 ships.
+
+        ########################################
+        # You should only edit the pattern below
+        pattern_cs = """
+            # Placeholder to make the termination condition never hold:
+            :GlobalCondition {
+                condition = `False`;
+            }
+        """
+        # You should only edit the pattern above
+        ########################################
+
+        self.pattern = parse_od(state, pattern_cs, rt_mm_ramified)
+
+    def __call__(self, od):
+        for match in match_od(self.state, od.m, od.mm, self.pattern, self.rt_mm_ramified):
+            # stop after the first match (no need to look for more matches):
+            return "There are 2 ships served." # Termination condition statisfied

examples/semantics/operational/port/rules/README.txt

@@ -0,0 +1,13 @@
+The names of the files in this directory are important.
+
+A rule must always be named:
+  r_<rule_name>_<lhs|rhs|nac>.od
+
+It is allowed to have more than one NAC. In this case, the NACs must be named:
+  r_<rule_name>_nac.od
+  r_<rule_name>_nac2.od
+  r_<rule_name>_nac3.od
+  ...
+
+
+For the assignment, you can delete the existing rules (they are nonsense) and start fresh.

examples/semantics/operational/port/rules/r_ship_appears_in_berth_lhs.od

@@ -0,0 +1,4 @@
+berthState:RAM_BerthState {
+  RAM_numShips = `get_value(this) == 0`;
+  RAM_status   = `get_value(this) == "empty"`;
+}

examples/semantics/operational/port/rules/r_ship_appears_in_berth_rhs.od

@@ -0,0 +1,4 @@
+berthState:RAM_BerthState {
+  RAM_numShips = `1`;
+  RAM_status   = `"served"`;
+}

examples/semantics/operational/port/rules/r_ship_sinks_lhs.od

@@ -0,0 +1,5 @@
+# Find any place that has at least one ship:
+
+placeState:RAM_PlaceState {
+  RAM_numShips = `get_value(this) > 0`;
+}

examples/semantics/operational/port/rules/r_ship_sinks_rhs.od

@@ -0,0 +1,4 @@
+placeState:RAM_PlaceState {
+  # Decrement number of ships:
+  RAM_numShips = `get_value(this) - 1`;
+}