From 5240c7e21a5a71062b9e1b51005c9120c035c192 Mon Sep 17 00:00:00 2001 From: Joeri Exelmans Date: Thu, 21 Nov 2024 12:10:28 +0100 Subject: [PATCH] Add petrinet language --- .gitignore | 4 +- examples/cbd/fibonacci_runner.py | 3 -- examples/conformance/abstract_assoc.py | 2 - examples/petrinet/metamodels/mm_design.od | 11 ++++ examples/petrinet/metamodels/mm_runtime.od | 16 ++++++ examples/petrinet/models/m_example_simple.od | 10 ++++ .../models/m_example_simple_rt_initial.od | 11 ++++ .../r_fire_transition_lhs.od | 1 + .../r_fire_transition_nac.od | 13 +++++ .../r_fire_transition_rhs.od | 19 +++++++ examples/petrinet/runner.py | 52 +++++++++++++++++++ examples/semantics/operational/simulator.py | 2 +- 12 files changed, 137 insertions(+), 7 deletions(-) create mode 100644 examples/petrinet/metamodels/mm_design.od create mode 100644 examples/petrinet/metamodels/mm_runtime.od create mode 100644 examples/petrinet/models/m_example_simple.od create mode 100644 examples/petrinet/models/m_example_simple_rt_initial.od create mode 100644 examples/petrinet/operational_semantics/r_fire_transition_lhs.od create mode 100644 examples/petrinet/operational_semantics/r_fire_transition_nac.od create mode 100644 examples/petrinet/operational_semantics/r_fire_transition_rhs.od create mode 100644 examples/petrinet/runner.py diff --git a/.gitignore b/.gitignore index c65f2a1..6705455 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,7 @@ -# Never accidently commit solutions to assignments :) +# Never accidentally commit solutions to assignments :) *_solution.py +# Never accidentally commit student submissions +*_submission.py # ---> Python # Byte-compiled / optimized / DLL files diff --git a/examples/cbd/fibonacci_runner.py b/examples/cbd/fibonacci_runner.py index 62f689d..30aee00 100644 --- a/examples/cbd/fibonacci_runner.py +++ b/examples/cbd/fibonacci_runner.py @@ -10,9 +10,6 @@ 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 import match_od -from transformation.rewriter import rewrite -from transformation.cloner import clone_od from transformation.ramify import ramify from transformation.rule import RuleMatcherRewriter, ActionGenerator diff --git a/examples/conformance/abstract_assoc.py b/examples/conformance/abstract_assoc.py index 902e70f..27d4c7c 100644 --- a/examples/conformance/abstract_assoc.py +++ b/examples/conformance/abstract_assoc.py @@ -10,7 +10,6 @@ state = DevState() scd_mmm = bootstrap_scd(state) -# Change this: mm_cs = """ BaseA:Class { abstract = True; @@ -49,7 +48,6 @@ print("Is our meta-model a valid class diagram?") conf = Conformance(state, mm, scd_mmm) print(render_conformance_check_result(conf.check_nominal())) -# Change this: m_cs = """ a0:A b0:B diff --git a/examples/petrinet/metamodels/mm_design.od b/examples/petrinet/metamodels/mm_design.od new file mode 100644 index 0000000..f315e6c --- /dev/null +++ b/examples/petrinet/metamodels/mm_design.od @@ -0,0 +1,11 @@ +# Places, transitions, arcs (and only one kind of arc) + +Connectable:Class { abstract = True; } + +arc:Association (Connectable -> Connectable) + +Place:Class +Transition:Class + +:Inheritance (Place -> Connectable) +:Inheritance (Transition -> Connectable) \ No newline at end of file diff --git a/examples/petrinet/metamodels/mm_runtime.od b/examples/petrinet/metamodels/mm_runtime.od new file mode 100644 index 0000000..731afdb --- /dev/null +++ b/examples/petrinet/metamodels/mm_runtime.od @@ -0,0 +1,16 @@ +# A place has a number of tokens, and that's it. + +PlaceState:Class +PlaceState_numTokens:AttributeLink (PlaceState -> Integer) { + name = "numTokens"; + optional = False; + constraint = `"numTokens cannot be negative" if get_value(get_target(this)) < 0 else None`; +} + +of:Association (PlaceState -> Place) { + # one-to-one + source_lower_cardinality = 1; + source_upper_cardinality = 1; + target_lower_cardinality = 1; + target_upper_cardinality = 1; +} \ No newline at end of file diff --git a/examples/petrinet/models/m_example_simple.od b/examples/petrinet/models/m_example_simple.od new file mode 100644 index 0000000..136242d --- /dev/null +++ b/examples/petrinet/models/m_example_simple.od @@ -0,0 +1,10 @@ +p0:Place +p1:Place + +t0:Transition +:arc (p0 -> t0) +:arc (t0 -> p1) + +t1:Transition +:arc (p1 -> t1) +:arc (t1 -> p0) \ No newline at end of file diff --git a/examples/petrinet/models/m_example_simple_rt_initial.od b/examples/petrinet/models/m_example_simple_rt_initial.od new file mode 100644 index 0000000..6cf3076 --- /dev/null +++ b/examples/petrinet/models/m_example_simple_rt_initial.od @@ -0,0 +1,11 @@ +p0s:PlaceState { + numTokens = 1; +} + +:of (p0s -> p0) + +p1s:PlaceState { + numTokens = 0; +} + +:of (p1s -> p1) diff --git a/examples/petrinet/operational_semantics/r_fire_transition_lhs.od b/examples/petrinet/operational_semantics/r_fire_transition_lhs.od new file mode 100644 index 0000000..bfe4c69 --- /dev/null +++ b/examples/petrinet/operational_semantics/r_fire_transition_lhs.od @@ -0,0 +1 @@ +t:RAM_Transition \ No newline at end of file diff --git a/examples/petrinet/operational_semantics/r_fire_transition_nac.od b/examples/petrinet/operational_semantics/r_fire_transition_nac.od new file mode 100644 index 0000000..d5b0cdb --- /dev/null +++ b/examples/petrinet/operational_semantics/r_fire_transition_nac.od @@ -0,0 +1,13 @@ +# A place with no tokens: + +p:RAM_Place +ps:RAM_PlaceState { + RAM_numTokens = `get_value(this) == 0`; +} +:RAM_of (ps -> p) + +# An incoming arc from that place to our transition: + +t:RAM_Transition + +:RAM_arc (p -> t) diff --git a/examples/petrinet/operational_semantics/r_fire_transition_rhs.od b/examples/petrinet/operational_semantics/r_fire_transition_rhs.od new file mode 100644 index 0000000..bef4b52 --- /dev/null +++ b/examples/petrinet/operational_semantics/r_fire_transition_rhs.od @@ -0,0 +1,19 @@ +t:RAM_Transition { + condition = ``` + # remove 1 token from every place connected with incoming arc + for incoming in get_incoming(this, "arc"): + in_place = get_source(incoming) + in_place_state = get_source(get_incoming(in_place, "of")[0]) + in_num_tokens = get_slot_value(in_place_state, "numTokens") + set_slot_value(in_place_state, "numTokens", in_num_tokens - 1) + print("place", get_name(in_place_state), "now has", in_num_tokens-1, "tokens") + + # add 1 token to every place connected with outgoing arc + for outgoing in get_outgoing(this, "arc"): + out_place = get_target(outgoing) + out_place_state = get_source(get_incoming(out_place, "of")[0]) + out_num_tokens = get_slot_value(out_place_state, "numTokens") + set_slot_value(out_place_state, "numTokens", out_num_tokens + 1) + print("place", get_name(out_place_state), "now has", out_num_tokens+1, "tokens") + ```; +} diff --git a/examples/petrinet/runner.py b/examples/petrinet/runner.py new file mode 100644 index 0000000..d7995c8 --- /dev/null +++ b/examples/petrinet/runner.py @@ -0,0 +1,52 @@ +from state.devstate import DevState +from api.od import ODAPI +from bootstrap.scd import bootstrap_scd +from util import loader +from transformation.rule import RuleMatcherRewriter, ActionGenerator +from transformation.ramify import ramify +from examples.semantics.operational import simulator + + +if __name__ == "__main__": + import os + THIS_DIR = os.path.dirname(__file__) + + # get file contents as string + def read_file(filename): + with open(THIS_DIR+'/'+filename) as file: + return file.read() + + + state = DevState() + scd_mmm = bootstrap_scd(state) + + # Read models from their files + mm_cs = read_file('metamodels/mm_design.od') + mm_rt_cs = mm_cs + read_file('metamodels/mm_runtime.od') + m_cs = read_file('models/m_example_simple.od') + m_rt_initial_cs = m_cs + read_file('models/m_example_simple_rt_initial.od') + + # Parse them + mm = loader.parse_and_check(state, mm_cs, scd_mmm, "Petri-Net Design meta-model") + mm_rt = loader.parse_and_check(state, mm_rt_cs, scd_mmm, "Petri-Net Runtime meta-model") + m = loader.parse_and_check(state, m_cs, mm, "Example model") + m_rt_initial = loader.parse_and_check(state, m_rt_initial_cs, mm_rt, "Example model initial state") + + + mm_rt_ramified = ramify(state, mm_rt) + + rules = loader.load_rules(state, + lambda rule_name, kind: f"{THIS_DIR}/operational_semantics/r_{rule_name}_{kind}.od", + mm_rt_ramified, + ["fire_transition"]) # only 1 rule :( + + matcher_rewriter = RuleMatcherRewriter(state, mm_rt, mm_rt_ramified) + action_generator = ActionGenerator(matcher_rewriter, rules) + + sim = simulator.Simulator( + action_generator=action_generator, + decision_maker=simulator.InteractiveDecisionMaker(auto_proceed=False), + # decision_maker=simulator.RandomDecisionMaker(seed=0), + ) + + sim.run(ODAPI(state, m_rt_initial, mm_rt)) \ No newline at end of file diff --git a/examples/semantics/operational/simulator.py b/examples/semantics/operational/simulator.py index 133c502..ac559b6 100644 --- a/examples/semantics/operational/simulator.py +++ b/examples/semantics/operational/simulator.py @@ -17,7 +17,7 @@ class Simulator(MinimalSimulator): def __init__(self, action_generator, decision_maker: DecisionMaker, - termination_condition, + termination_condition=lambda od: None, check_conformance=True, verbose=True, renderer=lambda od: render_od(od.state, od.m, od.mm),