diff --git a/anno3/vpc/consegne/1/1.definizioni.org b/anno3/vpc/consegne/1/1.definizioni.org index 68b294e..5613a9f 100644 --- a/anno3/vpc/consegne/1/1.definizioni.org +++ b/anno3/vpc/consegne/1/1.definizioni.org @@ -1,3 +1,16 @@ +#+TITLE: Esercizio Definizioni Matematiche +#+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 * Insiemi ** Numeri naturali diff --git a/anno3/vpc/consegne/1/1.pdf b/anno3/vpc/consegne/1/1.pdf index 5f72c61..0096203 100644 Binary files a/anno3/vpc/consegne/1/1.pdf and b/anno3/vpc/consegne/1/1.pdf differ diff --git a/anno3/vpc/consegne/2.b/2.b.org b/anno3/vpc/consegne/2.b/2.b.org index 7b1094f..daf701a 100644 --- a/anno3/vpc/consegne/2.b/2.b.org +++ b/anno3/vpc/consegne/2.b/2.b.org @@ -1,3 +1,16 @@ +#+TITLE: Esercizio CPN +#+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 E #+CAPTION: Rete E diff --git a/anno3/vpc/consegne/2.b/2.b.pdf b/anno3/vpc/consegne/2.b/2.b.pdf index e8d3b98..0090fa2 100644 Binary files a/anno3/vpc/consegne/2.b/2.b.pdf and b/anno3/vpc/consegne/2.b/2.b.pdf differ diff --git a/anno3/vpc/consegne/2/2.pdf b/anno3/vpc/consegne/2/2.pdf index eef9898..70ec305 100644 Binary files a/anno3/vpc/consegne/2/2.pdf and b/anno3/vpc/consegne/2/2.pdf differ diff --git a/anno3/vpc/consegne/2/2.pn.org b/anno3/vpc/consegne/2/2.pn.org index 2144ae6..f0e3a8a 100644 --- a/anno3/vpc/consegne/2/2.pn.org +++ b/anno3/vpc/consegne/2/2.pn.org @@ -1,3 +1,16 @@ +#+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. @@ -6,12 +19,12 @@ M master identici e S slave identici di tipo 1. 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_Locale, Richiesta_Servizio, Attesa_Elaborazione e Reset_M -Lo slave è modellato dai posti S0, S1_a, S1_b, S2_a, S2_b e -S3 e dalle transizioni Inizio_Servizio, Azione_Locale_Sa, -Azione_Locale_Sb, Fine_Servizio e Reset_S. La richiesta del servizio -verso lo slave e` gestita attraverso due buffer, posti Buffer_Input e -posto Buffer_Output. +/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 @@ -52,18 +65,16 @@ Una rete di petri puo` essere ridotta usando le seguendi tecniche: - eliminazione - rimozione dei loop Nelle figure vengono mostrate alcune fasi di riduzione della rete in -analisi; in ordine sono stati applicati: -- fusione di alcuni posti -- fusione di alcune transizioni -- eliminazione di alcuni posti -- eliminazione di alcune transizioni -- riduzione di self loop - -[[./riduzione/fusione1.jpg]] -[[./riduzione/fusione2.jpg]] +analisi. +#+CAPTION: eliminazione di posti identici [[./riduzione/eliminazione1.jpg]] -# [[./riduzione/eliminazione2.jpg]] -[[./riduzione/rimozione1.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 @@ -71,30 +82,29 @@ Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi [[./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_output + Buffer_input + M0 + M1 + M3 -| S1_b + S2_b + Buffer_output + Buffer_input + M0 + M1 + M3 +| • 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_servizio + azione_locale_sa + azione_locale_sb + \\ -Fine_servizio + Reset_s + azione_locale_m + Richiesta_servizio + \\ -Attesa_elaborazione + Reset_m + Reset_s -\] +| • 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 +| • 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 @@ -110,24 +120,24 @@ precedenti uguaglianze che: | 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 + | • 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_Servizio/ e /Fine_Servizio/ non vengano abilitate: - | m[Buffer_input] + M[S0] ≤ 1 - | m[S2ₐ] + m[S2_{b}] ≤ 1 + 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 + | • 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. @@ -139,19 +149,23 @@ liberamente dai master. [[./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_Locale, Richiesta_Servizio, Attesa_Elaborazione e Reset_M -Lo slave di tipo 1 è modellato dai posti S0, S1_a, S1_b, S2_a, S2_b e -S3 e dalle transizioni Inizio_Servizio, Azione_Locale_Sa, -Azione_Locale_Sb, Fine_Servizio e Reset_S. -Lo slave di tipo 2 è modellato dai posti R0, R1_a, R1_b, R2_a, R2_b e -R3 e dalle transizioni Inizio_Servizio_R, Azione_Locale_R, Fine_Servizio e Reset_R. -La richiesta del servizio -verso lo slave scelto e` gestita attraverso due buffer, posti -FreeChoice e Risultato. +è 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 | @@ -165,7 +179,7 @@ FreeChoice e Risultato. | 9, 2 | 69784 | 373252 | | 10, 2 | 116116 | 642928 | -Parametrizzando anche il numero di slaves: +Parametrizzando anche il marking sugli slaves (R+S): | master, slaves | Stati | Archi | |----------------+---------+----------| | 1, 2 | 40 | 76 | @@ -187,25 +201,20 @@ Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi [[./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 +| • 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_servizio_R + azione_locale_R + \\ -Fine_servizio_R + Reset_R + azione_locale_m + Richiesta_servizio + \\ -Attesa_elaborazione + Reset_M + Scelta_2 -\] -\[ -Inizio_servizio_S + azione_locale_sa + azione_locale_sb + \\ -Fine_servizio_S + Reset_s + azione_locale_m + Richiesta_servizio + \\ -Attesa_elaborazione + Reset_m + Scelta_1 -\] +| • 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 @@ -218,34 +227,37 @@ In tal caso non avremmo starvation e la proprieta` di liveness sarebbe rispettat 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] + 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] + m[M3] + m[Freechoice] + m[P0] + m[P1] + m[Risultato] = 1 +| • 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_Servizio_R/, -/Attesa_Elaborazione/, /Fine_Servizioₛ/ e /Inizio_Servizioₛ/ non vengano abilitati: -| m[P0] = 0 -| m[Risultato] = 0 -| m[S2ₐ] + m[S2_{b}] ≤ 1 -| m[P1] + m[S0] ≤ 1 +| • 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 +| • 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 @@ -257,13 +269,13 @@ liberamente dai master. 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_Servizio, Attesa_Elaborazione e Reset_M +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_Servizio, Azione_Locale_Sa, -Azione_Locale_Sb, Fine_Servizio e Reset_S (il secondo master e` una +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_Servizio_R, Azione_Locale_R, Fine_Servizio e Reset_R. +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. @@ -289,56 +301,54 @@ 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] + m[M1] + m[M3] + m[Freechoice] + m[P0] + m[P1] + - m[Risultato] + m[copy_M0] + m[copy_M1] + m[copy_M3] = 1 -\] -\[ - m[S1_{b}] + m[S2_{b}] + m[R1] + m[R2] + m[M0] + m[M1] + m[M3] + m[Freechoice] + m[P0] + m[P1] + - m[Risultato] + m[copy_M0] + m[copy_M1] + m[copy_M3] = 1 -\] +| • 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_Servizio_R/, -/Attesa_Elaborazione/, /copy_Attesa_Elaborazione/, /Fine_Servizioₛ/ e /Inizio_Servizioₛ/ non vengano abilitati: -| m[P0] = 0 -| m[Risultato] = 0 -| m[S2ₐ] + m[S2_{b}] ≤ 1 -| m[P1] + m[S0] ≤ 1 +| • 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 +| • 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_Servizioᵣ + Azione_Locale + Fine_Servizioᵣ + T3 + - azione_localeₘ + Richiesta_Servizio + Attesa_Elaborazione + Reset_M + Scelta₁ -- Inizio_Servizioₛ + Azione_Locale_{sa} + Azione_Locale_{sb} + Fine_Servizioₛ + T3 + - azione_localeₘ + Richiesta_Servizio + Attesa_Elaborazione + - Reset_M + Scelta₁ -- Inizio_Servizioᵣ + Azione_Locale + Fine_Servizioᵣ + T3 + Scelta₂ + - copyₐzione_localeₘ + copy_Richiesta_Servizio + - copy_Attesa_Elaborazione + copy_Resetₘ -- Inizio_Servizioₛ + Azione_Locale_{sa} + Azione_Locale_{sb} + - Fine_Servizioₛ + Reset + Scelta₁ + copy_azione_localeₘ + - copy_Richiesta_Servizio + copy_Attesa_Elaborazione + copy_Resetₘ +- 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. @@ -356,16 +366,17 @@ Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi [[./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₂ +| • 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 @@ -373,11 +384,11 @@ 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_Servizioₛ + azione_locale_{sa} + azione_locale_{sb} + - Fine_Servizioₛ + Reset + azione_localeₘ + Richiesta_Servizio + - Attesa_Elaborazione + Resetₘ -- Inizio_Servizioᵣ + Azione_locale + Fine_Servizioᵣ + T3 - azione_locale_{m2} + Richiesta_Servizio₂ + Attesa_Elaborazione₂ + +- 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. @@ -389,7 +400,7 @@ 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 -- (advanced) Cuthill-McKee: un altro algoritmo di riduzione della banda di +- 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 @@ -400,16 +411,16 @@ assegnazioni i seguenti algoritmi: in analisi ha restituito il risultato peggiore #+CAPTION: Algoritmo di Sloan -[[./diagrammi/sloan.jpg]] +\includepdf{./diagrammi/sloan.png} #+CAPTION: Algoritmo di Cuthull-McKee -[[./diagrammi/mckee.jpg]] +\includepdf{./diagrammi/mckee.png} #+CAPTION: Algoritmo di Tovchigrechko -[[./diagrammi/tovchi.jpg]] +\includepdf{./diagrammi/tovchi.png} #+CAPTION: Algoritmo di Noack -[[./diagrammi/noack.jpg]] +\includepdf{./diagrammi/noack.png} #+CAPTION: Algoritmo P-Chain -[[./diagrammi/p-chain.jpg]] +\includepdf{./diagrammi/p-chain.png} #+CAPTION: Algoritmo Gradient-P -[[./diagrammi/gradient.jpg]] +\includepdf{./diagrammi/gradient.png} #+CAPTION: Algoritmo di Gibbs-Poole-Stockmeier -[[./diagrammi/gibbs.jpg]] +\includepdf{./diagrammi/gibbs.png} diff --git a/anno3/vpc/consegne/2/diagrammi/gibbs.png b/anno3/vpc/consegne/2/diagrammi/gibbs.png new file mode 100644 index 0000000..b50453d Binary files /dev/null and b/anno3/vpc/consegne/2/diagrammi/gibbs.png differ diff --git a/anno3/vpc/consegne/2/diagrammi/gradient.png b/anno3/vpc/consegne/2/diagrammi/gradient.png new file mode 100644 index 0000000..677efd7 Binary files /dev/null and b/anno3/vpc/consegne/2/diagrammi/gradient.png differ diff --git a/anno3/vpc/consegne/2/diagrammi/mckee.png b/anno3/vpc/consegne/2/diagrammi/mckee.png new file mode 100644 index 0000000..042c1f5 Binary files /dev/null and b/anno3/vpc/consegne/2/diagrammi/mckee.png differ diff --git a/anno3/vpc/consegne/2/diagrammi/noack.png b/anno3/vpc/consegne/2/diagrammi/noack.png new file mode 100644 index 0000000..bf6615a Binary files /dev/null and b/anno3/vpc/consegne/2/diagrammi/noack.png differ diff --git a/anno3/vpc/consegne/2/diagrammi/p-chain.png b/anno3/vpc/consegne/2/diagrammi/p-chain.png new file mode 100644 index 0000000..c9adfad Binary files /dev/null and b/anno3/vpc/consegne/2/diagrammi/p-chain.png differ diff --git a/anno3/vpc/consegne/2/diagrammi/sloan.png b/anno3/vpc/consegne/2/diagrammi/sloan.png new file mode 100644 index 0000000..3db96ab Binary files /dev/null and b/anno3/vpc/consegne/2/diagrammi/sloan.png differ diff --git a/anno3/vpc/consegne/2/diagrammi/tovchi.png b/anno3/vpc/consegne/2/diagrammi/tovchi.png new file mode 100644 index 0000000..c271c68 Binary files /dev/null and b/anno3/vpc/consegne/2/diagrammi/tovchi.png differ diff --git a/anno3/vpc/consegne/2/gspn/Es2.PNPRO b/anno3/vpc/consegne/2/gspn/Es2.PNPRO index 1103644..81e29fd 100644 --- a/anno3/vpc/consegne/2/gspn/Es2.PNPRO +++ b/anno3/vpc/consegne/2/gspn/Es2.PNPRO @@ -104,6 +104,59 @@ + + + + + + + + + + + + +