diff --git a/examples/petrinet/models/m_example_mutex.od b/examples/petrinet/models/m_example_mutex.od new file mode 100644 index 0000000..75cc67b --- /dev/null +++ b/examples/petrinet/models/m_example_mutex.od @@ -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) \ No newline at end of file diff --git a/examples/petrinet/models/m_example_mutex_rt_initial.od b/examples/petrinet/models/m_example_mutex_rt_initial.od new file mode 100644 index 0000000..83efc8c --- /dev/null +++ b/examples/petrinet/models/m_example_mutex_rt_initial.od @@ -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) diff --git a/examples/petrinet/runner.py b/examples/petrinet/runner.py index d7995c8..ece1e9e 100644 --- a/examples/petrinet/runner.py +++ b/examples/petrinet/runner.py @@ -23,8 +23,10 @@ if __name__ == "__main__": # 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') + # 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_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 mm = loader.parse_and_check(state, mm_cs, scd_mmm, "Petri-Net Design meta-model")