From 6571d8556c37de4a210f1e2decbccc0b9debe8d3 Mon Sep 17 00:00:00 2001 From: Joeri Exelmans Date: Tue, 3 Dec 2024 23:25:10 +0100 Subject: [PATCH] petri net formalism: add inhibitor arc --- examples/petrinet/metamodels/mm_design.od | 3 +++ .../r_fire_transition_nac2.od | 13 ++++++++++++ examples/petrinet/renderer.py | 2 +- .../translational/{rules => }/.gitignore | 4 +++- examples/semantics/translational/merged_mm.od | 21 ++++++++++--------- transformation/rewriter.py | 3 ++- 6 files changed, 33 insertions(+), 13 deletions(-) create mode 100644 examples/petrinet/operational_semantics/r_fire_transition_nac2.od rename examples/semantics/translational/{rules => }/.gitignore (68%) diff --git a/examples/petrinet/metamodels/mm_design.od b/examples/petrinet/metamodels/mm_design.od index a5889b3..44a6aa1 100644 --- a/examples/petrinet/metamodels/mm_design.od +++ b/examples/petrinet/metamodels/mm_design.od @@ -7,5 +7,8 @@ arc:Association (PNConnectable -> PNConnectable) PNPlace:Class PNTransition:Class +# inhibitor arc +inh_arc:Association (PNPlace -> PNTransition) + :Inheritance (PNPlace -> PNConnectable) :Inheritance (PNTransition -> PNConnectable) \ No newline at end of file diff --git a/examples/petrinet/operational_semantics/r_fire_transition_nac2.od b/examples/petrinet/operational_semantics/r_fire_transition_nac2.od new file mode 100644 index 0000000..b6a685b --- /dev/null +++ b/examples/petrinet/operational_semantics/r_fire_transition_nac2.od @@ -0,0 +1,13 @@ +# A place with tokens: + +p:RAM_PNPlace +ps:RAM_PNPlaceState { + RAM_numTokens = `get_value(this) > 0`; +} +:RAM_pn_of (ps -> p) + +# An incoming inhibitor arc from that place to our transition: + +t:RAM_PNTransition + +:RAM_inh_arc (p -> t) diff --git a/examples/petrinet/renderer.py b/examples/petrinet/renderer.py index 9f2e93f..a4ba336 100644 --- a/examples/petrinet/renderer.py +++ b/examples/petrinet/renderer.py @@ -42,5 +42,5 @@ def render_petri_net(od: ODAPI): src_name = od.get_name(od.get_source(arc)) tgt_name = od.get_name(od.get_target(arc)) dot += f"{src_name} -> {tgt_name};" - show_graphviz(dot, engine="dot") + show_graphviz(dot, engine="neato") return "" diff --git a/examples/semantics/translational/rules/.gitignore b/examples/semantics/translational/.gitignore similarity index 68% rename from examples/semantics/translational/rules/.gitignore rename to examples/semantics/translational/.gitignore index d5877da..dfcb5e1 100644 --- a/examples/semantics/translational/rules/.gitignore +++ b/examples/semantics/translational/.gitignore @@ -1,2 +1,4 @@ # Let's not accidently add the solution to assignment 5... -r_*.od \ No newline at end of file +r_*.od + +snapshot_after_*.od \ No newline at end of file diff --git a/examples/semantics/translational/merged_mm.od b/examples/semantics/translational/merged_mm.od index 512940e..7ebee4a 100644 --- a/examples/semantics/translational/merged_mm.od +++ b/examples/semantics/translational/merged_mm.od @@ -3,7 +3,7 @@ # Merged run-time meta-models of 'Petri Net' and 'Port' formalisms. # An abstract 'Top'-class (superclass of everything else), and a 'generic_link'-association (which can connect everything with everything) have also been added. -# PlantUML visualization: https://deemz.org/plantuml/pdf/hPTDZzem48Rl-HKMnqgWa0sKeAg7tKFL2ui4KezeuXWs8jYHOofLxVxtZiE7s5KatY3dm8bvF3Flp7WSoOgQHWnUg2PPkZylHZVEKgcT60XgH7p-DXq__alZMIh-Ha8qRsLzWOYv-AcTsYaRlKVd0vQBPKLIhHmv1QFp5gsFXxNPAzrqSNyPkrTsfM1_i-G2FPbsKdkvcMLCV8yezvcJJjmojiSAnL3SZJ57As5VygA5N5IjZDoByMWq1iqBQfFZoeFgIikpikwjJsx6SN6g3hOv-aold2trhYFCjQbHPaAtCRPbXPgcNszDhxNJAwHKtJBQbA2caycjwG-bbILdB6mkFmI-M5lIJUbAer72zAcpnfOBxdkjfAEyWlCmfUvwBVKUHSm-o77sWSFffGUT1j31_5O5LzYpCPKY_Qb0-X6lSsV5KwrpG9p76KhCapRGwEu__HJuzcyulCzCPtGVvti5m_4S3ubZQKFYqcqCuBYxGUycav1Iy9q2u7WqWzwbGExyhGFYA0zQA5aM59SNGN55sAuWeExmGe6KxT5aKo3O7eMIAi2x6TnaKB0yQq5SZ1JA5C_TKzWc2pe-UVKDEb4cCcWP8-EpXnHvWjoChCLWB4OZmSliSFYThzu1jbNFXTbY_dfaYuxzELy0lhUQ2x98VldbSJrW31_0E-DSIDAljLyMWGxrPV508DpNVCvr1GFEuUTPVq7yAZGNjTv0cYGFQP9uJNP-koxbfk9z5DaTr2CdjUAKpKaR_x01ifO-KWLfgyxvVVsw_Gy= +# PlantUML visualization: https://deemz.org/plantuml/pdf/hPTFYzim4CNl_XGYnqA27P8uDgM7tSEobsmWWHw3RCk9Y2CPMIcKThzxHyuViiMGPwCSzhJpqxoPfz4uo2lUD6pqockUI_lxLQl66YwLPIF66nPUVxkEF-ut2uk8_GaOQmwola5OojwL5NjXWi_WUi1wjQvuBZQMMm6ZborQdKzRVHIgwUB-rEOep4RW-POtw2MqazehJR4WucV0CrUvtB97HdckO4pHZT5dawEvH25l8RUkLZe_icWoYS3mQTmMnygJw2hBYp3sqASsqPnVt44nPrVfZJLIxJjaRdMDCkFuKMDhApGqcJs6thtJIrAIFJBQag2XVFeO-YQKCDng0uSdNuIljeQhHbgf5Kh8mawFhLTqxvN8BSygk0vPtErNgOueelZIZciE9ATNFyhB03hfNtI3KlQYTIMu-iyW_OZtkREXgTOv8AxZ32QMhT3WwN-wAV3zxtZyd3ahn7ESkoiOZkQuJnorrYTkFaDmTBl1xFZKPoleJG6oez4CPfS0Ojsh0-BAfLUZY8LNeuJSAsuQ-nLR-3GArDaUOZD0R0-Z91cGNG5VCaWipLeGDqUCak6r2_rUCg_ZarPVhnE59rvjZ8pF7gqeI-XbNB1Hn2OJHiliUFo3djuHjbMdJ2FpcV9ro1OTkdE-0NmNbJ9kSa00VNdS3uZW0sXdJ5dErKVjbaNapI_BGK92EaUgmmuIuxmtu10Q7YJclkSXHLiEwBehGSfgjOCQ7mzgVEmQltShlCnt5Iszo8AI3JcfTO1iBWPmNqz0rQ8XLalQxbm_uZ_AVm== CapacityConstraint:Class @@ -17,8 +17,8 @@ Source:Class { abstract = True; } Clock:Class { - upper_cardinality = 1; lower_cardinality = 1; + upper_cardinality = 1; } BerthState:Class { constraint = ``` @@ -77,14 +77,14 @@ operatingCapacities:GlobalConstraint { ```; } WorkerSet_numWorkers:AttributeLink (WorkerSet -> Integer) { + name = "numWorkers"; constraint = `get_value(get_target(this)) >= 0`; optional = False; - name = "numWorkers"; } PlaceState_numShips:AttributeLink (PlaceState -> Integer) { + constraint = `get_value(get_target(this)) >= 0`; optional = False; name = "numShips"; - constraint = `get_value(get_target(this)) >= 0`; } ConnectionState_moved:AttributeLink (ConnectionState -> Boolean) { name = "moved"; @@ -107,28 +107,28 @@ ConnectionState_moved:AttributeLink (ConnectionState -> Boolean) { optional = False; } BerthState_status:AttributeLink (BerthState -> String) { + optional = False; name = "status"; constraint = ``` ( get_value(get_target(this)) in { "empty", "unserved", "served" } ) ```; - optional = False; } PNPlaceState_numTokens:AttributeLink (PNPlaceState -> Integer) { - optional = False; name = "numTokens"; constraint = `"numTokens cannot be negative" if get_value(get_target(this)) < 0 else None`; + optional = False; } Clock_time:AttributeLink (Clock -> Integer) { + optional = False; name = "time"; constraint = `get_value(get_target(this)) >= 0`; - optional = False; } CapacityConstraint_shipCapacity:AttributeLink (CapacityConstraint -> Integer) { - constraint = `get_value(get_target(this)) >= 0`; optional = False; name = "shipCapacity"; + constraint = `get_value(get_target(this)) >= 0`; } of:Association (State -> Stateful) { target_lower_cardinality = 1; @@ -140,12 +140,13 @@ arc:Association (PNConnectable -> PNConnectable) canOperate:Association (WorkerSet -> Berth) { target_lower_cardinality = 1; } +inh_arc:Association (PNPlace -> PNTransition) connection:Association (Source -> Sink) pn_of:Association (PNPlaceState -> PNPlace) { - target_upper_cardinality = 1; - target_lower_cardinality = 1; source_upper_cardinality = 1; source_lower_cardinality = 1; + target_upper_cardinality = 1; + target_lower_cardinality = 1; } generic_link:Association (Top -> Top) isOperating:Association (WorkerSetState -> Berth) { diff --git a/transformation/rewriter.py b/transformation/rewriter.py index f1e2e71..ba9999f 100644 --- a/transformation/rewriter.py +++ b/transformation/rewriter.py @@ -61,7 +61,8 @@ def rewrite(state, lhs_m: UUID, rhs_m: UUID, pattern_mm: UUID, lhs_match: dict, if "GlobalCondition" not in k and not k.endswith("_condition") and not k.endswith(".condition") and (not k.endswith("_name") or k.endswith("RAM_name")) and (not k.endswith(".name"))) - print('filtered out:', set(k for k in bottom.read_keys(rhs_m) if k.endswith(".name") or k.endswith("_name"))) + # See which keys were ignored by the rewriter: + # print('filtered out:', set(k for k in bottom.read_keys(rhs_m) if k.endswith(".name") or k.endswith("_name"))) common = lhs_keys & rhs_keys to_delete = lhs_keys - common