diff --git a/anno3/vpc/consegne/2/2.pn.org b/anno3/vpc/consegne/2/2.pn.org index f70bc0a..10c2f35 100644 --- a/anno3/vpc/consegne/2/2.pn.org +++ b/anno3/vpc/consegne/2/2.pn.org @@ -189,17 +189,35 @@ La richiesta del servizio verso lo slave scelto e` gestita attraverso due buffer, posti FreeChoice e Risultato. ** TODO P e T invarianti -[ ] Immagini Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi -[[./semiflowsBT.jpg]] -[[./semiflowsBP.jpg]] +[[./semiflowsCT.jpg]] +[[./semiflowsCP.jpg]] Gli P-invarianti sono i seguenti: -Gli T-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 + +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ₘ -Dato che la reteB e` interamente coperta dagli P-semiflussi, possiamo -affermare che la rete sia bounded. [ ] Deadlock [ ] Liveness @@ -210,7 +228,27 @@ associati ciascuno ad un master diverso. #+CAPTION: Modello della reteD [[./reteD.jpg]] -** TODO P e T invarianti +** P e T invarianti +Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi + +[[./semiflowsDT.jpg]] +[[./semiflowsDP.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 +- 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₂ +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₂ + Reset_{m2} ** Decision Diagram L'efficacia dei decision diagram sulla generazione dello stato degli spazi dipende fortemente dall'ordine delle variabili. diff --git a/anno3/vpc/consegne/2/semiflowsCP.jpg b/anno3/vpc/consegne/2/semiflowsCP.jpg new file mode 100644 index 0000000..42abf0b Binary files /dev/null and b/anno3/vpc/consegne/2/semiflowsCP.jpg differ diff --git a/anno3/vpc/consegne/2/semiflowsCT.jpg b/anno3/vpc/consegne/2/semiflowsCT.jpg new file mode 100644 index 0000000..1bab9f1 Binary files /dev/null and b/anno3/vpc/consegne/2/semiflowsCT.jpg differ diff --git a/anno3/vpc/consegne/2/semiflowsDP.jpg b/anno3/vpc/consegne/2/semiflowsDP.jpg new file mode 100644 index 0000000..3e3178d Binary files /dev/null and b/anno3/vpc/consegne/2/semiflowsDP.jpg differ diff --git a/anno3/vpc/consegne/2/semiflowsDT.jpg b/anno3/vpc/consegne/2/semiflowsDT.jpg new file mode 100644 index 0000000..e65c69a Binary files /dev/null and b/anno3/vpc/consegne/2/semiflowsDT.jpg differ diff --git a/todo.org b/todo.org index 123db09..494884f 100644 --- a/todo.org +++ b/todo.org @@ -5,6 +5,7 @@ - [ ] chiedi dell'esame - [X] Es1: definizioni - [ ] rete A, b, c, d +- [ ] Spiega p-t-semiflows analysis: deadlock e liveness, boundness - [X] rete E, F - [ ] analisi - [ ] uppal