130

ALCUNE ESTENSIONI DELLE RETI DI PETRI Le reti di Petri classiche o P/T sono reti untimed (senza tempo) e risultano utili per analisi qualitative di un sistema, es. per verificare se una marcatura è raggiungibile a partire da un’altra. L’analisi può basarsi sulla costruzione dell’albero di raggiungibilità o sulla rappresentazione matematica di una rete. Per ampliare il loro potere di modellazione, le reti P/T sono state variamente estese per diventare, ad esempio: 1. reti che ammettono archi inibitori (o negatori) 2. reti temporizzate 3. reti di alto livello, genericamente dette anche reti colorate. Nel caso 1 si consente che l’abilitazione di una transizione dipenda anche dall’assenza di token in qualche posto. Nelle reti di cui al punto 2, nel modello è esplicitamente presente la variabile tempo. Essa può essere agganciata ai posti e/o alle transizioni. La nozione di tempo può essere sfruttata per ragioni di analisi di sistemi in tempo reale, es. per verificare se una marcatura può essere raggiunta entro un certo tempo (deadline). In questa classe rientrano le Time Petri Nets di Merlin e Farber. Il tempo può anche essere introdotto per scopi di simulazione e si parla spesso di reti temporizzate (Timed Petri Nets o TPN) e stocastiche. In queste reti il tempo è spesso associato alle transizioni e serve ad esprimere la durata (delay) di un’attività del sistema modellato. Nelle TPN sono normalmente presenti transizioni immediate (o istantanee) che corrispondono alle transizioni di una rete P/T, e transizioni timed. Alle transizioni immediate possono essere legate informazioni di priorità e probabilità. Nelle reti di alto livello, i token (e quindi i posti) diventano tipati ed è possibile esprimere l’abilitazione delle transizioni non solo in relazione alla disponibilità di un certo numero di token ma anche al contenuto informativo di questi token. L’abilitazione può essere condizionata da funzioni (es. guardie) associate agli archi e alle transizioni. In questo capitolo l’attenzione è posta esclusivamente su estensioni di cui ai punti 1 e 2. Si osserva, infine, che le estensioni, mentre aumentano il potere espressivo dei modelli di reti di Petri, purtroppo ne compromettono o complicano le possibilità di analisi. Ad esempio, la limitatezza diviene una questione non decidibile se la rete ammette archi negatori o priorità. Le estensioni avvicinano le reti a dei veri linguaggi di programmazione ad alto livello. Un modello corrisponde così ad un programma. Diventa difficile provare (ossia dimostrare) proprietà di un modello esteso e spesso ciò che rimane al modellatore è l’esecuzione diretta della rete. Questo è quanto accade, ad es., nella simulazione di modelli TPN la cui finalità è la valutazione quantitativa delle prestazioni di un sistema.

131

ARCHI INIBITORI L’utilità degli archi inibitori può essere messa in evidenza con un esempio. Si consideri il problema del “pigrone” (lazy lad) che vive da solo e mangia ciò che si cucina. Quando il pigrone ha fame ed il frigo è vuoto, allora egli passa a cucinare un certo numero di pietanze e a metterle nel frigo. L’operazione di cottura di cibo termina non appena il pigrone diventa “affamato” nel qual caso egli consuma le pietanze riposte nel frigo fino a svuotare completamente il frigo, e cosi via ripetendo. Un modello di rete di Petri per questo problema è mostrato in Figura 1.

Figura 1:Modello del “pigrone” con arco negatore

L’arco inibitore collega il posto p1 con la transizione t3. Tale arco termina con un cerchietto nero e non con la freccia. La transizione t3 è abilitata quando esiste almeno un token in p3 ma non esistono token in p1. La marcatura iniziale del modello consiste nel porre un solo token nel posto p2. Tale token rappresenta il pigrone. Nel posto p2 il pigrone cucina una serie di pietanze (token) che vengono depositate, ad ogni sparo di t1, in p1 (frigo). Il pigrone “è affamato” quando scatta t4, nel qual caso il token-pigrone si sposta in p3. In questo stato si modella il pigrone che consuma tutto il contenuto del frigo, una pietanza alla volta, tramite la transizione t2. Per via dell’arco negatore, la transizione t3 che specifica il cambio di stato da “mangia” a “cucina” del pigrone, non può scattare sino a quando in p1 esiste almeno un token (il frigo non è vuoto). È facile convincersi che un tale modello non è esprimibile con una normale rete P/T nell’ipotesi che il posto p1 sia illimitato. Se, invece, si fissa un tetto massimo al numero di token che il frigo può contenere, allora si riesce a modellare il sistema con una rete P/T introducendo il posto p1’ complementare di p1 (si veda la Figura 3.2 in cui il posto p1 è limitato a 7 token).

p3

132

Figura 2 Modello P/T del “pigrone” con p1 limitato a 7

In letteratura è possibile trovare una definizione più generale di arco inibitore che ha associato anche un peso, diciamolo k. In questo caso, l’abilitazione della transizione è possibile solo se nel posto da cui origina l’arco esistono meno di k token. Secondo questa definizione, il normale arco inibitore, utilizzato in Figura 1, ha associato a sé il peso 1. In questa tesi si considerano solo archi inibitori semplici (peso implicito unitario). Si mostra, per completezza, in Figura 3 una differente modellazione del problema del “pigrone” che non fa uso di arco inibitore ma di transizioni con priorità. Mentre per altri dettagli sulle priorità si rimanda a più avanti in questo capitolo, qui è sufficiente assumere che le transizioni di un modello P/T siano etichettabili con un parametro priorità. Di momento in momento, intuitivamente, tra le transizioni abilitate può scattare quella (o una) avente priorità massima. Assumendo che t2 sia più prioritaria di t3 che, ad es., ha la minima priorità del modello (t1, t2 e t4 possono essere egualmente alla stessa priorità) anche il modello di Figura 3 costituisce una specifica accettabile del comportamento del pigrone. Infatti, la maggiore priorità di t2 impedisce a t3 di scattare anche se t3 è abilitata, purchè t2 sia abilitata a sua volta (nel frigo ci sono altre pietanze da consumare).

