Scheduler petrinet example
This commit is contained in:
parent
2c64ebda67
commit
87fc7362db
9 changed files with 139 additions and 6 deletions
70
examples/petrinet/models/schedule.od
Normal file
70
examples/petrinet/models/schedule.od
Normal file
|
|
@ -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)
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -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)
|
||||||
13
examples/petrinet/operational_semantics/all_inputs.od
Normal file
13
examples/petrinet/operational_semantics/all_inputs.od
Normal file
|
|
@ -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)
|
||||||
13
examples/petrinet/operational_semantics/all_output_places.od
Normal file
13
examples/petrinet/operational_semantics/all_output_places.od
Normal file
|
|
@ -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)
|
||||||
|
|
@ -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)
|
||||||
0
examples/petrinet/operational_semantics/delete_all.od
Normal file
0
examples/petrinet/operational_semantics/delete_all.od
Normal file
|
|
@ -1 +1 @@
|
||||||
t:RAM_PNTransition
|
t:RAM_PNTransition
|
||||||
|
|
|
||||||
1
examples/petrinet/operational_semantics/transition.od
Normal file
1
examples/petrinet/operational_semantics/transition.od
Normal file
|
|
@ -0,0 +1 @@
|
||||||
|
tr:RAM_PNTransition
|
||||||
|
|
@ -1,3 +1,4 @@
|
||||||
|
from examples.schedule.RuleExecuter import RuleExecuter
|
||||||
from state.devstate import DevState
|
from state.devstate import DevState
|
||||||
from api.od import ODAPI
|
from api.od import ODAPI
|
||||||
from concrete_syntax.textual_od.renderer import render_od
|
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.semantics.operational import simulator
|
||||||
from examples.petrinet.renderer import show_petri_net
|
from examples.petrinet.renderer import show_petri_net
|
||||||
|
|
||||||
|
from examples.schedule.ScheduledActionGenerator import *
|
||||||
|
from examples.schedule.RuleExecuter import *
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
if __name__ == "__main__":
|
if __name__ == "__main__":
|
||||||
import os
|
import os
|
||||||
|
|
@ -46,19 +51,24 @@ if __name__ == "__main__":
|
||||||
mm_rt_ramified,
|
mm_rt_ramified,
|
||||||
["fire_transition"]) # only 1 rule :(
|
["fire_transition"]) # only 1 rule :(
|
||||||
|
|
||||||
matcher_rewriter = RuleMatcherRewriter(state, mm_rt, mm_rt_ramified)
|
# matcher_rewriter = RuleMatcherRewriter(state, mm_rt, mm_rt_ramified)
|
||||||
action_generator = ActionGenerator(matcher_rewriter, rules)
|
# 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):
|
def render_callback(od):
|
||||||
show_petri_net(od)
|
show_petri_net(od)
|
||||||
return render_od(state, od.m, od.mm)
|
return render_od(state, od.m, od.mm)
|
||||||
|
|
||||||
sim = simulator.Simulator(
|
action_generator.generate_dot()
|
||||||
|
|
||||||
|
sim = simulator.MinimalSimulator(
|
||||||
action_generator=action_generator,
|
action_generator=action_generator,
|
||||||
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=render_callback,
|
termination_condition=action_generator.termination_condition,
|
||||||
# renderer=lambda 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))
|
||||||
Loading…
Add table
Add a link
Reference in a new issue