esercizio analisi, svista

2020-05-21 19:27:27 +02:00 · 2020-05-21 19:27:27 +02:00 · 71d824f3ce
commit 71d824f3ce
parent 9147d35cea
19 changed files with 517 additions and 144 deletions
--- a/anno3/vpc/consegne/2/2.pn.org
+++ b/anno3/vpc/consegne/2/2.pn.org
@ -64,29 +64,70 @@ analisi; in ordine sono stati applicati:
 [[./riduzione/eliminazione1.jpg]]
 # [[./riduzione/eliminazione2.jpg]]
 [[./riduzione/rimozione1.jpg]]
-** TODO P e T invarianti
+** P e T invarianti
 Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi

 [[./semiflowsAT.jpg]]
 [[./semiflowsAP.jpg]]

-Gli P-invarianti sono i seguenti:
+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
-Il T-invariante e` il seguento:
+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
 \]
-
+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.
-[ ] Deadlock
-[ ] Liveness
+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_Servizio/ e /Fine_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
@ -137,7 +178,7 @@ 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.

-** TODO P e T invarianti
+** P e T invarianti
 Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi

 [[./semiflowsBT.jpg]]
@ -149,7 +190,7 @@ Gli P-invarianti sono i seguenti:
 | 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 + Risultbto
+| 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 + \\
@ -161,11 +202,47 @@ 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
 \]
+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.
-[ ] Deadlock
-[ ] Liveness
+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
+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
+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
@ -186,7 +263,7 @@ R3 e dalle transizioni Inizio_Servizio_R, Azione_Locale_R, Fine_Servizio e Reset
 La richiesta del servizio
 verso lo slave scelto e` gestita attraverso due buffer, posti
 FreeChoice e Risultato.
-** TODO P e T invarianti
+** P e T invarianti
 Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi

 [[./semiflowsCT.jpg]]
@ -202,6 +279,47 @@ Gli P-invarianti sono i seguenti:
  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] + 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
+\]
+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
+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_Servizioᵣ + Azione_Locale + Fine_Servizioᵣ + T3 +
@ -215,9 +333,8 @@ Gli T-invarianti sono i seguenti:
 - Inizio_Servizioₛ + Azione_Locale_{sa} + Azione_Locale_{sb} +
  Fine_Servizioₛ + Reset + Scelta₁ + copy_azione_localeₘ +
  copy_Richiesta_Servizio + copy_Attesa_Elaborazione + copy_Resetₘ
-
-[ ] Deadlock
-[ ] Liveness
+Come nella rete B, in assenza di fairness non possiamo rispettare la
+condizione di liveness e c'e` possiblita` di starvation.

 * Rete D
 Due master identici, uno slave di tipo 1 e uno slave di tipo 1 scelti
@ -241,12 +358,22 @@ Gli P-invarianti sono i seguenti:
 - 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_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}
+  azione_locale_{m2} + Richiesta_Servizio₂ + Attesa_Elaborazione₂ +
+  Reset_{m2}
+Come nella rete B, in assenza di fairness non possiamo rispettare la
+condizione di liveness e c'e` possiblita` di starvation.
+
 ** Decision Diagram
 L'efficacia dei decision diagram sulla generazione dello stato degli
 spazi dipende fortemente dall'ordine delle variabili.
--- a/anno3/vpc/consegne/2/gspn/Es2-Measures.solution/PT.bnd
+++ b/anno3/vpc/consegne/2/gspn/Es2-Measures.solution/PT.bnd
@ -1,12 +1,12 @@
-0 25
-0 25
-0 25
-0 25
-0 25
-0 25
-0 25
-0 25
-0 25
-0 25
-0 25
-0 25
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
--- a/anno3/vpc/consegne/2/gspn/Es2-Measures.solution/PT.net
+++ b/anno3/vpc/consegne/2/gspn/Es2-Measures.solution/PT.net
@ -1,7 +1,8 @@
 |0|
 |
-f 0 12 0 9 0 0 0
-S0            25 2.6666666666666665 0.8333333333333334 2.6279166666666667 1.0289583333333334 0
+f 1 12 0 9 0 0 0
+n -7134 9.463541666666666 6.265625 0
+S0            -1 2.6666666666666665 0.8333333333333334 2.6279166666666667 1.0289583333333334 0
 S1_a          0 1.6666666666666667 2.3333333333333335 1.9716666666666667 2.278958333333333 0
 S1_b          0 3.6666666666666665 2.3333333333333335 3.216458333333333 2.278958333333333 0
 S2_a          0 1.6666666666666667 3.6666666666666665 1.9716666666666667 3.6122916666666662 0