Figura 3 Modello del “pigrone” con t3 meno prioritaria di t2

7

7

133

Quanto discusso in precedenza ha carattere di generalità: è possibile implementare un modello basato con archi inibitori mediante transizioni prioritarie e viceversa. Si nota, comunque, che la soluzione con archi inibitori è graficamente “più visibile” che non l’utilizzo delle priorità, e pertanto preferibile nei casi pratici.

RETI DI PETRI ESTESE COL TEMPO Il parametro “tempo” può essere aggiunto al formalismo in diversi modi, dando luogo a differenti tipi di reti di Petri temporizzate, ad esempio: - Transition-Timed Petri Nets (TTPN)

→T:τ IR assegna tempi di scatto iτ alle transizioni .Tti ∈ Le transizioni sono viste come attività: un’attività inizia non appena la corrispondente transizione diventa abilitata; il termine dell’attività è segnalato dallo scatto della transizione.

- Place-Timed Petri Nets (PTPN) →P:τ IR assegna tempi di conservazione iτ ai posti .Ppi ∈

I token che arrivano in un posto devono rimanervi per un certo tempo di conservazione, prima di rendersi disponibili per lo scatto di una transizione alimentata da quel posto.

La Figura 4 mostra come l’aggiunta del tempo ad un posto di una PTPN possa essere riprodotta con una sotto rete (un posto, una transizione timed, un posto) di una TTPN. Per queste ragioni, così come spesso si fà in letteratura, ci si limita, nel seguito, a considerare solo le TTPN. In più, anche quando dovesse essere genericamente utilizzata la sigla TPN – Timed Petri Nets, si farà implicito riferimento alle TTPN.

Figura 4 Trasformazione di una PTPN in una TTPT e viceversa

τ* τ∗

134

UNA DEFINIZIONE DI TIMED PETRI NETS TPN=(P, T, F, W, τ, M) dove • P = {p1, p2, ..., pnP} è un insieme finito di posti • T = {t1, t2, ..., tnT} è un insieme finito di transizioni, con P T∩ = ∅ e un insieme

non vuoto di nodi ( P T∪ ≠ ∅ ) • F P T T P⊆ × ∪ ×( ) ( ) è un insieme finito di archi tra posti e transizioni • W F: → Ν assegna pesi w(f) agli elementi f F∈ che denotano la molteplicità degli

archi unitari tra gli elementi connessi • ℜ→T:τ assegna ritardi di sparo τi agli elementi t Ti ∈ • M: P N→ +0 è la marcatura degli elementi p Pi ∈ . Esistono tre casi importanti nella definizione dei ritardi di sparo (firing delays): (a) il caso quando τi=0 (transizioni immediate), cioè le transizioni sparano

consumando un tempo nullo (b) il caso quando τ i ∈ℜ è un valore deterministico (deterministic timed transitions o

reti D-TPN) e (c) il caso quando τi è un’istanza di una variabile casuale (stochastic timed

transitions). Se T contiene solo transizioni temporizzate e stocastiche in cui il ritardo di sparo è una variabile casuale con distribuzione esponenziale, la rete TPN appartiene alla classe delle Stochastic Petri Nets (SPNs). Le reti Generalized SPNs (GSPNs) (Marsan et al., 1987) consentono l’utilizzo di una combinazione di transizioni senza tempo (o immediate) e transizioni temporizzate stocastiche. Più precisamente, una GSPN è formalmente una tripla GSPN=(TPN, Π, P) in cui • N:T →Π assegna priorità πi alle transizioni immediate t Ti ∈ • [0,1]TP →: assegna pesi di selezione (probabilità) Pi alle transizioni immediate

Tti ∈ .

ABILITAZIONE TEMPORIZZATA E SEMANTICA DI SPARO

REGOLA DI ABILITAZIONE IN UNA TPN

Una transizione Tt ∈ è abilitata nella marcatura Μ al tempo τ, se e solo se

