Refactor 'port' demo to include starting point for assignment

examples/semantics/operational/port/assignment.py

@@ -0,0 +1,144 @@
+import functools
+from concrete_syntax.common import indent
+from examples.semantics.operational.port.helpers import design_to_state, state_to_design, get_time
+from examples.semantics.operational.simulator import make_actions_pure, filter_valid_actions
+
+
+def precondition_can_move_from(od, from_state):
+
+    # TO IMPLEMENT
+
+    # Function should return True if a ship can move out of 'from_state'
+
+    return False
+
+def precondition_can_move_to(od, to_state):
+
+    # TO IMPLEMENT
+
+    # Function should return True if a ship can move into 'to_state'
+
+    return False
+
+def precondition_all_successors_moved(od, conn):
+
+    # TO IMPLEMENT
+
+    # A move (or skip) can only be made along a connection after all subsequent connections have already made their move (or were skipped).
+
+    return True
+
+def precondition_workers_available(od, workerset):
+
+    # TO IMPLEMENT
+
+    # A worker in a WorkerSet can only be allocated to a berth, if the number of 'isOperating'-links is smaller than the number of workers in the WorkerSet.
+
+    return True
+
+def precondition_berth_unserved(od, berth):
+
+    # TO IMPLEMENT
+
+    # A worker can only be allocated to a berth, if the berth contains an 'unserved' ship.
+
+    return True
+
+def action_skip(od, conn_name):
+    # SERVES AS AN EXAMPLE - NO NEED TO EDIT THIS FUNCTION
+    conn = od.get(conn_name)
+    conn_state = design_to_state(od, conn)
+    od.set_slot_value(conn_state, "moved", True)
+    return [f"skip {conn_name}"]
+
+def action_move(od, conn_name):
+    action_skip(od, conn_name) # flag the connection as 'moved'
+
+    conn = od.get(conn_name)
+    from_place = od.get_source(conn)
+    to_place = od.get_target(conn)
+
+    from_state = design_to_state(od, from_place) # beware: Generator does not have State
+    to_state = design_to_state(od, to_place)
+
+    # TO IMPLEMENT:
+    #  - move a ship along the connection
+
+    return [f"unimplemented! nothing changed!"]
+
+def action_serve_berth(od, workerset_name, berth_name):
+
+    # TO IMPLEMENT:
+    #  - A worker starts operating a berth
+
+    return [f"unimplemented! nothing changed!"]
+
+def action_advance_time(od):
+    _, clock = od.get_all_instances("Clock")[0]
+    time = od.get_slot_value(clock, "time")
+    new_time = time + 1
+    od.set_slot_value(clock, "time", new_time)
+
+    # TO IMPLEMENT:
+    #  - all 'moved'-attributes need to be reset (to False)
+    #  - if there is a worker operating a Berth, then:
+    #      (1) the Berth's status becomes 'served'
+    #      (2) the worker is no longer operating the Berth
+
+    return [f"time is now {new_time}"]
+
+# This function is called to discover the possible steps that can be made.
+# It should not be necessary to edit this function
+def get_actions(od):
+    actions = {}
+
+    # Add move-actions (or skip-actions)
+    for conn_name, conn in od.get_all_instances("connection"):
+        already_moved = od.get_slot_value(design_to_state(od, conn), "moved")
+        if already_moved or not precondition_all_successors_moved(od, conn):
+            # a move was already made along this connection in the current time-step
+            continue
+
+        from_place = od.get_source(conn)
+        to_place = od.get_target(conn)
+        from_name = od.get_name(from_place)
+        to_name = od.get_name(to_place)
+        from_state = design_to_state(od, from_place)
+        to_state = design_to_state(od, to_place)
+
+        if (precondition_can_move_from(od, from_state)
+          and precondition_can_move_to(od, to_state)):
+            actions[f"move {conn_name} ({from_name} -> {to_name})"] = functools.partial(action_move, conn_name=conn_name)
+        else:
+            actions[f"skip {from_name} -> {to_name}"] = functools.partial(action_skip, conn_name=conn_name)
+
+    # Add actions to assign workers
+    for _, workerset in od.get_all_instances("WorkerSet"):
+        if not precondition_workers_available(od, workerset):
+            continue
+        for lnk in od.get_outgoing(workerset, "canOperate"):
+            berth = od.get_target(lnk)
+            if precondition_berth_unserved(od, berth):
+                berth_name = od.get_name(berth)
+                workerset_name = od.get_name(workerset)
+                actions[f"{workerset_name} operates {berth_name}"] = functools.partial(action_serve_berth, workerset_name=workerset_name, berth_name=berth_name)
+
+    # Only when no other action can be performed, can time advance
+    if len(actions) == 0:
+        actions["advance time"] = action_advance_time
+
+    # This wrapper turns our actions into pure functions: they will clone the model before modifying it. This is useful if we ever want to rollback an action.
+    return make_actions_pure(actions.items(), od)
+
+
+# Called every time the runtime state changes.
+# When this function returns a string, the simulation ends.
+# The string should represent the reason for ending the simulation.
+# When this function returns None, the simulation continues.
+def termination_condition(od):
+
+    # TO IMPLEMENT: terminate simulation when the place 'served' contains 2 ships.
+
+    if len(od.get_all_instances("Place")) > 5:
+        return "More places than I can count :("
+

