Retele Petri

Reþele Petri

RP = (L, T, I, O)

L = locuri

T = tranziþii

I = funcþie de incidenþã înainte, I : L x T ->

O = funcþie de incidenþã înapoi, O : T x L ->

M = marcaj, M : L -> N

Reprezentare

Tranziþia t executabilã în M dacã:   M(l) >= I(l,t) , " l L

Execuþia lui t în M duce în M' cu  M'(l) = M(l) - I (l,t) + O (t,l) , " l L

notãm M-t->M'

$ = t1,t2,t3,...tn este o secvenþã posib 12112s181m ilã de execuþii din M în M' ºi notãm M =$=> M'

dacã marcajele M1, M2, M3,..., Mn a.î.

M -t1-> M1 -t2-> M2 -t3-> M3 -.... -tn-> Mn=M'

Fie RP ºi M0 un marcaj iniþial. Clasa marcajelor accesibile din M0 este A(M0).

Retelele Petri permit reprezentarea urmatoarelor aspecte ale

sistemelor paralele asincrone:

- paralelismul

- sincronizarea

(a) rendez-vous (b) semafor

- excluderea mutuala

- memorarea unei condiþii ºi a opusului sãu

- citirea unei conditii, fara modificarea ei

Modelul algoritmic al protocolului Start-Stop

Modelul cu automate al protocolului Start-Stop

t1 = preluare mesaj produs de utilizatorul

transmitator,

t2 = transmitere de mesaj mediului de comunicare,

t3 = receptie mesaj de la mediu,

t4 = transmitere confirmare,

t5 = receptie confirmare,

t6 = consumare mesaj de utilizator receptor.

marcajul  corespunzator  unei  stari   initiale M0

entitatea  emitatoare  asteapta producerea  unui mesaj (A)

entitatea receptoare  este  pregatita pentru receptie (D)

mediul de transmisie este gol.  

Caracteristici structurale ale Reþelelor Petri

graf de stãri

graf de evenimente

RP fãrã conflict

RP cu alegere liberã

RP pure

RP fãrã bucle

RP generalizatã

RP cu capacitãþi

RP colorate

RP cu arce inhibitoare

RP cu prioritãþi

RP continue

Validarea protocoalelor

(A) Proprietãþi generale

mãrginire

siguranþã

viabilitate

cvasi-viabilitate

home state

persistenþa

conflicte efective

conflicte structurale, dar ne-efective

(B) Proprietãþi specifice

invarianþi

pe locuri (L-invarianþi):

M(A) + M(B) + M(C) = 1

pentru orice M A(M0)

reþea conservativã

pe tranziþii (T-invarianþi):

avans sincron 0 <= N(t3) - N(t4) <= 1

secvenþe repetitive

Arbori ºi grafuri de acoperire

[100] M0

| t1

|

[011] M1

t2/ \t3

/ \

[000] M2 [10&] M0+

| t1

|

[01&] M1+

t2/ \t3

/ \

[00&] M2+ [10&] M0+

[100] M0

| t1

|

[011] M1

t2/ \t3

/ \

[000] M2 [10&] M0+

t1| ^

v | t3

[01&] M1+

t2/

/

[00&] M2+

construire_ arbore_ acoperire()

} }