( ) ( )tpwpMtprep ,),( ≥∈∀ in Μ

( )MEτ rappresenta l’insieme di tutte le transizioni abilitate in Μ, al tempo τ.

135

REGOLA DI SELEZIONE DELLE TRANSIZIONI IMMEDIATE IN UNA TPN

Nell’ipotesi che ( )MEτ contenga solo transizioni immediate, Ttt ji ∈, sono in conflitto effettivo al tempo τ ( )ji tECt τ se e solo se al tempo τ la marcatura attuale è

Μ e ( )MEtt ji τ∈, , e 'MM it⎯→⎯ potrebbe causare che ( )'MEt j τ∉ . ti è selezionata per il firing (sparo) al tempo τ secondo la probabilità:

( )( ) ( )∑ jtECtj

ii t

tatfiringforselectedtjTi

PP

|

= ] P[ τ

Una transizione immediata selezionata per lo sparo deve scattare.

PRIORITÀ DELLE TRANSIZIONI IMMEDIATE Se ( )MEτ contiene transizioni immediate e temporizzate, le transizioni immediate sono sempre selezionate prima di quelle temporizzate ai fini dello sparo. Inoltre, tra le transizioni immediate viene fatta sparare sempre quella (o una) avente priorità massima. A parità di priorità, si applicano le probabilità come spiegato nella sezione 3.2.2.2.

SCELTA DELLE TRANSIZIONI TEMPORIZZATE

Si supponga che ( )MEτ contenga solo transizioni temporizzate e sia RET(ti), ( )MEti τ∈ , il tempo rimanente di abilitazione di ti. La transizione t∈ ( )MEτ che

prossimamente deve sparare è quella che ha minimo RET(ti).

SEMANTICA SINGLE SERVER E INFINITE SERVER

Se ( ) ( )tpwcpMtprep ,*),( ≥∈∀ , e 1>c , allora t è detta essere multiplamente abilitata di grado c. Se t può sparare una sola abilitazione alla volta, essa adotta la semantica Single Server (SS). La semantica Infinite Server (IS) consente invece di sparare un qualunque ammontare di abilitazioni ad uno stesso tempo. Se una transizione t segue SS allora il tempo di occorrenza (occurrence time) ot(t(toki)) di t che consuma l’i-esima tupla abilitante, sarà

ot(t(toki))=ot(t(toki-1))+ Xi dove Xi ~ exp(λi) è una variabile casuale con distribuzione esponenziale. Se t applica IS allora ot(t(toki)) = Xi, per ogni tupla abilitante, così esprimendo una nozione di parallelismo tra gli spari.

136

Figura 5 Orizzonte temporale e semantica SS, IS e k-S

La Figura 5 esemplifica l’orizzonte temporale rispetto al quale sono valutati i ritardi di sparo di una transizione supposta dotata di 3 abilitazioni al tempo corrente. Nella parte a) si mostra l’applicazione della semantica Single Server; nella parte b) della semantica Infinite Server, nella parte c) di una semantica intermedia tra SS ed IS (k-Server) che fissa il livello di concorrenza a k (qui assunto 2) e non al massimo valore possibile. Si nota che, senza ledere alla generalità, un motore di esecuzione per le TPN può limitarsi ad offrire la semantica IS. Il modellatore, infatti, può comunque ottenere la semantica SS aggiungendo un posto di auto-anello con un token ad ogni transizione temporizzata.

POLITICHE DI SPARO “RACE” E “PRE-SELECTION” Una varietà di regole di sparo possono essere definite per le TPN, ciascuna delle quali ha una differente semantica e finalità di intenti rispetto a specifici domini di modellazione. In SPN, ad esempio, l’operazione di sparo di una transizione è atomica, nel senso che la rimozione dei token dai posti d’ingresso e il deposito dei token nei posti di uscita costituisce una singola operazione indivisibile. Un tempo random trascorre tra l’abilitazione e lo scatto di una transizione ti, durante il quale i token abilitanti risiedono nei posti di ingresso. La transizione ti deve rimanere continuamente abilitata durante il tempo τi, e spara a quel tempo (politica race o pre-

137

emptiva). Nel caso ti perde l’abilitazione durante il periodo τi, o un nuovo valore, calcolato secondo la funzione distribuzione, τi o la parte rimanente (non trascorsa) di τi (age memory) possono essere usati per la prossima abilitazione di ti. Un’altra regola di esecuzione per le TPN definisce lo sparo di una transizione in tre tempi (scatto tri-fase): nella prima fase (“start firing”) i token sono prelevati dai posti di ingresso e rimangono invisibili per altre abilitazioni per tutta la durata della seconda fase (“firing in progress”); nella terza fase (“end firing”) i token sono finalmente rilasciati nei posti di output (meglio: i token di uscita sono generati) (politica preselettiva o non pre-emptiva). L’adozione della politica “race” con o senza memoria è esemplificata in Figura 6. Nella parte a) la transizione dimentica il tempo residuo dello sparo interrotto. Infatti, la successiva abilitazione usa un ritardo valutato ex-novo. Nella parte c), il tempo rimanente allo sparo al momento della disabilitazione è utilizzato come ritardo di sparo nella prossima abilitazione. La parte b) illustra una situazione intermedia. La porzione rimanente allo sparo interrotto è dimenticata come in a) ma alla prossima abilitazione si ripropone come ritardo di sparo lo stesso valore dell’ultimo ritardo (interrotto). È utile osservare che la politica race assume una visione delle transizioni temporizzate come serventi. Quando una transizione timed è abilitata, il server “comincia” a processare i token, salvo poi accusare un problema di pre-emption e di interruzione se lo sparo di un’altra transizione ruba qualche token di abilitazione (fenomeno di corsa). Tutto ciò è rilevante in presenza appunto di conflitti. Se due transizioni temporizzate t1 e t2, che condividono qualche posto di ingresso, si abilitano nello stesso momento, t1 e t2 “iniziano” il loro processo secondo il proprio ritardo di sparo valutato indipendentemente. Ovviamente, la transizione col minimo ritardo pre-empta l’altra. In questo modo, la politica race risolve i conflitti automaticamente e dinamicamente sulla base di quale transizione scatta prima. Diverso è il discorso della preselezione. In questo caso, essendo t1 e t2 in conflitto, una scelta a priori tra le due deve essere fatta (es. randomaticamente od anche sulla base dei possibili tempi di sparo), della transizione scelta viene valutato il ritardo di sparo e fatta partire la prima fase di acquisizione dei token. Le osservazioni di cui sopra sono rilevanti nella realizzazione di un motore di simulazione discreta ad eventi di modelli TPN. Un tale motore processa eventi del tipo: transition-fire (per schedulare lo sparo di una transizione) e transition-unfire (per de-schedulare un corrispondente transition_fire). Un evento del primo tipo ammette come attributi: l’identificatore della transizione, il tipo di transizione (se immediata o temporizzata) e, a seconda dei casi, ulteriori parametri come il ritardo di sparo etc. Un evento di transition_unfire si accompagna all’identificatore della transizione il cui evento di fire va de-schedulato etc.

138

