invio donatelli

anno3/vpc/consegne/2/2.pn.org

@@ -49,16 +49,11 @@ marcature.
 | 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 nei seguenti modi:
+stesso padre attraverso differenti strutture slaves  o usando reti WN.
-- attraverso differenti strutture slaves
-- usando reti WN
-
-
 ** Riduzione
 Una rete di petri puo` essere ridotta usando le seguendi tecniche:
 - fusione

anno3/vpc/consegne/3/analisi.org

@@ -85,6 +85,7 @@ while true:
 Si e` deciso di modellare l'algoritmo usando per ognuno dei due
 processi un'enumerazione di 4 stati ed una variabile turno di tipo intero.
 | state: {begin, wait, critical, done};
+
 \hrulefill
 \lstinputlisting[breaklines]{3.2.b.smv}
 \hrulefill
@@ -103,7 +104,7 @@ AG (#Q1==1 -> EF (#Q3 == 1))
 Riportiamo il modello dell'algoritmo 3.2 secondo l'algebra dei
 processi CSP.
 | System = {(P₁ \vert{}\vert{} Q₁) \vert{}\vert{} Tₚ} \ttvar{/ }Sync
-| S =  {localₚ, local_{q}, criticalₚ, critical_{q}}
+| Act = {localₚ, local_{q}, criticalₚ, critical_{q}}
 | Sync = {isₚ, is_{q}, setₚ, set_{q}}
 
 | Tₚ ::= isₚ.Tₚ + setₚ.Tₚ + set_{q}.T_{q}
@@ -139,8 +140,11 @@ Ne segue che anche l'assenza di starvation individuale non e`
 garantita.
 NuSMV conferma quanto detto mostrandoci un trace che fa da
 controesempio alla formula CTL:
+
+\hrulefill
 #+BEGIN_SRC
--- specification AG (p.state = wait -> AF (p.state = critical | q.state = critical))  is false
+-- specification 
+      AG (p.state = wait -> AF (p.state = critical | q.state = critical))  is false
 -- as demonstrated by the following execution sequence
 Trace Description: CTL Counterexample 
 Trace Type: Counterexample 
@@ -187,7 +191,9 @@ Trace Type: Counterexample
     p.running = FALSE
   -> State: 1.9 <-
 #+END_SRC
-Si vede che il processo q rimane nella fase begin e p, dopo essere
+\hrulefill
+\clearpage
+La traccia mostra che il processo q rimane nella fase begin e p, dopo essere
 entrato nella regione critica una volta, rimane bloccato in begin.
 Lo stesso trace mostra la possibilita` di starvation del processo.
 La rete modellata con GreatSPN ci conferma quanto visto con NuSMV.
@@ -195,6 +201,8 @@ Inoltre il trace di GreatSPN ci mostra che non potendo forzare la
 fairness del modello, i processi possono iterare indefinitamente
 nella transizione iniziale, impedendo quindi il progresso dell'altro
 processo.
+
+\hrulefill
 #+BEGIN_SRC
 Initial state is: P1(1), Turn_P(1), Q1(1)
 Initial state satisfies: E F (not ((not (Q1 = 1)) or (not E G (not (Q3 = 1))))). 
@@ -213,6 +221,8 @@ Initial state satisfies: E F (not ((not (Q1 = 1)) or (not E G (not (Q3 = 1))))).
     1.1.R.2: loop back to state 1.1.R.1.
 #+END_SRC
 
+\hrulefill
+\clearpage
 Prendiamo in considerazione la seguente formula CTL
 | AG (wₚ -> EF cₚ)
 Sia GreatSPN che NuSMV ci mostrano che il sistema modellato rispetta
@@ -234,6 +244,10 @@ while true:
 Si e` deciso di modellare l'algoritmo usando per ognuno dei due
 processi un'enumerazione di due stati e un contatore di turni intero
 | state: {await, done};
+Non si e` utilizzata la direttiva /process/ di NuSMV dato che un
+automa a stati finiti e` sufficiente a dimostrare le proprieta` del
+modello.
+
 \hrulefill
 \lstinputlisting[breaklines]{3.5.smv}
 \hrulefill
@@ -298,7 +312,6 @@ questa semplificazione.
         p.state = await
         q.state = await
     -> State: 3.2 <-
-    – specification AG (q.state = await -> EF q.state = done)  is true
   #+END_SRC
 - Possibilita` di compiere progresso:
   #+BEGIN_SRC
@@ -323,6 +336,7 @@ processi usando 5 stati
 \hrulefill
 \lstinputlisting[breaklines]{3.6.b.smv}
 \hrulefill
+\clearpage
 
 ** GreatSPN
 Il codice utilizzato per le proprieta` CTL e` il seguente:
@@ -381,6 +395,8 @@ Nella tabella mostriamo i risultati ottenuti
 Il trace di NuSMV mostra che la mutua esclusione puo` non essere
 rispettata dato che le due variabili /wantP/ e /wantQ/ possono essere
 contemporaneamente false.
+
+\hrulefill
 #+BEGIN_SRC
 -- specification AG (p.state != critical | q.state != critical)  is false
 -- as demonstrated by the following execution sequence
@@ -425,6 +441,8 @@ Trace Type: Counterexample
     wantQ = TRUE
     q.state = critical
 #+END_SRC
+\hrulefill
+\clearpage
 L'incoerenza del risultato dell'assenza di deadlock e` spiegabile dal
 fatto che nel caso di NuSMV non e` possibile che un processo rimanga
 nel primo stato (/local/) per un tempo indefinito mentre nel caso di
@@ -444,6 +462,8 @@ L'assenza di starvation individuale non e` rispettata ne` in NuSmv ne` in
 GreatSPN in quanto e`  possibile che uno dei due processi continui ad
 accedere alla sezione critica senza permettere all’altro di fare lo
 stesso.
+
+\hrulefill
 #+BEGIN_SRC
 -- specification AG (q.state = await -> AF q.state = critical)  is false
 -- as demonstrated by the following execution sequence
@@ -491,7 +511,8 @@ Trace Type: Counterexample
     wantP = FALSE
     p.state = local
 #+END_SRC
-
+\hrulefill
+\clearpage
 * Algoritmo 3.8
 Due processi iterano all'infinito seguendo questo pseudocodice
 
@@ -521,7 +542,7 @@ AG (#await_Q==1 -> AF (#critical_Q == 1))
 Inoltre, per confermare alcune ipotesi, si e` testata anche la
 seguente formula CTL:
 #+BEGIN_SRC
-AG(#await_P == 1 -> EF(#critical_Q==1 || #critical_P == 1))
+AG(#await_P == 1 -> EF(#critical_Q==1 \vert{}\vert{} #critical_P == 1))
 #+END_SRC
 che conferma la presenza di deadlock causata dalle due variabili booleane.
 #+CAPTION: Rete 3.8
@@ -539,6 +560,8 @@ conseguenza neanche la starvation individuale).
 
 Di seguito riportiamo la traccia di NuSMV che mostra che il deadlock
 avviene quando i progetti eseguono /setTrue/ nello stesso momento.
+
+\hrulefill
 #+BEGIN_SRC
 -- specification AG ((p.state = await | q.state = await) -> AF (p.state = critical | q.state = critical))  is false
 -- as demonstrated by the following execution sequence
@@ -601,9 +624,13 @@ Trace Type: Counterexample
     p.running = FALSE
   -> State: 1.10 <-
 #+END_SRC
+\hrulefill
+\clearpage
 Mostriamo invece il controesempio generato da GreatSPN che ci mostra
 una condizione di starvation individuale, dove, come in precedenza, il
 processo Q rimane in /local_Q/.
+
+\hrulefill
 #+BEGIN_SRC
 Generated counter-example: 
 ==================================== Trace ====================================
@@ -636,7 +663,8 @@ Initial state satisfies:
 
     3.1.R.2: loop back to state 3.1.R.1.
 #+END_SRC
-
+\hrulefill
+\clearpage
 * Algoritmo 3.9
 Due processi iterano all'infinito seguendo questo pseudocodice
 
@@ -661,9 +689,11 @@ Benche` non fosse necessario distinguere il set della variabile
 booleana /wantP/, si e` preferito farlo in quanto l'enumerazione di
 tutti gli stati possibili, come evidenziato dal codice che segue, non
 risulta complesso.
+
 \hrulefill
 \lstinputlisting[breaklines]{3.9.smv}
 \hrulefill
+\clearpage
 ** GreatSPN
 Il codice utilizzato per le proprieta` CTL e` il seguente:
 #+BEGIN_SRC
@@ -695,6 +725,7 @@ la condizione di deadlock.
 Viene riportato il trace di NuSMV che conferma questa ipotesi.
 GreatSPN fallisce per mancanza di RAM sulla macchina usata ma e`
 facile riprodurre il deadlock manualmente.
+\hrulefill
 #+BEGIN_SRC
 -- specification AG ((p.state = setTrue | q.state = setTrue) -> AF (p.state = critical | q.state = critical))  is false
 -- as demonstrated by the following execution sequence
@@ -792,8 +823,12 @@ Trace Type: Counterexample
     wantP = TRUE
     p.state = resetFalse
 #+END_SRC
+\hrulefill
+\clearpage
 Di seguito il trace che conferma la presenza di starvation
 individuale, sia in GreatSPN che NuSMV.
+
+\hrulefill
 #+BEGIN_SRC
 Generated counter-example: 
 ==================================== Trace ====================================
@@ -820,6 +855,9 @@ Initial state satisfies:
 
     2.1.R.2: loop back to state 2.1.R.1.
 #+END_SRC
+\hrulefill
+\clearpage
+\hrulefill
 #+BEGIN_SRC
 -- specification AG (q.state = setTrue -> AF q.state = critical)  is false
 -- as demonstrated by the following execution sequence
@@ -902,9 +940,10 @@ Trace Type: Counterexample
   -> State: 3.13 <-
     p.state = setFalse
 #+END_SRC
+\hrulefill
+\clearpage
 * Algoritmo di Dekker per la mutua esclusione
 Due processi iterano all'infinito seguendo questo pseudocodice
-
 #+BEGIN_SRC 
 while true:
     non-critical section
@@ -923,11 +962,13 @@ while true:
 ** NuSMV
 Si e` deciso di modellare l'algoritmo usando per ognuno dei due
 processi usando 9 stati 
-| state: {local, set_true, while, loop_set_false, await, loop_set_true, critical, switch_turn, set_false};
+- state: {local, set_true, while, loop_set_false, await,
+  loop_set_true, critical, switch_turn, set_false};
+
 \hrulefill
 \lstinputlisting[breaklines]{dekker_WN.smv}
 \hrulefill
-
+\clearpage
 ** GreatSPN
 Il codice utilizzato per le proprieta` CTL e` il seguente:
 #+BEGIN_SRC

anno3/vpc/consegne/Makefile

@@ -4,5 +4,5 @@ all:
 	cd 2.b && make
 	cd 3 && make
 	cd 4 && make
-	gs -dBATCH -dNOPAUSE -q -sDEVICE=pdfwrite -dPDFSETTINGS=/prepress -sOutputFile=relazione.pdf \
+	gs -dBATCH -dNOPAUSE -q -sDEVICE=pdfwrite -dPDFSETTINGS=/prepress -sOutputFile=relazione_868611_Francesco_Mecca.pdf \
 		1/1.pdf 2/2.pdf 2.b/2.b.pdf 3/analisi.pdf 4/4.pdf

todo.org

@@ -1,7 +1,7 @@
-* TODO VPC [16/21]
+* TODO VPC [21/22]
-- [ ] Controlla good latex
+- [X] Controlla good latex
-- [ ] Uppaal muovi cartella file
+- [X] Uppaal muovi cartella file
-- [ ] Rimuovi "Contents" da ogni .org
+- [X] Rimuovi "Contents" da ogni .org
 - [X] chiedi della riduzione
 - [X] calcolo semiflussi come da mail
 - [X] chiedi dell'esame
@@ -21,16 +21,16 @@
   - [ ] Vedi da relazioni procedure dimostrazione deadlock
   - [ ] Impara equivalenze come le spiega lei
   - [ ] Formalizza algoritmo bisimulazione
-- [X] rete A, b, c, d [5/5]
+- [X] rete A, b, c, d [6/6]
   - [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] Controlla riduzione se hai fuso posti con archi uscenti
   - [X] Rifai la riduzione e controlla fusione con archi uscenti
-  - [ ] chiedi Daniel riduzione
+  - [X] chiedi Daniel riduzione
 - [X] rete E, F -> Controlla sia finito
-- [-] Analisi [26/27]
+- [X] Analisi [27/27]
-  - [ ] clearpage su ultime immagini 
+  - [X] clearpage su ultime immagini 
   - [X] Riduzione???
   - [X] Inverti S14 e S13
   - [X] Derivation graph errori [5/5]
@@ -73,7 +73,7 @@
 - [X] CSP: che significa sync?
 - [X] controlla esercizi nuovi
 - [X] Controlla bene e studia Symbolic Reachability Graph: perche` cosi` buono?
-- [ ] Confrontare esercizi con Galla`
+- [X] Confrontare esercizi con Galla`
 
 
 * Prog Mobile [2/5]