From 8fe7b0ea040df2447bd64775561fa7f9f190d7bf Mon Sep 17 00:00:00 2001 From: Joeri Exelmans Date: Mon, 27 Jan 2025 16:03:45 +0100 Subject: [PATCH] Commit some outstanding changes. Add TODO for cleanup. --- TODO.txt | 44 +++++++++++++++++++ .../textual_od/objectdiagrams.jinja2 | 23 ++++++---- examples/conformance/woods.py | 4 +- examples/model_transformation/woods.py | 6 +-- examples/petrinet/runner.py | 13 +++--- .../tapaal/tapaal.jinja2 | 15 ++++++- examples/semantics/operational/port/models.py | 10 ++--- .../operational/port/rulebased_runner.py | 2 +- .../rules/gen_pn/r_00_place2place_rhs.od | 4 +- .../rules/gen_pn/r_10_conn2trans_lhs.od | 4 +- .../rules/gen_pn/r_10_conn2trans_rhs.od | 20 +++++++-- .../translational/runner_translate.py | 4 +- 12 files changed, 114 insertions(+), 35 deletions(-) create mode 100644 TODO.txt diff --git a/TODO.txt b/TODO.txt new file mode 100644 index 0000000..8df5fc8 --- /dev/null +++ b/TODO.txt @@ -0,0 +1,44 @@ +Things that need to be cleaned up: + + - At several places in the code, it is assumed that from the root node, there is an edge labeled 'SCD' containing the self-conforming meta-meta-model. It would be better for parts of the code that need the meta-meta-model to receive this model as a (function) parameter. + + - The whole 'ModelRef'-construct does not work as originally foreseen. It is currently only used for attributes of primitive types, where it unnecessarily complicates things. Better to get rid of it. + + +Known bugs: + - Cannot parse negative numbers + + + - When merging models, the model element names must not overlap. Maybe allow some kind of prefixing of the overlapping names? Difficulty porting existing models to the merged models if the type names have changed... + + + +Merging (meta-)models is a nightmare: + + - Prefixing the type names (to avoid naming collisions) is not an option: + (*) constraints (and transformation rules) already contain API calls that mention type names -> all of these would break + (*) don't want to prefix primitive types like "Integer", "String", ... because the existing code already assumes these exact names + + - Not prefixing the type names leads to naming collisions, even if names are carefully chosen: + (*) anonymous names, e.g., Inheritance-links still result in naming collisions (requiring auto-renaming?) + + +Feature requests: + + - Support custom functions in 'conditions' + + - When matching edge, match 'any' src/tgt + + - Support 'return'-statement in conditions? + + - Separate script for running LHS (+NAC) on any model, and visualizing the match. + + - Syntax highlighting: + most students use: + - VS Code + - PyCharm + i use: + - Sublime Text + nobody uses: + - Eclipse + diff --git a/concrete_syntax/textual_od/objectdiagrams.jinja2 b/concrete_syntax/textual_od/objectdiagrams.jinja2 index 51425d2..a559347 100644 --- a/concrete_syntax/textual_od/objectdiagrams.jinja2 +++ b/concrete_syntax/textual_od/objectdiagrams.jinja2 @@ -1,18 +1,23 @@ {% macro render_name(name) %}{{ name if not hide_names or name.startswith("__") else "" }}{% endmacro %} -{% macro render_attributes(obj) %} { +{% macro render_attributes(obj) %} +{% if len(odapi.get_slots(obj)) > 0 %} { {% for attr_name in odapi.get_slots(obj) %} {{ attr_name}} = {{ display_value( val=odapi.get_slot_value(obj, attr_name), type_name=odapi.get_type_name(odapi.get_slot(obj, attr_name)), indentation=4) }}; - {% endfor %} -}{% endmacro %} + {% endfor -%} +} +{% endif -%} +{%- endmacro %} -{% for obj_name, obj in objects %} -{{ render_name(obj_name) }}:{{ odapi.get_type_name(obj) }}{{ render_attributes(obj) }} -{% endfor %} +{%- for obj_name, obj in objects %} +{{ render_name(obj_name) }}:{{ odapi.get_type_name(obj) }} +{{- render_attributes(obj) }} +{% endfor -%} -{% for lnk_name, lnk in links %} -{{ render_name(obj_name) }}:{{ odapi.get_type_name(lnk) }} ({{odapi.get_name(odapi.get_source(lnk))}} -> {{odapi.get_name(odapi.get_target(lnk))}}){{ render_attributes(lnk) }} -{% endfor %} +{%- for lnk_name, lnk in links %} +{{ render_name(obj_name) }}:{{ odapi.get_type_name(lnk) }} ({{odapi.get_name(odapi.get_source(lnk))}} -> {{odapi.get_name(odapi.get_target(lnk))}}) +{{- render_attributes(lnk) }} +{% endfor -%} diff --git a/examples/conformance/woods.py b/examples/conformance/woods.py index 633e1e9..7475ac9 100644 --- a/examples/conformance/woods.py +++ b/examples/conformance/woods.py @@ -4,6 +4,7 @@ from framework.conformance import Conformance, render_conformance_check_result from concrete_syntax.textual_od import parser, renderer from concrete_syntax.common import indent from concrete_syntax.plantuml import renderer as plantuml +from concrete_syntax.plantuml.make_url import make_url from util.prompt import yes_no, pause state = DevState() @@ -153,6 +154,7 @@ woods_m_cs = """ bear2:Bear :afraidOf (george -> bear1) :afraidOf (george -> bear2) + :afraidOf (billy -> george) """ print() @@ -194,7 +196,7 @@ if yes_no("Print PlantUML?"): uml += plantuml.render_trace_conformance(state, woods_m, woods_mm) print("==================================") - print(uml) + print(make_url(uml)) print("==================================") print("Go to either:") print(" ▸ https://www.plantuml.com/plantuml/uml") diff --git a/examples/model_transformation/woods.py b/examples/model_transformation/woods.py index f321037..e6e88e5 100644 --- a/examples/model_transformation/woods.py +++ b/examples/model_transformation/woods.py @@ -113,9 +113,7 @@ def main(): # object to match man:{prefix}Man {{ # match only men heavy enough - {prefix}weight = ``` - get_value(this) > 60 - ```; + {prefix}weight = `get_value(this) > 60`; }} # object to delete @@ -142,6 +140,7 @@ def main(): # object to create bill:{prefix}Man {{ + # name = `"billie"+str(get_slot_value(matched("man"), "weight"))`; {prefix}weight = `100`; }} @@ -208,6 +207,7 @@ def main(): generator = match_od(state, dsl_m_id, dsl_mm_id, lhs_id, ramified_mm_id) for i, (match, color) in enumerate(zip(generator, ["red", "orange"])): + print("\nMATCH:\n", match) uml += plantuml.render_trace_match(state, match, lhs_id, dsl_m_id, color) # rewrite happens in-place (which sucks), so we will only modify a clone: diff --git a/examples/petrinet/runner.py b/examples/petrinet/runner.py index b2d0c51..df516e7 100644 --- a/examples/petrinet/runner.py +++ b/examples/petrinet/runner.py @@ -1,7 +1,7 @@ from state.devstate import DevState from api.od import ODAPI from concrete_syntax.textual_od.renderer import render_od -# from concrete_syntax.textual_od.renderer_jinja2 import render_od_jinja2 +from concrete_syntax.textual_od.renderer_jinja2 import render_od_jinja2 from bootstrap.scd import bootstrap_scd from util import loader from transformation.rule import RuleMatcherRewriter, ActionGenerator @@ -28,10 +28,10 @@ if __name__ == "__main__": mm_rt_cs = mm_cs + read_file('metamodels/mm_runtime.od') # m_cs = read_file('models/m_example_simple.od') # m_rt_initial_cs = m_cs + read_file('models/m_example_simple_rt_initial.od') - # m_cs = read_file('models/m_example_mutex.od') - # m_rt_initial_cs = m_cs + read_file('models/m_example_mutex_rt_initial.od') - m_cs = read_file('models/m_example_inharc.od') - m_rt_initial_cs = m_cs + read_file('models/m_example_inharc_rt_initial.od') + m_cs = read_file('models/m_example_mutex.od') + m_rt_initial_cs = m_cs + read_file('models/m_example_mutex_rt_initial.od') + # m_cs = read_file('models/m_example_inharc.od') + # m_rt_initial_cs = m_cs + read_file('models/m_example_inharc_rt_initial.od') # Parse them mm = loader.parse_and_check(state, mm_cs, scd_mmm, "Petri-Net Design meta-model") @@ -51,7 +51,8 @@ if __name__ == "__main__": def render_callback(od): show_petri_net(od) - return render_od(state, od.m, od.mm) + # return render_od(state, od.m, od.mm) + return render_od_jinja2(state, od.m, od.mm) sim = simulator.Simulator( action_generator=action_generator, diff --git a/examples/petrinet/translational_semantics/tapaal/tapaal.jinja2 b/examples/petrinet/translational_semantics/tapaal/tapaal.jinja2 index 445dc99..7c2596c 100644 --- a/examples/petrinet/translational_semantics/tapaal/tapaal.jinja2 +++ b/examples/petrinet/translational_semantics/tapaal/tapaal.jinja2 @@ -12,11 +12,22 @@ nameOffsetY="0" positionX="{{ i * 100 + 100 }}" positionY="100" - /> + /> {% endfor %} {% for i, (transition_name, transition) in enumerate(odapi.get_all_instances("PNTransition")) %} - + {% endfor %} {% for arc_name, arc in odapi.get_all_instances("arc") %} diff --git a/examples/semantics/operational/port/models.py b/examples/semantics/operational/port/models.py index dd7e7a3..b4a7c10 100644 --- a/examples/semantics/operational/port/models.py +++ b/examples/semantics/operational/port/models.py @@ -270,7 +270,7 @@ port_rt_m_cs = port_m_cs + """ time = 0; } - waitingState:PlaceState { numShips = 0; } :of (waitingState -> waiting) + waitingState:PlaceState { numShips = 2; } :of (waitingState -> waiting) inboundPassageState:PlaceState { numShips = 0; } :of (inboundPassageState -> inboundPassage) outboundPassageState:PlaceState { numShips = 0; } :of (outboundPassageState -> outboundPassage) @@ -282,7 +282,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:PlaceState { numShips = 0; } :of (servedState -> served) + servedState:PlaceState { numShips = 1; } :of (servedState -> served) workersState:WorkerSetState :of (workersState -> workers) @@ -396,12 +396,12 @@ smaller_model2_rt_cs = smaller_model2_cs + """ } waitingState:PlaceState { numShips = 1; } :of (waitingState -> waiting) - berthState:BerthState { numShips = 0; status = "empty"; } :of (berthState -> berth) - servedState:PlaceState { numShips = 0; } :of (servedState -> served) + berthState:BerthState { numShips = 1; status = "served"; } :of (berthState -> berth) + servedState:PlaceState { numShips = 1; } :of (servedState -> served) gen2waitState:ConnectionState { moved = False; } :of (gen2waitState -> gen2wait) wait2berthState:ConnectionState { moved = False; } :of (wait2berthState -> wait2berth) - berth2servedState:ConnectionState { moved = False; } :of (berth2servedState -> berth2served) + berth2servedState:ConnectionState { moved = True; } :of (berth2servedState -> berth2served) workersState:WorkerSetState :of (workersState -> workers) """ diff --git a/examples/semantics/operational/port/rulebased_runner.py b/examples/semantics/operational/port/rulebased_runner.py index ce73ca5..56cf67f 100644 --- a/examples/semantics/operational/port/rulebased_runner.py +++ b/examples/semantics/operational/port/rulebased_runner.py @@ -53,7 +53,7 @@ sim = Simulator( termination_condition=termination_condition, check_conformance=True, verbose=True, - renderer=render_port_textual, + # renderer=render_port_textual, # renderer=render_port_graphviz, ) diff --git a/examples/semantics/translational/rules/gen_pn/r_00_place2place_rhs.od b/examples/semantics/translational/rules/gen_pn/r_00_place2place_rhs.od index 47e7b57..ea6a227 100644 --- a/examples/semantics/translational/rules/gen_pn/r_00_place2place_rhs.od +++ b/examples/semantics/translational/rules/gen_pn/r_00_place2place_rhs.od @@ -9,7 +9,7 @@ pn_place:RAM_PNPlace { # new feature: you can control the name of the object to be created: - name = `f"pn_{get_name(matched("port_place"))}"`; + name = `f"ships_{get_name(matched("port_place"))}"`; } place2place:RAM_generic_link (pn_place -> port_place) @@ -19,4 +19,4 @@ pn_place_state:RAM_PNPlaceState { RAM_numTokens = `get_slot_value(matched('port_place_state'), "numShips")`; } - :RAM_pn_of(pn_place_state -> pn_place) \ No newline at end of file + :RAM_pn_of(pn_place_state -> pn_place) diff --git a/examples/semantics/translational/rules/gen_pn/r_10_conn2trans_lhs.od b/examples/semantics/translational/rules/gen_pn/r_10_conn2trans_lhs.od index f15843f..bdde559 100644 --- a/examples/semantics/translational/rules/gen_pn/r_10_conn2trans_lhs.od +++ b/examples/semantics/translational/rules/gen_pn/r_10_conn2trans_lhs.od @@ -1,5 +1,7 @@ -# Just look for a connection: +# Just look for a connection and its state: port_src:RAM_Source port_snk:RAM_Sink port_conn:RAM_connection (port_src -> port_snk) +port_conn_state:RAM_ConnectionState +port_of:RAM_of (port_conn_state -> port_conn) \ No newline at end of file diff --git a/examples/semantics/translational/rules/gen_pn/r_10_conn2trans_rhs.od b/examples/semantics/translational/rules/gen_pn/r_10_conn2trans_rhs.od index edc7d07..a21b72f 100644 --- a/examples/semantics/translational/rules/gen_pn/r_10_conn2trans_rhs.od +++ b/examples/semantics/translational/rules/gen_pn/r_10_conn2trans_rhs.od @@ -3,12 +3,26 @@ port_src:RAM_Source port_snk:RAM_Sink port_conn:RAM_connection (port_src -> port_snk) +port_conn_state:RAM_ConnectionState +port_of:RAM_of (port_conn_state -> port_conn) # Create a Petri Net transition, and link it to our port-connection: -pn_transition:RAM_PNTransition { - name = `f"pn_{get_name(matched("port_conn"))}"`; +move_transition:RAM_PNTransition { + name = `f"move_{get_name(matched("port_conn"))}"`; } -trans2conn:RAM_generic_link (pn_transition -> port_conn) + +moved_place:RAM_PNPlace { + name = `f" moved_{get_name(matched("port_conn"))}"`; +} +moved_place_state:RAM_PNPlaceState { + RAM_numTokens = `1 if get_slot_value(matched('port_conn_state'), "moved") else 0`; +} +:RAM_pn_of (moved_place_state -> moved_place) +# when firing a 'move', put a token in the 'moved'-place +:RAM_arc (move_transition -> moved_place) + +trans2conn:RAM_generic_link (move_transition -> port_conn) +moved2conn:RAM_generic_link (moved_place -> port_conn) # Note that we are not yet creating any incoming/outgoing petri net arcs! This will be done in another rule. \ No newline at end of file diff --git a/examples/semantics/translational/runner_translate.py b/examples/semantics/translational/runner_translate.py index 7a6bf6e..3949b9d 100644 --- a/examples/semantics/translational/runner_translate.py +++ b/examples/semantics/translational/runner_translate.py @@ -62,9 +62,9 @@ if __name__ == "__main__": print('loading model...') port_m_rt_initial = loader.parse_and_check(state, - m_cs=models.port_rt_m_cs, # <-- your final solution should work with the full model + # m_cs=models.port_rt_m_cs, # <-- your final solution should work with the full model # m_cs=models.smaller_model_rt_cs, # <-- simpler model to try first - # m_cs=models.smaller_model2_rt_cs, # <-- simpler model to try first + m_cs=models.smaller_model2_rt_cs, # <-- simpler model to try first mm=merged_mm, descr="initial model", check_conformance=False, # no need to check conformance every time