第10讲petri之基本网系统

工作流基本技术MainContentsPetriNetNetElementaryNetSystem2HistoryofPetrinetCarlAdamPetri (1962,PhDthesis)InsixtiesandseventiesfocusmainlyontheorySinceeightiesalsofocusontoolsandapplications(cf.CPNworkbyKurtJensen)3WhyPetriNet?ThechiefattractionoftheareaofPetriNetisthewayinwhichthebasicaspectsofdistributedsystemsareidentifiedbothconceptuallyandmathematicallyG.ROZENBURG LeidenUniversity,TheNetherlands4MainContentsPetriNetNetElementaryNetSystem567DefinitionofNetANetisatripleN=(S,T,F)S

T

andST=F(ST)(TS)dom(F)cod(F)=S

T

dom(F)={x|

y:(x,y)

F}cod(F)={x|

y:(y,x)

F}SNSB S-elementsofNTNTE T-elementsofNXN elementsofNFNFF flowrelationofN8NotationsinPetriNetCalledconditionsinElementaryNetSystemCalledplacesinPlace/TransitionSystemCalledeventsinElementaryNetSystemCalledtransitionsinPlace/TransitionSystem9ANetExamplet8t1t2t4t7t3t6t5s0s1s2s4s3s9s5s8s6s7N=(B,E,F)B={s0,…,s9}E={t1,…,t8}F={(s1,t1),(s0,t1),(s0,t2),(s2,t2),……(t5,s1),(t8,s0),(t7,s2)}10CaseandStepCase(情态）Distributed(global)stateSetofconditionsholdingconcurrentlyConstellation(条件丛)E.g.{s0,s1,s9}Step(步)Distributed(global)transitionSetofeventsoccurringconcurrentlyE.g.{t1,t8}t8t1t2t4t7t3t7t5s0s1s2s4s3s9s5s8s6s711pre-Set&post-Setpre-Set(前集)/pre-conditionspost-Set(后集)/pre-conditions N=(B,E,F),xXN,YXN

·x={yXN:(y,x)F}

x·={yXN:(x,y)F}

·Y=

·x Y·=

x·

x

Y

x

Y

t8t1t2t4t7t3t6t5s0s1s2s4s3s9s5s8s6s712PureNet&SimpleNetPurenet(纯网/单纯网)对于网N(S,T;F), xX;xx=，其中X=STSimplenet(简单网）对于网N(S,T;F), 若x,yX,x=yx=y则x=y，其中X=ST13KeyQuestionsWhencanastep

occur(concurrently)atacase?Whatistheresultingcasewhenastepoccursatacase

‘Structural’transitionrelationrelatingpotentialcasestopotentialcasesviapotentialsteps14Question1Q:Whencananevente

occuratacaseC?A:ecanoccuratC

allpre-conditionsholdatC(e

C)and nopost-conditionsholdatC(e

C=

)记作，C[e>NEnabled 可实施的/有发生权的/受权的15Question1(c1)NotethatifC[e>N then·e

e·= Henceweoftenconsideronlypurenetst8t1t2t4t7t3t7t5s0s1s2s4s3s9s5s8s6s716Question2Q:Whatistheresultofanevente

occurringatacaseC?A:WheneoccursatCthepre-conditionsofeceasetoholdandthepost-conditionsofebegintohold;theremainingpartofthecaseremainsunaffected.(HencetheresultingcaseC’is(C

e)e)记作，C[e>NC’Firing 实施/发生17Question2(c1)N=(B,E,F),C,C’B,eEC[e>NC’iff

C-C’=e&C’-C=e

e=eeistheextensionofe

18Question3N=(B,E,F),CB,uEQ:WhencantheeventsinuoccurconcurrentlyatC? (whencanthestepuoccuratC)A:ucanoccuratCifftheeventsinucanindividuallyoccuratCwithoutinterferingwitheachother记作，C[u>N19Question4N=(B,E,F),CB,uE,uisenabledtooccuratCQ:WhatistheresultofuoccurringatC?A:Theresultisthe‘sum’oftheresultsoftheeventsinuoccurringindividuallyatC (C’=(C-u)u)记作，C[u>NC’20Question4(c1)N=(B,E,F),CB,uEuisindependent,indN(u),iff (e1,e2)uif

e1e2then (e1e1)(e2e2)=UisastepenabledatC,C[u>N,iff

indN(u),uCanduC=

21Question4(c2)Theorem(diamondproperty)N=(B,E,F),C,DB,uELet{u1,u2}beapartitionofu(u1,u2,u1u2=,u1u2=u)IfC[u

>ND,thenQBsuchthat C[u1

>NQandQ[u2

>ND22Question5N=(B,E,F),CB,=e1e2…enE+Q:Whencan

occuratC?A:

canoccuratCiff theeventsin

canindividuallyoccurintheorderdeterminedby

记作，C[

>N23Question5(c1)THEOREMN=(B,E,F),CB,e1,e2EIfC[e1,e2

>NandC[e2

>N,thenC[{e1,e2}>N24Question5(c2)THEOREM(sequentializationproperty)N=(B,E,F),C,DB,uE(1)IfC[u

>Nifforderinge1,…,enu, C[e1,…,en

>N(2)IfC[u

>NDifforderinge1,…,enu, C[e1,…,en

>ND25MainContentsPetriNetNetElementaryNetSystem

26DefinitionofENSystemAnElementaryNetSystem(ENsystem)isa4-tupleN=(B,E,F,Cin)where(B,E,F)isanetcalledtheunderlyingnetofN,und(N),Cin

BistheinitialcaseofN,inc(N)NotationsofENsystem BN EN FNCN=[Cin> thesetofcasesofNUN={u

E:(C1,C2)CNC1[u>NC2

thesetofstepsofN27ENSystemENsystemasanabstractmodelofadistributedsystem:

N=(B,E,F, Cin)GraphicalnotationforanENsystemconsistsofthemarkingofCinbytokensUnderlyingStaticStructureDynamicBehaviourt8t1t2t4t7t3t7t5s0s1s2s4s3s9s5s8s6s72829Relationof2Events LetNbeanENsystem,letC

CN,andlete1,e2

EN. e1,e2canberelatedtoeachotheratCin(atleast)threeways

sequence, conflict, concurrency30Relationof2Events:Sequence LetNbeanENsystem,letC

CN,andlete1,e2

EN. e1canoccuratCbutnote2.However,aftere1hasoccurrede2canoccur.e1,e2areinsequenceatCiff C[e1>,

C[e2>,andC’[e2>,whereC[e1>C’t8t1t2t4t7t3t7t5s0s1s2s4s3s9s5s8s6s731Relationof2Events:Choice LetNbeanENsystem,letC

CN,andlete1,e2

EN. e1ande2canoccurindividuallyatC,buttheycannotoccurtogetheratC. {e1,e2}isnotastepatC. whethere1ore2