421 lines
18 KiB
Org Mode
Executable file
421 lines
18 KiB
Org Mode
Executable file
#+TITLE: Esercizio P/N
|
|
#+AUTHOR: Francesco Mecca
|
|
#+EMAIL: me@francescomecca.eu
|
|
#+LANGUAGE: en
|
|
#+LaTeX_CLASS: article
|
|
#+LaTeX_HEADER: \linespread{1.25}
|
|
#+LaTeX_HEADER: \usepackage{pdfpages}
|
|
#+LaTeX_HEADER: \usepackage{comment}
|
|
|
|
#+EXPORT_SELECT_TAGS: export
|
|
#+EXPORT_EXCLUDE_TAGS: noexport
|
|
#+OPTIONS: H:2 toc:nil \n:nil @:t ::t |:t ^:{} _:{} *:t TeX:t LaTeX:t
|
|
#+STARTUP: showall
|
|
* Rete A
|
|
M master identici e S slave identici di tipo 1.
|
|
|
|
#+CAPTION: Modello della reteA
|
|
[[./reteA.jpg]]
|
|
|
|
La figura rappresenta la rete di Petri P/T dell'esercizio A. Il master
|
|
è modellato dai posti M0, M1, M2, M3 e dalle transizioni
|
|
/Azione\under{}Locale/, /Richiesta\under{}Servizio/, /Attesa\under{}Elaborazione/ e /Reset\under{}M/
|
|
Lo slave è modellato dai posti /S0/, /S1_a/, /S1_b/, /S2_a/, /S2_b/ e
|
|
/S3/ e dalle transizioni /Inizio\under{}Servizio/, /Azione\under{}Locale\under{}S_a/,
|
|
/Azione\under{}Locale\under{}S_b/, /Fine\under{}Servizio/ e /Reset\under{}S/. La richiesta del servizio
|
|
verso lo slave e` gestita attraverso due buffer, posti /Buffer\under{}Input/ e
|
|
posto /Buffer\under{}Output/.
|
|
|
|
** Risultati
|
|
Nella tabella vengono mostrate il numero di archi e di nodi al variare
|
|
dei parametri M e S. Le cifre sono indicative dell'aumentare della
|
|
dimensione dello spazio degli stati proporzionalmente al numero di
|
|
marcature.
|
|
|
|
| master, slaves | Nodi | Archi |
|
|
|----------------+---------+----------|
|
|
| 1, 1 | 14 | 19 |
|
|
| 2, 2 | 94 | 222 |
|
|
| 3, 3 | 426 | 334 |
|
|
| 4, 4 | 1500 | 5610 |
|
|
| 5, 5 | 4422 | 18720 |
|
|
| 6, 6 | 11418 | 52998 |
|
|
| 7, 7 | 26598 | 132594 |
|
|
| 8, 8 | 57057 | 301158 |
|
|
| 9, 9 | 114400 | 632775 |
|
|
| 10, 10 | 216788 | 1246960 |
|
|
| 11, 11 | 391612 | 2328612 |
|
|
| 12, 12 | 678912 | 4153916 |
|
|
| 13, 13 | 1135668 | 7123272 |
|
|
| 14, 14 | 1841100 | 11802420 |
|
|
| 15, 15 | 2903124 | 18973020 |
|
|
** Considerazioni su Fork/Join
|
|
Il modello non garantisce che avvenga il join di due processi dello
|
|
stesso padre quando la marcatura degli slave e` maggiore di 2.
|
|
Si puo` garantire che avvenga il join di due processi forkati dallo
|
|
stesso padre attraverso differenti strutture slaves o usando reti WN.
|
|
** Riduzione
|
|
Una rete di petri puo` essere ridotta usando le seguendi tecniche:
|
|
- fusione
|
|
- eliminazione
|
|
- rimozione dei loop
|
|
Nelle figure vengono mostrate alcune fasi di riduzione della rete in
|
|
analisi.
|
|
#+CAPTION: eliminazione di posti identici
|
|
[[./riduzione/eliminazione1.jpg]]
|
|
#+CAPTION: fusione di posti
|
|
[[./riduzione/fusione1.jpg]]
|
|
#+CAPTION: fusione di transizioni
|
|
[[./riduzione/fusione2.jpg]]
|
|
#+CAPTION: fusione di transizioni e posti
|
|
[[./riduzione/fusione3.jpg]]
|
|
\clearpage
|
|
** P e T invarianti
|
|
Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi
|
|
|
|
#+CAPTION: T-semiflows
|
|
[[./semiflowsAT.jpg]]
|
|
#+CAPTION: P-semiflows
|
|
[[./semiflowsAP.jpg]]
|
|
\clearpage
|
|
|
|
Gli P-semiflussi sono i seguenti:
|
|
| • S0 + S1_{a} + S2_{a} + S3
|
|
| • S0 + S1_{b} + S2_{b} + S3
|
|
| • M0 + M1 + M2 + M3
|
|
| • S1_{a} + S2_{a} + Buffer\under{}output + Buffer\under{}input + M0 + M1 + M3
|
|
| • S1_{b} + S2_{b} + Buffer\under{}output + Buffer\under{}input + M0 + M1 + M3
|
|
Il T-semiflusso e` il seguente:
|
|
| • Inizio\under{}servizio + azione\under{}locale\under{}sa + azione\under{}locale\under{}sb +
|
|
| \space{}\space{} Fine\under{}servizio + azione\under{}locale\under{}m + Richiesta\under{}servizio +
|
|
| \space\space Attesa\under{}elaborazione + Reset\under{}M + Reset\under{}S
|
|
e dato che comprende tutte le transizioni, il sistema rispetta la
|
|
proprieta` di liveness.
|
|
Dato che la reteA e` interamente coperta dagli P-semiflussi, possiamo
|
|
affermare che la rete sia bounded.
|
|
Gli P-semiflussi ci permettono di ricavare i seguenti invarianti
|
|
lineari relativi ai marking /m/:
|
|
| • m[S0] + m[S1ₐ] + m[S2ₐ] + m[S3] = 1
|
|
| • m[S0] + m[S1_{b}] + m[S2_{b}] + m[S3] = 1
|
|
| • m[M0] + m[M1] + m[M2] + m[M3] = 1
|
|
| • m[S1ₐ] + m[S2ₐ] + m[Buffer_output] + m[Buffer_input] + m[M0] + m[M1] + m[M3] = 1
|
|
| • m[S1_{b}] + m[S2_{b}] + m[Buffer_output] + m[Buffer_input] + m[M0] + m[M1] + m[M3] = 1
|
|
Dato che ∀p ∈ P, m[p] ≥ 0 possiamo affermare, a partire dalle
|
|
precedenti uguaglianze che:
|
|
- ogni posto nei seguenti insieme e` in mutua esclusione con gli
|
|
elementi dello stesso insieme:
|
|
| {S0, S1ₐ, S2ₐ, S3}
|
|
| {S0, S1_{b}, S2_{b}, S3}
|
|
| {M0, M1, M2, M3}
|
|
| {S1ₐ, S2ₐ, Buffer_output, Buffer_input, M0, M1, M3}
|
|
| {S1_{b}, S2_{b}, Buffer_output, Buffer_input, M0, M1, M3}
|
|
- ∀pᵢ∈P, m[pᵢ]≤1 (bounds)
|
|
- dato che i posti che sono gli unici /enablers/ di una transizione
|
|
sono i seguenti:
|
|
| S1ₐ, S1_{b}, S3, M0, M1, M3
|
|
e quindi possiamo provare a dimostrare l'assenza di deadlock
|
|
partendo dagli invarianti lineari relativi ai marking:
|
|
| • m[S0] + m[S2ₐ] = 1
|
|
| • m[S0] + m[S2_{b}] = 1
|
|
| • m[M2] = 1
|
|
| • m[S2ₐ] + m[Buffer_output] + m[Buffer_input] = 1
|
|
| • m[S2_{b}] + m[Buffer_output] + m[Buffer_input] = 1
|
|
Dato che M2 e` marcata, per far si` che /attesa_elaborazione/ non
|
|
venga abilitata:
|
|
| m[Buffer_output] = 0
|
|
Inoltre per far si` che //Inizio\under{}Servizio// e //Fine\under{}Servizio// non vengano abilitate:
|
|
| • m[Buffer_input] + M[S0] ≤ 1
|
|
| • m[S2ₐ] + m[S2_{b}] ≤ 1
|
|
Riassumendo, il sistema e` il seguente:
|
|
| • m[S0] + m[S2ₐ] = 1
|
|
| • m[S0] + m[S2_{b}] = 1
|
|
| • m[S2ₐ] + m[Buffer_input] = 1
|
|
| • m[S2_{b}] + m[Buffer_input] = 1
|
|
| • m[Buffer_input] + M[S0] ≤ 1
|
|
| • m[S2ₐ] + m[S2_{b}] ≤ 1
|
|
che per la legge di conservazione dei token, non puo` essere
|
|
soddisfatto. Quindi nel sistema non vi e` la possibilita` di deadlock.
|
|
|
|
* Rete B
|
|
M master identici, uno slave di tipo 1 e uno slave di tipo 1 scelti
|
|
liberamente dai master.
|
|
|
|
#+CAPTION: Modello della reteB
|
|
[[./reteB.jpg]]
|
|
|
|
La figura rappresenta la rete di Petri P/T dell'esercizio B. Il master
|
|
è modellato dai posti /M0/, /M1/, /M2/, /M3/ e dalle transizioni
|
|
/Azione\under{}Locale/, /Richiesta\under{}Servizio/,
|
|
/Attesa\under{}Elaborazione/ e /Reset\under{}M/ Lo slave di tipo 1 è
|
|
modellato dai posti /S0/, /S1_a/, /S1_b/, /S2_a/, /S2_b/ e S3 e dalle
|
|
transizioni /Inizio\under{}Servizio/,
|
|
/Azione\under{}Locale\under{}S_a/, /Azione\under{}Locale\under{}S_b/,
|
|
/Fine\under{}Servizio/ e /Reset\under{}S/. Lo slave di tipo 2 è
|
|
modellato dai posti /R0/, /R1_a/, /R1_b/, /R2_a/, /R2_b/ e /R3/ e dalle
|
|
transizioni /Inizio\under{}Servizio\under{}R/,
|
|
/Azione\under{}Locale\under{}R/, /Fine\under{}Servizio/ e /Reset\under{}R/. La
|
|
richiesta del servizio verso lo slave scelto e` gestita attraverso due
|
|
buffer, /FreeChoice/ e /Risultato/.
|
|
\clearpage
|
|
|
|
|
|
** Risultati
|
|
Al variare del marking del master:
|
|
| master, slaves | Stati | Archi |
|
|
|----------------+--------+--------|
|
|
| 1, 2 | 40 | 76 |
|
|
| 2, 2 | 204 | 544 |
|
|
| 3, 2 | 728 | 2400 |
|
|
| 4, 2 | 2072 | 7896 |
|
|
| 5, 2 | 5040 | 21336 |
|
|
| 6, 2 | 10920 | 50064 |
|
|
| 7, 2 | 21648 | 105648 |
|
|
| 8, 2 | 39996 | 205260 |
|
|
| 9, 2 | 69784 | 373252 |
|
|
| 10, 2 | 116116 | 642928 |
|
|
|
|
Parametrizzando anche il marking sugli slaves (R+S):
|
|
| master, slaves | Stati | Archi |
|
|
|----------------+---------+----------|
|
|
| 1, 2 | 40 | 76 |
|
|
| 2, 2 | 204 | 544 |
|
|
| 4, 4 | 7265 | 32674 |
|
|
| 6, 6 | 113464 | 664234 |
|
|
| 8, 8 | 1073226 | 7405654 |
|
|
| 10, 10 | 7212128 | 55762000 |
|
|
|
|
** Considerazioni su Fork/Join
|
|
Lo slave di tipo 1 processa una sola richiesta alla volta.
|
|
Il master in attesa del risultato (M2) potrebbe ricevere il risultato
|
|
di un lavoro richiesto da un altro master.
|
|
|
|
** P e T invarianti
|
|
Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi
|
|
|
|
#+CAPTION: T-semiflows
|
|
[[./semiflowsBT.jpg]]
|
|
#+CAPTION: P-semiflows
|
|
[[./semiflowsBP.jpg]]
|
|
Gli P-invarianti sono i seguenti:
|
|
| • S0 + S1_a + S2_a + S3
|
|
| • S0 + S1_b + S2_b + S3
|
|
| • R0 + R1 + R2 + R3
|
|
| • M0 + M1 + M2 + M3
|
|
| • S1_a + S2_a + R1 + R2 + M0 + M1 + M3 + Freechoice + P0 + P1 + Risultato
|
|
| • S1_b + S2_b + R1 + R2 + M0 + M1 + M3 + Freechoice + P0 + P1 + Risultato
|
|
Gli T-invarianti sono i seguenti:
|
|
| • Inizio\under{}servizio\under{}R + azione\under{}locale\under{}R +
|
|
| \space\space Fine\under{}servizio\under{}R + Reset\under{}R + azione\under{}locale\under{}m + Richiesta\under{}servizio +
|
|
| \space\space Attesa\under{}elaborazione + Reset\under{}M + Scelta\under{}2
|
|
| • Inizio\under{}servizio\under{}S + azione\under{}locale\under{}sa + azione\under{}locale\under{}sb +
|
|
| \space\space Fine\under{}servizio\under{}S + Reset\under{}s + azione\under{}locale\under{}m + Richiesta\under{}servizio +
|
|
| \space\space Attesa\under{}elaborazione + Reset\under{}m + Scelta\under{}1
|
|
Dato che ci sono due semiflussi, ognuno relativo alle transizioni dei
|
|
due diversi slaves, c'e` possibilita` di starvation.
|
|
Possiamo infatti immaginare una traccia di esecuzione in cui il master
|
|
in seguito a FreeChoice sceglie sempre il primo slave.
|
|
Questo non succederebbe in un sistema fair, ovvero se si obbliga
|
|
un'automa che entra in uno stato infinite volte ad eseguire tutte le
|
|
possibili transizioni da quello stato.
|
|
In tal caso non avremmo starvation e la proprieta` di liveness sarebbe rispettata.
|
|
|
|
Dato che la reteB e` interamente coperta dagli P-semiflussi, possiamo
|
|
affermare che la rete sia bounded.
|
|
Dimostriamo invece che la rete non ha possibilita` di deadlock.
|
|
| • m[S0] + m[S1_a] + m[S2_a] + m[S3] = 1
|
|
| • m[S0] + m[S1_{b}] + m[S2_{b}] + m[S3] = 1
|
|
| • m[R0] + m[R1] + m[R2] + m[R3] = 1
|
|
| • m[M0] + m[M1] + m[M2] + m[M3] = 1
|
|
| • m[S1_a] + m[S2_a] + m[R1] + m[R2] + m[M0] + m[M1] +
|
|
| \space{}\space{} m[M3] + m[Freechoice] + m[P0] + m[P1] + m[Risultato] = 1
|
|
| • m[S1_{b}] + m[S2_{b}] + m[R1] + m[R2] + m[M0] + m[M1] +
|
|
| \space{}\space{} m[M3] + m[Freechoice] + m[P0] + m[P1] + m[Risultato] = 1
|
|
|
|
I posti che sono gli unici enablers di una sola transizione sono:
|
|
| M0, M1, M3, R1, R2, R3, FreeChoice, S1ₐ, S1_{b}, S3
|
|
Gli invarianti lineari dei marking diventano:
|
|
| • m[S0] + m[S2_a] = 1
|
|
| • m[S0] + m[S2_{b}] = 1
|
|
| • m[R0] = 1
|
|
| • m[M2] = 1
|
|
| • m[S2_a] + m[P0] + m[P1] + m[Risultato] = 1
|
|
| • m[S2_{b}] m[P0] + m[P1] + m[Risultato] = 1
|
|
Dati i marking in R0 e M2, per far si` che //Inizio\under{}Servizio/_R/,
|
|
//Attesa\under{}Elaborazione//, //Fine\under{}Servizio/ₛ/ e //Inizio\under{}Servizio/ₛ/ non vengano abilitati:
|
|
| • m[P0] = 0
|
|
| • m[Risultato] = 0
|
|
| • m[S2ₐ] + m[S2_{b}] ≤ 1
|
|
| • m[P1] + m[S0] ≤ 1
|
|
Il sistema si riduce a:
|
|
| • m[S0] + m[S2_a]= 1
|
|
| • m[S0] + m[S2_{b}] = 1
|
|
| • m[S2_a] + m[P1] = 1
|
|
| • m[S2_{b}] + m[P1] = 1
|
|
| • m[S2ₐ] + m[S2_{b}] ≤ 1
|
|
| • m[P1] + m[S0] ≤ 1
|
|
che non puo` essere soddisfatto per la legge di conservazione dei token.
|
|
|
|
* Rete C
|
|
Due master identici, uno slave di tipo 1 e uno slave di tipo 1 scelti
|
|
liberamente dai master.
|
|
|
|
#+CAPTION: Modello della reteC
|
|
[[./reteC.jpg]]
|
|
|
|
La figura rappresenta la rete di Petri P/T dell'esercizio C. Il master
|
|
è modellato dai posti M0, M1, M2, M3 e dalle transizioni
|
|
Azione_Locale, /Richiesta\under{}Servizio/, /Attesa\under{}Elaborazione/ e /Reset\under{}M/
|
|
Lo slave di tipo 1 è modellato dai posti S0, S1_a, S1_b, S2_a, S2_b e
|
|
S3 e dalle transizioni /Inizio\under{}Servizio/, /Azione\under{}Locale\under{}S_a/,
|
|
/Azione\under{}Locale\under{}S_b/, /Fine\under{}Servizio/ e /Reset\under{}S/ (il secondo master e` una
|
|
copia del primo).
|
|
Lo slave di tipo 2 è modellato dai posti R0, R1_a, R1_b, R2_a, R2_b e
|
|
R3 e dalle transizioni /Inizio\under{}Servizio/_R, Azione_Locale_R, /Fine\under{}Servizio/ e Reset_R.
|
|
La richiesta del servizio
|
|
verso lo slave scelto e` gestita attraverso due buffer, posti
|
|
FreeChoice e Risultato.
|
|
** P e T invarianti
|
|
Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi
|
|
|
|
#+CAPTION: T-semiflows
|
|
[[./semiflowsCT.jpg]]
|
|
#+CAPTION: P-semiflows
|
|
[[./semiflowsCP.jpg]]
|
|
|
|
Gli P-invarianti sono i seguenti:
|
|
- S0 + S1ₐ + S2ₐ + S3
|
|
- S0 + S1_{b} + S2_{b} + S3
|
|
- R0 + R1 + R2 + R3
|
|
- M0 + M1 + M2 + M3
|
|
- copy_M0 + copy_M1 + copy_M2 + copy_M3
|
|
- S1ₐ + S2ₐ + R1 + R2 + M0 + M1 + M3 + Freechoice + P0 + P1 +
|
|
Risultato + copy_M0 + copy_M1 + copy_M3
|
|
- S1_{b} + S2_{b} + R1 + R2 + M0 + M1 + M3 + Freechoice + P0 + P1 +
|
|
Risultato + copy_M0 + copy_M1 + copy_M3
|
|
Dato che la reteC e` interamente coperta dagli P-semiflussi, possiamo
|
|
affermare che la rete sia bounded.
|
|
Gli P-semiflussi ci permettono di ricavare i seguenti invarianti
|
|
lineari relativi ai marking /m/:
|
|
| • m[S0] + m[S1ₐ] + m[S2ₐ] + m[S3] = 1
|
|
| • m[S0] + m[S1_{b}] + m[S2_{b}] + m[S3] = 1
|
|
| • m[R0] + m[R1] + m[R2] + m[R3] = 1
|
|
| • m[M0] + m[M1] + m[M2] + m[M3] = 1
|
|
| • m[copy_M0] + m[copy_M1] + m[copy_M2] + m[copy_M3] = 1
|
|
| • m[S1ₐ] + m[S2ₐ] + m[R1] + m[R2] + m[M0] +
|
|
| \space\space m[M1] + m[M3] + m[Freechoice] + m[P0] + m[P1] +
|
|
| \space\space m[Risultato] + m[copy_M0] + m[copy_M1] + m[copy_M3] = 1
|
|
| • m[S1_{b}] + m[S2_{b}] + m[R1] + m[R2] + m[M0] +
|
|
| \space\space m[M1] + m[M3] + m[Freechoice] + m[P0] + m[P1] +
|
|
| \space\space m[Risultato] + m[copy_M0] + m[copy_M1] + m[copy_M3] = 1
|
|
Gli spazi /enablers/ di una sola transizione sono i seguenti:
|
|
| R1, R2, R3, S1ₐ, S1_{b}, S3, Risultato, M0, M1, M3, copy_M0, copy_M1, copy_M3, FreeChoice
|
|
il sistema precedente diventa:
|
|
| • m[S0] + m[S2ₐ] = 1
|
|
| • m[S0] + m[S2_{b}] = 1
|
|
| • m[R0] = 1
|
|
| • m[M2] = 1
|
|
| • m[copy_M2] = 1
|
|
| • m[S2_{b}] + m[P0] + m[P1] = 1
|
|
| • m[S2_{a}] + m[P0] + m[P1] = 1
|
|
Dati i marking in R0 e M2 e copy_M2, per far si` che //Inizio\under{}Servizio/_R/,
|
|
//Attesa\under{}Elaborazione//, /copy_/Attesa\under{}Elaborazione//, //Fine\under{}Servizio/ₛ/ e //Inizio\under{}Servizio/ₛ/ non vengano abilitati:
|
|
| • m[P0] = 0
|
|
| • m[Risultato] = 0
|
|
| • m[S2ₐ] + m[S2_{b}] ≤ 1
|
|
| • m[P1] + m[S0] ≤ 1
|
|
Il sistema si riduce allo stesso della precedente rete B:
|
|
| • m[S0] + m[S2ₐ] = 1
|
|
| • m[S0] + m[S2_{b}] = 1
|
|
| • m[S2_{b}] + m[P1] = 1
|
|
| • m[S2_{a}] + m[P1] = 1
|
|
| • m[S2ₐ] + m[S2_{b}] ≤ 1
|
|
| • m[P1] + m[S0] ≤ 1
|
|
e non puo` essere soddisfatto per la legge di conservazione dei token.
|
|
|
|
Gli T-invarianti sono i seguenti:
|
|
- Inizio\under{}Servizioᵣ + Azione\under{}Locale + Fine\under{}Servizioᵣ + T3 +
|
|
azione\under{}localeₘ + Richiesta\under{}Servizio + Attesa\under{}Elaborazione + Reset\under{}M + Scelta₁
|
|
- Inizio\under{}Servizioₛ + Azione\under{}Locale_{sa} + Azione\under{}Locale_{sb} + Fine\under{}Servizioₛ + T3 +
|
|
azione\under{}localeₘ + Richiesta\under{}Servizio + Attesa\under{}Elaborazione +
|
|
Reset\under{}M + Scelta₁
|
|
- Inizio\under{}Servizioᵣ + Azione\under{}Locale + Fine\under{}Servizioᵣ + T3 + Scelta₂ +
|
|
copyₐzione\under{}localeₘ + copy\under{}Richiesta\under{}Servizio +
|
|
copy\under{}Attesa\under{}Elaborazione + copy\under{}Resetₘ
|
|
- Inizio\under{}Servizioₛ + Azione\under{}Locale_{sa} + Azione\under{}Locale_{sb} +
|
|
Fine\under{}Servizioₛ + Reset + Scelta₁ + copy\under{}azione\under{}localeₘ +
|
|
copy\under{}Richiesta\under{}Servizio + copy\under{}Attesa\under{}Elaborazione + copy\under{}Resetₘ
|
|
Come nella rete B, in assenza di fairness non possiamo rispettare la
|
|
condizione di liveness e c'e` possibilita` di starvation.
|
|
|
|
* Rete D
|
|
Due master identici, uno slave di tipo 1 e uno slave di tipo 1 scelti
|
|
associati ciascuno ad un master diverso.
|
|
|
|
#+CAPTION: Modello della reteD
|
|
[[./reteD.jpg]]
|
|
|
|
** P e T invarianti
|
|
Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi
|
|
|
|
#+CAPTION: T-semiflows
|
|
[[./semiflowsDT.jpg]]
|
|
#+CAPTION: P-semiflows
|
|
[[./semiflowsDP.jpg]]
|
|
\clearpage
|
|
|
|
Gli P-invarianti sono i seguenti:
|
|
| • S0 + S1ₐ + S2ₐ + S3
|
|
| • S0 + S1_{b} + S2_{b} + S3
|
|
| • R0 + R1 + R2 + R3
|
|
| • M0 + M1 + M2 + M3
|
|
| • S1ₐ + S2ₐ + M0 + M1 + M3 + Bufferₛ + Risultato
|
|
| • S1_{b} + S2_{b} + M0 + M1 + M3 + Bufferₛ + Risultato
|
|
| • M0₂ + M1₂ + M3₂
|
|
| • R1 + R2 + M0₂ + M1₂ + M3₂ + Buffer₂ + Risultato₂
|
|
Ai fini della dimostrazione dell'assenza di deadlock, possiamo notare
|
|
che lo slave di tipo 2 e` equivalente allo slave di tipo 1 se
|
|
si applicano due riduzioni alla rete (vengono fusi in un unico posto
|
|
S1ₐ-S2ₐ e S1_{b}-S2_{b}, poi eliminata la fork).
|
|
Inoltre i master sono indipendenti fra di loro e ciascuno rispetta l'assenza
|
|
di deadlock come gia` dimostrato nella rete A.
|
|
Gli T-invarianti sono i seguenti:
|
|
- Inizio\under{}Servizioₛ + azione_locale_{sa} + azione_locale_{sb} +
|
|
Fine\under{}Servizioₛ + Reset + azione_localeₘ + Richiesta\under{}Servizio +
|
|
Attesa\under{}Elaborazione + Resetₘ
|
|
- Inizio\under{}Servizioᵣ + Azione\under{}locale + Fine\under{}Servizioᵣ + T3
|
|
azione\under{}locale_{m2} + Richiesta\under{}Servizio₂ + Attesa\under{}Elaborazione₂ +
|
|
Reset_{m2}
|
|
Come nella rete B, in assenza di fairness non possiamo rispettare la
|
|
condizione di liveness e c'e` possibilita` di starvation.
|
|
|
|
** Decision Diagram
|
|
L'efficacia dei decision diagram sulla generazione dello stato degli
|
|
spazi dipende fortemente dall'ordine delle variabili.
|
|
Di seguito vengono mostrati i decision diagram usando per le
|
|
assegnazioni i seguenti algoritmi:
|
|
- Sloan: un algoritmo di riduzione della banda di matrici sparse con
|
|
una buona performance
|
|
- Cuthill-McKee: un altro algoritmo di riduzione della banda di
|
|
matrici sparse
|
|
- Tovchigrechko e Noack: due algoritmo appositamente ideati per le reti
|
|
di Petri, anch'essi con una buona performance
|
|
- P-chaining: un algoritmo che sfrutta le informazioni strutturali
|
|
della rete ma ha una bassa performance
|
|
- Gradient-P
|
|
- Gibbs-Poole-Stockmeier: un altro algoritmo matriciale che nella rete
|
|
in analisi ha restituito il risultato peggiore
|
|
|
|
#+CAPTION: Algoritmo di Sloan
|
|
\includepdf{./diagrammi/sloan.png}
|
|
#+CAPTION: Algoritmo di Cuthull-McKee
|
|
\includepdf{./diagrammi/mckee.png}
|
|
#+CAPTION: Algoritmo di Tovchigrechko
|
|
\includepdf{./diagrammi/tovchi.png}
|
|
#+CAPTION: Algoritmo di Noack
|
|
\includepdf{./diagrammi/noack.png}
|
|
#+CAPTION: Algoritmo P-Chain
|
|
\includepdf{./diagrammi/p-chain.png}
|
|
#+CAPTION: Algoritmo Gradient-P
|
|
\includepdf{./diagrammi/gradient.png}
|
|
#+CAPTION: Algoritmo di Gibbs-Poole-Stockmeier
|
|
\includepdf{./diagrammi/gibbs.png}
|