Figura 6 Politica race senza o con memoria Naturalmente, la politica race utilizza tutte e due i tipi di eventi. La politica pre-selection può basarsi solo sugli eventi transition_fire in quanto la schedulazione di un evento di sparo costituisce un evento committed, ossia non più revocabile. Un motore simulativo che supporta le TPN descritte in questo capitolo, con in più gli archi negatori, è disponibile nell’ambito dello strumento TPN Designer descritto nel capitolo che segue, utile per modellare e simulare sistemi complessi e scalabili.

RACE O PRE-SELECTION? Si consideri il modello TPN di Figura 7 che ammette diversi tipi di transizioni in conflitto. Tale modello consente di verificare che, in generale, più politiche di sparo possono essere richieste da una stessa rete TPN. Le transizioni disegnate come rettangolini sono timed, quelle rappresentate da lineette sono immediate. In Figura 7 esistono le seguenti situazioni di conflitto: a) (free-choice) conflitto tra le transizioni timed t1 e t2 b) (non free-choice) conflitto tra le transizioni timed t3 e immediata t4 c) (free-choice) conflitto tra le transizioni immediate t5 e t6.

139

Figura 7 Conflitti e politiche di sparo

Per risolvere il conflitto a) potrebbe essere utilizzata tanto la politica race quanto quella preselection. Con race, come già spiegato in precedenza, al tempo τ in cui si abilitano t1 e t2, si valutano (sampling) i tempi di sparo di t1 e t2 separatamente (in accordo alla funzione distribuzione associata) e si lascia che quella col minimo tempo di sparo preempti l’altra in modo “spontaneo”. L’adozione di preselection comporta che a priori, al tempo τ, si effettua una scelta tra t1 e t2, e per la transizione “vincente” si valuta il tempo di sparo e si pre-seleziona il token in p1. La transizione non vincente viene trascurata: è come se essa non fosse mai stata abilitata al tempo τ. Per il caso c) che coinvolge solo transizioni immediate, la scelta più ovvia è la politica preselection in cui una transizione tra t5 e t6 viene prescelta (tenendo conto dei parametri di priorità/probabilità associati; per transizioni equi-prioritarie ed equi-probabili la scelta ridiventa non deterministica come nelle P/T) e quindi spara in modo committed. Il caso b) è in un certo senso “anomalo” dal momento che il conflitto coinvolge una transizione timed ed una immediata. Qui potrebbe essere “più naturale” la politica race, dal momento che t3 e t4 potrebbero non essere abilitate allo stesso tempo. Se prima si abilita t3, essa inizia a “sparare”. Se però, durante il firing, si abilita anche t4, allora il firing di t3 è interrotto in quanto t4 è più prioritaria. Volendo, si può “simulare” la pre-selection tra transizioni timed ed in conflitto adottando comunque la politica race e sostituendo i casi come a) con casi come c) in cui le transizioni immediate sono seguite subito dopo dalle transizioni temporizzate (Figura 8).

140

Figura 8 Simulazione di preselection con race, per transizioni timed in conflitto Si osserva, infine, che per evitare comportamenti diversi di uno stesso modello a seconda della politica di sparo scelta, uno strumento può richiedere che i casi free-choice siano uniformi, ossia riguardino o solo transizioni temporizzate o solo transizioni istantanee.

UN PROTOCOLLO CON TIMEOUT La politica race è naturale in modelli che coinvolgono timer e timeout. In Figura 9 si riporta un semplice modello di un protocollo di comunicazione. I rettangoli trasparenti sono transizioni timed. Le altre transizioni sono immediate. Il token in p1 rappresenta un messaggio che il sender (rappresentato dal posto p1) trasmette al ricevitore (posto p3). La trasmissione è seguita dall’invio da parte del receiver di un messaggio di acknowledgment (o di conferma) al sender. L’invio del messaggio è catturato dallo sparo di t1. Il ritardo di sparo di t2 esprime il ritardo di comunicazione del messaggio. Quando t2 scatta, un token è rilasciato in p3 (il receiver). p3 è un posto free-choice: t3 e t4 sono entrambe abilitate ma solo una delle due transizioni potrà scattare. Lo sparo di t3 corrisponde (in modo alquanto semplificato) alla perdita del messaggio o alla sua corruzione etc. Lo scatto di t4, invece, denota la corretta ricezione del messaggio e la spedizione indietro al mittente dell’acknowledgment. La transizione timed t5 rappresenta il ritardo di comunicazione associato al messaggio di ack. Lo scatto di t5 genera un token in p1 e uno in p6. Il token in p1 consente al sender di spedire un nuovo messaggio. Quello in p6 ha una diversa finalità. In realtà il mittente usa un timer ed un massimo ammontare di tempo (timeout, riflesso dal ritardo associato a t6) per aspettare il messaggio di ack. Se t6 scatta prima di t5 allora il messaggio di replica si considera inesistente e si rigenera in p1 un token con l’obiettivo di rispedire il messaggio originario (non confermato e dunque perso). Se invece, il messaggio di replica arriva prima che scatti t6, allora il firing di t6 è interrotto, in quanto il token in p6 toglie (per l’arco negatore) l’abilitazione alla t6. Ciò corrisponde a disattivare il timer. La t7 serve a consumare il token in p5 per evitare che esso influenzi, erroneamente, la gestione del prossimo messaggio.

141

Figura 9 Un semplice protocollo con timeout Si intuisce che in questa modellazione l’ammontare del timeout possa e debba essere definito ogni volta ex-novo in quanto non occorre avere memoria del firing interrotto. Ogni nuovo messaggio trasmesso dal mittente deve avere il suo nuovo timeout. La transizione t4 anche se ridondante preserva l’uniformità del free-choice p3 (composto solo di transizioni immediate). Il modello di Figura 9 è dimostrativo ma incompleto. Nella realtà, non solo i messaggi normali ma anche le repliche possono perdersi per cui il protocollo è necessariamente più complesso.

