Lezione 8. Petri Nets ed estensioni • • [GMJ91, Sez. 5.5] [G87] Condition-Event nets Place-Transition nets Time Petri Nets [Merlin] Priorità Token con valore Richiami di logica Predicate-Transition (PrT-) nets [Genrich’87] Slide 1 Slide 2 ‘Place-Transition’ Petri net - definizioni PN = (P, T, A, M0) (* Place-Transition net *) • • • • P: T: A (P x T) (T x P) M0: P-->Nat. insieme finito di posti insieme finito di transizioni insieme fin. di archi marcatura iniziale Slide 3 PN per il linguaggio delle parentesi bilanciate () ( () ( ( ) ) ) ( ( ) ( ) ) (( ) ( ) (( ))) ( ) ) ……... () ( ( ( ) ( () ) ) ( ) Slide 4 -- ‘Condition-event’ nets - Sono Place-transition nets in cui • • • I posti sono chiamati (e rappresentano) condizioni Nessun posto puo’ ospitare piu’ di un token (‘1-safe’) Firing rule per trans. t (evento): » Un token in ciascun input place (pre-condizioni) » Nessun token negli output place (post-condizioni) Slide 5 Uso esclusivo di risorsa comune (Condition-event) Terminologia Stato = marcatura Input place - output place Transizione abilitata Transition firing rule (‘token game’) Firing sequence Slide 6 Concorrenza - nondeterminismo - (t1, t2) Conflitto - (t3, t4), solo quando la risorsa è condivisa Comportamento ‘unfair’: (t1; t3; t5; t1; t3; t5; … ) Slide 7 Per forzare un comportamento ‘fair’: Slide 8 Uso non esclusivo di risorsa (Place-transition) … o risorsa duplicata Slide 9 Deadlock Sia P1 che P2 richiedono entrambe le risorse... …e possono raggiungere un marking con nessuna transizione abilitata Slide 10 Liveness Assenza di deadlock Slide 11 Deadlock parziale Alcune transizioni diventano permanentemente disabilitate La rete e’ comunque live, cioè non va mai in deadlock Slide 12 Composizione di automi via PN - Componenti: Slide 13 Composizione Da confrontare con l’analoga composizione di FSMs Slide 14 ‘Limiti’ di Place-Transition Nets Trattano il controllo, non i dati • I token sono indistinguibili, anonimi, non hanno un valore P ToTrash Non si puo’ scegliere la transizione In base alle proprieta’ del messaggio (token). Non si puo’ arricchire il messaggio con … un francobollo (token) ToDestination Q Slide 15 Non si possono assegnare priorita’ alle transizioni (quando due o piu’ sono abilitate) Non si possono esprimere parametri temporali. Slide 16 Time Petri Nets (Merlin-Farber 76) Transizioni etichettate da coppie (tmin, tmax) I tempi si riferiscono all’istante t0 in cui la transizione viene abilitata Nelle PN senza tempo si assume una etichettatura (0, infinito) per ogni transizione. Slide 17 Es. di TPN: Sender-Receiver e… msgLoss sendMsg (0, 5) (0, 0) produceMsg Sender (3, 3) (5, 5) Channel (5, 5) receiveAck receiveMsg Receiver consumeMsg (2, 2) (1, 1) (0, 5) ackLoss sendAck Slide 18 ...timeout nel Sender (0, 5) (0, 0) (5, 5) Sender (3, 3) Receiver Channel (5, 5) (2, 2) (1, 1) (0, 5) Slide 19 PN con priorita’ Etichette di priorita’ associate alle transizioni Le priorita’ inducono un ordinamento sulle transizioni abilitate Slide 20 Priorita’ e temporizzazione... ... possono coesistere. La priorità induce un ordinamento fra le transizioni abilitate (sia dai token che dal tempo). …….I token arrivano a tempo zero……. (Maggior priorità = coeff. piu’ alto) Slide 21 Token con valore I token ‘portano’ un valore • Le transizioni sono arricchite da • • un predicato sui token in input una funzione input tokens ---> output token Ready-tuple • Un intero, un vettore di byte, un ambiente (Var--> Val) I token in input che soddisfano il predicato Gli input-token usati (gli output-token prodotti) sono identificati, in predicati e funzioni, dai nomi dei relativi posti di partenza (arrivo) Slide 22 Esempio P1 P2 4 3 t1 P3 7 4 1 [P2 > P1] P4 := P2 + P1 P4 [P2 = P3] P4 := 0 P5 := P2 + P3 t2 P5 Slide 23 Relazioni extended PN - Data Flow diagrams Slide 24 Esercizio 1 (PN a token con valore) La scelta della transizione deve dipendere dalla parita’ del messaggio (token) P ToTrash …??? Trash …??? ToDestination Sender Slide 25 Esercizio 2 - PN a token con valore per Dispatcher a 2 input (cfr. esempio per Extended FSM) Un dispatcher riceve messaggi da due diversi input channel ChanA e ChanB, e ne controlla la parita’: se la parita’ e’ sbagliata, manda un ‘nack’ attraverso, rispettivamente, il canale ReplyA o ReplyB; se la parita’ e’ corretta il dispatcher pone il messaggio ricevuto in un buffer, che puo’ tenere fino a 10 messaggi. Quando il buffer e’ pieno, l’intero contenuto viene spedito a una processing unit attraverso un altro canale. Nessun messaggio puo’ essere messo nel buffer pieno. [GJM9, Es. 5.15] Slide 26 Una soluzione ReplyA Parity(a1) not OK -------------------ReplyA := ‘nack’ ChanA a1 ChanB ReplyB b1 Parity(a1) = OK Length (q) < 10 -------------------q := append (q, a1) Parity(b1) = OK Length (q) < 10 -------------------q := append (q, a1) Parity(b1) not OK -------------------ReplyB := ‘nack’ nil q Length (q) = 10 ------------------------ProcessingUnit := q q := nil Processing Unit Slide 27 Predicate/Transition nets - Richiami di logica Per introdurre le Predicate-Transition (PrT-) Net [G87] si rende necessario introdurre/richiamare alcuni concetti di logica... Slide 28 Linguaggi del 1o ordine (calcolo dei predicati) Simboli di variabile: x, y, ... Simboli di costante: a, b, … Simboli di funzione: f i, gi, … Simboli di predicato: Ai, Bi, … • ‘i’ = num. di argomenti della funzione/predicato Connettivi logici: ~, /\, \/, , Virgola e parentesi: , ( ) Quantificatori universale ed esistenziale: , Slide 29 Termine • Variabile, costante, o simbolo di funzione a i argomenti, seguito da i termini fra parentesi, separati da virgole. » x » 2 » exp(sum(x, 9), 2)) Formula atomica • Simbolo di predicato a i argomenti, seguito da i termini fra parentesi, separati da virgole: > (exp(sum(x, 9), 2)), 4). Slide 30 Formula ben formata (fbf) • • • Formula atomica ~A, A/\B , A\/B, AB, AB x. A, x. A » dove A, B sono fbf e x e’ una variabile. Esempio: • x. (A(x, y) B(f(g(x)), y))) Nel seguito assumiamo che una formula sia sempre una fbf. Slide 31 x e’ legata in una formula se • • x e’ libera nella formula se non e’ legata Nella formula F = x.(A(x, y) B(f(g(x)), y))) • 3 simboli x sono legati, i 2 simboli y sono liberi Free(F) denota l’insieme delle variabili libere di F • E’ preceduto da un quantificatore, oppure E’ sotto l’azione di un quantificatore della stessa x nell’esempio: Free(F) = {y} Una formula e’ chiusa se non ha variabili libere Slide 32 Dati • • • • Un dominio di valori D (Nat, ...) Una interpretaz. dei simboli di costante (0, 1, 2…) Una interpretaz. dei simboli di funzione (+, *, ...) Una interpretazione dei simboli di predicato (‘>’, ...): Data una interpretazione, ogni formula chiusa e’ sempre vera o falsa Ogni formula F tale che Free(F) = x1…xn puo’ essere pensata come un predicato F(x1…xn) • che è vero o falso a seconda dei valori assegnati a x1…xn Slide 33 Predicate-Transition (PrT-) Nets [G87] Generalizzano il caso dei token con valore Gli archi sono etichettati da multi-insiemi di termini di un linguaggio L del primo ordine • Ogni transizione T e’ etichettata da una formula di L (tipicamente non chiusa), che denotiamo PT. Around(T) • [[ t1, t2, …, tx, tx, …]] l’insieme di variabili che appaiono nei termini che etichettano gli archi adiacenti a T Free(PT) • • l’insieme di variabili libere di PT. Deve valere: Free(PT) Around(T) Slide 34 Esempio di PrT-net 9 5 5 3 [[z, x+y, x-y, x-y]] T Around(T) = {z, x, y, h, k} 1 3 [[h]] [[y, y]] ((k) x+y = k*3 /\ y = h*2 ) [[k]] Free(PT) = {x, y, h} Variabili libere in PT che non fossero in Around(T) sarebbero assunte implicitamente legate da quantificatore esistenziale (‘dangling variables’) Slide 35 Firing rule per PrT-net Se esiste un assegnamento per le variabili in Around(T) tale che • • La valutazione di PT via e’ TRUE La valutazione via dei termini sugli archi in input a T fornisce multi-insiemi di valori che corrispondono a token effettivamente disponibili allora T viene eseguita, producendo token i cui valori sono espressi dai termini sugli archi in output di T, via . Slide 36 Esempio di esecuzione di trans. in PrT-net 9 5 5 3 [[z, x+y, x-y, x-y]] [[3, 9, 5, 5]] T Around(T) = {x, y, z, h, k} 1 [[h]] [[1]] 3 [[y, y]] [[2, 2]] ((k) x+y = k*3 /\ y = h*2 ) ((k) 9 = k*3 /\ 2 = 1*2 ) = TRUE (x) = 7 (y) = 2 (z) = 3 (h) = 1 (k) = 102 [[k]] [[102]] (non 3!) Slide 37 Da Cond.-Event a Predicate-Trans.(PrT) nets Sistema = insieme di individui e relazioni dinamiche Gli eventi cambiano le relazioni fra individui Individui: Sezioni = {0, 1, 2, 3, 4, 5, 6}; Treni {a, b} Relazione U Sezioni x Treni • (1, a) U significa ‘treno a occupa (Uses) sez. 1 Slide 38 V Sezioni • (3) V significa ‘sezione 3 e successiva libere (Vacant) Requisito di sicurezza: • I due treni non devono mai trovarsi contemporaneamente in due sezioni adiacenti Slide 39 C-E net: un posto per ogni (s, t) in U Slide 40 Un posto per ogni (s, x) in U (x variabile) Slide 41 Fusione di transizioni, etichette parametriche Slide 42 Predicate-Transition (PrT) net finale [[ ]] [[ ]] [[ ]] [[ ]] Un posto modella una relazione Un token modella un elemento della relazione Una transizione modella un cambiamento nelle relazioni Slide 43