Színezett Petri-hálók

Színezett Petri-hálók

dr. Bartha Tamás BME Méréstechnika és Információs Rendszerek Tanszék

Bevezetés • Mik a színezett Petri-hálók? – “A színezett Petri-hálók olyan modellek, amik a grafikus reprezentációt ötvözik a jól definiált (matematikai) szemantikával, így lehetővé téve a formális analízist.” – A színezetlen hálók kiterjesztései rugalmas adatszerkezetekkel és adatmanipulációs nyelvvel – CPN háló diagram = háló struktúra + deklarációk + háló jelölések, kifejezések + inicializáló kifejezések

2

Színezetlen és színezett Petri-hálók összehasonlítása Színezetlen (P-T) Petri-hálók

Színezett Petri-hálók

• színezetlen tokenek

• színes tokenek

• tokenek halmaza (számosság)

• tokenek multihalmaza

• token manipuláció

• adat manipuláció

• kezdeti jelölés

• inicializáló kifejezések

• tiltó élek

• őrfeltételek

• élsúlyok

• élkifejezések (változókkal)

• tranzíció engedélyezése

• lekötés engedélyezése

• konfliktus különböző engedélyezett tranzíciók között

• konfliktus ugyanazon tranzíció engedélyezett lekötései között

• ~ assembly nyelv

• ~ magas szintű programnyelv 3

Színezett Petri-háló alkotóelemei • Háló struktúra: – megjeleníti a rendszer vezérlési-/adatfolyam struktúráját – helyek, tranzíciók, (tiltó)élek

• Deklarációk: – definiálják: adatstruktúrákat + felhasznált függvényeket – deklarációk, jelölések, kódrészletek CPN ML-ben

– színosztályok, változók, élkifejezések 3 3`(q,0)

Helyek

Tranzíciók

Tokenek Élek 4

Színezett Petri-háló alkotóelemei • Jelölések, elnevezések: – megadják a háló szintaktikai és adatmanipulációs elemeit – nevek, színosztályok, bemenő/kimenő élkifejezések, őrkifejezések, aktuális állapot

• Inicializációs kifejezések: – Megadják a modell kezdőállapotát

– konstansok, kezdőállapot

5

color U = with p | q; color I = int; color P = product U * I; color E = with e; var x : U; var i : I;

deklarációs mező if x=q then 1`(q,i+1) else empty

kezdeti jelölés

3

3`(q,0) P

A

• CPN háló alkotóelemei:

(x,i)

– Helyek • név • színosztály • kezdő tokeneloszlás

T1

kimenő élkifejezés

• aktuális tokeneloszlás

– Tranzíciók

2

P

(x,i)

• őrfeltétel • élkifejezések

[x=q]

őrfeltétel

2`(p,0)

1`e

hely név E

B

• név

– Élek

bemenő élkifejezés

(x,i) 2`(p,0)

színosztály

aktuális jelölés

3`(q,0)

T2

e

S 1 1`e

tranzíció név

6

Multihalmazok • Multihalmaz: azonos elemből több példány is lehet benne





– leképezés: Bag(A), a  A  – formálisan: a 



xA

a( x)  x más jelölés (CPN): a   xA a( x) ' x

• Műveletek multihalmazokkal: – összehasonlítás: a2  a1

ha x  A, a2 ( x)  a1 ( x)

a2  a1 ha x  A, a2 ( x)  a1 ( x) – számosság: a 



–

a( x)

  a ( x)  a ( x)   x különbség: a  a    a ( x)  a ( x)   x szorzás skalárral: n  a    n  a( x)   x

– összegzés: a1  a2  –

xA

1

2

xA

1

2

xA

1

2

feltéve, hogy a2  a1

xA

7

Műveletek multihalmazokkal Összegzés: a1 + a2

Összehasonlítás: a1 ≤ a2, a1 ≠ a2

Számosság: |a1|

Szorzás skalárral: n∙a1