examples/semantics/operational/port/helpers.py

@@ -0,0 +1,18 @@
+# Some helper functions
+
+def get_num_ships(od, place):
+    place_state = design_to_state(od, place)
+    return od.get_slot_value(place_state, "numShips")
+
+def design_to_state(od, design):
+    incoming = od.get_incoming(design, "of")
+    if len(incoming) == 1:
+        # not all design-objects have a state
+        return od.get_source(incoming[0])
+
+def state_to_design(od, state):
+    return od.get_target(od.get_outgoing(state, "of")[0])
+    
+def get_time(od):
+    _, clock = od.get_all_instances("Clock")[0]
+    return clock, od.get_slot_value(clock, "time")

examples/semantics/operational/port/models.py

@@ -47,16 +47,12 @@ port_mm_cs = """
     Generator:Class
     :Inheritance (Generator -> Source)
 
-    BlackHole:Class
-    :Inheritance (BlackHole -> Sink)
-
 
     # Those classes to which we want to attach a runtime state object
     Stateful:Class {
         abstract = True;
     }
     :Inheritance (Place      -> Stateful)
-    :Inheritance (BlackHole  -> Stateful)
     :Inheritance (WorkerSet  -> Stateful)
     :Inheritance (Berth      -> Stateful)
     :Inheritance (connection -> Stateful)
@@ -157,6 +153,7 @@ port_rt_mm_cs = port_mm_cs + """
         name = "moved";
         optional = False;
         constraint = ```
+            result = True
             all_successors_moved = True
             moved = get_value(get_target(this))
             conn_state = get_source(this)
@@ -167,18 +164,12 @@ port_rt_mm_cs = port_mm_cs + """
                 next_conn_state = get_source(get_incoming(next_conn, "of")[0])
                 if not get_slot_value(next_conn_state, "moved"):
                     all_successors_moved = False
-            not moved or all_successors_moved
+            if moved and not all_successors_moved:
+                result = f"Connection {get_name(conn)} played before its turn."
+            result
         ```;
     }
 