RIFERIMENTI G. Chiola. Timed Petri Nets. The MATCH Performance Book Draft. http://www.disi.unige.it/project/match/ A. Ferscha. Concurrent execution of timed Petri Nets. Proc. Of 1994 Winter Simulation Conference (WSC94), Lake Buena Vista, Florida, USA, pp. 229-236, 1994. M.A Marsan, G. Balbo, G. Conte. A class of generalized stochastic Petri nets for the performance evaluation of systems. ACM Transactions on Computer Systems, vol. 2, n. 2, pp. 93-122, 1984.

142

TIME PETRI NETS In quanto segue, le Time Petri Nets verranno riferite con la sigla MF (Merlin&Farber Nets). Esse sono utili per specificare i vincoli di temporizzazione di sistemi in tempo reale. In una rete MF alle transizioni sono associati intervalli temporali [a,b] con a≤b, in cui a può essere 0 e b può essere infinito. L’esistenza di un tale intervallo indica che ad una transizione è associata un’attività la cui durata minima è a e quella massima è b. La durata effettiva è non deterministicamente un valore scelto nell’intervallo. Una classica rete P/T corrisponde ad una rete MF nella quale tutti gli intervalli sono del tipo [0,∞]. Se una transizione di una rete MF non ha un intervallo esplicito, essa possiede l’intervallo di default [0,∞]. Le transizioni obbediscono ad una semantica forte dello sparo. Detto τ l’istante temporale in cui una transizione t diviene abilitata, essa non può sparare prima di τ+a, ma deve sparare entro τ+b, o al più a τ+b, a patto che nel frattempo non perda token a causa dello sparo di qualche altra transizione in conflitto. Si capisce che per stabilire se una transizione t può sparare, non basta esaminare solo il suo preset, ma occorre indagare in generale tutte le altre transizioni della rete per stabilire se esse devono sparare prima di t. Figura 10 riporta un semplice esempio di una rete MF. Nell’ipotesi che t1 risulti abilitata al tempo 0, e che essa spari al tempo (minimo) 2, allora si può verificare che tra le due transizioni che si abilitano al tempo 2, e cioè t2 e t3, solo t3 spara in quanto essa è costretta a farlo tra i tempi 2+4=6 e 2+7=9, mentre t2 non può sparare prima dell’istante 2+9=11. Dunque spara certamente t3 e con questo disabilita t2 che non può più sparare.

Figura 10 Una rete MF Una rete MF è una sestupla MF=(P,T,F,W,M0,SI) in cui le prime cinque componenti definiscono una classica rete P/T. SI (Static Interval) denota una funzione per il mapping statico di intervalli temporali alle transizioni: SI: T→Q+x(Q+∪{∞}) Cioè: ∀t∈T, SI(t)=[αS,βS], αS≤βS.

t1 [2,5]

[4,7][9,14] t2 t3

p1

p2 p3

p5p4

143

La quantità αS è detta anche Earliest Firing Time (EFT), mentre βS è il Latest Firing Time (LFT) della transizione. Si definisce stato di una rete MF una tupla S=(M,I) dove M è un marking della rete, I un vettore di possibili tempi di sparo delle transizioni abilitate in M: I:T→(ℜ+x(ℜ+∪{∞})). È possibile in modo ovvio esprimere la situazione di una transizione t abilitata in M, M[t>, anche come S[t>, ossia t è abilitata nello stato S. Lo stato iniziale di una rete MF è S0=(M0,I0), dove M0 è la marcatura iniziale della rete, I0 è il vettore iniziale dei possibili intervalli di sparo, cosi definito: ∀t∈T, se S0[t>, allora I0(t)=SI(t). Nello stato S=(M,I) una transizione t è sparabile (firable) al tempo θ∈ℜ+, e si scrive S[t>θ, se solo se: a) t è abilitata in S, S[t> b) θ appartiene all’intervallo di sparo, ossia θ ∈I(t)=[α,β] c) nessun’altra transizione ti≠t spara prima di t: S[ti> ⇒ θ≤βi, essendo I(ti)=[αi,βi]. Il punto c) implica che una qualsiasi transizione abilitata t con intervallo [a,b] deve sparare entro b, se nessun’altra transizione spara prima che disabilita t. Si nota ancora, che t può sparare ad un tempo appartenente al suo intervallo e minore o uguale al minimo degli upper bound degli intervalli delle transizioni abilitate in S. Lo scatto di una transizione t sparabile al tempo θ nello stato S=(M,I), cambia istantaneamente lo stato in S’=(M’,I’) dove M’ è definito dalla regola di scatto delle reti classiche P/T: ∀p∈P, M’(p)=M(p)-W(p,t)+W(t,p) se p è coinvolto nello scatto di t, M’(p)=M(p) altrimenti. il nuovo vettore I’ degli intervalli di sparo è calcolabile da I in tre passi come segue: 1) si eliminano da I le transizioni che si disabilitano a seguito dello sparo di t. Queste transizioni formano l’insieme Disabled(S,t) 2) si shiftano a sinistra di θ tutti gli intervalli relativi a transizioni che erano abilitate in M e restano abilitate in M’. Queste transizioni definiscono l’insieme Shifted(S,t). Detta tj una transizione in Shifted(S,t) si ha:

144

I’(tj)=[max(0,αj-θ), βj-θ] Proprio a causa delle operazioni di shift, gli intervalli di sparo, durante l’evoluzione di una rete MF, sono intervalli dinamici per distinguerli dagli intervalli statici attributi dalla specificazione 3) si assegnano gli intervalli statici [αi

S,βiS] a quelle transizioni ti che erano

