Petri Net Supplement Kenneth M Anderson Foundations of Software Engineering CSCI 5828 Spring Semester 2008 Petri Nets Formal Definition 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 Lecture 17 2 Graphical Representation In1 In2 Sem Out1 Lecture 17 CR1 CR2 Out2 3 Graphical Representation In1 In2 place Sem Out1 Lecture 17 CR1 CR2 Out2 4 Graphical Representation In1 In2 place transition Sem Out1 Lecture 17 CR1 CR2 Out2 5 Graphical Representation In1 In2 arc place transition Sem Out1 Lecture 17 CR1 CR2 Out2 6 Graphical Representation In1 In2 arc token place transition Sem Out1 Lecture 17 CR1 CR2 Out2 7 Graphical Representation In1 In2 arc token place transition Sem Out1 Lecture 17 CR1 CR2 Out2 8 Petri Nets Intuitive Meaning 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 Lecture 17 9 Execution Model Input and Output Places 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 Enabled Transition A transition is enabled if there is at least one token at each of its input places Lecture 17 10 Petri Net Semaphore In1 In2 Sem Out1 Lecture 17 CR1 CR2 Out2 11 Enabled Transitions In1 In2 Sem Out1 Lecture 17 CR1 CR2 Out2 12 Execution Model Firing a Transition 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 Firing Sequence 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 Lecture 17 13 Enabled Transitions In1 In2 Sem Out1 Lecture 17 CR1 CR2 Out2 14 After Firing In1 In2 Sem Out1 Lecture 17 CR1 CR2 Out2 15 Enabled Transition In1 In2 Sem Out1 Lecture 17 CR1 CR2 Out2 16 After Firing In1 In2 Sem Out1 Lecture 17 CR1 CR2 Out2 17 Enabled Transition In1 In2 Sem Out1 Lecture 17 CR1 CR2 Out2 18 Breaking the Semaphore Lets look at the semaphore example again and see how a change to the initial marking will change the semantics of the Petri Net In particular we will break the semantics of the semaphore by adding one token Lecture 17 19 Petri Net Semaphore In1 In2 Sem Out1 Lecture 17 CR1 CR2 Out2 20 Enabled Transitions In1 In2 Sem Out1 Lecture 17 CR1 CR2 Out2 21 After Firing In1 In2 Sem Out1 Lecture 17 CR1 CR2 Out2 22 Enabled Transitions In1 In2 Sem Out1 Lecture 17 CR1 CR2 Out2 23 After Firing In1 In2 Sem Out1 Lecture 17 CR1 CR2 Out2 24 Enabled Transitions In1 In2 Sem Out1 Lecture 17 CR1 CR2 Out2 25 After Firing In1 In2 Sem Out1 Lecture 17 CR1 CR2 Out2 26
View Full Document
Unlocking...