-    BlackHoleState:Class
-    :Inheritance (BlackHoleState -> State)
-    BlackHoleState_counter:AttributeLink (BlackHoleState -> Integer) {
-        name = "counter";
-        optional = False;
-        constraint = `get_value(get_target(this)) >= 0`; # non-negative
-    }
-
     Clock:Class {
         lower_cardinality = 1;
         upper_cardinality = 1;
@@ -255,7 +246,7 @@ port_m_cs = """
 
 
     # ships that have been served are counted here
-    served:BlackHole
+    served:Place
     c11:connection (outboundPassage -> served)
 
 
@@ -284,7 +275,7 @@ port_rt_m_cs = port_m_cs + """
     berth1State:BerthState { status = "empty"; numShips = 0; }  :of (berth1State -> berth1)
     berth2State:BerthState { status = "empty"; numShips = 0; }  :of (berth2State -> berth2)
 
-    servedState:BlackHoleState { counter = 0; }  :of (servedState -> served)
+    servedState:PlaceState { numShips = 0; }  :of (servedState -> served)
 
     workersState:WorkerSetState  :of (workersState -> workers)
 

examples/semantics/operational/port/renderer.py

@@ -0,0 +1,73 @@
+from examples.semantics.operational.port.helpers import design_to_state, state_to_design, get_time, get_num_ships
+
+def render_port_graphviz(od):
+    txt = ""
+
+    def render_place(place):
+        name = od.get_name(place)
+        return f'"{name}" [ label = "{name}\\n ships = {get_num_ships(od, place)}", style = filled, fillcolor = lightblue ]\n'
+
+    for _, cap in od.get_all_instances("CapacityConstraint", include_subtypes=False):
+        name = od.get_name(cap)
+        capacity = od.get_slot_value(cap, "shipCapacity")
+        txt += f'subgraph cluster_{name} {{\n  label = "{name}\\n capacity = {capacity}";\n'
+        for lnk in od.get_outgoing(cap, "capacityOf"):
+            place = od.get_target(lnk)
+            txt += f'  {render_place(place)}'
+        txt += f'}}\n'
+
+    for _, place_state in od.get_all_instances("PlaceState", include_subtypes=False):
+        place = state_to_design(od, place_state)
+        if len(od.get_incoming(place, "capacityOf")) == 0:
+            txt += render_place(place)
+
+    for _, berth_state in od.get_all_instances("BerthState", include_subtypes=False):
+        berth = state_to_design(od, berth_state)
+        name = od.get_name(berth)
+        txt += f'"{name}" [ label = "{name}\\n numShips = {get_num_ships(od, berth)}\\n status = {od.get_slot_value(berth_state, "status")}", fillcolor = yellow, style = filled]\n'
+
+    for _, gen in od.get_all_instances("Generator", include_subtypes=False):
+        txt += f'"{od.get_name(gen)}" [ label = "+", shape = diamond, fillcolor = green, fontsize = 30, style = filled ]\n'
+
+    for _, blackhole in od.get_all_instances("BlackHole", include_subtypes=False):
+        txt += f'"{od.get_name(blackhole)}" [ label = "-", shape = diamond, fillcolor = red, fontsize = 30, style = filled ]\n'
+
+    for _, conn in od.get_all_instances("connection"):
+        src = od.get_source(conn)
+        tgt = od.get_target(conn)
+        moved = od.get_slot_value(design_to_state(od, conn), "moved")
+        src_name = od.get_name(src)
+        tgt_name = od.get_name(tgt)
+        txt += f"{src_name} -> {tgt_name} [color=deepskyblue3, penwidth={1 if moved else 2}];\n"
+
+    for _, workers in od.get_all_instances("WorkerSet"):
+        already_have = []
+        name = od.get_name(workers)
+        num_workers = od.get_slot_value(workers, "numWorkers")
+        txt += f'{name} [label="{num_workers} worker(s)", shape=parallelogram, fillcolor=chocolate, style=filled];\n'
+        for lnk in od.get_outgoing(design_to_state(od, workers), "isOperating"):
+            berth = od.get_target(lnk)
+            already_have.append(berth)
+            txt += f"{name} -> {od.get_name(berth)} [arrowhead=none, color=chocolate];\n"
+        for lnk in od.get_outgoing(workers, "canOperate"):
+            berth = od.get_target(lnk)
+            if berth not in already_have:
+                txt += f"{name} -> {od.get_name(berth)} [style=dotted, arrowhead=none, color=chocolate];\n"
+
+    graphviz = f"digraph {{\n{indent(txt, 2)}}}"
+
+    return "https://dreampuf.github.io/GraphvizOnline/#"+urllib.parse.quote(graphviz)
+
+def render_port_textual(od):
+    txt = ""
+    for _, place_state in od.get_all_instances("PlaceState", include_subtypes=False):
+        place = state_to_design(od, place_state)
+        name = od.get_name(place)
+        txt += f'place "{name}" {"🚢"*get_num_ships(od, place)}\n'
+
+    for _, berth_state in od.get_all_instances("BerthState", include_subtypes=False):
+        berth = state_to_design(od, berth_state)
+        name = od.get_name(berth)
+        txt += f'berth "{name}" {"🚢"*get_num_ships(od, berth)} {od.get_slot_value(berth_state, "status")}\n'
+
+    return txt

examples/semantics/operational/port/runner.py

@@ -0,0 +1,56 @@
+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 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.joeris_solution import termination_condition, get_actions
+from examples.semantics.operational.port.assignment import termination_condition, get_actions
+
+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 ###
+
+sim = Simulator(
+    action_generator=get_actions,
+    # 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)

framework/conformance.py

@@ -427,6 +427,8 @@ class Conformance:
                 return code
 
         def check_result(result, description):
+            if result == None:
+                return # OK
             if isinstance(result, str):
                 errors.append(f"{description} not satisfied. Reason: {result}")
             elif isinstance(result, bool):
@@ -434,7 +436,7 @@ class Conformance:
                     errors.append(f"{description} not satisfied.")
             elif isinstance(result, list):
                 if len(result) > 0:
-                    reasons = indent('\n'.join(result), 2)
+                    reasons = indent('\n'.join(result), 4)
                     errors.append(f"{description} not satisfied. Reasons:\n{reasons}")
             else:
                 raise Exception(f"{description} evaluation result should be boolean or string! Instead got {result}")