diff --git a/examples/semantics/operational/port/assignment.py b/examples/semantics/operational/port/assignment.py new file mode 100644 index 0000000..b448265 --- /dev/null +++ b/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 :(" + diff --git a/examples/semantics/operational/port/helpers.py b/examples/semantics/operational/port/helpers.py new file mode 100644 index 0000000..12ecdfc --- /dev/null +++ b/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") diff --git a/examples/semantics/operational/port_models.py b/examples/semantics/operational/port/models.py similarity index 94% rename from examples/semantics/operational/port_models.py rename to examples/semantics/operational/port/models.py index e30a11d..74607b5 100644 --- a/examples/semantics/operational/port_models.py +++ b/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) diff --git a/examples/semantics/operational/port/renderer.py b/examples/semantics/operational/port/renderer.py new file mode 100644 index 0000000..4332ff5 --- /dev/null +++ b/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 diff --git a/examples/semantics/operational/port/runner.py b/examples/semantics/operational/port/runner.py new file mode 100644 index 0000000..bdb4a8d --- /dev/null +++ b/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) diff --git a/examples/semantics/operational/woods_pysem.py b/examples/semantics/operational/woods_runner.py similarity index 100% rename from examples/semantics/operational/woods_pysem.py rename to examples/semantics/operational/woods_runner.py diff --git a/framework/conformance.py b/framework/conformance.py index 634419c..b953b2e 100644 --- a/framework/conformance.py +++ b/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}")