disabilitate in M ma che si abilitano in M’. Queste transizioni formano l’insieme Enabled(S,t). Detto Empty(S,t)={ti∈T | not S[ti>), è possibile verificare le seguenti proprietà: Shifted(S,t)∩Enabled(S,t)=∅ Shifted(S,t)∩Disabled(S,t)=∅ Shifted(S,t)∩Empty(S,t)=∅ Enabled(S,t)∩Empty(S,t)=∅ Shifted(S,t)∪Enabled(S,t)∪Empty(S,t)=T Spesso, in letteratura, una rete MF viene studiata nell’ipotesi che sussista, di momento in momento, al più un solo enabling per transizione (safe net). Tutto ciò evita la questione semantica di dover specificare il comportamento di una transizione multiplamente abilitata al tempo τ. Come nel caso delle reti temporizzate per scopi di simulazione, due soluzioni sono possibili: • semantica single-server– la transizione spara i suoi enabling in successione

temporale, vale a dire se il primo spara al tempo θ, il secondo potrà avvenire con riferimento alla finestra [α+θ,β+θ] che è re-interpretata da capo dopo ogni sparo, etc.

• semantica multiple-server (o infinite-server): tutti gli enabling possono sparare nell’ambito della stessa finestra corrente di sparo, con i tempi di sparo dei vari enabling che ovviamente sono non decrescenti.

In realtà, alcune “sottigliezze” semantiche accompagnano l’infinite server, in particolare la possibilità che più finestre temporali possano essere associate ai vari enablings della transizione, per cui lo sparo propone il dilemma di quale finestra utilizzare per prima. Infatti, se una transizione t abilitata al tempo τ, ad es. con un solo enabling, non scatta ma viene preceduta da un’altra transizione che genera token in grado di creare qualche altro enabling per t, allora il vecchio enabling è regolato dall’intervallo dinamico, il nuovo da quello statico. Per evitare queste situazioni, si preferisce spesso la strategia single-server o si considerano reti in cui le transizioni ammettono in ogni momento al più un solo enabling. Si osserva, infine, che nella definizione originale di Merlin e Farber, l’intervallo statico è definito da una coppia di numeri reali. Altri autori, come riportato nelle

145

definizioni precedenti, assumono che gli estremi dell’intervallo statico possano essere razionali, anche se poi i tempi di sparo sono reali.

ALBERO DI RAGGIUNGIBILITÀ E PROBLEMATICHE DI ANALISI Una rete MF è utile per analisi di temporizzazione di sistemi di controllo in tempo reale, es. per verificare proprietà end-to-end (bounded liveness o deadline), es. “succede sempre che dall’arrivo di un evento esterno, il sistema reagisce ad esso entro un intervallo di tempo prestabilito?”, o di sicurezza (safety) “è possibile che le luci dei due semafori ad un incrocio possano valere verde contemporaneamente?”, etc. Per far questo, oltre che ispezionare “a mano” un modello MF, sono utili strumenti in grado di costruire l’albero di raggiungibilità anche in presenza del tempo. Ovviamente, la cosa è complicata, dal momento che i tempi di sparo associati alla sequenza di sparo che determina una certa marcatura, possono essere infiniti a causa degli intervalli associati alle transizioni e al modello denso di tempo adottato dalle reti MF. Per rendere compatto l’albero di raggiungibilità, è pratica comune riunire un gruppo di stati in una singola classe di stati, ossia partizionare l’insieme degli stati in classi di equivalenza. Si parla di classe di stati (state class) per denotare un insieme di stati caratterizzati da una stessa marcatura, determinata da una certa sequenza di sparo. Una classe di stati C è una coppia C=(M,D) dove M è una marcatura, D un dominio di sparo. C è rappresentativa di tutti gli stati che si possono generare sparando a tutti i possibili tempi ammissibili le transizioni della sequenza di sparo che dalla marcatura iniziale porta ad M. Il dominio di sparo D è l’unione dei domini di sparo di tutti gli stati rappresentati da C. Una transizione t abilitata in M può sparare, come si è visto in precedenza, sino ad un tempo minore o uguale del minimo degli upper bound dei domini di sparo delle altre transizioni abilitate in M. Infatti, stante il carattere di semantica forte dello sparo nelle reti MF, una di queste altre transizioni tk, al più al suo upper bound, deve scattare e dunque se scatta potrebbe influenzare l’abilitazione di t. Per capire in che modo un albero di raggiungibilità possa essere costruito in termini di classi di stati, è utile riferirsi al semplice esempio di Figura 11 che mostra due transizioni concorrenti entrambe abilitate al tempo 0 nella marcatura iniziale.

Figura 11 Una semplice rete MF Inizialmente (ossia al tempo 0) esiste la classe C0=(M0,D0), in cui M0=(1100) e D0 è definito dall’unione degli intervalli statici di t1 e t2 entrambe abilitate: D0(t1)=[2,4],

t1 [2,4]

p1

p3

p2

p4

t2 [3,5]

146

D0(t2)=[3,5]. Una qualsiasi transizione tra t1 e t2 può sparare per prima. In particolare, t1 può sparare tra 2 e 4 (il minimo degli upper bound o LFT delle transizioni abilitate), mentre t2 può sparare tra 3 e 4. In realtà, siccome le transizioni sono indipendenti, nulla impedisce a t2 di sparare anche al tempo 5. Quando si computa il minimo upper bound, ci si riferisce ad un tempo prima del quale nessun’altra delle transizioni abilitate è forzata a sparare prima. Se spara t1, si genera una nuova classe C1=(M1,D1) in cui M1=(0110) e D1(t2)=[0,3]. Per comprendere perché il dominio D1(t2) sia [0,3] è utile osservare che il tempo di sparo di t1 è scelto non deterministicamente nell’intervallo [2,4]. L’albero di raggiungibilità riflette il non determinismo: pertanto, se (considerando solo i valori interi dell’intervallo di t1) l’istante di sparo θ1 di t1 fosse 2, allora la finestra dinamica di t2 (che rimane abilitata) si modificherebbe in [1,3], se θ1 fosse 3, allora la finestra di t2 cambierebbe in [0,2], se θ1 fosse 4, la finestra di t2 diventerebbe [0,1]. Stante il non determinismo nel tempo di sparo di t1, si può riassumere la finestra dei possibili tempi di sparo che rimangono per t2 (da qui il significato di dominio di sparo) proprio con [0,3], che ingloba gli intervalli [1,3] [0,2] e [0,1] (si prende il minimo dei tempi EFT ed il massimo degli LFT di tutti gli intervalli). Dunque il tempo di sparo di t2, a partire dalla nuova classe, cadrà nella finestra [0,3]. Attenzione: questa finestra non è l’intervallo dinamico di t2 nella nuova situazione. Quest’ultimo sarà concretamente stabilito dal valore (specifico) di θ1 e dalla regola di scorrimento a sinistra vista precedentemente. In generale, il dominio di sparo associato ad una transizione tk che rimane abilitata nel passaggio da una classe Ci a una classe Cj a seguito dello scatto di tj, è calcolabile come: [max(0,EFTi(tk)-LFTi(tj)), LFTi(tk)-EFTi(tj)] ossia, l’estremo inferiore è determinato dal caso peggiore che tj sia scattata al suo tempo ultimo; l’estremo superiore che sia scattata al suo tempo minimo (EFT). La notazione EFTi(tk) indica il tempo EFT di tk nella classe Ci, etc. Se, invece, a partire da C0 scatta prima la t2, si raggiunge la classe C2=(M2,D2) dove M2=(1001) e D2(t1)=[0,1]. Infatti, se t2 scatta al tempo 3, resterebbe solo una unità di tempo a t1 per scattare a sua volta; se t2 scattasse al tempo 4, allora a t1 non resterebbe alcun altro tempo di sparo se non scattare anch’essa al tempo 4. Dunque il dominio di sparo di t1 in D2 è rappresentato dall’intervallo [0,1]. A partire dalla classe C1 può scattare solo la t2. Dalla classe C2 solo la t1. In ogni caso si ottiene la classe C3=(M3,D3) in cui M3=(0011) (marcatura finale di deadlock) e D3 consiste dell’insieme vuoto ∅. Tutto l’albero di raggiungibilità è mostrato in Figura 12. Naturalmente, se in una classe si abilita una nuova transizione, il suo dominio di sparo coincide con il suo intervallo statico. Le classi di stato utilizzate in Figura 12 sono dette classiche. Esse hanno il vantaggio di mostrare come cambiano i domini di sparo. Tuttavia soffrono di limitazioni nel

147

momento in cui si cerchi di derivare dall’albero di raggiungibilità informazioni di time span ossia di distanza temporale tra gli istanti in cui due classi sono visitate, ad es. una classe finale è raggiunta a partire da un’altra o addirittura dalla classe iniziale C0.

Figura 12 Albero di raggiungibilità della rete MF di Figura 11 Ad esempio, sommando gli intervalli di cui ai domini di sparo, si potrebbe esser “tentati” di dire che la sequenza di sparo t1t2 (quella a sinistra in Figura 12) consente di raggiungere la marcatura finale M3 in un tempo compreso nella finestra [2,4]+[0,3]=[2,7]. Similmente, la sequenza t2t1 porterebbe la rete da M0 ad M3 in un tempo appartenente alla finestra [3,5]+[0,1]=[3,6]. Tuttavia, entrambe le conclusioni sono errate. Infatti, essendo le due transizioni t1 e t2 indipendenti e concorrenti, si può affermare con certezza che M3 non sarà raggiunta prima di 3 (EFT di t2) e nel caso peggiore sarà raggiunta al tempo 5 (LFT di t2) allorquando sicuramente anche la t1 sarà scattata. Dunque la finestra effettiva degli istanti di arrivo alla classe C3 è [3,5].

CLOCK-STAMPED STATE CLASSES Wang ed altri hanno proposto una diversa definizione di classi di stato e quindi di costruzione dell’albero di raggiungibilità, che meglio si presta ad analisi di temporizzazione. E’ utile osservare che nelle classi di stato classiche, i domini di sparo sono relativi all’istante (non deterministico) in cui la classe è raggiunta. Proprio da questa nozione relativa nascono le difficoltà a compiere analisi end-to-end di temporizzazione. La nuova nozione di classe di stati è detta Clock-stamped state class (CS-class). In pratica, ad ogni classe si associa ora una finestra temporale che esprime l’intervallo di tempi globali (cioè relativi all’istante iniziale di funzionamento della rete) in cui la

C0: M0=(1100) D0: D0(t1)=[2,4] D0(t2)=[3,5]

C1: M1=(0110) D1: D1(t2)=[0,3]

C2: M2=(1001) D2: D2(t1)=[0,1]

C3: M3=(0011) D3: ∅

t1 t2

t1 t2

148

classe è visitata. In più, anche gli intervalli di sparo delle transizioni abilitate sono ridefiniti in modo da essere essi stessi globali. Una clock-stamped state class C è una tripla C=(M,D,ST) in cui ST è il clock stamp della classe. Nella classe iniziale C0, ST0 è l’intervallo [0,0] e, come prima, il dominio D0 è costituito dagli intervalli statici delle transizioni abilitate in M0. Sono utili le definizioni che seguono. Una transizione tf è sparabile (firable) in una classe Ch, se EFTh(tf) è minore o uguale al minimo LFT di tutte le transizioni abilitate in Ch. Sia Fr(Ch) l’insieme delle transizioni sparabili di Ch. Si definisce MLFT(Ch)=min{ LFTh(tk), tk∈Fr(Ch) } MLFT è il minimo degli upper bound degli intervalli di tutte le transizioni sparabili in Ch. Se a partire da Ch spara una transizione tk∈Fr(Ch), allora si raggiunge una nuova classe Ck=(Mk,Dk,STk). Il clock stamp di Ck è dato da: STk=ST(Ck)=[EFTh(tk),MLFT(Ch)] Riguardo alle modifiche indotte al dominio di sparo, sussiste quanto segue: Se la transizione tf era abilitata in Ch e rimane abilitata in Ck, allora il suo intervallo di sparo nel nuovo dominio Dk cambia in: Dk(tf)=[max(EFTh(tf),EFTh(tk)), LFTh(tf)] ossia, l’estremo inferiore dell’intervallo di tf in Dk è aggiustato in modo da non essere pregresso rispetto all’estremo inferiore della transizione che ha sparato tk. Se invece la transizione tf era disabilitata in Ch e si abilita in Ck, allora essa riceve come intervallo di sparo: Dk(tf)=SI(tf)+ST(Ck) dove SI(tf) rappresenta al solito l’intervallo statico di sparo associato a tf. Questa stessa regola, governa anche l’aggiornamento dell’intervallo di tk, ossia la transizione che ha portato nella nuova classe Ck, qualora essa risulti ancora abilitata in Ck. In altre parole, sussiste il modello semantico single-server, per cui una transizione multiplamente abilitata spara un solo enabling per volta. Dopo ogni sparo, ogni enabling è considerato come uno appena formatosi. Ovviamente, se tf era abilitata in Ch ma si disabilita a causa dello sparo di tk, in Dk scompare il suo intervallo di sparo.

149

Le regole di sparo richiamate di sopra sono esemplificate nella costruzione del nuovo albero di raggiungibilità secondo Wang ed altri in Figura 13, sempre con riferimento alla rete MF di Figura 11.

Figura 13 Albero di raggiungibilità della rete MF di Figura 11 con classi CS Poiché le informazioni di clock stamp ST sono globali, risulta ora dall’albero di Figura 13, che la marcatura finale (0011) è raggiunta nella sequenza t1t2 in un tempo in [3,5], e nella sequenza t2t1 in un tempo in [3,4]. Complessivamente, si può dire che partendo dalla marcatura iniziale (1100), la marcatura finale (0011) non è raggiunta prima di 3 unità di tempo ma sicuramente entro 5 unità di tempo. Il risultato è quello corretto che ci si aspettava.

ESERCIZIO Data la rete MF di Figura 14, costruire il suo albero di raggiungibilità secondo le classi di stato classiche e quindi utilizzando classi CS. Verificare se la marcatura finale [0,0,0,0,0,1] è raggiungibile a partire dalla marcatura iniziale [1,1,0,0,0,0] entro 150 unità di tempo.

OSSERVAZIONI CONCLUSIVE Affinché si possano compiere analisi di temporizzazione, il numero delle classi di stato deve essere finito. Diversamente l’albero di raggiungibilità non è costruibile per via dell’esplosione degli stati. La finitezza del numero delle classi è in relazione alla limitatezza della rete. Purtroppo, in una rete MF le proprietà di raggiungibilità e limitatezza non sono decidibili. Pertanto, il progettista deve considerare attentamente gli aspetti di limitatezza di un modello. Alcune condizioni sufficienti sulla limitatezza sono proposte da Berthomieu e Diaz.

C0: ST0: [0,0] M0=(1100) D0: D0(t1)=[2,4]

D0(t2)=[3,5]

C1: ST1: [2,4] M1=(0110) D1: D1(t2)=[3,5]

C2: ST2: [3,4] M2=(1001) D2: D2(t1)=[3,4]

C3: ST3: [3,5] M3=(0011) D3: ∅

t1 t2

t1 t2

C4: ST4: [3,4] M4=(0011) D4: ∅

150

Figura 14 Un altro esempio di rete MF

Più avanti nel corso verrà presentato un approccio all’analisi di reti di Petri di Merlin e Farber basato su una traduzione preliminare di un modello sui Timed Automata che rappresentano un formalismo più potente. L’approccio, applicato ben inteso a sistemi di non elevata dimensione, permette l’analisi completa funzionale e temporale mediante verifica esaustiva (model checking) di proprietà consultando lo spazio degli stati del modello.

RIFERIMENTI P. Merlin, Farber D. Recoverability of communication protocols-implication of a theoretical study. IEEE Transactions on Software Engineering, Vol. 15, nr. 7, pp. 1036-1045, 1976. C. Ghezzi, D. Mandrioli, S. Morasca, M. Pezzè. A unified high-level Petri net formalism for timed-critical systems. IEEE Transactions on Software Engineering, Vol. 17, nr. 2, pp.160-172, 1991. B. Berthomieu, M. Diaz. Modeling and verification of time-dependent systems using Time Petri Nets. IEEE Transactions on Software Engineering, Vol. 17, nr. 3, pp.259-273, 1991. J. Wang, Y. Deng, G. Xu. Reachability analysis of real-time systems using Time Petri Nets. IEEE Transactions on Systems, Man and Cybernetics, Vol. 30, nr. 5, pp. 725-736, October, 2000. J.J.P. Tsai, S.J. Yang, Y.H. Chang. Timing constraint Petri nets and their applications to schedulability analysis of real-time system specification. IEEE Transactions on Software Engineering, Vol. 21, nr. 1, pp. 32-49, 1991.

t1: [30,50]

t3: [40,90] t4: [20,40]

t2: [10,70]t5: [10,30]

p2

p1

p4

p6

p5

p3