es 3.6

anno3/vpc/consegne/3/.#3.2.b.smv

@@ -1 +0,0 @@
-user@thinkgentoo.14302:1588838104

anno3/vpc/consegne/3/3.6-Measures.solution/PT.bnd

@@ -0,0 +1,14 @@
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1
+0 1

anno3/vpc/consegne/3/3.6-Measures.solution/PT.ctl

@@ -0,0 +1,8 @@
+% MEASURE1
+AG(!(#critical_P == 1) || !(#critical_Q == 1)) 
+% MEASURE2
+AG ((#await_P==1 || #await_Q == 1) -> AF (#critical_P == 1 || #critical_Q == 1)) 
+% MEASURE3
+AG(#await_P == 1 -> EF(#critical_Q==1 || #critical_P == 1))
+% MEASURE4
+AG (#await_P==1 -> AF (#critical_P == 1))

anno3/vpc/consegne/3/3.6-Measures.solution/PT.def

@@ -0,0 +1,3 @@
+|256
+%
+|

anno3/vpc/consegne/3/3.6-Measures.solution/PT.ilpbnd

@@ -0,0 +1,2 @@
+0
+0

anno3/vpc/consegne/3/3.6-Measures.solution/PT.net

@@ -0,0 +1,90 @@
+|0|
+|
+f 0 14 0 10 0 0 0
+local_P     1 2.6666666666666665 1.0 2.9612499999999997 0.945625 0
+await_P     0 2.6666666666666665 2.3333333333333335 2.8518749999999997 2.1122916666666667 0
+SetTrue_P   0 2.6666666666666665 3.6666666666666665 2.857083333333333 3.6122916666666662 0
+critical_P  0 2.6666666666666665 5.166666666666667 3.0549999999999997 5.278958333333333 0
+setFalse_P  0 2.6666666666666665 6.666666666666667 2.857083333333333 6.695625 0
+wantP_FALSE 1 5.166666666666667 6.5 4.716458333333333 6.695625 0
+wantP_TRUE  0 4.0 6.166666666666667 4.320625 6.028958333333333 0
+wantQ_FALSE 1 6.0 2.3333333333333335 5.794583333333333 2.6122916666666667 0
+wantQ_TRUE  0 7.166666666666667 2.3333333333333335 6.39875 1.945625 0
+setFalse_Q  0 8.333333333333334 2.1666666666666665 8.518541666666666 2.3622916666666667 0
+critical_Q  0 8.333333333333334 3.6666666666666665 8.627916666666666 3.8622916666666662 0
+setTrue_Q   0 8.333333333333334 5.166666666666667 8.695625 5.195625 0
+await_Q     0 8.333333333333334 6.166666666666667 8.096666666666666 6.362291666666667 0
+local_Q     1 8.333333333333334 7.5 8.700833333333334 7.112291666666667 0
+T0  1.0 0 0 1 0 2.6666666666666665 1.6666666666666667 2.6458333333333335 1.4739583333333333 2.75 1.734375 0
+   1 1 0 0
+   1
+   1 2 0 0
+   0
+T8  1.0 0 0 2 0 2.6666666666666665 7.5 2.6458333333333335 7.307291666666667 2.75 7.567708333333333 0
+   1 5 1 0
+2.6666666666666665 7.25
+   1 7 0 0
+   2
+   1 1 2 0
+0.75 7.5
+0.75 1.0
+   1 6 1 0
+5.166666666666667 7.5
+   0
+T3  1.0 0 0 1 0 2.6666666666666665 5.833333333333333 2.6458333333333335 5.640625 2.75 5.901041666666667 0
+   1 4 0 0
+   1
+   1 5 0 0
+   0
+T1  1.0 0 0 2 0 2.6666666666666665 3.0 2.6458333333333335 2.8072916666666665 2.75 3.0677083333333335 0
+   1 2 0 0
+   1 8 0 0
+   2
+   1 3 0 0
+   1 8 1 0
+5.166666666666667 2.3333333333333335
+   0
+T2  1.0 0 0 2 0 2.6666666666666665 4.5 2.6458333333333335 4.307291666666667 2.75 4.567708333333333 0
+   1 3 0 0
+   1 6 1 0
+5.166666666666667 4.5
+   2
+   1 4 0 0
+   1 7 0 0
+   0
+T5  1.0 0 0 2 0 8.333333333333334 1.1666666666666667 8.3125 0.9739583333333334 8.416666666666666 1.234375 0
+   1 10 0 0
+   1 9 0 0
+   2
+   1 14 2 0
+10.0 1.1666666666666667
+10.0 7.5
+   1 8 1 0
+6.0 1.1666666666666667
+   0
+T6  1.0 0 0 1 0 8.333333333333334 6.833333333333333 8.3125 6.640625 8.416666666666666 6.901041666666667 0
+   1 14 0 0
+   1
+   1 13 0 0
+   0
+T7  1.0 0 0 2 0 8.333333333333334 5.666666666666667 8.3125 5.473958333333333 8.416666666666666 5.734375 0
+   1 13 0 0
+   1 6 0 0
+   2
+   1 12 0 0
+   1 6 1 0
+6.333333333333333 5.916666666666667
+   0
+T9  1.0 0 0 2 0 8.333333333333334 4.5 8.3125 4.307291666666667 8.416666666666666 4.567708333333333 0
+   1 12 0 0
+   1 8 1 0
+6.0 4.5
+   2
+   1 11 0 0
+   1 9 0 0
+   0
+T10 1.0 0 0 1 0 8.333333333333334 2.8333333333333335 8.286458333333334 2.640625 8.416666666666666 2.9010416666666665 0
+   1 11 0 0
+   1
+   1 10 0 0
+   0

anno3/vpc/consegne/3/3.6-Measures.solution/PT.pba

@@ -0,0 +1,8 @@
+6
+5 1 1 1 2 1 3 1 4 1 5 
+4 1 1 1 2 1 3 1 7 
+4 -1 1 -1 2 -1 3 1 6 
+5 1 10 1 11 1 12 1 13 1 14 
+3 1 9 -1 10 -1 11 
+3 1 8 1 10 1 11 
+0

anno3/vpc/consegne/3/3.6-Measures.solution/PT.pin

@@ -0,0 +1,10 @@
+8
+5 1 10 1 11 1 12 1 13 1 14 
+4 1 9 1 12 1 13 1 14 
+3 1 8 1 10 1 11 
+2 1 8 1 9 
+5 1 1 1 2 1 3 1 4 1 5 
+4 1 1 1 2 1 3 1 7 
+3 1 4 1 5 1 6 
+2 1 6 1 7 
+0

anno3/vpc/consegne/3/3.6.b.smv

@@ -0,0 +1,43 @@
+MODULE main
+VAR
+    wantP: boolean;
+    wantQ: boolean;
+    p: process proc(wantP, wantQ);
+    q: process proc(wantQ, wantP);
+ASSIGN
+    init(wantP) := FALSE;
+    init(wantQ) := FALSE;
+
+CTLSPEC -- no mutual exclusion
+  AG (p.state != critical | q.state != critical)
+
+CTLSPEC -- no deadlock
+  AG ((p.state = await | q.state = await) -> AF (p.state = critical | q.state = critical))
+
+CTLSPEC -- no individual starvation
+  AG (p.state = await -> AF p.state = critical)
+CTLSPEC
+  AG (q.state = await -> AF q.state = critical)
+
+CTLSPEC -- prova: path senza starvation
+  AG (q.state = await -> EF q.state = critical)
+
+
+MODULE proc(mine, other)
+VAR
+    state: {local, await, critical, setTrue, setFalse};
+ASSIGN
+    init(state) := local;
+    next(state) := case
+                    state = local: {local, await};
+                    state = await & other = FALSE: setTrue;
+                    state = await: await;
+                    state = setTrue: critical;
+                    state = critical: setFalse;
+                    state = setFalse: local;
+                   esac;
+    next(mine) := case
+                    state = setTrue: TRUE;
+                    state = setFalse: FALSE;
+                    TRUE: mine;
+                   esac;

anno3/vpc/consegne/3/3.6.smv

@@ -33,9 +33,6 @@ CTLSPEC
 CTLSPEC -- prova: path senza starvation
   AG (q.state = await -> EF q.state = critical)
 
-CTLSPEC
-  EF(p.state = await -> AG(!(p.state = critical)))
-
 
 MODULE proc(mine, other)
 VAR

anno3/vpc/consegne/3/analisi.org

@@ -29,6 +29,9 @@ Nella tabella mostriamo i risultati ottenuti
 - [ ] Vedi necessita` di Sync e /
 - [ ] Finisci tutto con algebra dei processi
 - [ ] Reachability graph vs Derivation Graph
+- [ ] Controlla in 3.6 Starvation: nusmv no, greatspn si`
+- [ ] 3.6, dealock: correttezza spiegazione della differenza greatspn nusmv?
+- [ ] 3.6, starvation: perche` nusmv con processi non ha starvation?
 
 * TODO Proprieta` del modello
 
@@ -73,7 +76,7 @@ processi un'enumerazione di 4 stati ed una variabile turno di tipo intero.
 Il codice utilizzato per le proprieta` CTL e` il seguente:
 #+BEGIN_SRC
 AG(!(#Critical_P == 1) || !(#Critical_Q == 1)) = true
-AG ((#Wait_P==1 || \#Critical_Q == 1) -> AF (#Critical_P == 1 || \#Critical_Q == 1)) = false
+AG ((#Wait_P==1 || \#Wait_Q == 1) -> AF (#Critical_P == 1 || \#Critical_Q == 1)) = false
 AG (#Wait_P==1 -> AF (#Critical_P == 1)) = false
 #+END_SRC
 [[./3.2.jpg]]
@@ -213,10 +216,39 @@ while true:
 
 ** NuSMV
 Si e` deciso di modellare l'algoritmo usando per ognuno dei due
-processi ...
+processi usando 5 stati per ogni processo
-| CODE
+| state: {local, await, critical, setTrue, setFalse};
 #+include 3.6.smv
 
 ** GreatSPN
+Il codice utilizzato per le proprieta` CTL e` il seguente:
+#+BEGIN_SRC
+AG(!(#critical_P == 1) || !(#critical_Q == 1)) 
+AG ((#await_P==1 || \#await_Q == 1) -> AF (#critical_P == 1 || \#critical_Q == 1)) 
+AG (#await_P==1 -> AF (#critical_P == 1))
+#+END_SRC
+
 ** TODO CCS
-** Risultati
+** TODO Risultati
+Nella tabella mostriamo i risultati ottenuti
+|                     | NuSMV | GreatSPN |
+|---------------------+-------+----------|
+| Mutua Esclusione    | false | false    |
+| Assenza di deadlock | true  | false    |
+| No Starvation       | true  | false    |
+
+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
+GreatSPN e` possibile che il processo P vada nello spazio await e il
+processo Q decida di rimanere nel loop /local_Q/ all'infinito.
+Notiamo che se forziamo i processi a fare del progresso dallo stato
+/local/, allora la formula CTL 
+| G(wₚ → F(cₚ∨c_{q})
+risulta rispettata.
+Ancora meglio, piuttosto che rimuovere una transizione possibile,
+possiamo restringere la verifica dell'assenza di deadlock alla
+seguente formula CTL
+| AG (wₚ → EF (cₚ || c_{q}))
+| AG(#await_P == 1 -> EF(#critical_Q==1 || \#critical_P == 1))
+che risulta rispettata.