add petrinet 'mutex'-example from MoSIS slides
This commit is contained in:
parent
5240c7e21a
commit
c9c5a5214d
3 changed files with 59 additions and 2 deletions
30
examples/petrinet/models/m_example_mutex.od
Normal file
30
examples/petrinet/models/m_example_mutex.od
Normal file
|
|
@ -0,0 +1,30 @@
|
||||||
|
# from slides:
|
||||||
|
# http://msdl.uantwerpen.be/people/hv/teaching/MoSIS/lectures/presentation.PetriNets.pdf
|
||||||
|
# page 51
|
||||||
|
|
||||||
|
general_1:Place
|
||||||
|
general_2:Place
|
||||||
|
critical_1:Place
|
||||||
|
critical_2:Place
|
||||||
|
semaphore:Place
|
||||||
|
|
||||||
|
enterCritical_1:Transition
|
||||||
|
leaveCritical_1:Transition
|
||||||
|
enterCritical_2:Transition
|
||||||
|
leaveCritical_2:Transition
|
||||||
|
|
||||||
|
:arc (general_1 -> enterCritical_1)
|
||||||
|
:arc (semaphore -> enterCritical_1)
|
||||||
|
:arc (enterCritical_1 -> critical_1)
|
||||||
|
|
||||||
|
:arc (critical_1 -> leaveCritical_1)
|
||||||
|
:arc (leaveCritical_1 -> semaphore)
|
||||||
|
:arc (leaveCritical_1 -> general_1)
|
||||||
|
|
||||||
|
:arc (semaphore -> enterCritical_2)
|
||||||
|
:arc (general_2 -> enterCritical_2)
|
||||||
|
:arc (enterCritical_2 -> critical_2)
|
||||||
|
|
||||||
|
:arc (leaveCritical_2 -> semaphore)
|
||||||
|
:arc (leaveCritical_2 -> general_2)
|
||||||
|
:arc (critical_2 -> leaveCritical_2)
|
||||||
25
examples/petrinet/models/m_example_mutex_rt_initial.od
Normal file
25
examples/petrinet/models/m_example_mutex_rt_initial.od
Normal file
|
|
@ -0,0 +1,25 @@
|
||||||
|
general_1_s:PlaceState {
|
||||||
|
numTokens = 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
general_2_s:PlaceState {
|
||||||
|
numTokens = 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
critical_1_s:PlaceState {
|
||||||
|
numTokens = 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
critical_2_s:PlaceState {
|
||||||
|
numTokens = 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
semaphore_s:PlaceState {
|
||||||
|
numTokens = 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
:of (general_1_s -> general_1)
|
||||||
|
:of (general_2_s -> general_2)
|
||||||
|
:of (critical_1_s -> critical_1)
|
||||||
|
:of (critical_2_s -> critical_2)
|
||||||
|
:of (semaphore_s -> semaphore)
|
||||||
|
|
@ -23,8 +23,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_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")
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue