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, AB, AB
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