UniTO/anno3/vpc/consegne/3/analisi.org

* TODO [1/4]
- [X] Cosa significa FAIRNESS running alla fine dei .smv
- [ ] Completa tabelle e immagine con greatspn
- [ ] Riformula liveness
- [ ] chiedi a lei di safety, liveness, fairness

* TODO Proprieta` del modello

Ogni modello successivamente mostrato rispetta le seguenti proprieta`:
Siano /p/ e /q/ due generici processi,
1. Mutua esclusione (safety): garantisce che al piu` un solo processo e` nella
   sezione critica ad ogni istante
   | G (¬cₚ∨¬c_{q}) 
2. Assenza di deadlock (liveness): ogni qualvolta un processo e` in
   attesa di entrare nella sezione critica, eventualmente verra`
   concesso ad un processo di entrare nella sezione critica
   | G(wₚ → F(cₚ∨c_{q})
3. Assenza di starvation individuale (strong fairness): ogni qualvolta un processo e` in
   attesa di entrare nella sezione critica, eventualmente gli verra` concesso
   | G(wₚ → Fcₚ)
Possiamo convertire queste tre formule LTL in formule equivalenti CTL
anteponendo l'operatore di stato A:
   | AG (¬cₚ∨¬c_{q}) 
   | AG(wₚ → AF(cₚ∨c_{q})
   | AG(wₚ → AFcₚ)
Benche` non tutte le formule LTL possono essere convertite in una
formula CTL equivalente anteponendo ad ogni operatore temporale
l'operatore di stato A, per queste tre proprieta` possiamo.
 
* Algoritmo 3.2
Due processi iterano all'infinito seguendo questo pseudocodice

#+BEGIN_SRC 
while true:
      non-critical section
      await turn = ID
      critical section
      turn <- (ID%2)+1
#+END_SRC

** NuSMV
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};

#+include 3.2.b.smv
Nella tabella mostriamo i risultati ottenuti
|                     | NuSMV | GreatSPN |
|---------------------+-------+----------|
| Mutua Esclusione    | True  |          |
| Assenza di deadlock | True  |          |
| No Starvation       | False |          |
Il risultato della possibilita` di deadlock non deve
stupire: la specifica non obbliga un processo a terminare la fase
begin.
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:
#+BEGIN_SRC
-- specification AG ((p.state = wait | q.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
  -> State: 1.1 <-
    turn = 1
    p.state = begin
    q.state = begin
  -- Loop starts here
  -> State: 1.2 <-
    q.state = wait
  -> State: 1.3 <-

#+END_SRC
Si vede 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.