Kivonás: a1 - a2 (csak ha a2 ≤ a1) 8

Multihalmazok (folyt.) • Unió, multihalmazok egyesítése: a1  a2  …  am – tartomány: A1  A2  …  Am – eleme: ei 

m 1

Ak

ha Aj , ei  Aj

• n-esek képzése: A1, A2, …, An – tartomány: A1  A2  – eleme: e , e , 1 2

 A2

, en 1n Aj

ha ei  Ai

– általánosítás: a1, a2, …, an

9

Coloured Petri Nets (CPN) hálók eszközkészlete

CPN hálók: színosztályok definiálása • Egyszerű színosztályok – színezetlen tokenek: unit – alapvető típusok: int, bool, real, string

• Alábbi elemek definíciójában szerepelnek: – összetett színosztályok – hely jelölések (kezdőállapot) – változók, konstansok

– függvények, operátorok

– részhalmaz: with 1..4;

– felsorolás: with true | false; – indexelés: index d with 1..4; 11

Összetett színosztályok • Módszerek kombinált színosztályok létrehozására – unió képzés: union s1:S + s2:S + T;

– n-esek képzése (Descartes szorzat): product P * Q * R;

– rekord (címkézett n-esek): record p:P * q:Q * r:R;

– lista: list int with 2..6;

12

További CPN háló elemek: változók • változók Tokenek szimbolikus nevei – változódeklaráció:

• az alábbi kifejezésekben: – élkifejezések – őrfeltételek

var proc : P;

• konstansok

• alábbi deklarációkban:

Áttekinthetőbb, kezelhetőbb

– színosztályok

– konstansdeklaráció:

– függvények, operátorok

val n = 10; val d1 = d(1) : D;

– élkifejezések, őrfeltételek, inicializáló kifejezések

13

További CPN háló elemek: függvények • függvények mellékhatás-mentes SML nyelvű függvények

• műveletek, operátorok infix jelölésrendszer

• az alábbi kifejezésekben: – színosztályok – függvények, operátorok, konstansok

– élkifejezések, őrfeltételek, inicializáló kifejezések

14

További CPN háló elemek: kifejezések • háló kifejezések – értéke: a változók egy adott lekötésével értékelhető ki

• felhasználásuk: – élkifejezések, őrfeltételek, inicializáló kifejezések

– típusa: az összes lehetséges

kiértékelési eredmény halmaza – példák: x=q

2`(x,i) if x=q then 2`i else empty Mes(s) let n=5 in n * x + 2 end

15

Színezett Petri-hálók működése

Működés: engedélyezés és tüzelés Engedélyezés fogalma megváltozik:

• Lezárt élkifejezés: nem tartalmaz változókat – Változók • rendelkeznek típussal: Type(v)

• értékük a multihalmaz egy eleme

• Nyílt élkifejezés: változókat le kell kötni egy értékkel – lekötés: egy konkrét értékhozzárendelés minden változóhoz • adott lekötéssel az élkifejezés kiértékelhető

– rendelkezik típussal: Type(expr) = C(p)MS • az értékül kapott színosztály típusa

– kifejezésben szereplő változók halmaza: Var(expr) 17

Őrfeltétel • Őrfeltételek: – Tranzíciókhoz rendelt kifejezések • multihalmazok felett értelmezett kifejezések (lásd élkifejezés) • DE boolean visszatérési értékkel! (élkifejezés: multihalmaz v.é.)

– „Igaz” kiértékelési érték esetén engedélyezik a tranzíciót • „szűrik” az engedélyezett lekötéseket

– Jelölés: szögletes zárójelekben megadott kifejezés a tranzíció mellett [x=q] (x,i)

(x,q) q 18

Engedélyezettség színezett Petri-hálókban • Tranzíció lekötése – Érvényes lekötés: v  Var(t): b(v)  Type(v)  G(t)b Var(t )  v | v  Var  G(t )   a  A(t ) : v  Var  E(a)  • G(t)b az őrfeltétel

