Petri-Net Supplement:Kenneth M. AndersonFoundations of Software EngineeringCSCI 5828 - Spring Semester, 2008Lecture 17 2Petri NetsN = {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 NFormal DefinitionLecture 17 3Graphical RepresentationIn1In2Out1Out2CR1CR2SemLecture 17 4Graphical RepresentationplaceIn1In2Out1Out2CR1CR2SemLecture 17 5Graphical RepresentationplacetransitionIn1In2Out1Out2CR1CR2SemLecture 17 6Graphical RepresentationarcplacetransitionIn1In2Out1Out2CR1CR2SemLecture 17 7Graphical RepresentationarctokenplacetransitionIn1In2Out1Out2CR1CR2SemLecture 17 8Graphical RepresentationarctokenplacetransitionIn1In2Out1Out2CR1CR2SemLecture 17 9Petri NetsIntuitive Meaning A place holds tokens A transition represents activity An arc connects a place and a transition A marking is an arrangement of tokens inplaces, representing state An initial marking represents an initial stateLecture 17 10Execution ModelInput and Output Places Place P is an input place for transition T if thereis an arc from P to T Place P is an output place for transition T ifthere is an arc from T to PEnabled Transition A transition is enabled if there is at least onetoken at each of its input placesLecture 17 11Petri Net SemaphoreIn1In2Out1Out2CR1CR2SemLecture 17 12Enabled TransitionsIn1In2Out1Out2CR1CR2SemLecture 17 13Execution ModelFiring a Transition An enabled transition is nondeterministicallyselected and fired by removing one token fromeach of its input places and depositing onetoken at each of its output placesFiring Sequence A firing sequence is a sequence <t0,t1,…,tn>such that t0 is enabled and fired in M0, t1 isenabled and fired in M1, etc.Lecture 17 14Enabled TransitionsIn1In2Out1Out2CR1CR2SemLecture 17 15After FiringIn1In2Out1Out2CR1CR2SemLecture 17 16Enabled TransitionIn1In2Out1Out2CR1CR2SemLecture 17 17After FiringIn1In2Out1Out2CR1CR2SemLecture 17 18Enabled TransitionIn1In2Out1Out2CR1CR2SemLecture 17 19Breaking the SemaphoreLets look at the semaphore example againand see how a change to the initial markingwill change the semantics of the Petri Net In particular, we will break the semantics of thesemaphore by adding one tokenLecture 17 20Petri Net SemaphoreIn1In2Out1Out2CR1CR2SemLecture 17 21Enabled TransitionsIn1In2Out1Out2CR1CR2SemLecture 17 22After FiringIn1In2Out1Out2CR1CR2SemLecture 17 23Enabled TransitionsIn1In2Out1Out2CR1CR2SemLecture 17 24After FiringIn1In2Out1Out2CR1CR2SemLecture 17 25Enabled TransitionsIn1In2Out1Out2CR1CR2SemLecture 17 26After
View Full Document
Unlocking...