diff --git a/README.md b/README.md index daffc34..1171f46 100644 --- a/README.md +++ b/README.md @@ -30,7 +30,3 @@ The following branches exist: * `master` - currently equivalent to `mde2425` (this is the branch that was cloned by the students). This branch will be deleted after Sep 2025, because the name is too vague. * `development` - in this branch, new development will occur, primarily cleaning up the code to prepare for next year's MDE classes. - -## Tutorial - -A good place to learn how to use muMLE is the `tutorial` directory. Each file is an executable Python script that explains muMLE step-by-step (read the comments). diff --git a/tutorial/04_transformation.py b/tutorial/04_transformation.py index b143622..9343969 100644 --- a/tutorial/04_transformation.py +++ b/tutorial/04_transformation.py @@ -9,7 +9,6 @@ from concrete_syntax.textual_od.renderer import render_od from concrete_syntax.common import indent from concrete_syntax.plantuml import renderer as plantuml from concrete_syntax.plantuml.make_url import make_url as make_plantuml_url -from framework.conformance import Conformance, render_conformance_check_result mm_cs = """ Bear:Class @@ -59,12 +58,6 @@ ramified_mm = ramify(state, mm) print("RAMified meta-model:") print(indent(render_od(state, ramified_mm, mmm), 2)) -# Note that our RAMified meta-model is also a valid class diagram: - -print() -print("Is valid class diagram?") -print(render_conformance_check_result(Conformance(state, ramified_mm, mmm).check_nominal())) - # We now specify our patterns. # We create a rule that looks for a Man with weight > 60, who is afraid of an animal: diff --git a/tutorial/05_advanced_transformation.py b/tutorial/05_advanced_transformation.py deleted file mode 100644 index 02d9d30..0000000 --- a/tutorial/05_advanced_transformation.py +++ /dev/null @@ -1,176 +0,0 @@ -# Consider the following Petri Net language meta-model: - -mm_cs = """ - Place:Class - Transition:Class - - Place_tokens:AttributeLink (Place -> Integer) { - optional = False; - name = "tokens"; - constraint = `get_value(get_target(this)) >= 0`; - } - - P2T:Association (Place -> Transition) - T2P:Association (Transition -> Place) - - P2T_weight:AttributeLink (P2T -> Integer) { - optional = False; - name = "weight"; - constraint = `get_value(get_target(this)) >= 0`; - } - - T2P_weight:AttributeLink (T2P -> Integer) { - optional = False; - name = "weight"; - constraint = `get_value(get_target(this)) >= 0`; - } -""" - -# We now create the following Petri Net: -# https://upload.wikimedia.org/wikipedia/commons/4/4d/Two-boundedness-cb.png - -m_cs = """ - p1:Place { tokens = 0; } - p2:Place { tokens = 0; } - cp1:Place { tokens = 2; } - cp2:Place { tokens = 2; } - - t1:Transition - t2:Transition - t3:Transition - - :T2P (t1 -> p1) { weight = 1; } - :P2T (p1 -> t2) { weight = 1; } - :T2P (t2 -> cp1) { weight = 1; } - :P2T (cp1 -> t1) { weight = 1; } - - :T2P (t2 -> p2) { weight = 1; } - :P2T (p2 -> t3) { weight = 1; } - :T2P (t3 -> cp2) { weight = 1; } - :P2T (cp2 -> t2) { weight = 1; } -""" - -# The usual... - -from state.devstate import DevState -from bootstrap.scd import bootstrap_scd -from util import loader -from transformation.ramify import ramify -from transformation.matcher import match_od -from transformation.cloner import clone_od -from transformation import rewriter -from concrete_syntax.textual_od.renderer import render_od -from concrete_syntax.common import indent - -state = DevState() -mmm = bootstrap_scd(state) -mm = loader.parse_and_check(state, mm_cs, mmm, "mm") -m = loader.parse_and_check(state, m_cs, mm, "m") - -mm_ramified = ramify(state, mm) - - -# We will now implement Petri Net operational semantics by means of model transformation. - - -# Look for any transition -lhs_transition_cs = """ - t:RAM_Transition -""" - -# A transition is disabled if it has an incoming arc (P2T) from a place with 0 tokens: -lhs_transition_disabled_cs = """ - t:RAM_Transition - p:RAM_Place - :RAM_P2T (p -> t) { - condition = ``` - place = get_source(this) - tokens = get_slot_value(place, "tokens") - weight = get_slot_value(this, "weight") - tokens < weight # True means: cannot fire - ```; - } -""" - -lhs_transition = loader.parse_and_check(state, lhs_transition_cs, mm_ramified, "lhs_transition") -lhs_transition_disabled = loader.parse_and_check(state, lhs_transition_disabled_cs, mm_ramified, "lhs_transition_disabled") - -# We write a generator function, that yields all enabled transitions. -# Notice that we nest two calls to 'match_od', and the result of the first call is passed as a pivot to the second: - -def find_enabled_transitions(m): - for match in match_od(state, m, mm, lhs_transition, mm_ramified): - for match_nac in match_od(state, m, mm, lhs_transition_disabled, mm_ramified, pivot=match): - # transition is disabled - break # find next transition - else: - # transition is enabled - yield match - - -enabled = list(find_enabled_transitions(m)) -print("enabled PN transitions:", enabled) - - -# To fire a transition, decrement the number of tokens of every incoming place: - -lhs_incoming_cs = """ - t:RAM_Transition - inplace:RAM_Place { - RAM_tokens = `True`; # this needs to be here, otherwise, the rewriter will try to create a new attribute rather than update the existing one - } - inarc:RAM_P2T (inplace -> t) -""" -rhs_incoming_cs = """ - t:RAM_Transition - inplace:RAM_Place { - RAM_tokens = ``` - weight = get_slot_value(matched("inarc"), "weight") - print("adding", weight, "tokens to", get_name(this)) - get_value(this) - weight - ```; - } - inarc:RAM_P2T (inplace -> t) -""" - -# And increment for every outgoing place: - -lhs_outgoing_cs = """ - t:RAM_Transition - outplace:RAM_Place { - RAM_tokens = `True`; # this needs to be here, otherwise, the rewriter will try to create a new attribute rather than update the existing one - } - outarc:RAM_T2P (t -> outplace) -""" -rhs_outgoing_cs = """ - t:RAM_Transition - outplace:RAM_Place { - RAM_tokens = ``` - weight = get_slot_value(matched("outarc"), "weight") - print("removing", weight, "tokens from", get_name(this)) - get_value(this) + weight - ```; - } - outarc:RAM_T2P (t -> outplace) -""" - -lhs_incoming = loader.parse_and_check(state, lhs_incoming_cs, mm_ramified, "lhs_incoming") -rhs_incoming = loader.parse_and_check(state, rhs_incoming_cs, mm_ramified, "rhs_incoming") -lhs_outgoing = loader.parse_and_check(state, lhs_outgoing_cs, mm_ramified, "lhs_outgoing") -rhs_outgoing = loader.parse_and_check(state, rhs_outgoing_cs, mm_ramified, "rhs_outgoing") - -def fire_transition(m, transition_match): - print("firing transition:", transition_match['t']) - for match_incoming in match_od(state, m, mm, lhs_incoming, mm_ramified, pivot=transition_match): - rewriter.rewrite(state, lhs_incoming, rhs_incoming, mm_ramified, match_incoming, m, mm) - for match_outgoing in match_od(state, m, mm, lhs_outgoing, mm_ramified, pivot=transition_match): - rewriter.rewrite(state, lhs_outgoing, rhs_outgoing, mm_ramified, match_outgoing, m, mm) - - -# Let's see if it works: -while len(enabled) > 0: - print("press ENTER to fire", enabled[0]['t']) - input() - fire_transition(m, enabled[0]) - enabled = list(find_enabled_transitions(m)) - print("\nenabled PN transitions:", enabled)