diff --git a/anno3/vpc/consegne/1/1.pdf b/anno3/vpc/consegne/1/1.pdf index 0096203..076c82a 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.pdf b/anno3/vpc/consegne/2.b/2.b.pdf index 0090fa2..ab8abdd 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 70ec305..76fa5ec 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 f0e3a8a..415f661 100644 --- a/anno3/vpc/consegne/2/2.pn.org +++ b/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: -- attraverso differenti strutture slaves -- usando reti WN - - +stesso padre attraverso differenti strutture slaves o usando reti WN. ** Riduzione Una rete di petri puo` essere ridotta usando le seguendi tecniche: - fusione diff --git a/anno3/vpc/consegne/3/analisi.org b/anno3/vpc/consegne/3/analisi.org index 6fbcbb9..1cfb151 100644 --- a/anno3/vpc/consegne/3/analisi.org +++ b/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 diff --git a/anno3/vpc/consegne/3/analisi.pdf b/anno3/vpc/consegne/3/analisi.pdf index a7e2136..ad5c2cf 100644 Binary files a/anno3/vpc/consegne/3/analisi.pdf and b/anno3/vpc/consegne/3/analisi.pdf differ diff --git a/anno3/vpc/consegne/4/4.pdf b/anno3/vpc/consegne/4/4.pdf index 01fe9ff..e2766c8 100644 Binary files a/anno3/vpc/consegne/4/4.pdf and b/anno3/vpc/consegne/4/4.pdf differ diff --git a/anno3/vpc/consegne/Makefile b/anno3/vpc/consegne/Makefile index a9ebd8f..0d93969 100644 --- a/anno3/vpc/consegne/Makefile +++ b/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 diff --git a/anno3/vpc/consegne/relazione.pdf b/anno3/vpc/consegne/relazione_868611_Francesco_Mecca.pdf similarity index 96% rename from anno3/vpc/consegne/relazione.pdf rename to anno3/vpc/consegne/relazione_868611_Francesco_Mecca.pdf index e3aa310..01c9c42 100644 Binary files a/anno3/vpc/consegne/relazione.pdf and b/anno3/vpc/consegne/relazione_868611_Francesco_Mecca.pdf differ diff --git a/todo.org b/todo.org index 5c3e25a..96a3d31 100644 --- a/todo.org +++ b/todo.org @@ -1,7 +1,7 @@ -* TODO VPC [16/21] -- [ ] Controlla good latex -- [ ] Uppaal muovi cartella file -- [ ] Rimuovi "Contents" da ogni .org +* TODO VPC [21/22] +- [X] Controlla good latex +- [X] Uppaal muovi cartella file +- [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] - - [ ] clearpage su ultime immagini +- [X] Analisi [27/27] + - [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]