From 80cba4b9f896005001525448840e3c65b0a4cb73 Mon Sep 17 00:00:00 2001 From: Joeri Exelmans Date: Thu, 7 Nov 2024 15:38:13 +0100 Subject: [PATCH] CBD model is computing Fibonacci numbers! :) --- concrete_syntax/plantuml/renderer.py | 8 +- examples/cbd/models.py | 2 +- examples/cbd/models/m_fibonacci.od | 2 +- examples/cbd/models/m_fibonacci_initial.od | 8 +- examples/cbd/models/mm_design.od | 75 +------------- examples/cbd/models/mm_runtime.od | 72 ++++---------- examples/cbd/models/r_advance_time_lhs.od | 3 + examples/cbd/models/r_advance_time_nac.od | 36 +++++++ examples/cbd/models/r_advance_time_rhs.od | 10 ++ examples/cbd/models/r_delay_in_lhs.od | 27 +++++ examples/cbd/models/r_delay_in_nac.od | 6 ++ examples/cbd/models/r_delay_in_rhs.od | 26 +++++ examples/cbd/models/r_delay_lhs.od | 16 --- examples/cbd/models/r_delay_nac.od | 14 --- examples/cbd/models/r_delay_out_lhs.od | 14 +++ examples/cbd/models/r_delay_out_nac.od | 10 ++ examples/cbd/models/r_delay_out_rhs.od | 20 ++++ examples/cbd/models/r_delay_rhs.od | 23 ----- examples/cbd/models/r_function_out_lhs.od | 22 +++++ examples/cbd/models/r_function_out_nac.od | 14 +++ examples/cbd/models/r_function_out_rhs.od | 26 +++++ examples/cbd/runner.py | 68 ++++++++----- services/od.py | 5 +- transformation/matcher/mvs_adapter.py | 110 ++++++++++++++------- transformation/ramify.py | 8 ++ transformation/rewriter.py | 63 ++++++++---- util/eval.py | 10 +- 27 files changed, 429 insertions(+), 269 deletions(-) create mode 100644 examples/cbd/models/r_advance_time_lhs.od create mode 100644 examples/cbd/models/r_advance_time_nac.od create mode 100644 examples/cbd/models/r_advance_time_rhs.od create mode 100644 examples/cbd/models/r_delay_in_lhs.od create mode 100644 examples/cbd/models/r_delay_in_nac.od create mode 100644 examples/cbd/models/r_delay_in_rhs.od delete mode 100644 examples/cbd/models/r_delay_lhs.od delete mode 100644 examples/cbd/models/r_delay_nac.od create mode 100644 examples/cbd/models/r_delay_out_lhs.od create mode 100644 examples/cbd/models/r_delay_out_nac.od create mode 100644 examples/cbd/models/r_delay_out_rhs.od delete mode 100644 examples/cbd/models/r_delay_rhs.od create mode 100644 examples/cbd/models/r_function_out_lhs.od create mode 100644 examples/cbd/models/r_function_out_nac.od create mode 100644 examples/cbd/models/r_function_out_rhs.od diff --git a/concrete_syntax/plantuml/renderer.py b/concrete_syntax/plantuml/renderer.py index bf984a5..d82325a 100644 --- a/concrete_syntax/plantuml/renderer.py +++ b/concrete_syntax/plantuml/renderer.py @@ -150,14 +150,18 @@ def render_trace_ramifies(state, mm, ramified_mm, render_attributes=True, prefix # Render RAMifies-edges between classes for ram_name, ram_class_node in ramified_mm_scd.get_classes().items(): - original_class, = bottom.read_outgoing_elements(ram_class_node, ramify.RAMIFIES_LABEL) + original_class = ramify.get_original_type(bottom, ram_class_node) + if original_class == None: + continue # not all classes come from original (e.g., 'GlobalCondition') original_name = mm_scd.get_class_name(original_class) output += f"\n{make_ram_id(ram_class_node)} ..> {make_orig_id(original_class)} #line:green;text:green : RAMifies" if render_attributes: # and between attributes for (ram_attr_name, ram_attr_edge) in od.get_attributes(bottom, ram_class_node): - orig_attr_edge, = bottom.read_outgoing_elements(ram_attr_edge, ramify.RAMIFIES_LABEL) + orig_attr_edge = ramify.get_original_type(bottom, ram_attr_edge) + if orig_attr_edge == None: + continue # not all attributes come from original (e.g., 'condition') orig_class_node = bottom.read_edge_source(orig_attr_edge) # dirty AF: orig_attr_name = mm_scd.get_class_name(orig_attr_edge)[len(original_name)+1:] diff --git a/examples/cbd/models.py b/examples/cbd/models.py index fcd694c..28c0c9b 100644 --- a/examples/cbd/models.py +++ b/examples/cbd/models.py @@ -51,7 +51,7 @@ def get_fibonacci(state, scd_mmm): return (mm, mm_rt, m, m_rt_initial) -RULE_NAMES = ["delay"] +RULE_NAMES = ["delay_out", "function_out", "delay_in", "advance_time"] KINDS = ["nac", "lhs", "rhs"] def get_rules(state, rt_mm): diff --git a/examples/cbd/models/m_fibonacci.od b/examples/cbd/models/m_fibonacci.od index a093965..9fe9dd7 100644 --- a/examples/cbd/models/m_fibonacci.od +++ b/examples/cbd/models/m_fibonacci.od @@ -1,7 +1,7 @@ # Adder, two inputs, one output adder:Function { func = ``` - n2_out = n0_in + n1_in + read('n0_in') + read('n1_in') ```; } n0_in:InPort diff --git a/examples/cbd/models/m_fibonacci_initial.od b/examples/cbd/models/m_fibonacci_initial.od index 984e606..4111d51 100644 --- a/examples/cbd/models/m_fibonacci_initial.od +++ b/examples/cbd/models/m_fibonacci_initial.od @@ -1,9 +1,13 @@ # Initial state for both delay blocks: d0s:State { - state = 0; + x = 0; } d1s:State { - state = 1; + x = 1; } :delay2State (d0 -> d0s) :delay2State (d1 -> d1s) + +clock:Clock { + time = 0; +} \ No newline at end of file diff --git a/examples/cbd/models/mm_design.od b/examples/cbd/models/mm_design.od index c5f8512..cd7c74b 100644 --- a/examples/cbd/models/mm_design.od +++ b/examples/cbd/models/mm_design.od @@ -2,12 +2,8 @@ Block:Class { abstract = True; } -InPort:Class { - # abstract = True; -} -OutPort:Class { - # abstract = True; -} +InPort:Class +OutPort:Class hasInPort:Association (Block -> InPort) { # Every Port contained by exactly one Block: @@ -21,27 +17,12 @@ hasOutPort:Association (Block -> OutPort) { } link:Association (OutPort -> InPort) { - #abstract = True; - # Every InPort connected to exactly one OutPort source_lower_cardinality = 1; source_upper_cardinality = 1; } -# In- and Out-Ports are labeled: - -# hasInPort_label:AttributeLink (hasInPort -> String) { -# name = "label"; -# optional = False; -# } -# hasOutPort_label:AttributeLink (hasOutPort -> String) { -# name = "label"; -# optional = False; -# } - - - # Function Block: pure function that computes outputs based on inputs Function:Class @@ -69,61 +50,9 @@ Delay:Class { num_outports = len(get_outgoing(this, "hasOutPort")) if num_inports != 1: errors.append(f"Delay block must have one inport, instead got {num_inports}") - in_type = None - else: - in_type = get_type_name(get_target(get_outgoing(this, "hasInPort")[0])) if num_outports != 1: errors.append(f"Delay block must have one inport, instead got {num_outports}") - out_type = None - else: - out_type = get_type_name(get_target(get_outgoing(this, "hasOutPort")[0])) - # if in_type != None and out_type != None and in_type[0:3] != out_type[0:3]: - # errors.append(f"Inport type ({in_type}) differs from outport type ({out_type})") errors ```; } :Inheritance (Delay -> Block) - - - - -# Object Diagrams are statically typed, so we must create in/out-ports, and MemorySlots for all primitive types: - - -# # Port types - -# BoolInPort:Class -# IntInPort:Class -# StrInPort:Class - -# BoolOutPort:Class -# IntOutPort:Class -# StrOutPort:Class - -# :Inheritance (BoolInPort -> InPort) -# :Inheritance (IntInPort -> InPort) -# :Inheritance (StrInPort -> InPort) - -# :Inheritance (BoolOutPort -> OutPort) -# :Inheritance (IntOutPort -> OutPort) -# :Inheritance (StrOutPort -> OutPort) - -# # Link types - -# boolLink:Association (BoolOutPort -> BoolInPort) -# intLink:Association (IntOutPort -> IntInPort) -# strLink:Association (StrOutPort -> StrInPort) - -# :Inheritance (boolLink -> link) -# :Inheritance (intLink -> link) -# :Inheritance (strLink -> link) - -# # Delay block types - -# BoolDelay:Class -# IntDelay:Class -# StrDelay:Class - -# :Inheritance (BoolDelay -> Delay) -# :Inheritance (IntDelay -> Delay) -# :Inheritance (StrDelay -> Delay) diff --git a/examples/cbd/models/mm_runtime.od b/examples/cbd/models/mm_runtime.od index 0355eb6..4479ecf 100644 --- a/examples/cbd/models/mm_runtime.od +++ b/examples/cbd/models/mm_runtime.od @@ -1,85 +1,47 @@ # Link state ("signal") -Signal:Class { - # abstract = True; -} +Signal:Class -Signal_signal:AttributeLink (Signal -> Integer) { - name = "signal"; +Signal_x:AttributeLink (Signal -> Integer) { + name = "x"; optional = False; } -hasSignal:Association (link -> Signal) { +hasSignal:Association (OutPort -> Signal) { # every Signal has 1 link source_lower_cardinality = 1; source_upper_cardinality = 1; + # every link has 0..1 Signals: target_upper_cardinality = 1; } -# BoolSignal:Class -# IntSignal:Class -# StrSignal:Class - -# :Inheritance (BoolSignal -> Signal) -# :Inheritance (IntSignal -> Signal) -# :Inheritance (StrSignal -> Signal) - -# BoolSignal_signal:AttributeLink (BoolSignal -> Boolean) { -# name = "signal"; -# optional = False; -# } -# IntSignal_signal:AttributeLink (IntSignal -> Integer) { -# name = "signal"; -# optional = False; -# } -# StrSignal_signal:AttributeLink (StrSignal -> String) { -# name = "signal"; -# optional = False; -# } - - # Delay block state # mandatory - otherwise we cannot determine the output signal of a delay block -State:Class { - # abstract = True; -} +State:Class -State_state:AttributeLink (State -> Integer) { - name = "state"; +State_x:AttributeLink (State -> Integer) { + name = "x"; optional = False; } delay2State:Association (Delay -> State) { + # one-to-one source_lower_cardinality = 1; source_upper_cardinality = 1; target_lower_cardinality = 1; target_upper_cardinality = 1; } -# BoolState:Class -# IntState:Class -# StrState:Class +Clock:Class { + lower_cardinality = 1; + upper_cardinality = 1; +} -# :Inheritance (BoolState -> State) -# :Inheritance (IntState -> State) -# :Inheritance (StrState -> State) - - -# BoolState_state:AttributeLink (BoolState -> Boolean) { -# name = "state"; -# optional = False; -# } - -# IntState_state:AttributeLink (IntState -> Integer) { -# name = "state"; -# optional = False; -# } - -# StrState_state:AttributeLink (StrState -> String) { -# name = "state"; -# optional = False; -# } +Clock_time:AttributeLink (Clock -> Integer) { + name = "time"; + optional = False; +} \ No newline at end of file diff --git a/examples/cbd/models/r_advance_time_lhs.od b/examples/cbd/models/r_advance_time_lhs.od new file mode 100644 index 0000000..d66e3ef --- /dev/null +++ b/examples/cbd/models/r_advance_time_lhs.od @@ -0,0 +1,3 @@ +clock:RAM_Clock { + RAM_time = `True`; +} diff --git a/examples/cbd/models/r_advance_time_nac.od b/examples/cbd/models/r_advance_time_nac.od new file mode 100644 index 0000000..a1546ab --- /dev/null +++ b/examples/cbd/models/r_advance_time_nac.od @@ -0,0 +1,36 @@ + +# If there is a Delay-block whose input signal differs from its state, we cannot yet advance time: + +delay:RAM_Delay + +delay_in:RAM_InPort + +delay_has_input:RAM_hasInPort (delay -> delay_in) + +some_outport:RAM_OutPort + +delay_in_conn:RAM_link (some_outport -> delay_in) + +in_signal:RAM_Signal + +port_has_signal:RAM_hasSignal (some_outport -> in_signal) + +state:RAM_State { + RAM_x = `get_slot_value(matched('in_signal'), 'x') != get_value(this)`; +} + +delay_to_state:RAM_delay2State (delay -> state) + + +# Also, we cannot advance time until all outports have signals: + +:GlobalCondition { + condition = ``` + missing_signals = False + for _, outport in get_all_instances("OutPort"): + if len(get_outgoing(outport, 'hasSignal')) == 0: + missing_signals = True + break + missing_signals + ```; +} diff --git a/examples/cbd/models/r_advance_time_rhs.od b/examples/cbd/models/r_advance_time_rhs.od new file mode 100644 index 0000000..490cf0b --- /dev/null +++ b/examples/cbd/models/r_advance_time_rhs.od @@ -0,0 +1,10 @@ +clock:RAM_Clock { + RAM_time = `get_value(this) + 1`; +} + +:GlobalCondition { + condition = ``` + for _, signal in get_all_instances("Signal"): + delete(signal) + ```; +} \ No newline at end of file diff --git a/examples/cbd/models/r_delay_in_lhs.od b/examples/cbd/models/r_delay_in_lhs.od new file mode 100644 index 0000000..d7e1393 --- /dev/null +++ b/examples/cbd/models/r_delay_in_lhs.od @@ -0,0 +1,27 @@ +# We look for a Delay-block, its inport connected to an outport that has a signal + +delay:RAM_Delay + +delay_in:RAM_InPort + +delay_has_input:RAM_hasInPort (delay -> delay_in) + +some_outport:RAM_OutPort + +delay_in_conn:RAM_link (some_outport -> delay_in) + +in_signal:RAM_Signal + +port_has_signal:RAM_hasSignal (some_outport -> in_signal) + + + +# State of Delay block... (will be updated in RHS) + +state:RAM_State { + # Attention: you MUST match the existing attribute, in order to force an UDPATE of the attribute, rather than CREATION + + RAM_x = `True`; +} + +delay_to_state:RAM_delay2State (delay -> state) diff --git a/examples/cbd/models/r_delay_in_nac.od b/examples/cbd/models/r_delay_in_nac.od new file mode 100644 index 0000000..aced4c5 --- /dev/null +++ b/examples/cbd/models/r_delay_in_nac.od @@ -0,0 +1,6 @@ +state:RAM_State # <- must repeat elements from LHS that we refer to + +in_signal:RAM_Signal { + # If the signal is already equal to the state, the NAC holds: + RAM_x = `get_value(this) == get_slot_value(matched('state'), 'x')`; +} diff --git a/examples/cbd/models/r_delay_in_rhs.od b/examples/cbd/models/r_delay_in_rhs.od new file mode 100644 index 0000000..9353dc5 --- /dev/null +++ b/examples/cbd/models/r_delay_in_rhs.od @@ -0,0 +1,26 @@ +# Everything from our LHS (don't delete anything) + +delay:RAM_Delay + +delay_in:RAM_InPort + +delay_has_input:RAM_hasOutPort (delay -> delay_in) + +some_outport:RAM_OutPort + +delay_in_conn:RAM_link (some_outport -> delay_in) + +in_signal:RAM_Signal + +port_has_signal:RAM_hasSignal (some_outport -> in_signal) + +state:RAM_State { + # Update: + RAM_x = ``` + new_state = get_slot_value(matched('in_signal'), 'x') + print(f"Updating delay {get_name(matched('delay'))} state: {new_state}") + new_state + ```; +} + +delay_to_state:RAM_delay2State (delay -> state) diff --git a/examples/cbd/models/r_delay_lhs.od b/examples/cbd/models/r_delay_lhs.od deleted file mode 100644 index 3186b6d..0000000 --- a/examples/cbd/models/r_delay_lhs.od +++ /dev/null @@ -1,16 +0,0 @@ -# We look for a Delay-block, its outgoing connection, and its State - -delay:RAM_Delay - -delay_out:RAM_OutPort # abstract - -delay_has_output:RAM_hasOutPort (delay -> delay_out) - -some_inport:RAM_InPort # abstract - -delay_out_conn:RAM_link (delay_out -> some_inport) - - -state:RAM_State - -delay_to_state:RAM_delay2State (delay -> state) diff --git a/examples/cbd/models/r_delay_nac.od b/examples/cbd/models/r_delay_nac.od deleted file mode 100644 index b605f44..0000000 --- a/examples/cbd/models/r_delay_nac.od +++ /dev/null @@ -1,14 +0,0 @@ -# From our LHS: - -delay_out:RAM_OutPort # abstract - -some_inport:RAM_InPort # abstract - -delay_out_conn:RAM_link (delay_out -> some_inport) # abstract - - -# The delay block's outgoing connection already has a signal: - -some_signal:RAM_Signal - -:RAM_hasSignal (delay_out_conn -> some_signal) diff --git a/examples/cbd/models/r_delay_out_lhs.od b/examples/cbd/models/r_delay_out_lhs.od new file mode 100644 index 0000000..f063681 --- /dev/null +++ b/examples/cbd/models/r_delay_out_lhs.od @@ -0,0 +1,14 @@ +# We look for a Delay-block, its outport, and its State + +delay:RAM_Delay + +delay_out:RAM_OutPort + +delay_has_output:RAM_hasOutPort (delay -> delay_out) + + +state:RAM_State + +delay_to_state:RAM_delay2State (delay -> state) + +clock:RAM_Clock \ No newline at end of file diff --git a/examples/cbd/models/r_delay_out_nac.od b/examples/cbd/models/r_delay_out_nac.od new file mode 100644 index 0000000..93c80e5 --- /dev/null +++ b/examples/cbd/models/r_delay_out_nac.od @@ -0,0 +1,10 @@ +# From our LHS: + +delay_out:RAM_OutPort + + +# We don't want to see the delay block's outport already having a signal: + +some_signal:RAM_Signal + +:RAM_hasSignal (delay_out -> some_signal) diff --git a/examples/cbd/models/r_delay_out_rhs.od b/examples/cbd/models/r_delay_out_rhs.od new file mode 100644 index 0000000..94abd70 --- /dev/null +++ b/examples/cbd/models/r_delay_out_rhs.od @@ -0,0 +1,20 @@ +# Our entire LHS (don't delete anything): + +delay:RAM_Delay + +delay_out:RAM_OutPort + +delay_has_output:RAM_hasOutPort (delay -> delay_out) + +state:RAM_State + +delay_to_state:RAM_delay2State (delay -> state) + +clock:RAM_Clock + +# To create: + +new_signal:RAM_Signal { + RAM_x = `get_slot_value(matched('state'), 'x')`; +} +:RAM_hasSignal (delay_out -> new_signal) diff --git a/examples/cbd/models/r_delay_rhs.od b/examples/cbd/models/r_delay_rhs.od deleted file mode 100644 index a77c38a..0000000 --- a/examples/cbd/models/r_delay_rhs.od +++ /dev/null @@ -1,23 +0,0 @@ -# Our entire LHS (don't delete anything): - -delay:RAM_Delay - -delay_out:RAM_OutPort # abstract - -delay_has_output:RAM_hasOutPort (delay -> delay_out) - -some_inport:RAM_InPort # abstract - -delay_out_conn:RAM_link (delay_out -> some_inport) # abstract - -state:RAM_State - -delay_to_state:RAM_delay2State (delay -> state) - - -# To create: - -new_signal:RAM_Signal { - RAM_signal = `get_slot_value(match('state'), 'state')`; -} -:RAM_hasSignal (delay_out_conn -> new_signal) diff --git a/examples/cbd/models/r_function_out_lhs.od b/examples/cbd/models/r_function_out_lhs.od new file mode 100644 index 0000000..dd1a4d8 --- /dev/null +++ b/examples/cbd/models/r_function_out_lhs.od @@ -0,0 +1,22 @@ +# Match function and its out-connection + +f:RAM_Function { + # Only match if the signal of all inputs has been computed: + condition = ``` + ok = True + for o in get_outgoing(this, "hasInPort"): + inport = get_target(o) + in_conn = get_incoming(inport, "link")[0] + some_outport = get_source(in_conn) + if len(get_outgoing(some_outport, "hasSignal")) == 0: + ok = False + break + ok + ```; +} + +f_outport:RAM_OutPort + +f_has_outport:RAM_hasOutPort (f -> f_outport) + +clock:RAM_Clock diff --git a/examples/cbd/models/r_function_out_nac.od b/examples/cbd/models/r_function_out_nac.od new file mode 100644 index 0000000..c6fd7f2 --- /dev/null +++ b/examples/cbd/models/r_function_out_nac.od @@ -0,0 +1,14 @@ +# From our LHS: + +f:RAM_Function + +f_outport:RAM_OutPort + +f_has_outport:RAM_hasOutPort (f -> f_outport) + + +# We don't want to see the function's out-connection already having a signal: + +some_signal:RAM_Signal + +:RAM_hasSignal (f_outport -> some_signal) diff --git a/examples/cbd/models/r_function_out_rhs.od b/examples/cbd/models/r_function_out_rhs.od new file mode 100644 index 0000000..688cd8f --- /dev/null +++ b/examples/cbd/models/r_function_out_rhs.od @@ -0,0 +1,26 @@ +# Our entire LHS (don't delete anything): + +f:RAM_Function + +f_outport:RAM_OutPort + +f_has_outport:RAM_hasOutPort (f -> f_outport) + +clock:RAM_Clock + +# To create: + +f_out_signal:RAM_Signal { + RAM_x = ``` + def read(inport_name): + inport = get(inport_name) + outport = get_source(get_incoming(inport, "link")[0]) + signal = get_target(get_outgoing(outport, "hasSignal")[0]) + return get_slot_value(signal, "x") + + code = get_slot_value(matched('f'), 'func') + + eval(code, {}, { 'read': read }) + ```; +} +:RAM_hasSignal (f_outport -> f_out_signal) diff --git a/examples/cbd/runner.py b/examples/cbd/runner.py index a69d247..ac92aca 100644 --- a/examples/cbd/runner.py +++ b/examples/cbd/runner.py @@ -1,6 +1,8 @@ from state.devstate import DevState from bootstrap.scd import bootstrap_scd +from framework.conformance import Conformance, render_conformance_check_result + from concrete_syntax.common import indent from concrete_syntax.textual_od import renderer as od_renderer from concrete_syntax.plantuml import renderer as plantuml @@ -17,12 +19,10 @@ import models state = DevState() scd_mmm = bootstrap_scd(state) +print("Parsing models...") mm, mm_rt, m, m_rt_initial = models.get_fibonacci(state, scd_mmm) - mm_rt_ram, rules = models.get_rules(state, mm_rt) - - # print("RT-MM") # print(make_plantuml_url(plantuml.render_class_diagram(state, mm_rt))) @@ -42,28 +42,40 @@ def get_matches(): pattern_m=lhs, pattern_mm=mm_rt_ram) - for i, lhs_match in enumerate(lhs_matcher): + try: + for i, lhs_match in enumerate(lhs_matcher): + nac_matcher = match_od(state, + host_m=m_rt, + host_mm=mm_rt, + pattern_m=rule["nac"], + pattern_mm=mm_rt_ram, + pivot=lhs_match) - nac_matcher = match_od(state, - host_m=m_rt, - host_mm=mm_rt, - pattern_m=rule["nac"], - pattern_mm=mm_rt_ram, - pivot=lhs_match) + try: + for j, nac_match in enumerate(nac_matcher): + break # there may be more NAC-matches, but we already now enough + else: + # We got a match! + yield (rule_name, lhs, rule["rhs"], lhs_match) + except Exception as e: + # Make exceptions raised in eval'ed code easier to trace: + e.add_note(f"while matching NAC of '{rule_name}'") + raise - for j, nac_match in enumerate(nac_matcher): - break # there may be more NAC-matches, but we already now enough - else: - # We got a match! - yield (rule_name, lhs, rule["rhs"], lhs_match) + except Exception as e: + # Make exceptions raised in eval'ed code easier to trace: + e.add_note(f"while matching LHS of '{rule_name}'") + raise while True: # print(make_graphviz_url(graphviz.render_object_diagram(state, m_rt, mm_rt))) cs = od_renderer.render_od(state, m_rt, mm_rt, hide_names=False) print(indent(cs, 6)) - + conf = Conformance(state, m_rt, mm_rt) + print(render_conformance_check_result(conf.check_nominal())) matches = list(get_matches()) + print(f"There are {len(matches)} matches.") if len(matches) == 0: break @@ -75,21 +87,23 @@ while True: # txt += graphviz.render_trace_match(state, lhs_match, lhs, m_rt, color="orange") # match_urls.append(make_graphviz_url(txt)) - print('picking', lhs_match) - - print('rewriting') + print(f"executing rule '{rule_name}' ", lhs_match) # copy or will be overwritten in-place m_rt = clone_od(state, m_rt, mm_rt) rhs_match = dict(lhs_match) - - rewrite(state, - lhs_m=lhs, - rhs_m=rhs, - pattern_mm=mm_rt_ram, - name_mapping=rhs_match, - host_m=m_rt, - mm=mm_rt) + try: + rewrite(state, + lhs_m=lhs, + rhs_m=rhs, + pattern_mm=mm_rt_ram, + name_mapping=rhs_match, + host_m=m_rt, + host_mm=mm_rt) + except Exception as e: + # Make exceptions raised in eval'ed code easier to trace: + e.add_note(f"while executing RHS of '{rule_name}'") + raise # import subprocess # subprocess.run(["firefox", "--new-window", *match_urls]) diff --git a/services/od.py b/services/od.py index 04c8725..25116af 100644 --- a/services/od.py +++ b/services/od.py @@ -254,7 +254,10 @@ def is_typed_by(bottom, el: UUID, typ: UUID): def get_typed_by(bottom, model, type_node: UUID): name_to_instance = {} for key in bottom.read_keys(model): - element, = bottom.read_outgoing_elements(model, key) + els = bottom.read_outgoing_elements(model, key) + if len(els) > 1: + raise Exception(f"Assertion failed: Model contains more than one object named '{key}'!") + element = els[0] element_types = bottom.read_outgoing_elements(element, "Morphism") if type_node in element_types: name_to_instance[key] = element diff --git a/transformation/matcher/mvs_adapter.py b/transformation/matcher/mvs_adapter.py index 0931c9a..bce23f3 100644 --- a/transformation/matcher/mvs_adapter.py +++ b/transformation/matcher/mvs_adapter.py @@ -76,7 +76,8 @@ UUID_REGEX = re.compile(r"[0-9a-z][0-9a-z][0-9a-z][0-9a-z][0-9a-z][0-9a-z][0-9a- # Converts an object diagram in MVS state to the pattern matcher graph type # ModelRefs are flattened -def model_to_graph(state: State, model: UUID, metamodel: UUID, prefix=""): +def model_to_graph(state: State, model: UUID, metamodel: UUID, + _filter=lambda node: True, prefix=""): # with Timer("model_to_graph"): od = services_od.OD(model, metamodel, state) scd = SCD(model, state) @@ -121,7 +122,7 @@ def model_to_graph(state: State, model: UUID, metamodel: UUID, prefix=""): return node # Objects and Links become vertices - uuid_to_vtx = { node: to_vtx(node, prefix+key) for key in bottom.read_keys(model) for node in bottom.read_outgoing_elements(model, key) } + uuid_to_vtx = { node: to_vtx(node, prefix+key) for key in bottom.read_keys(model) for node in bottom.read_outgoing_elements(model, key) if _filter(node) } graph.vtxs = [ vtx for vtx in uuid_to_vtx.values() ] # For every Link, two edges are created (for src and tgt) @@ -183,7 +184,6 @@ def model_to_graph(state: State, model: UUID, metamodel: UUID, prefix=""): # # print(type_edge) # graph.edges.append(type_edge) - # Add typing information for: # - classes # - attributes @@ -192,25 +192,31 @@ def model_to_graph(state: State, model: UUID, metamodel: UUID, prefix=""): objects = scd.get_typed_by(class_node) # print("typed by:", class_name, objects) for obj_name, obj_node in objects.items(): - add_types(obj_node) + if _filter(obj_node): + add_types(obj_node) for attr_name, attr_node in scd_mm.get_attributes(class_name).items(): attrs = scd.get_typed_by(attr_node) for slot_name, slot_node in attrs.items(): - add_types(slot_node) + if _filter(slot_node): + add_types(slot_node) for assoc_name, assoc_node in scd_mm.get_associations().items(): objects = scd.get_typed_by(assoc_node) # print("typed by:", assoc_name, objects) for link_name, link_node in objects.items(): - add_types(link_node) + if _filter(link_node): + add_types(link_node) return names, graph def match_od(state, host_m, host_mm, pattern_m, pattern_mm, pivot={}): + bottom = Bottom(state) # compute subtype relations and such: cdapi = CDAPI(state, host_mm) odapi = ODAPI(state, host_m, host_mm) + pattern_odapi = ODAPI(state, pattern_m, pattern_mm) + pattern_mm_odapi = ODAPI(state, pattern_mm, cdapi.mm) # Function object for pattern matching. Decides whether to match host and guest vertices, where guest is a RAMified instance (e.g., the attributes are all strings with Python expressions), and the host is an instance (=object diagram) of the original model (=class diagram) class RAMCompare: @@ -221,6 +227,9 @@ def match_od(state, host_m, host_mm, pattern_m, pattern_mm, pivot={}): type_model_id = bottom.state.read_dict(bottom.state.read_root(), "SCD") self.scd_model = UUID(bottom.state.read_value(type_model_id)) + # constraints need to be checked at the very end, after a complete match is established, because constraint code may refer to matched elements by their name + self.conditions_to_check = [] + def match_types(self, g_vtx_type, h_vtx_type): # types only match with their supertypes # we assume that 'RAMifies'-traceability links have been created between guest and host types @@ -256,26 +265,10 @@ def match_od(state, host_m, host_mm, pattern_m, pattern_mm, pivot={}): return False python_code = services_od.read_primitive_value(self.bottom, g_vtx.node_id, pattern_mm)[0] - return exec_then_eval(python_code, - _globals=bind_api_readonly(odapi), - _locals={'this': h_vtx.node_id}) - # nested_matches = [m for m in match_od(state, h_ref_m, h_ref_mm, g_ref_m, g_ref_mm)] + self.conditions_to_check.append((python_code, h_vtx.node_id)) - - # print('begin recurse') - # g_ref_m, g_ref_mm = g_vtx.modelref - # h_ref_m, h_ref_mm = h_vtx.modelref - # print('nested_matches:', nested_matches) - # if len(nested_matches) == 0: - # return False - # elif len(nested_matches) == 1: - # return True - # else: - # raise Exception("We have a problem: there is more than 1 match in the nested models.") - # print('end recurse') - - # Then, match by value + return True # do be determined later, if it's actually a match if g_vtx.value == None: return h_vtx.value == None @@ -293,20 +286,26 @@ def match_od(state, host_m, host_mm, pattern_m, pattern_mm, pivot={}): if h_vtx.value == IS_MODELREF: return False - # python_code = g_vtx.value - # try: - # return exec_then_eval(python_code, - # _globals=bind_api_readonly(odapi), - # _locals={'this': h_vtx.node_id}) - # except Exception as e: - # print(e) - # return False return True # Convert to format understood by matching algorithm h_names, host = model_to_graph(state, host_m, host_mm) - g_names, guest = model_to_graph(state, pattern_m, pattern_mm) + # Only match matchable pattern elements + # E.g., the 'condition'-attribute that is added to every class, cannot be matched with anything + def is_matchable(pattern_el): + pattern_el_name = pattern_odapi.get_name(pattern_el) + if pattern_odapi.get_type_name(pattern_el) == "GlobalCondition": + return False + # Super-cheap and unreliable way of filtering out the 'condition'-attribute, added to every class: + return not (pattern_el_name.endswith("condition") + # as an extra safety measure, if the user defined her own 'condition' attribute, RAMification turned this into 'RAM_condition', and we can detect this + # of course this breaks if the class name already ended with 'RAM', but let's hope that never happens + # also, we are assuming the default "RAM_" prefix is used, but the user can change this... + and not pattern_el_name.endswith("RAM_condition")) + + g_names, guest = model_to_graph(state, pattern_m, pattern_mm, + _filter=is_matchable) graph_pivot = { g_names[guest_name] : h_names[host_name] @@ -314,7 +313,46 @@ def match_od(state, host_m, host_mm, pattern_m, pattern_mm, pivot={}): if guest_name in g_names } - matcher = MatcherVF2(host, guest, RAMCompare(Bottom(state), services_od.OD(host_mm, host_m, state))) + obj_conditions = [] + for class_name, class_node in pattern_mm_odapi.get_all_instances("Class"): + for obj_name, obj_node in pattern_odapi.get_all_instances(class_name): + python_code = pattern_odapi.get_slot_value_default(obj_node, "condition", 'True') + if class_name == "GlobalCondition": + obj_conditions.append((python_code, None)) + else: + obj_conditions.append((python_code, obj_name)) + + + def check_conditions(name_mapping): + def check(python_code: str, loc): + return exec_then_eval(python_code, + _globals={ + **bind_api_readonly(odapi), + 'matched': lambda name: bottom.read_outgoing_elements(host_m, name_mapping[name])[0], + }, + _locals=loc) + + # Attribute conditions + for python_code, host_node in compare.conditions_to_check: + if not check(python_code, {'this': host_node}): + return False + + for python_code, pattern_el_name in obj_conditions: + if pattern_el_name == None: + # GlobalCondition + if not check(python_code, {}): + return False + else: + # object-lvl condition + host_el_name = name_mapping[pattern_el_name] + host_node = odapi.get(host_el_name) + if not check(python_code, {'this': host_node}): + return False + return True + + + compare = RAMCompare(bottom, services_od.OD(host_mm, host_m, state)) + matcher = MatcherVF2(host, guest, compare) for m in matcher.match(graph_pivot): # print("\nMATCH:\n", m) # Convert mapping @@ -322,4 +360,8 @@ def match_od(state, host_m, host_mm, pattern_m, pattern_mm, pivot={}): for guest_vtx, host_vtx in m.mapping_vtxs.items(): if isinstance(guest_vtx, NamedNode) and isinstance(host_vtx, NamedNode): name_mapping[guest_vtx.name] = host_vtx.name + + if not check_conditions(name_mapping): + continue # not a match after all... + yield name_mapping diff --git a/transformation/ramify.py b/transformation/ramify.py index 1406e49..f07c5d2 100644 --- a/transformation/ramify.py +++ b/transformation/ramify.py @@ -54,8 +54,13 @@ def ramify(state: State, model: UUID, prefix = "RAM_") -> UUID: # create traceability link bottom.create_edge(ramified_attr_link, attr_edge, RAMIFIES_LABEL) + # Additional constraint that can be specified + ramified_scd._create_attribute_link(prefix+class_name, actioncode_modelref, "condition", optional=True) + already_ramified.add(class_name) + glob_cond = ramified_scd.create_class("GlobalCondition", abstract=None) + ramified_scd._create_attribute_link("GlobalCondition", actioncode_modelref, "condition", optional=False) assocs_to_ramify = m_scd.get_associations() @@ -90,6 +95,9 @@ def ramify(state: State, model: UUID, prefix = "RAM_") -> UUID: # create traceability link bottom.create_edge(ramified_assoc, assoc_node, RAMIFIES_LABEL) + # Additional constraint that can be specified + ramified_scd._create_attribute_link(prefix+assoc_name, actioncode_modelref, "condition", optional=True) + already_ramified.add(assoc_name) assocs_to_ramify = ramify_later diff --git a/transformation/rewriter.py b/transformation/rewriter.py index 43c0be2..b0b84a5 100644 --- a/transformation/rewriter.py +++ b/transformation/rewriter.py @@ -11,25 +11,34 @@ from services import od from services.primitives.string_type import String from services.primitives.actioncode_type import ActionCode from services.primitives.integer_type import Integer -from util.eval import exec_then_eval +from util.eval import exec_then_eval, simply_exec -def process_rule(state, lhs: UUID, rhs: UUID): +def preprocess_rule(state, lhs: UUID, rhs: UUID, name_mapping): bottom = Bottom(state) - to_delete = { name for name in bottom.read_keys(lhs) if name not in bottom.read_keys(rhs) } - to_create = { name for name in bottom.read_keys(rhs) if name not in bottom.read_keys(lhs) } - common = { name for name in bottom.read_keys(lhs) if name in bottom.read_keys(rhs) } + to_delete = { name for name in bottom.read_keys(lhs) if name not in bottom.read_keys(rhs) and name in name_mapping } + to_create = { name for name in bottom.read_keys(rhs) if name not in bottom.read_keys(lhs) + # extremely dirty: + and "GlobalCondition" not in name } + common = { name for name in bottom.read_keys(lhs) if name in bottom.read_keys(rhs) and name in name_mapping } - # print("to_delete:", to_delete) - # print("to_create:", to_create) + print("to_delete:", to_delete) + print("to_create:", to_create) return to_delete, to_create, common # Rewrite is performed in-place (modifying `host_m`) # Also updates the `mapping` in-place, to become RHS -> host -def rewrite(state, lhs_m: UUID, rhs_m: UUID, pattern_mm: UUID, name_mapping: dict, host_m: UUID, mm: UUID): +def rewrite(state, lhs_m: UUID, rhs_m: UUID, pattern_mm: UUID, name_mapping: dict, host_m: UUID, host_mm: UUID): bottom = Bottom(state) + orig_name_mapping = dict(name_mapping) + + # function that can be called from within RHS action code + def matched_callback(pattern_name: str): + host_name = orig_name_mapping[pattern_name] + return bottom.read_outgoing_elements(host_m, host_name)[0] + scd_metamodel_id = state.read_dict(state.read_root(), "SCD") scd_metamodel = UUID(state.read_value(scd_metamodel_id)) @@ -38,12 +47,12 @@ def rewrite(state, lhs_m: UUID, rhs_m: UUID, pattern_mm: UUID, name_mapping: dic assoc_type = od.get_scd_mm_assoc_node(bottom) modelref_type = od.get_scd_mm_modelref_node(bottom) - m_od = od.OD(mm, host_m, bottom.state) + m_od = od.OD(host_mm, host_m, bottom.state) rhs_od = od.OD(pattern_mm, rhs_m, bottom.state) - to_delete, to_create, common = process_rule(state, lhs_m, rhs_m) + to_delete, to_create, common = preprocess_rule(state, lhs_m, rhs_m, orig_name_mapping) - odapi = ODAPI(state, host_m, mm) + odapi = ODAPI(state, host_m, host_mm) # Perform deletions for pattern_name_to_delete in to_delete: @@ -89,7 +98,7 @@ def rewrite(state, lhs_m: UUID, rhs_m: UUID, pattern_mm: UUID, name_mapping: dic # print(' -> postpone (is link)') edges_to_create.append((pattern_name_to_create, rhs_el_to_create, original_type, 'link', model_el_name_to_create)) else: - original_type_name = od.get_object_name(bottom, mm, original_type) + original_type_name = od.get_object_name(bottom, host_mm, original_type) print(" -> warning: don't know about", original_type_name) else: # print(" -> no original (un-RAMified) type") @@ -100,7 +109,11 @@ def rewrite(state, lhs_m: UUID, rhs_m: UUID, pattern_mm: UUID, name_mapping: dic # Assume the string is a Python expression to evaluate python_expr = ActionCode(UUID(bottom.read_value(rhs_el_to_create)), bottom.state).read() - result = exec_then_eval(python_expr, _globals=bind_api(odapi)) + result = exec_then_eval(python_expr, _globals={ + **bind_api(odapi), + 'matched': matched_callback, + }) + # Write the result into the host model. # This will be the *value* of an attribute. The attribute-link (connecting an object to the attribute) will be created as an edge later. if isinstance(result, int): @@ -109,7 +122,8 @@ def rewrite(state, lhs_m: UUID, rhs_m: UUID, pattern_mm: UUID, name_mapping: dic m_od.create_string_value(model_el_name_to_create, result) name_mapping[pattern_name_to_create] = model_el_name_to_create else: - raise Exception(f"RHS element '{pattern_name_to_create}' needs to be created in host, but has no un-RAMified type, and I don't know what to do with it. It's type is '{type_name}'") + msg = f"RHS element '{pattern_name_to_create}' needs to be created in host, but has no un-RAMified type, and I don't know what to do with it. It's type is '{type_name}'" + raise Exception(msg) # print("create edges....") for pattern_name_to_create, rhs_el_to_create, original_type, original_type_name, model_el_name_to_create in edges_to_create: @@ -130,7 +144,7 @@ def rewrite(state, lhs_m: UUID, rhs_m: UUID, pattern_mm: UUID, name_mapping: dic tgt = bottom.read_edge_target(rhs_el_to_create) tgt_name = od.get_object_name(bottom, rhs_m, tgt) obj_name = name_mapping[src_name] # name of object in host graph to create slot for - attr_name = od.get_object_name(bottom, mm, original_type) + attr_name = od.get_object_name(bottom, host_mm, original_type) m_od.create_link(model_el_name_to_create, attr_name, obj_name, name_mapping[tgt_name]) @@ -146,7 +160,7 @@ def rewrite(state, lhs_m: UUID, rhs_m: UUID, pattern_mm: UUID, name_mapping: dic # nothing to do pass elif od.is_typed_by(bottom, host_type, assoc_type): - print(' -> is association') + # print(' -> is association') # nothing to do pass elif od.is_typed_by(bottom, host_type, attr_link_type): @@ -154,12 +168,15 @@ def rewrite(state, lhs_m: UUID, rhs_m: UUID, pattern_mm: UUID, name_mapping: dic # nothing to do pass elif od.is_typed_by(bottom, host_type, modelref_type): - print(' -> is modelref') - old_value, _ = od.read_primitive_value(bottom, host_el, mm) + # print(' -> is modelref') + old_value, _ = od.read_primitive_value(bottom, host_el, host_mm) rhs_el, = bottom.read_outgoing_elements(rhs_m, pattern_el_name) python_expr, _ = od.read_primitive_value(bottom, rhs_el, pattern_mm) result = exec_then_eval(python_expr, - _globals=bind_api(odapi), + _globals={ + **bind_api(odapi), + 'matched': matched_callback, + }, _locals={'this': host_el}) # print('eval result=', result) if isinstance(result, int): @@ -172,3 +189,11 @@ def rewrite(state, lhs_m: UUID, rhs_m: UUID, pattern_mm: UUID, name_mapping: dic msg = f"Don't know what to do with element '{pattern_el_name}'->'{host_el_name}' of type ({host_type})" # print(msg) raise Exception(msg) + + rhs_odapi = ODAPI(state, rhs_m, pattern_mm) + for cond_name, cond in rhs_odapi.get_all_instances("GlobalCondition"): + python_code = rhs_odapi.get_slot_value(cond, "condition") + simply_exec(python_code, _globals={ + **bind_api(odapi), + 'matched': matched_callback, + }) diff --git a/util/eval.py b/util/eval.py index e022929..611e399 100644 --- a/util/eval.py +++ b/util/eval.py @@ -6,8 +6,16 @@ def exec_then_eval(code, _globals={}, _locals={}): # assumes last node is an expression last = ast.Expression(block.body.pop().value) extended_globals = { - '__builtins__': {'isinstance': isinstance, 'print': print, 'int': int, 'float': float, 'bool': bool, 'str': str, 'tuple': tuple, 'len': len, 'set': set, 'dict': dict }, + '__builtins__': {'isinstance': isinstance, 'print': print, 'int': int, 'float': float, 'bool': bool, 'str': str, 'tuple': tuple, 'len': len, 'set': set, 'dict': dict, 'eval': eval }, **_globals, } exec(compile(block, '', mode='exec'), extended_globals, _locals) return eval(compile(last, '', mode='eval'), extended_globals, _locals) + +def simply_exec(code, _globals={}, _locals={}): + block = ast.parse(code, mode='exec') + extended_globals = { + '__builtins__': {'isinstance': isinstance, 'print': print, 'int': int, 'float': float, 'bool': bool, 'str': str, 'tuple': tuple, 'len': len, 'set': set, 'dict': dict, 'eval': eval }, + **_globals, + } + exec(compile(block, '', mode='exec'), extended_globals, _locals)