(WIP) implementing CBD language... Meta-meta-model: Association inherits from Class. Matcher accepts pivot. Add generic graphviz renderer.
This commit is contained in:
parent
a26ceef10f
commit
1eb8a84553
25 changed files with 542 additions and 170 deletions
|
|
@ -1,7 +1,9 @@
|
|||
# This module loads all the models (including the transformation rules) and performs a conformance-check on them.
|
||||
|
||||
import os
|
||||
from framework.conformance import Conformance, render_conformance_check_result
|
||||
from concrete_syntax.textual_od import parser
|
||||
|
||||
from transformation.ramify import ramify
|
||||
|
||||
# get file contents as string
|
||||
def read_file(filename):
|
||||
|
|
@ -9,15 +11,6 @@ def read_file(filename):
|
|||
with open(dir+'/'+filename) as file:
|
||||
return file.read()
|
||||
|
||||
# def parse_and_check(state, cs_file, mm):
|
||||
# m_cs = read_file(cs_file)
|
||||
# try:
|
||||
# _parse_and_check(state, m_cs, mm)
|
||||
# except Exception as e:
|
||||
# e.add_note(f"While parsing '{cs_file}'")
|
||||
# raise
|
||||
# return m
|
||||
|
||||
def parse_and_check(state, m_cs, mm, descr: str):
|
||||
try:
|
||||
m = parser.parse_od(
|
||||
|
|
@ -25,12 +18,16 @@ def parse_and_check(state, m_cs, mm, descr: str):
|
|||
m_text=m_cs,
|
||||
mm=mm,
|
||||
)
|
||||
except Exception as e:
|
||||
e.add_note("While parsing model " + descr)
|
||||
raise
|
||||
try:
|
||||
conf = Conformance(state, m, mm)
|
||||
errors = conf.check_nominal()
|
||||
if len(errors) > 0:
|
||||
raise Exception(render_conformance_check_result(errors))
|
||||
print(render_conformance_check_result(errors))
|
||||
except Exception as e:
|
||||
e.add_note("While parsing model " + descr)
|
||||
e.add_note("In model " + descr)
|
||||
raise
|
||||
return m
|
||||
|
||||
|
|
@ -53,3 +50,22 @@ def get_fibonacci(state, scd_mmm):
|
|||
m_rt_initial = parse_and_check(state, m_rt_initial_cs, mm_rt, "Fibonacci initial state")
|
||||
|
||||
return (mm, mm_rt, m, m_rt_initial)
|
||||
|
||||
RULE_NAMES = ["delay"]
|
||||
KINDS = ["nac", "lhs", "rhs"]
|
||||
|
||||
def get_rules(state, rt_mm):
|
||||
rt_mm_ramified = ramify(state, rt_mm)
|
||||
|
||||
rules = {} # e.g., { "delay": {"nac": <UUID>, "lhs": <UUID>, ...}, ...}
|
||||
|
||||
for rule_name in RULE_NAMES:
|
||||
rule = {}
|
||||
for kind in KINDS:
|
||||
filename = f"models/r_{rule_name}_{kind}.od";
|
||||
cs = read_file(filename)
|
||||
rule_m = parse_and_check(state, cs, rt_mm_ramified, descr=f"'{filename}'")
|
||||
rule[kind] = rule_m
|
||||
rules[rule_name] = rule
|
||||
|
||||
return (rt_mm_ramified, rules)
|
||||
|
|
@ -1,34 +1,34 @@
|
|||
# Adder, two inputs, one output
|
||||
adder:Function {
|
||||
func = ```
|
||||
n2_out = in0 + in1
|
||||
n2_out = n0_in + n1_in
|
||||
```;
|
||||
}
|
||||
n0_in:IntInPort
|
||||
n1_in:IntInPort
|
||||
n2_out:IntOutPort
|
||||
n0_in:InPort
|
||||
n1_in:InPort
|
||||
n2_out:OutPort
|
||||
:hasInPort (adder -> n0_in)
|
||||
:hasInPort (adder -> n1_in)
|
||||
:hasOutPort (adder -> n2_out)
|
||||
|
||||
|
||||
|
||||
# Delay block 0
|
||||
d0:Delay
|
||||
d0_in:IntInPort
|
||||
d0_out:IntOutPort
|
||||
d0_in:InPort
|
||||
d0_out:OutPort
|
||||
:hasInPort (d0 -> d0_in)
|
||||
:hasOutPort (d0 -> d0_out)
|
||||
|
||||
|
||||
|
||||
# Delay block 1
|
||||
d1:Delay
|
||||
d1_in:IntInPort
|
||||
d1_out:IntOutPort
|
||||
d1_in:InPort
|
||||
d1_out:OutPort
|
||||
:hasInPort (d1 -> d1_in)
|
||||
:hasOutPort (d1 -> d1_out)
|
||||
|
||||
|
||||
|
||||
:intLink (n2_out -> d1_in)
|
||||
:intLink (d1_out -> n1_in)
|
||||
:intLink (d1_out -> d0_in)
|
||||
:intLink (d1_out -> n0_in)
|
||||
# Connections
|
||||
conn0:link (n2_out -> d1_in) # n2 becomes n1 in next step
|
||||
conn1:link (d1_out -> d0_in) # n1 becomes n0 in next step
|
||||
conn2:link (d1_out -> n1_in) # n1 input to adder
|
||||
conn3:link (d0_out -> n0_in) # n0 input to adder
|
||||
|
|
|
|||
|
|
@ -1,7 +1,8 @@
|
|||
d0s:IntState {
|
||||
# Initial state for both delay blocks:
|
||||
d0s:State {
|
||||
state = 0;
|
||||
}
|
||||
d1s:IntState {
|
||||
d1s:State {
|
||||
state = 1;
|
||||
}
|
||||
:delay2State (d0 -> d0s)
|
||||
|
|
|
|||
|
|
@ -3,10 +3,10 @@ Block:Class {
|
|||
}
|
||||
|
||||
InPort:Class {
|
||||
abstract = True;
|
||||
# abstract = True;
|
||||
}
|
||||
OutPort:Class {
|
||||
abstract = True;
|
||||
# abstract = True;
|
||||
}
|
||||
|
||||
hasInPort:Association (Block -> InPort) {
|
||||
|
|
@ -77,8 +77,8 @@ Delay:Class {
|
|||
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})")
|
||||
# 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
|
||||
```;
|
||||
}
|
||||
|
|
@ -90,40 +90,40 @@ Delay:Class {
|
|||
# Object Diagrams are statically typed, so we must create in/out-ports, and MemorySlots for all primitive types:
|
||||
|
||||
|
||||
# Port types
|
||||
# # Port types
|
||||
|
||||
BoolInPort:Class
|
||||
IntInPort:Class
|
||||
StrInPort:Class
|
||||
# BoolInPort:Class
|
||||
# IntInPort:Class
|
||||
# StrInPort:Class
|
||||
|
||||
BoolOutPort:Class
|
||||
IntOutPort:Class
|
||||
StrOutPort:Class
|
||||
# BoolOutPort:Class
|
||||
# IntOutPort:Class
|
||||
# StrOutPort:Class
|
||||
|
||||
:Inheritance (BoolInPort -> InPort)
|
||||
:Inheritance (IntInPort -> InPort)
|
||||
:Inheritance (StrInPort -> InPort)
|
||||
# :Inheritance (BoolInPort -> InPort)
|
||||
# :Inheritance (IntInPort -> InPort)
|
||||
# :Inheritance (StrInPort -> InPort)
|
||||
|
||||
:Inheritance (BoolOutPort -> OutPort)
|
||||
:Inheritance (IntOutPort -> OutPort)
|
||||
:Inheritance (StrOutPort -> OutPort)
|
||||
# :Inheritance (BoolOutPort -> OutPort)
|
||||
# :Inheritance (IntOutPort -> OutPort)
|
||||
# :Inheritance (StrOutPort -> OutPort)
|
||||
|
||||
# Link types
|
||||
# # Link types
|
||||
|
||||
boolLink:Association (BoolOutPort -> BoolInPort)
|
||||
intLink:Association (IntOutPort -> IntInPort)
|
||||
strLink:Association (StrOutPort -> StrInPort)
|
||||
# boolLink:Association (BoolOutPort -> BoolInPort)
|
||||
# intLink:Association (IntOutPort -> IntInPort)
|
||||
# strLink:Association (StrOutPort -> StrInPort)
|
||||
|
||||
:Inheritance (boolLink -> link)
|
||||
:Inheritance (intLink -> link)
|
||||
:Inheritance (strLink -> link)
|
||||
# :Inheritance (boolLink -> link)
|
||||
# :Inheritance (intLink -> link)
|
||||
# :Inheritance (strLink -> link)
|
||||
|
||||
# Delay block types
|
||||
# # Delay block types
|
||||
|
||||
BoolDelay:Class
|
||||
IntDelay:Class
|
||||
StrDelay:Class
|
||||
# BoolDelay:Class
|
||||
# IntDelay:Class
|
||||
# StrDelay:Class
|
||||
|
||||
:Inheritance (BoolDelay -> Delay)
|
||||
:Inheritance (IntDelay -> Delay)
|
||||
:Inheritance (StrDelay -> Delay)
|
||||
# :Inheritance (BoolDelay -> Delay)
|
||||
# :Inheritance (IntDelay -> Delay)
|
||||
# :Inheritance (StrDelay -> Delay)
|
||||
|
|
|
|||
|
|
@ -1,28 +1,58 @@
|
|||
# Link state ("signal")
|
||||
# is optional: absent for yet-to-compute signals
|
||||
|
||||
intLink_signal:AttributeLink (intLink -> Integer) {
|
||||
name = "signal";
|
||||
optional = True;
|
||||
Signal:Class {
|
||||
# abstract = True;
|
||||
}
|
||||
boolLink_signal:AttributeLink (boolLink -> Boolean) {
|
||||
|
||||
Signal_signal:AttributeLink (Signal -> Integer) {
|
||||
name = "signal";
|
||||
optional = True;
|
||||
optional = False;
|
||||
}
|
||||
strLink_signal:AttributeLink (strLink -> String) {
|
||||
name = "signal";
|
||||
optional = True;
|
||||
|
||||
hasSignal:Association (link -> 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;
|
||||
# abstract = True;
|
||||
}
|
||||
|
||||
State_state:AttributeLink (State -> Integer) {
|
||||
name = "state";
|
||||
optional = False;
|
||||
}
|
||||
|
||||
|
||||
delay2State:Association (Delay -> State) {
|
||||
source_lower_cardinality = 1;
|
||||
source_upper_cardinality = 1;
|
||||
|
|
@ -30,26 +60,26 @@ delay2State:Association (Delay -> State) {
|
|||
target_upper_cardinality = 1;
|
||||
}
|
||||
|
||||
BoolState:Class
|
||||
IntState:Class
|
||||
StrState:Class
|
||||
# BoolState:Class
|
||||
# IntState:Class
|
||||
# StrState:Class
|
||||
|
||||
:Inheritance (BoolState -> State)
|
||||
:Inheritance (IntState -> State)
|
||||
:Inheritance (StrState -> State)
|
||||
# :Inheritance (BoolState -> State)
|
||||
# :Inheritance (IntState -> State)
|
||||
# :Inheritance (StrState -> State)
|
||||
|
||||
|
||||
BoolState_state:AttributeLink (BoolState -> Boolean) {
|
||||
name = "state";
|
||||
optional = False;
|
||||
}
|
||||
# BoolState_state:AttributeLink (BoolState -> Boolean) {
|
||||
# name = "state";
|
||||
# optional = False;
|
||||
# }
|
||||
|
||||
IntState_state:AttributeLink (IntState -> Integer) {
|
||||
name = "state";
|
||||
optional = False;
|
||||
}
|
||||
# IntState_state:AttributeLink (IntState -> Integer) {
|
||||
# name = "state";
|
||||
# optional = False;
|
||||
# }
|
||||
|
||||
StrState_state:AttributeLink (StrState -> String) {
|
||||
name = "state";
|
||||
optional = False;
|
||||
}
|
||||
# StrState_state:AttributeLink (StrState -> String) {
|
||||
# name = "state";
|
||||
# optional = False;
|
||||
# }
|
||||
|
|
|
|||
16
examples/cbd/models/r_delay_lhs.od
Normal file
16
examples/cbd/models/r_delay_lhs.od
Normal file
|
|
@ -0,0 +1,16 @@
|
|||
# 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)
|
||||
14
examples/cbd/models/r_delay_nac.od
Normal file
14
examples/cbd/models/r_delay_nac.od
Normal file
|
|
@ -0,0 +1,14 @@
|
|||
# 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)
|
||||
23
examples/cbd/models/r_delay_rhs.od
Normal file
23
examples/cbd/models/r_delay_rhs.od
Normal file
|
|
@ -0,0 +1,23 @@
|
|||
# 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)
|
||||
|
|
@ -1,8 +1,97 @@
|
|||
from state.devstate import DevState
|
||||
from bootstrap.scd import bootstrap_scd
|
||||
|
||||
from concrete_syntax.common import indent
|
||||
from concrete_syntax.textual_od import renderer as od_renderer
|
||||
from concrete_syntax.plantuml import renderer as plantuml
|
||||
from concrete_syntax.plantuml.make_url import make_url as make_plantuml_url
|
||||
from concrete_syntax.graphviz.make_url import make_url as make_graphviz_url
|
||||
from concrete_syntax.graphviz import renderer as graphviz
|
||||
|
||||
from transformation.matcher.mvs_adapter import match_od
|
||||
from transformation.rewriter import rewrite
|
||||
from transformation.cloner import clone_od
|
||||
|
||||
import models
|
||||
|
||||
state = DevState()
|
||||
scd_mmm = bootstrap_scd(state)
|
||||
|
||||
mm, mm_rt, m, m_rt_initial = models.get_fibonacci(state, scd_mmm)
|
||||
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)))
|
||||
|
||||
|
||||
# print("RAMIFIED RT-MM")
|
||||
# print(make_plantuml_url(plantuml.render_class_diagram(state, mm_rt_ram)))
|
||||
|
||||
m_rt = m_rt_initial
|
||||
|
||||
def get_matches():
|
||||
for rule_name, rule in rules.items():
|
||||
lhs = rule["lhs"]
|
||||
|
||||
lhs_matcher = match_od(state,
|
||||
host_m=m_rt,
|
||||
host_mm=mm_rt,
|
||||
pattern_m=lhs,
|
||||
pattern_mm=mm_rt_ram)
|
||||
|
||||
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)
|
||||
|
||||
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)
|
||||
|
||||
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))
|
||||
|
||||
|
||||
matches = list(get_matches())
|
||||
print(f"There are {len(matches)} matches.")
|
||||
if len(matches) == 0:
|
||||
break
|
||||
rule_name, lhs, rhs, lhs_match = matches[0]
|
||||
|
||||
|
||||
# txt = graphviz.render_package("Host", graphviz.render_object_diagram(state, m_rt, mm_rt))
|
||||
# txt += graphviz.render_package("LHS", graphviz.render_object_diagram(state, lhs, mm_rt_ram))
|
||||
# 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')
|
||||
|
||||
# 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)
|
||||
|
||||
# import subprocess
|
||||
# subprocess.run(["firefox", "--new-window", *match_urls])
|
||||
|
||||
# get_actions(state, rules, m_rt_initial, mm_rt)
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
import urllib
|
||||
from concrete_syntax.common import indent
|
||||
from concrete_syntax.graphviz.make_url import make_url
|
||||
from examples.semantics.operational.port.helpers import design_to_state, state_to_design, get_time, get_num_ships
|
||||
|
||||
def render_port_graphviz(od):
|
||||
|
|
@ -53,9 +53,7 @@ def render_port_graphviz(od):
|
|||
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)
|
||||
return make_url(txt)
|
||||
|
||||
def render_port_textual(od):
|
||||
txt = ""
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue