Today s Lecture Introduce the Petri Net Formalism Lecture 8 Petri Nets Present several examples Kenneth M Anderson Foundations of Software Engineering CSCI 5828 Spring Semester 2000 February 10 2000 Petri Nets In1 N P T A M0 where P is a finite set of places T is a finite set of transitions A is a finite set of arcs arrows M0 is the initial marking of N Kenneth M Anderson 2000 2 Graphical Representation Formal Definition February 10 2000 Kenneth M Anderson 2000 In2 Sem Out1 3 February 10 2000 CR1 CR2 Kenneth M Anderson 2000 Out2 4 Graphical Representation In1 Graphical Representation In2 In1 place In2 place CR1 Out1 February 10 2000 CR2 Kenneth M Anderson 2000 5 In1 February 10 2000 CR2 Kenneth M Anderson 2000 6 In1 arc In2 arc place transition Sem CR1 CR2 Kenneth M Anderson 2000 Out2 Graphical Representation In2 February 10 2000 CR1 Out1 Out2 Graphical Representation Out1 transition Sem Sem Out2 transition Sem Out1 7 token place February 10 2000 CR1 CR2 Kenneth M Anderson 2000 Out2 8 Graphical Representation In1 Petri Nets Intuitive Meaning In2 arc token place transition Sem Out1 February 10 2000 CR1 CR2 Out2 Kenneth M Anderson 2000 9 A place holds tokens A transition represents activity An arc connects a place and a transition A marking is an arrangement of tokens in places representing state An initial marking represents an initial state February 10 2000 Execution Model Kenneth M Anderson 2000 Petri Net Semaphore Input and Output Places In1 In2 Place P is an input place for transition T if there is an arc from P to T Place P is an output place for transition T if there is an arc from T to P Sem Enabled Transition Out1 A transition is enabled if there is at least one token at each of its input places February 10 2000 Kenneth M Anderson 2000 10 11 February 10 2000 CR1 CR2 Kenneth M Anderson 2000 Out2 12 Enabled Transitions In1 Execution Model Firing a Transition In2 An enabled transition is nondeterministically selected and fired by removing one token from each of its input places and depositing one token at each of its output places Sem Out1 CR1 February 10 2000 CR2 Firing Sequence Out2 Kenneth M Anderson 2000 A firing sequence is a sequence t0 t1 tn such that t0 is enabled and fired in M0 t1 is enabled and fired in M1 etc 13 February 10 2000 Kenneth M Anderson 2000 Enabled Transitions In1 After Firing In2 In1 In2 Sem Out1 February 10 2000 CR1 Sem CR2 Kenneth M Anderson 2000 14 Out2 Out1 15 February 10 2000 CR1 CR2 Kenneth M Anderson 2000 Out2 16 Enabled Transition In1 After Firing In2 In1 In2 Sem Out1 CR1 February 10 2000 Sem CR2 Out2 Kenneth M Anderson 2000 17 February 10 2000 CR1 Kenneth M Anderson 2000 18 In particular we will break the semantics of the semaphore by adding one token CR2 Kenneth M Anderson 2000 Out2 Lets look at the semaphore example again and see how a change to the initial marking will change the semantics of the Petri Net In2 Sem Out1 February 10 2000 CR2 Breaking the Semaphore Enabled Transition In1 CR1 Out1 Out2 19 February 10 2000 Kenneth M Anderson 2000 20 Petri Net Semaphore In1 Enabled Transitions In2 In1 In2 Sem Out1 CR1 February 10 2000 Sem CR2 Out2 Kenneth M Anderson 2000 Out1 21 CR1 February 10 2000 After Firing In2 Kenneth M Anderson 2000 February 10 2000 In2 Sem CR2 Kenneth M Anderson 2000 22 In1 Sem CR1 Out2 Enabled Transitions In1 Out1 CR2 Out2 Out1 23 February 10 2000 CR1 CR2 Kenneth M Anderson 2000 Out2 24 After Firing Enable Transitions In1 In2 In1 In2 Sem Out1 CR1 February 10 2000 Sem CR2 Out2 Kenneth M Anderson 2000 CR1 Out1 25 February 10 2000 CR2 Kenneth M Anderson 2000 Out2 26 Filling Station Example After Firing In1 Lets model the following situation In2 Fuel Pumps Spaces next to Pumps A cashier that takes payment Sem Out1 February 10 2000 CR1 Questions CR2 Kenneth M Anderson 2000 What is the concurrency that we want modeled How do we handle the parameterization of the Petri net e g lets say I want to add a pump Out2 27 February 10 2000 Kenneth M Anderson 2000 28
View Full Document
Unlocking...