From 457aac48b3bb01ef3d15c652f5a4575f53c0d6ad Mon Sep 17 00:00:00 2001 From: Joeri Exelmans Date: Wed, 23 Jul 2025 15:15:17 +0200 Subject: [PATCH] fix --- tutorial/04_transformation.py | 2 +- tutorial/05_advanced_transformation.py | 43 +++++++++++++++++--------- 2 files changed, 30 insertions(+), 15 deletions(-) diff --git a/tutorial/04_transformation.py b/tutorial/04_transformation.py index b143622..2a50af4 100644 --- a/tutorial/04_transformation.py +++ b/tutorial/04_transformation.py @@ -139,7 +139,7 @@ from transformation import rewriter m_rewritten = clone_od(state, m, mm) # copy our model before rewriting (this is optional - we do this so we can later render the model before and after rewrite in a single PlantUML diagram) lhs_match = all_matches[0] # select one match -rhs_match = rewriter.rewrite(state, lhs, rhs, ramified_mm, lhs_match, m_rewritten, mm) +rhs_match = rewriter.rewrite(state, rhs, ramified_mm, lhs_match, m_rewritten, mm) # Let's render everything as PlantUML: diff --git a/tutorial/05_advanced_transformation.py b/tutorial/05_advanced_transformation.py index 194a381..f420b0e 100644 --- a/tutorial/05_advanced_transformation.py +++ b/tutorial/05_advanced_transformation.py @@ -1,3 +1,5 @@ +# In this tutorial, we implement the semantics of Petri Nets by means of model transformation. +# Compared to the previous tutorial, it only introduces one more feature: pivots. # Consider the following Petri Net language meta-model: mm_cs = """ @@ -74,12 +76,14 @@ mm_ramified = ramify(state, mm) # We will now implement Petri Net operational semantics by means of model transformation. -# Look for any transition +# 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: +# But, if that transition has an incoming arc (P2T) from a place with not enough tokens, the transition cannot fire. We can express this as a pattern: + lhs_transition_disabled_cs = """ t:RAM_Transition p:RAM_Place @@ -93,30 +97,37 @@ lhs_transition_disabled_cs = """ } """ +# Parse these patterns: 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: +# To find enabled transitions, we first match our first pattern (looking for a transition), and then we try to 'grow' that match with our second, "Negative Application Condition" (NAC) pattern. If growing the match with the second pattern is possible, we abort and look for another transition. +# To grow a match, we use the 'pivot'-argument of the match-function. A pivot is a partial match that needs to be grown. +# This results in the following generator function: 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): + for match_nac in match_od(state, m, mm, lhs_transition_disabled, mm_ramified, pivot=match): # <-- notice the pivot :) # transition is disabled break # find next transition else: - # transition is enabled + # we've found an enabled transition: yield match +# Let's see if it works: enabled = list(find_enabled_transitions(m)) print("enabled PN transitions:", enabled) -# To fire a transition, decrement the number of tokens of every incoming place: +# Next, to fire a transition: +# - we decrement the number of tokens of every incoming place +# - we increment the number of tokens of every outgoing place +# We do this also by growing our match: given an enabled transition (already matched), we match for *any* incoming place, and rewrite that place to reduce its tokens. Next, we look for *any* outgoing place, and increment its tokens. +# Decrement incoming lhs_incoming_cs = """ - t:RAM_Transition + t:RAM_Transition # <-- we already know this transition is enabled 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 } @@ -134,8 +145,7 @@ rhs_incoming_cs = """ inarc:RAM_P2T (inplace -> t) """ -# And increment for every outgoing place: - +# Increment outgoing lhs_outgoing_cs = """ t:RAM_Transition outplace:RAM_Place { @@ -155,17 +165,18 @@ rhs_outgoing_cs = """ outarc:RAM_T2P (t -> outplace) """ +# Parse all the patterns 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") +# Firing is really simple: 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) + rewriter.rewrite(state, 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) + rewriter.rewrite(state, rhs_outgoing, mm_ramified, match_outgoing, m, mm) def show_petri_net(m): odapi = ODAPI(state, m, mm) @@ -192,7 +203,11 @@ def show_petri_net(m): while len(enabled) > 0: print(show_petri_net(m)) print("\nenabled PN transitions:", enabled) - print("press ENTER to fire", enabled[0]['t']) + to_fire = enabled[0]['t'] + print("press ENTER to fire", to_fire) input() + print("firing transition:", to_fire) fire_transition(m, enabled[0]) enabled = list(find_enabled_transitions(m)) + +# That's it!