teaching/muMLE
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

i seem to have made some changes to the petrinet formalism

Browse source
This commit is contained in:
Joeri Exelmans 2024-12-03 17:58:49 +01:00
parent 9883e09ac2
commit 5633bf17a9
7 changed files with 26 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

2
examples/petrinet/metamodels/mm_design.od
View file

@ -2,7 +2,7 @@
PNConnectable:Class { abstract = True; } PNConnectable:Class { abstract = True; }
pn_arc:Association (PNConnectable -> PNConnectable) arc:Association (PNConnectable -> PNConnectable)
PNPlace:Class PNPlace:Class
PNTransition:Class PNTransition:Class

24
examples/petrinet/models/m_example_mutex.od
View file

@ -13,18 +13,18 @@ leaveCritical_1:PNTransition
enterCritical_2:PNTransition enterCritical_2:PNTransition
leaveCritical_2:PNTransition leaveCritical_2:PNTransition
:pn_arc (general_1 -> enterCritical_1) :arc (general_1 -> enterCritical_1)
:pn_arc (semaphore -> enterCritical_1) :arc (semaphore -> enterCritical_1)
:pn_arc (enterCritical_1 -> critical_1) :arc (enterCritical_1 -> critical_1)
:pn_arc (critical_1 -> leaveCritical_1) :arc (critical_1 -> leaveCritical_1)
:pn_arc (leaveCritical_1 -> semaphore) :arc (leaveCritical_1 -> semaphore)
:pn_arc (leaveCritical_1 -> general_1) :arc (leaveCritical_1 -> general_1)
:pn_arc (semaphore -> enterCritical_2) :arc (semaphore -> enterCritical_2)
:pn_arc (general_2 -> enterCritical_2) :arc (general_2 -> enterCritical_2)
:pn_arc (enterCritical_2 -> critical_2) :arc (enterCritical_2 -> critical_2)
:pn_arc (leaveCritical_2 -> semaphore) :arc (leaveCritical_2 -> semaphore)
:pn_arc (leaveCritical_2 -> general_2) :arc (leaveCritical_2 -> general_2)
:pn_arc (critical_2 -> leaveCritical_2) :arc (critical_2 -> leaveCritical_2)

8
examples/petrinet/models/m_example_simple.od
View file

@ -2,9 +2,9 @@ p0:PNPlace
p1:PNPlace p1:PNPlace
t0:PNTransition t0:PNTransition
:pn_arc (p0 -> t0) :arc (p0 -> t0)
:pn_arc (t0 -> p1) :arc (t0 -> p1)
t1:PNTransition t1:PNTransition
:pn_arc (p1 -> t1) :arc (p1 -> t1)
:pn_arc (t1 -> p0) :arc (t1 -> p0)

2
examples/petrinet/operational_semantics/r_fire_transition_nac.od
View file

@ -10,4 +10,4 @@ ps:RAM_PNPlaceState {
t:RAM_PNTransition t:RAM_PNTransition
:RAM_pn_arc (p -> t) :RAM_arc (p -> t)

4
examples/petrinet/operational_semantics/r_fire_transition_rhs.od
View file

@ -1,7 +1,7 @@
t:RAM_PNTransition { t:RAM_PNTransition {
condition = ``` condition = ```
# remove 1 token from every place connected with incoming arc # remove 1 token from every place connected with incoming arc
for incoming in get_incoming(this, "pn_arc"): for incoming in get_incoming(this, "arc"):
in_place = get_source(incoming) in_place = get_source(incoming)
in_place_state = get_source(get_incoming(in_place, "pn_of")[0]) in_place_state = get_source(get_incoming(in_place, "pn_of")[0])
in_num_tokens = get_slot_value(in_place_state, "numTokens") in_num_tokens = get_slot_value(in_place_state, "numTokens")
@ -9,7 +9,7 @@ t:RAM_PNTransition {
print("PNPlace", get_name(in_place_state), "now has", in_num_tokens-1, "tokens") print("PNPlace", get_name(in_place_state), "now has", in_num_tokens-1, "tokens")
# add 1 token to every place connected with outgoing arc # add 1 token to every place connected with outgoing arc
for outgoing in get_outgoing(this, "pn_arc"): for outgoing in get_outgoing(this, "arc"):
out_place = get_target(outgoing) out_place = get_target(outgoing)
out_place_state = get_source(get_incoming(out_place, "pn_of")[0]) out_place_state = get_source(get_incoming(out_place, "pn_of")[0])
out_num_tokens = get_slot_value(out_place_state, "numTokens") out_num_tokens = get_slot_value(out_place_state, "numTokens")

2
examples/petrinet/renderer.py
View file

@ -35,7 +35,7 @@ def render_petri_net(od: ODAPI):
for transition_name, _ in od.get_all_instances("PNTransition"): for transition_name, _ in od.get_all_instances("PNTransition"):
dot += f" {transition_name} [label=\"{transition_name}\\n\\n\\n­\"];\n" dot += f" {transition_name} [label=\"{transition_name}\\n\\n\\n­\"];\n"
dot += "}\n" dot += "}\n"
for _, arc in od.get_all_instances("pn_arc"): for _, arc in od.get_all_instances("arc"):
src_name = od.get_name(od.get_source(arc)) src_name = od.get_name(od.get_source(arc))
tgt_name = od.get_name(od.get_target(arc)) tgt_name = od.get_name(od.get_target(arc))
dot += f"{src_name} -> {tgt_name};" dot += f"{src_name} -> {tgt_name};"

10
examples/petrinet/runner.py
View file

@ -25,10 +25,10 @@ if __name__ == "__main__":
# Read models from their files # Read models from their files
mm_cs = read_file('metamodels/mm_design.od') mm_cs = read_file('metamodels/mm_design.od')
mm_rt_cs = mm_cs + read_file('metamodels/mm_runtime.od') mm_rt_cs = mm_cs + read_file('metamodels/mm_runtime.od')
m_cs = read_file('models/m_example_simple.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') # m_rt_initial_cs = m_cs + read_file('models/m_example_simple_rt_initial.od')
# m_cs = read_file('models/m_example_mutex.od') m_cs = read_file('models/m_example_mutex.od')
# m_rt_initial_cs = m_cs + read_file('models/m_example_mutex_rt_initial.od') m_rt_initial_cs = m_cs + read_file('models/m_example_mutex_rt_initial.od')
# Parse them # Parse them
mm = loader.parse_and_check(state, mm_cs, scd_mmm, "Petri-Net Design meta-model") mm = loader.parse_and_check(state, mm_cs, scd_mmm, "Petri-Net Design meta-model")
@ -36,7 +36,6 @@ if __name__ == "__main__":
m = loader.parse_and_check(state, m_cs, mm, "Example 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") 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) mm_rt_ramified = ramify(state, mm_rt)
rules = loader.load_rules(state, rules = loader.load_rules(state,
@ -52,6 +51,7 @@ if __name__ == "__main__":
decision_maker=simulator.InteractiveDecisionMaker(auto_proceed=False), decision_maker=simulator.InteractiveDecisionMaker(auto_proceed=False),
# decision_maker=simulator.RandomDecisionMaker(seed=0), # decision_maker=simulator.RandomDecisionMaker(seed=0),
renderer=lambda od: render_petri_net(od) + render_od(state, od.m, od.mm), renderer=lambda od: render_petri_net(od) + render_od(state, od.m, od.mm),
# 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))