From 87fc7362dba5be1c8039e3da517839daac9d94ee Mon Sep 17 00:00:00 2001 From: robbe Date: Thu, 24 Apr 2025 12:23:29 +0200 Subject: [PATCH] Scheduler petrinet example --- examples/petrinet/models/schedule.od | 70 +++++++++++++++++++ .../all_input_have_token.od | 13 ++++ .../operational_semantics/all_inputs.od | 13 ++++ .../all_output_places.od | 13 ++++ .../all_output_places_update.od | 13 ++++ .../operational_semantics/delete_all.od | 0 .../r_fire_transition_lhs.od | 2 +- .../operational_semantics/transition.od | 1 + examples/petrinet/runner.py | 20 ++++-- 9 files changed, 139 insertions(+), 6 deletions(-) create mode 100644 examples/petrinet/models/schedule.od create mode 100644 examples/petrinet/operational_semantics/all_input_have_token.od create mode 100644 examples/petrinet/operational_semantics/all_inputs.od create mode 100644 examples/petrinet/operational_semantics/all_output_places.od create mode 100644 examples/petrinet/operational_semantics/all_output_places_update.od create mode 100644 examples/petrinet/operational_semantics/delete_all.od create mode 100644 examples/petrinet/operational_semantics/transition.od diff --git a/examples/petrinet/models/schedule.od b/examples/petrinet/models/schedule.od new file mode 100644 index 0000000..3dce69d --- /dev/null +++ b/examples/petrinet/models/schedule.od @@ -0,0 +1,70 @@ +start:Start +end:End + +transitions:Match{ + file = "operational_semantics/transition"; +} + + +d:Data_modify +{ + rename = ' + { + "tr": null + }'; + delete = ' + { + "tr": null + }'; +} + +nac_input_without:Match{ + file = "operational_semantics/all_input_have_token"; + n = "1"; +} + +inputs:Match{ + file = "operational_semantics/all_inputs"; +} + +rewrite_incoming:Rewrite +{ + file = "operational_semantics/remove_incoming"; +} + +loop_trans:Loop +loop_input:Loop + +p:Print +{ +event = True; +label = "transition: "; +} + +p2:Print +{ +event = True; +label = "inputs: "; +} + +:Exec_con(start -> transitions){gate_from = 0;gate_to = 0;} +:Exec_con(transitions -> end){gate_from = 1;gate_to = 0;} +:Exec_con(transitions -> loop_trans){gate_from = 0;gate_to = 0;} +:Exec_con(loop_trans -> nac_input_without){gate_from = 0;gate_to = 0;} + +[//]: # (:Exec_con(nac_input_without -> loop_trans){gate_from = 0;gate_to = 0;}) +:Exec_con(nac_input_without -> inputs){gate_from = 1;gate_to = 0;} +:Exec_con(inputs -> loop_input){gate_from = 0;gate_to = 0;} +:Exec_con(inputs -> loop_trans){gate_from = 1;gate_to = 0;} + +:Exec_con(loop_trans -> end){gate_from = 1;gate_to = 0;} + +:Data_con(transitions -> loop_trans) +:Data_con(nac_input_without -> p) +:Data_con(d -> nac_input_without) +:Data_con(loop_trans -> d) +:Data_con(loop_trans -> rewrite_incoming) + + + + diff --git a/examples/petrinet/operational_semantics/all_input_have_token.od b/examples/petrinet/operational_semantics/all_input_have_token.od new file mode 100644 index 0000000..9207ce2 --- /dev/null +++ b/examples/petrinet/operational_semantics/all_input_have_token.od @@ -0,0 +1,13 @@ +# A place with no tokens: + +p:RAM_PNPlace +ps:RAM_PNPlaceState { + RAM_numTokens = `get_value(this) == 0`; +} +:RAM_pn_of (ps -> p) + +# An incoming arc from that place to our transition: + +t:RAM_PNTransition + +:RAM_arc (p -> t) diff --git a/examples/petrinet/operational_semantics/all_inputs.od b/examples/petrinet/operational_semantics/all_inputs.od new file mode 100644 index 0000000..1b87f1d --- /dev/null +++ b/examples/petrinet/operational_semantics/all_inputs.od @@ -0,0 +1,13 @@ +# A place with no tokens: + +p:RAM_PNPlace +ps:RAM_PNPlaceState { + RAM_numTokens = `True`; +} +:RAM_pn_of (ps -> p) + +# An incoming arc from that place to our transition: + +t:RAM_PNTransition + +:RAM_arc (p -> t) diff --git a/examples/petrinet/operational_semantics/all_output_places.od b/examples/petrinet/operational_semantics/all_output_places.od new file mode 100644 index 0000000..ab431cc --- /dev/null +++ b/examples/petrinet/operational_semantics/all_output_places.od @@ -0,0 +1,13 @@ +# A place with no tokens: + +p:RAM_PNPlace +ps:RAM_PNPlaceState { + RAM_numTokens = `True`; +} +:RAM_pn_of (ps -> p) + +# An incoming arc from that place to our transition: + +t:RAM_PNTransition + +:RAM_arc (t -> p) diff --git a/examples/petrinet/operational_semantics/all_output_places_update.od b/examples/petrinet/operational_semantics/all_output_places_update.od new file mode 100644 index 0000000..8d2908e --- /dev/null +++ b/examples/petrinet/operational_semantics/all_output_places_update.od @@ -0,0 +1,13 @@ +# A place with no tokens: + +p:RAM_PNPlace +ps:RAM_PNPlaceState { + RAM_numTokens = `set_value(this, get_value(this) + 1)`; +} +:RAM_pn_of (ps -> p) + +# An incoming arc from that place to our transition: + +t:RAM_PNTransition + +:RAM_arc (t -> p) diff --git a/examples/petrinet/operational_semantics/delete_all.od b/examples/petrinet/operational_semantics/delete_all.od new file mode 100644 index 0000000..e69de29 diff --git a/examples/petrinet/operational_semantics/r_fire_transition_lhs.od b/examples/petrinet/operational_semantics/r_fire_transition_lhs.od index c3bd82c..c05515b 100644 --- a/examples/petrinet/operational_semantics/r_fire_transition_lhs.od +++ b/examples/petrinet/operational_semantics/r_fire_transition_lhs.od @@ -1 +1 @@ -t:RAM_PNTransition \ No newline at end of file +t:RAM_PNTransition diff --git a/examples/petrinet/operational_semantics/transition.od b/examples/petrinet/operational_semantics/transition.od new file mode 100644 index 0000000..c7c8203 --- /dev/null +++ b/examples/petrinet/operational_semantics/transition.od @@ -0,0 +1 @@ +tr:RAM_PNTransition \ No newline at end of file diff --git a/examples/petrinet/runner.py b/examples/petrinet/runner.py index b2d0c51..df8692e 100644 --- a/examples/petrinet/runner.py +++ b/examples/petrinet/runner.py @@ -1,3 +1,4 @@ +from examples.schedule.RuleExecuter import RuleExecuter from state.devstate import DevState from api.od import ODAPI from concrete_syntax.textual_od.renderer import render_od @@ -9,6 +10,10 @@ from transformation.ramify import ramify from examples.semantics.operational import simulator from examples.petrinet.renderer import show_petri_net +from examples.schedule.ScheduledActionGenerator import * +from examples.schedule.RuleExecuter import * + + if __name__ == "__main__": import os @@ -46,19 +51,24 @@ if __name__ == "__main__": mm_rt_ramified, ["fire_transition"]) # only 1 rule :( - matcher_rewriter = RuleMatcherRewriter(state, mm_rt, mm_rt_ramified) - action_generator = ActionGenerator(matcher_rewriter, rules) + # matcher_rewriter = RuleMatcherRewriter(state, mm_rt, mm_rt_ramified) + # action_generator = ActionGenerator(matcher_rewriter, rules) + + matcher_rewriter2 = RuleExecuter(state, mm_rt, mm_rt_ramified) + action_generator = ScheduleActionGenerator(matcher_rewriter2, f"models/schedule.od") def render_callback(od): show_petri_net(od) return render_od(state, od.m, od.mm) - sim = simulator.Simulator( + action_generator.generate_dot() + + sim = simulator.MinimalSimulator( action_generator=action_generator, decision_maker=simulator.InteractiveDecisionMaker(auto_proceed=False), # decision_maker=simulator.RandomDecisionMaker(seed=0), - renderer=render_callback, + termination_condition=action_generator.termination_condition, # renderer=lambda od: render_od(state, od.m, od.mm), ) - sim.run(ODAPI(state, m_rt_initial, mm_rt)) + sim.run(ODAPI(state, m_rt_initial, mm_rt)) \ No newline at end of file