@ -9,7 +10,7 @@ S2_b          0 3.6666666666666665 3.6666666666666665 3.1331249999999997 3.61229
 S3            0 2.6666666666666665 5.166666666666667 2.6279166666666667 5.362291666666667 0
 Buffer_output 0 5.0 4.5 4.570625 4.695625 0
 Buffer_input  0 5.0 1.6666666666666667 4.6175 1.8622916666666667 0
-M0            25 7.666666666666667 0.3333333333333333 7.268541666666667 0.11229166666666668 0
+M0            -1 7.666666666666667 0.3333333333333333 7.268541666666667 0.11229166666666668 0
 M1            0 7.666666666666667 1.6666666666666667 7.601875 1.8622916666666667 0
 M2            0 7.666666666666667 2.5 7.601875 2.195625 0
 M3            0 7.666666666666667 4.0 7.351875 4.195625 0
--- a/anno3/vpc/consegne/2/gspn/Es2.PNPRO
+++ b/anno3/vpc/consegne/2/gspn/Es2.PNPRO
--- a/anno3/vpc/consegne/2/gspn/Es2B-CTL
+++ b/anno3/vpc/consegne/2/gspn/Es2B-CTL
@ -0,0 +1,18 @@
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 2
+0 2
+0 2
+0 2
+0 2
+0 2
+0 2
+0 2
--- a/anno3/vpc/consegne/2/gspn/Es2B-CTL
+++ b/anno3/vpc/consegne/2/gspn/Es2B-CTL
@ -0,0 +1,2 @@
+% MEASURE0
+AF(#S1_a == 1)
--- a/anno3/vpc/consegne/2/gspn/Es2B-CTL
+++ b/anno3/vpc/consegne/2/gspn/Es2B-CTL
@ -0,0 +1,3 @@
+|256
+%
+|
--- a/anno3/vpc/consegne/2/gspn/Es2B-CTL
+++ b/anno3/vpc/consegne/2/gspn/Es2B-CTL
@ -0,0 +1,2 @@
+0
+0
--- a/anno3/vpc/consegne/2/gspn/Es2B-CTL
+++ b/anno3/vpc/consegne/2/gspn/Es2B-CTL
@ -0,0 +1,130 @@
+|0|
+|
+f 3 18 0 15 0 0 0
+n -7134 11.296875 6.432291666666667 0
+r1 -7134 12.145833333333334 6.432291666666667 0
+r2 -7134 12.8125 6.432291666666667 0
+S0         -2 3.0 1.1666666666666667 2.9612499999999997 1.3622916666666667 0
+S1_a       0 2.0 2.6666666666666665 2.305 2.6122916666666667 0
+S1_b       0 4.0 2.6666666666666665 3.5497916666666662 2.6122916666666667 0
+S2_a       0 2.0 4.0 2.305 3.9456249999999997 0
+S2_b       0 4.0 4.0 3.466458333333333 3.9456249999999997 0
+S3         0 3.0 5.5 2.9612499999999997 5.695625 0
+R0         -3 6.5 1.1666666666666667 6.450833333333333 1.3622916666666667 0
+R1         0 6.5 2.6666666666666665 6.450833333333333 2.8622916666666662 0
+R2         0 6.5 4.0 6.450833333333333 4.195625 0
+R3         0 6.5 5.5 6.450833333333333 5.695625 0
+M0         -1 12.0 1.1666666666666667 11.601875 0.945625 0
+M1         0 12.0 2.5 11.935208333333334 2.6956249999999997 0
+M2         0 12.0 3.3333333333333335 11.935208333333334 3.028958333333333 0
+M3         0 12.0 4.833333333333333 11.685208333333334 5.028958333333333 0
+Freechoice 0 9.666666666666666 2.5 9.362291666666666 2.6956249999999997 0
+P0         0 7.833333333333333 1.6666666666666667 7.789375 1.8622916666666667 0
+P1         0 7.833333333333333 0.6666666666666666 7.789375 0.8622916666666667 0
+Risultato  0 9.666666666666666 4.333333333333333 8.89875 4.278958333333333 0
+Inizio_Servizio_s   1.0 0 0 2 0 3.0 2.0 1.6666666666666667 2.0572916666666665 3.0833333333333335 2.0677083333333335 0
+   1 1 0 0
+   1 17 2 0
+3.9166666666666665 2.0
+3.9166666666666665 0.6666666666666666
+   2
+   1 2 0 0
+   1 3 0 0
+   0
+azione_locale_sa    1.0 0 0 1 0 2.0 3.3333333333333335 2.1875 3.140625 2.0833333333333335 3.4010416666666665 0
+   1 2 0 0
+   1
+   1 4 0 0
+   0
+azione_locale_sb    1.0 0 0 1 0 4.0 3.3333333333333335 2.859375 3.640625 4.083333333333333 3.4010416666666665 0
+   1 3 0 0
+   1
+   1 5 0 0
+   0
+Fine_Servizio_s     1.0 0 0 2 0 3.0 4.833333333333333 1.8697916666666667 4.890625 3.0833333333333335 4.901041666666667 0
+   1 4 0 0
+   1 5 0 0
+   2
+   1 6 0 0
+   1 18 4 0
+4.166666666666667 4.833333333333333
+4.166666666666667 6.333333333333333
+9.583333333333334 6.333333333333333
+9.666666666666666 6.333333333333333
+   0
+Reset_S             1.0 0 0 1 1 1.5 5.5 1.3020833333333333 5.307291666666667 1.5833333333333333 5.567708333333333 0
+   1 6 0 0
+   1
+   1 1 2 0
+1.5 4.833333333333333
+1.5 1.1666666666666667
+   0
+Inizio_Servizio_R   1.0 0 0 2 0 6.5 2.0 6.734375 2.2239583333333335 6.583333333333333 2.0677083333333335 0
+   1 7 0 0
+   1 16 2 0
+7.083333333333333 2.0
+7.083333333333333 1.6666666666666667
+   1
+   1 8 0 0
+   0
+Azione_locale_R     1.0 0 0 1 0 6.5 3.3333333333333335 6.609375 3.640625 6.583333333333333 3.4010416666666665 0
+   1 8 0 0
+   1
+   1 9 0 0
+   0
+Fine_Servizio_R     1.0 0 0 1 0 6.5 4.833333333333333 6.604166666666667 5.140625 6.583333333333333 4.901041666666667 0
+   1 9 0 0
+   2
+   1 10 0 0
+   1 18 3 0
+8.0 4.833333333333333
+8.0 6.333333333333333
+9.666666666666666 6.333333333333333
+   0
+Reset_R             1.0 0 0 1 1 5.333333333333333 5.5 5.125 5.307291666666667 5.416666666666667 5.567708333333333 0
+   1 10 0 0
+   1
+   1 7 1 0
+5.333333333333333 1.1666666666666667
+   0
+azione_locale_m     1.0 0 0 1 1 12.0 1.8333333333333333 11.53125 1.5572916666666667 12.083333333333334 1.9010416666666667 0
+   1 11 2 0
+11.416666666666666 1.8333333333333333
+11.416666666666666 1.1666666666666667
+   1
+   1 12 2 0
+12.583333333333334 1.8333333333333333
+12.583333333333334 2.5
+   0
+Richiesta_Servizio  1.0 0 0 1 1 11.166666666666666 2.5 10.625 2.3072916666666665 11.25 2.5677083333333335 0
+   1 12 0 0
+   2
+   1 13 1 0
+11.166666666666666 3.3333333333333335
+   1 15 0 0
+   0
+Attesa_Elaborazione 1.0 0 0 2 0 12.0 4.333333333333333 10.5625 4.140625 12.083333333333334 4.401041666666667 0
+   1 13 0 0
+   1 18 0 0
+   1
+   1 14 0 0
+   0
+Reset_M             1.0 0 0 1 0 13.0 3.3333333333333335 12.776041666666666 3.140625 13.083333333333334 3.4010416666666665 0
+   1 14 1 0
+13.0 4.833333333333333
+   1
+   1 11 1 0
+13.0 1.1666666666666667
+   0
+Scelta_1            1.0 0 0 1 1 8.333333333333334 0.6666666666666666 8.135416666666666 0.4739583333333333 8.416666666666666 0.734375 0
+   1 15 1 0
+9.666666666666666 0.6666666666666666
+   1
+   1 17 0 0
+   0
+Scelta_2            1.0 0 0 1 1 8.333333333333334 1.6666666666666667 8.135416666666666 1.4739583333333333 8.416666666666666 1.734375 0
+   1 15 1 0
+9.666666666666666 1.6666666666666667
+   1
+   1 16 0 0
+   0
--- a/anno3/vpc/consegne/2/gspn/Es2B-CTL
+++ b/anno3/vpc/consegne/2/gspn/Es2B-CTL
@ -0,0 +1,7 @@
+5
+4 1 7 1 8 1 9 1 10 
+4 1 11 1 12 1 13 1 14 
+11 1 1 1 6 -1 8 -1 9 -1 11 -1 12 -1 14 -1 15 -1 16 -1 17 -1 18 
+11 1 3 1 5 1 8 1 9 1 11 1 12 1 14 1 15 1 16 1 17 1 18 
+11 1 2 1 4 1 8 1 9 1 11 1 12 1 14 1 15 1 16 1 17 1 18 
+0
--- a/anno3/vpc/consegne/2/gspn/Es2B-CTL
+++ b/anno3/vpc/consegne/2/gspn/Es2B-CTL
@ -0,0 +1,8 @@
+6
+11 1 3 1 5 1 8 1 9 1 11 1 12 1 14 1 15 1 16 1 17 1 18 
+4 1 1 1 3 1 5 1 6 
+11 1 2 1 4 1 8 1 9 1 11 1 12 1 14 1 15 1 16 1 17 1 18 
+4 1 1 1 2 1 4 1 6 
+4 1 11 1 12 1 13 1 14 
+4 1 7 1 8 1 9 1 10 
+0
--- a/anno3/vpc/consegne/2/gspn/Es2B.PNPRO
+++ b/anno3/vpc/consegne/2/gspn/Es2B.PNPRO
--- a/anno3/vpc/consegne/2/gspn/Es2C-Measures.solution/PT.net
+++ b/anno3/vpc/consegne/2/gspn/Es2C-Measures.solution/PT.net
@ -1,169 +1,169 @@
 |0|
 |
 f 0 22 0 19 0 0 0
-S0         1 3.3333333333333335 1.5 3.294583333333333 1.695625 0
-S1_a       0 2.3333333333333335 3.0 2.638333333333333 2.9456249999999997 0
-S1_b       0 4.333333333333333 3.0 3.8831249999999997 2.9456249999999997 0
-S2_a       0 2.3333333333333335 4.333333333333333 2.638333333333333 4.278958333333333 0
-S2_b       0 4.333333333333333 4.333333333333333 3.7997916666666662 4.278958333333333 0
-S3         0 3.3333333333333335 5.833333333333333 3.294583333333333 6.028958333333333 0
-R0         1 6.833333333333333 1.5 6.784166666666667 1.695625 0
-R1         0 6.833333333333333 3.0 6.784166666666667 3.1956249999999997 0
-R2         0 6.833333333333333 4.333333333333333 6.784166666666667 4.528958333333333 0
-R3         0 6.833333333333333 5.833333333333333 6.784166666666667 6.028958333333333 0
-M0         1 13.166666666666666 1.5 12.768541666666666 1.2789583333333334 0
-M1         0 13.166666666666666 2.8333333333333335 13.101875 3.028958333333333 0
-M2         0 13.166666666666666 3.6666666666666665 13.101875 3.3622916666666662 0
-M3         0 13.166666666666666 5.166666666666667 12.851875 5.362291666666667 0
-Freechoice 0 10.0 0.16666666666666666 9.695625 0.3622916666666667 0
-P0         0 8.166666666666666 2.0 8.122708333333334 2.195625 0
-P1         0 8.166666666666666 1.0 8.122708333333334 1.195625 0
-Risultato  0 10.5 6.666666666666667 9.64875 6.362291666666667 0
-copy_M0    1 16.5 1.5 15.919583333333334 1.2789583333333334 0
-copy_M1    0 16.5 2.8333333333333335 16.252916666666668 3.028958333333333 0
-copy_M2    0 16.5 3.6666666666666665 16.252916666666668 3.3622916666666662 0
-copy_M3    0 16.5 5.166666666666667 16.002916666666668 5.362291666666667 0
-Inizio_Servizio_s        1.0 0 0 2 0 3.3333333333333335 2.3333333333333335 2.0 2.390625 3.4166666666666665 2.4010416666666665 0
+S0         1 4.0 2.3333333333333335 3.9612499999999997 2.528958333333333 0
+S1_a       0 3.0 3.8333333333333335 3.3049999999999997 3.778958333333333 0
+S1_b       0 5.0 3.8333333333333335 4.549791666666667 3.778958333333333 0
+S2_a       0 3.0 5.166666666666667 3.3049999999999997 5.112291666666667 0
+S2_b       0 5.0 5.166666666666667 4.466458333333333 5.112291666666667 0
+S3         0 4.0 6.666666666666667 3.9612499999999997 6.862291666666667 0
+R0         1 6.666666666666667 2.3333333333333335 6.6175 2.528958333333333 0
+R1         0 6.666666666666667 3.8333333333333335 6.6175 4.028958333333333 0
+R2         0 6.666666666666667 5.166666666666667 6.6175 5.362291666666667 0
+R3         0 6.666666666666667 6.666666666666667 6.6175 6.862291666666667 0
+M0         1 12.5 2.3333333333333335 12.101875 2.1122916666666667 0
+M1         0 12.5 3.6666666666666665 12.435208333333334 3.8622916666666662 0
+M2         0 12.5 4.5 12.435208333333334 4.195625 0
+M3         0 12.5 6.0 12.185208333333334 6.195625 0
+Freechoice 0 9.833333333333334 1.0 9.528958333333334 1.195625 0
+P0         0 8.0 2.8333333333333335 7.956041666666667 3.028958333333333 0
+P1         0 8.0 1.8333333333333333 7.956041666666667 2.028958333333333 0
+Risultato  0 9.833333333333334 7.5 8.982083333333334 7.195625 0
+copy_M0    1 15.833333333333334 2.3333333333333335 15.252916666666666 2.1122916666666667 0
+copy_M1    0 15.833333333333334 3.6666666666666665 15.58625 3.8622916666666662 0
+copy_M2    0 15.833333333333334 4.5 15.58625 4.195625 0
+copy_M3    0 15.833333333333334 6.0 15.33625 6.195625 0
+Inizio_Servizio_s        1.0 0 0 2 0 4.0 3.1666666666666665 2.6666666666666665 3.2239583333333335 4.083333333333333 3.234375 0
   1 1 0 0
   1 17 2 0
-4.25 2.3333333333333335
-4.25 1.0
+4.916666666666667 3.1666666666666665
+4.916666666666667 1.8333333333333333
   2
   1 2 0 0
   1 3 0 0
   0
-azione_locale_sa         1.0 0 0 1 0 2.3333333333333335 3.6666666666666665 2.5208333333333335 3.4739583333333335 2.4166666666666665 3.734375 0
+azione_locale_sa         1.0 0 0 1 0 3.0 4.5 3.1875 4.307291666666667 3.0833333333333335 4.567708333333333 0
   1 2 0 0
   1
   1 4 0 0
   0
-azione_locale_sb         1.0 0 0 1 0 4.333333333333333 3.6666666666666665 3.1927083333333335 3.9739583333333335 4.416666666666667 3.734375 0
+azione_locale_sb         1.0 0 0 1 0 5.0 4.5 3.859375 4.807291666666667 5.083333333333333 4.567708333333333 0
   1 3 0 0
   1
   1 5 0 0
   0
-Fine_Servizio_s          1.0 0 0 2 0 3.3333333333333335 5.166666666666667 2.203125 5.223958333333333 3.4166666666666665 5.234375 0
+Fine_Servizio_s          1.0 0 0 2 0 4.0 6.0 2.8697916666666665 6.057291666666667 4.083333333333333 6.067708333333333 0
   1 4 0 0
   1 5 0 0
   2
   1 6 0 0
   1 18 4 0
-4.5 5.166666666666667
-4.5 6.666666666666667
-9.916666666666666 6.666666666666667
-10.0 6.666666666666667
+5.166666666666667 6.0
+5.166666666666667 7.5
+10.583333333333334 7.5
+10.666666666666666 7.5
   0
-Reset                    1.0 0 0 1 1 1.8333333333333333 5.833333333333333 1.7135416666666667 5.640625 1.9166666666666667 5.901041666666667 0
+Reset                    1.0 0 0 1 1 2.5 6.666666666666667 2.3802083333333335 6.473958333333333 2.5833333333333335 6.734375 0
   1 6 0 0
   1
   1 1 2 0
-1.8333333333333333 5.166666666666667
-1.8333333333333333 1.5
+2.5 6.0
+2.5 2.3333333333333335
   0
-Inizio_Servizio_r        1.0 0 0 2 0 6.833333333333333 2.3333333333333335 7.083333333333333 2.5572916666666665 6.916666666666667 2.4010416666666665 0
+Inizio_Servizio_r        1.0 0 0 2 0 6.666666666666667 3.1666666666666665 6.916666666666667 3.390625 6.75 3.234375 0
   1 7 0 0
   1 16 2 0
-7.416666666666667 2.3333333333333335
-7.416666666666667 2.0
+7.25 3.1666666666666665
+7.25 2.8333333333333335
   1
   1 8 0 0
   0
-Azione_locale            1.0 0 0 1 0 6.833333333333333 3.6666666666666665 7.03125 3.9739583333333335 6.916666666666667 3.734375 0
+Azione_locale            1.0 0 0 1 0 6.666666666666667 4.5 6.864583333333333 4.807291666666667 6.75 4.567708333333333 0
   1 8 0 0
   1
   1 9 0 0
   0
-Fine_Servizio_r          1.0 0 0 1 0 6.833333333333333 5.166666666666667 6.953125 5.473958333333333 6.916666666666667 5.234375 0
+Fine_Servizio_r          1.0 0 0 1 0 6.666666666666667 6.0 6.786458333333333 6.307291666666667 6.75 6.067708333333333 0
   1 9 0 0
   2
   1 10 0 0
   1 18 3 0
-8.333333333333334 5.166666666666667
-8.333333333333334 6.666666666666667
-10.0 6.666666666666667
+8.166666666666666 6.0
+8.166666666666666 7.5
+9.833333333333334 7.5
   0
-T3                       1.0 0 0 1 1 5.666666666666667 5.833333333333333 5.645833333333333 5.640625 5.75 5.901041666666667 0
+T3                       1.0 0 0 1 1 5.5 6.666666666666667 5.479166666666667 6.473958333333333 5.583333333333333 6.734375 0
   1 10 0 0
   1
   1 7 1 0
-5.666666666666667 1.5
+5.5 2.3333333333333335
   0
-azione_locale_m          1.0 0 0 1 1 13.166666666666666 2.1666666666666665 12.697916666666666 1.890625 13.25 2.234375 0
+azione_locale_m          1.0 0 0 1 1 12.5 3.0 12.03125 2.7239583333333335 12.583333333333334 3.0677083333333335 0
   1 11 2 0
-12.583333333333334 2.1666666666666665
-12.583333333333334 1.5
+11.916666666666666 3.0
+11.916666666666666 2.3333333333333335
   1
   1 12 2 0
-13.75 2.1666666666666665
-13.75 2.8333333333333335
+13.083333333333334 3.0
+13.083333333333334 3.6666666666666665
   0
-Richiesta_Servizio       1.0 0 0 1 1 12.333333333333334 2.8333333333333335 11.791666666666666 2.640625 12.416666666666666 2.9010416666666665 0
+Richiesta_Servizio       1.0 0 0 1 1 11.666666666666666 3.6666666666666665 11.125 3.4739583333333335 11.75 3.734375 0
   1 12 0 0
   2
   1 13 1 0
-12.333333333333334 3.6666666666666665
+11.666666666666666 4.5
   1 15 2 0
-11.25 2.8333333333333335
-11.25 0.16666666666666666
+10.916666666666666 3.6666666666666665
+10.916666666666666 1.0
   0
-Attesa_Elaborazione      1.0 0 0 2 0 13.166666666666666 4.666666666666667 11.729166666666666 4.473958333333333 13.25 4.734375 0
+Attesa_Elaborazione      1.0 0 0 2 0 12.5 5.5 11.0625 5.307291666666667 12.583333333333334 5.567708333333333 0
   1 13 0 0
   1 18 2 0
-10.5 4.666666666666667
-10.5 5.166666666666667
+9.833333333333334 5.416666666666667
+9.833333333333334 6.0
   1
   1 14 0 0
   0
-Reset_M                  1.0 0 0 1 0 14.166666666666666 3.6666666666666665 13.942708333333334 3.4739583333333335 14.25 3.734375 0
+Reset_M                  1.0 0 0 1 0 13.5 4.5 13.276041666666666 4.307291666666667 13.583333333333334 4.567708333333333 0
   1 14 1 0
-14.166666666666666 5.166666666666667
+13.5 6.0
   1
   1 11 1 0
-14.166666666666666 1.5
+13.5 2.3333333333333335
   0
-Scelta_1                 1.0 0 0 1 1 8.666666666666666 1.0 8.46875 0.8072916666666666 8.75 1.0677083333333333 0
+Scelta_1                 1.0 0 0 1 1 8.5 1.8333333333333333 8.302083333333334 1.640625 8.583333333333334 1.9010416666666667 0
   1 15 1 0
-10.0 1.0
+9.833333333333334 1.8333333333333333
   1
   1 17 0 0
   0
-Scelta_2                 1.0 0 0 1 1 8.666666666666666 2.0 8.46875 1.8072916666666667 8.75 2.0677083333333335 0
+Scelta_2                 1.0 0 0 1 1 8.5 2.8333333333333335 8.302083333333334 2.640625 8.583333333333334 2.9010416666666665 0
   1 15 1 0
-10.0 2.0
+9.833333333333334 2.8333333333333335
   1
   1 16 0 0
   0
-copy_azione_locale_m     1.0 0 0 1 1 16.5 2.1666666666666665 15.848958333333334 1.890625 16.583333333333332 2.234375 0
+copy_azione_locale_m     1.0 0 0 1 1 15.833333333333334 3.0 15.182291666666666 2.7239583333333335 15.916666666666666 3.0677083333333335 0
   1 19 2 0
-15.916666666666666 2.1666666666666665
-15.916666666666666 1.5
+15.25 3.0
+15.25 2.3333333333333335
   1
   1 20 2 0
-17.083333333333332 2.1666666666666665
-17.083333333333332 2.8333333333333335
+16.416666666666668 3.0
+16.416666666666668 3.6666666666666665
   0
-copy_Richiesta_Servizio  1.0 0 0 1 1 15.666666666666666 2.8333333333333335 14.942708333333334 2.640625 15.75 2.9010416666666665 0
+copy_Richiesta_Servizio  1.0 0 0 1 1 15.0 3.6666666666666665 14.276041666666666 3.4739583333333335 15.083333333333334 3.734375 0
   1 20 0 0
   2
   1 21 1 0
-15.666666666666666 3.6666666666666665
+15.0 4.5
   1 15 2 0
-15.0 2.8333333333333335
-15.0 0.16666666666666666
+14.333333333333334 3.6666666666666665
+14.333333333333334 1.0
   0
-copy_Attesa_Elaborazione 1.0 0 0 2 0 16.5 4.666666666666667 14.880208333333334 4.473958333333333 16.583333333333332 4.734375 0
+copy_Attesa_Elaborazione 1.0 0 0 2 0 15.833333333333334 5.5 14.213541666666666 5.307291666666667 15.916666666666666 5.567708333333333 0
   1 21 0 0
   1 18 3 0
-15.166666666666666 4.666666666666667
-15.166666666666666 5.166666666666667
-15.166666666666666 6.666666666666667
+14.5 5.5
+14.5 6.0
+14.5 7.5
   1
   1 22 0 0
   0
-copy_Reset_M             1.0 0 0 1 0 17.5 3.6666666666666665 17.09375 3.4739583333333335 17.583333333333332 3.734375 0
+copy_Reset_M             1.0 0 0 1 0 16.833333333333332 4.5 16.427083333333332 4.307291666666667 16.916666666666668 4.567708333333333 0
   1 22 1 0
-17.5 5.166666666666667
+16.833333333333332 6.0
   1
   1 19 1 0
-17.5 1.5
+16.833333333333332 2.3333333333333335
   0
--- a/anno3/vpc/consegne/2/gspn/Es2C.PNPRO
+++ b/anno3/vpc/consegne/2/gspn/Es2C.PNPRO
--- a/anno3/vpc/consegne/2/gspn/EsD.PNPRO
+++ b/anno3/vpc/consegne/2/gspn/EsD.PNPRO
--- a/anno3/vpc/consegne/3/analisi.org
+++ b/anno3/vpc/consegne/3/analisi.org
@ -87,13 +87,9 @@ AG (#Q1==1 -> EF (#Q3 == 1))
 #+END_SRC
 \includepdf{3.2.jpg}
 ** Algebra dei processi
-L'algoritmo 3.6 modellato secondo NuSMV e GreatSPN mostra che non c'e`
-la mutua esclusione.
-Questo viene evidenziato anche dal fatto che i nodi del Reachability
-Graph corrispondo al prodotto cartesiano P×Q.
-Anche il Derivation Graph del modello in algebra dei processi ha 25
-nodi ed e` equivalente al Reachability Graph.
-| System = {(P₁ \vert{}\vert{} Q₁) \vert{}\vert{} Tₚ} \ttvar{\ }Sync
+Riportiamo il modello dell'algoritmo 3.2 secondo l'algebra dei
+processi.
+| System = {(P₁ \vert{}\vert{} Q₁) \vert{}\vert{} Tₚ} \ttvar{/ }Sync
 | S =  {localₚ, local_{q}, criticalₚ, critical_{q}}
 | Sync = {isₚ, is_{q}, setₚ, set_{q}}

@ -110,8 +106,8 @@ nodi ed e` equivalente al Reachability Graph.
 | Q₃ ::= critical_{q}.Q₄
 | Q₄ ::= set_{p}.Q₁

-\includepdf{rg_3.6.jpg}
-\includepdf{derivation_3.6.jpg}
+\includepdf{rg_3.2.jpg}
+\includepdf{derivation_3.2.jpg}

 ** Risultati
 Nella tabella mostriamo i risultati ottenuti
@ -322,10 +318,14 @@ AG (#Q2 == 1 -> AF (#Q4 == 1))
 #+END_SRC
 \includepdf{3.6.jpg}
 ** Algebra dei processi
-Riportiamo il modello dell'algoritmo 3.2 secondo l'algebra dei
-processi.
+L'algoritmo 3.6 modellato secondo NuSMV e GreatSPN mostra che non c'e`
+la mutua esclusione.
+Questo viene evidenziato anche dal fatto che i nodi del Reachability
+Graph corrispondo al prodotto cartesiano P×Q.
+Anche il Derivation Graph del modello in algebra dei processi ha 25
+nodi ed e` equivalente al Reachability Graph.

-| System = {(P₁ \vert{}\vert{} Q₁) \vert{}\vert{} (Wantₚ₀ \vert{}\vert{} Want_{q}₀)} \ttvar{\ }Sync
+| System = {(P₁ \vert{}\vert{} Q₁) \vert{}\vert{} (Wantₚ₀ \vert{}\vert{} Want_{q}₀)} \ttvar{/ }Sync
 | Sync = { isTrueₚ, isFalseₚ, setTrueₚ, setFalseₚ,
 | \enspace{}\quad{}\quad{} isTrue_{q}, isFalse_{q}, setTrue_{q}, setFalse_{q} }
 | S = {localₚ, criticalₚ, local_{q}, critical_{q}}
@ -347,6 +347,9 @@ processi.
 | Q₅ ::= setFalse_{q}.Q₁


+\includepdf{rg_3.6.jpg}
+\includepdf{derivation_3.6.jpg}
+
 ** Risultati
 Nella tabella mostriamo i risultati ottenuti
 |                     | NuSMV | GreatSPN |
--- a/anno3/vpc/consegne/3/analisi.pdf
+++ b/anno3/vpc/consegne/3/analisi.pdf
--- a/anno3/vpc/consegne/4/uppaallC.xml
+++ b/anno3/vpc/consegne/4/uppaallC.xml
@ -285,6 +285,7 @@ clock fc;

 clock timer0;
 clock timer1;
+clock attesa;

 bool next = 0;
 </declaration>
@ -319,7 +320,8 @@ bool next = 0;
 			<target ref="id21"/>
 			<label kind="synchronisation" x="-1640" y="-145">ML!</label>
 			<label kind="assignment" x="-1666" y="-128">timer0 := 0,
-fc := 0</label>
+fc := 0,
+attesa := 0</label>
 		</transition>
 		<transition>
 			<source ref="id23"/>
@ -353,7 +355,7 @@ fc := 0</label>
 next := !next</label>
 		</transition>
 	</template>
-	<system>sender = Sender_2t();
+	<system>sender = Sender_1t();
 receiver = Receiver();
 link = Link();

--- a/todo.org
+++ b/todo.org
@ -1,24 +1,29 @@
-* TODO VPC [10/19]
+* TODO VPC [16/19]
 - [X] chiedi della riduzione
 - [X] calcolo semiflussi come da mail
 - [X] chiedi dell'esame
 - [X] Es1: definizioni
 - [X] Rimuovi parte in cui parli di archi inibitori
- [ ] Chiedi a Daniel come da p-semiflows deadlock
- [ ] Chiedi a Daniel come da p-semiflows liveness
- [ ] spiega nelle relazioni che bounded se RS finito
- [ ] spiega nelle relazioni che bounded quando coperta da p-semiflows
+- [X] Chiedi a Daniel come da p-semiflows deadlock
+- [X] Chiedi a Daniel come da p-semiflows liveness
+- [X] spiega nelle relazioni che bounded se RS finito
+- [X] spiega nelle relazioni che bounded quando coperta da p-semiflows
 - [X] Vedi bisimulazione ed equivalenze in teoria analisi
- [ ] Teoria [0/3]
+- [ ] Teoria [0/8]
  - [ ] Hierarchy of equivalences
  - [ ] algebra.extra.lucca: internal/external choices
  - [ ] Observer e testing equivalence
- [-] rete A, b, c, d [2/3]
-  - [ ] Spiega p-t-semiflows analysis: deadlock e liveness, boundness
+  - [ ] Vedi bene legge conservazione token
+  - [ ] Vedi bene fairness, liveness come formule?
+  - [ ] Vedi da relazioni procedure dimostrazione deadlock
+  - [ ] Impara equivalenze come le spiega lei
+  - [ ] Formalizza algoritmo bisimulazione
+- [X] rete A, b, c, d [3/3]
+  - [X] Spiega p-t-semiflows analysis: deadlock e liveness, boundness
  - [X] sulle slide, quando si chiede come deve  decidere il master
  - [X] Sistema screenshots di GSPN non tagliati
 - [X] rete E, F -> Controlla sia finito
- [-] Analisi [18/23]
+- [-] Analisi [18/22]
  - [X] Spiega perche` non hai usato process
  - [X] Riguardo RGGMED4, non posso scrivere ltl equiparabile a ctl?
  - [X] Specifica all'inizio che usi condizione piu` bassa per deadlock
@ -28,7 +33,6 @@
    - [X] modellazione
    - [X] rg vs dg
    - [ ] equivalenza e bisimulazione
-  - [ ] Spiega p-t-semiflows analysis: deadlock e liveness, boundness
  - [X] 3.2, 3.5 rifai immagini e ctl con nuovi nomi spazi / transizioni
  - [ ] E` algebra CSP? Specifica
  - [X] Vedi necessita` di Sync e /
@ -46,11 +50,11 @@
  - [X] chiedi a lei di safety, liveness, fairness
  - [ ] mi sa non finito
 - [X] uppal, es 4 [4/4]
-  - [X] Galla`: su uppaall e` stato lui a scegliere i valori numerici_tempo
+  - [X] Galla`: su uppaal e` stato lui a scegliere i valori numerici_tempo
  - [X] Come si prende intervallo attesa richiesto da Donatelli?
  - [X] Fai intervallo attesa
  - [X] Cambia nomi
- [ ] CSP: che significa sync?
+- [X] CSP: che significa sync?
 - [X] controlla esercizi nuovi
 - [X] Controlla bene e studia Symbolic Reachability Graph: perche` cosi` buono?
 - [ ] Confrontare esercizi con Galla`