– Az összes érvényes lekötés halmaza: B(t)

• Egy érvényes lekötés engedélyezett, ha – A bemenő helyeken „van elég színezett token”:

p t : E  ( p, t )b  M ( p)  E h ( p, t )b  M ( p)

19

Tüzelés színezett Petri-hálókban • Egy engedélyezett tranzíció tüzelhet, ha – Magasabb prioritású tranzíció nem engedélyezett: t  :  (t )   (t ), p t  : E  ( p, t )b  M ( p)  E h ( p, t )b  M ( p)

– Magasabb prioritású tranzíció őrfeltétele nem teljesül G(t’)b’

20

Tüzelés színezett Petri-hálókban • Tüzelés menete: – Engedélyezett lekötések keresése • meghatározzák a bemenő élkifejezések, őrfeltételek

– Tranzíció engedélyezett adott lekötéssel  tüzelés – Színezett tokenek elvétele a bemenő helyekről – Színezett tokenek kitétele a kimenő helyekre    p  P : M ( p)  M ( p)   E ( p, t )b   E (t , p)b pt

pt 

– Ekkor M’ közvetlenül elérhető M-ből: M[(t,b) M’

21

Lekötött és lekötetlen változók • Lekötött változók – Az értékhozzárendelést a bemenő élek határozzák meg – Konzisztencia: változó értéke lekötésen belül azonos! • minden a tranzícióhoz tartozó élen: azonos név  azonos érték

• Lekötetlen változók – Csak kimenő élkifejezésekben szereplő változók – Az engedélyezés nem rendelt hozzá értéket: lekötetlen – Tüzeléshez le kell kötni! • a színosztályából bármilyen értéket felvehet • annyi lehetséges lekötés, amennyi a színosztály számossága • nemdeterminisztikus választás 22

Színezett Petri-háló példa: elosztott adatbázis

CPN háló példa: elosztott adatbázis • Specifikáció: – n különböző szerver, minden szerverhez egy adatbázis példány, amit egy lokális adatbázis menedzser kezel DBM = {d1, d2, …, dn}, n ≥ 3 – lokális frissítés lehetséges, de a menedzsernek minden más menedzsert egy üzenettel értesítenie kell a frissítésről – üzenet fejléc: küldő és fogadó (címzett) MES = {(s,r) | s,r  DBM  s≠r}, Mes(s) = ∑r  DBM-{s} 1`(s,r)

– rendszer állapota: Active, Passive – adatbázis menedzserek állapota: Inactive, Waiting (nyugtázásra vár), Performing

– üzenetek állapota: Unused, Sent, Received, Acknowledged 24

Elosztott adatbáziskezelő rendszer: deklarációk Deklarációs mező val n = 4; color DBM = index d with 1..n declare ms;

Jelentése:

DBM  d1 ,d 2 ,

,d n 

color PR = product DBM * DBM declare mult; fun diff(x,y) = (x<>y); color MES = subset PR by diff declare ms;

MES  (s, r ) | s, r  DBM  s  r

color E = with e;

fun Mes(s) = mult’PR(1`s, DBM--1`s) var s, r : DBM;

Mes(s) 



1'( s, r )

rDBM-{s}

25

Elosztott adatbáziskezelő rendszer CP háló modellje Sent Mes(s)

(s,r)

MES Update and Send Messages

s e

s

Mes(s) Active

DBM

r

e

Unused

DBM

Passive

Inactive

MES e s

Received DBM

Mes(s)

r

(s,r)

e

MES Waiting

Receive a Message

MES

Performing DBM

(s,r)

e

Receive all Acknowledgments

s

r

Mes(s)

Send an Acknowledgment

r

(s,r) Acknowledged MES

26

Színezett Petri-hálók dinamikus tulajdonságai

Színezett Petri-hálók dinamikus tulajdonságai • A színezetlen hálóknál megismert tulajdonságok kiterjesztései multihalmazokra • Korlátosság Egy hely korlátos, ha a tokenek száma bármely állapotban korlátos

– n egy felső integer korlát p-re, ha M   M 0  : M ( p)  n 



– m egy felső multihalmaz korlát p-re, ha M  M 0  : M ( p)  m

• Visszatérő tulajdonság Egy visszatérő állapotba mindig lehetséges visszajutni

 

 

– M egy visszatérő állapot, ha M   M 0  : M  M  – X egy visszatérő csoport, ha M   M 0  : X  M   

28

Színezett Petri-hálók dinamikus tulajdonságai • Élőség Az élőség garantálja, hogy a lekötési elemek egy része aktív marad – halott állapot (deadlock): egy lekötési elem sem engedélyezett

b  BE :  M b – halott tranzíció: egyik lekötése sem válhat engedélyezetté

M    M  , b  B(t ) :  M  b – élő tranzíció: nincs olyan állapot, amelyben minden lekötése halott

M    M 0  , M    M , b  B(t ) : M  b

29

Színezett Petri-hálók dinamikus tulajdonságai • Fair tulajdonság Fairség megmutatja, hogy egy lekötési elem milyen gyakran tüzel – elfogulatlan (impartial) tranzíció: végtelen sokszor tüzel

b  B(t ),    : OCb ( )  

– fair tranzíció: végtelen sok engedélyezés  végtelen sok tüzelés

b  B(t ),    : ENb ( )    OCb ( )   – igazságos (just) tranzíció: perzisztens engedélyezés  tüzelés

b  B(t ), i  1: ENb,i ( )  0  k  i : ENb,k ( )  0  OCb,k ( )  0  

• Elérhetőségi gráf

Színezetlen hálók elérhetőségi gráfjának generálásával analóg módon – állapot ekvivalencia osztályok, erősen összekötött komponensek 30

Színezett Petri-hálók strukturális tulajdonságai

Dekompozíció: a rendszer állapota

Update and Send Messages e

e

e Active

Passive

e

e Receive all Acknowledgments

32

Dekompozíció: adatbázis menedzserek

s

Update and Send Messages

s

r

Receive a Message

r

DBM Waiting

Inactive

DBM

Performing DBM

s

Receive all Acknowledgments

s

r

DBM

Send an Acknowledgment

r

33

Dekompozíció: üzenettovábbító alrendszer Sent Mes(s)

(s,r)

MES Update and Send Messages

Receive a Message (s,r)

Mes(s)

MES Unused

Received

MES

MES

(s,r)

Mes(s) Receive all Acknowledgments

Send an Acknowledgment Mes(s)

(s,r) Acknowledged MES

34

P-invariánsok az adatbázis-kezelő modellben 2 Id 5 Id

INV Sent Mes(s)

(s,r)

MES Update and Send Messages

s INV

e

s

Mes(s)

DBM

DBM

Passive

Inactive

MES INV

INV

1 Id 5 -Mes 6 -Ign

Unused

e s

3 Id 6 Id

Received DBM

Mes(s)

e

INV

MES

r

1 Id

Mes(s)

Send an Acknowledgment

Acknowledged INV

DBM INV

(s,r)

MES

Performing

(s,r)

INV

3 Id s

Receive all Acknowledgments

r

(s,r)

e

MES Active

r

e

2 Id Waiting

Receive a Message

INV r

1 Id 4 Id

1 Id 4 -Rec 5 Id

2 Id 5 Id

35

A modell tulajdonságai • Strukturális tulajdonságok: a háló uniform és konzervatív

• Korlátosság: multihalmaz

integer

– Inactive

DBM

n

– Waiting

DBM

1

– Performing

DBM

n-1

– Unused

MES

n*(n - 1)

– Sent, Received, Acknowledged

MES

n-1

– Passive, Active

E

1

36