diff --git a/anno3/vpc/consegne/3/3.6-Measures.solution/PT.ctl b/anno3/vpc/consegne/3/3.6-Measures.solution/PT.ctl index bfc8e84..c7f2c4c 100644 --- a/anno3/vpc/consegne/3/3.6-Measures.solution/PT.ctl +++ b/anno3/vpc/consegne/3/3.6-Measures.solution/PT.ctl @@ -1,8 +1,2 @@ -% 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)) +% MEASURE0 +AG(AF(#critical_P == 1)) diff --git a/anno3/vpc/consegne/3/3.6-Measures.solution/PT.net b/anno3/vpc/consegne/3/3.6-Measures.solution/PT.net index 8894082..153c1e2 100644 --- a/anno3/vpc/consegne/3/3.6-Measures.solution/PT.net +++ b/anno3/vpc/consegne/3/3.6-Measures.solution/PT.net @@ -1,6 +1,6 @@ |0| | -f 0 14 0 10 0 0 0 +f 0 14 0 12 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 @@ -52,6 +52,18 @@ T2 1.0 0 0 2 0 2.6666666666666665 4.5 2.6458333333333335 4.307291666666667 2.75 1 4 0 0 1 7 0 0 0 +T00 1.0 0 0 1 0 1.3333333333333333 0.5 1.2864583333333333 0.3072916666666667 1.4166666666666667 0.5677083333333334 0 + 1 1 1 0 +2.0833333333333335 0.5833333333333334 + 1 + 1 1 0 0 + 0 +T4 1.0 0 0 1 1 9.0 8.333333333333334 8.979166666666666 8.140625 9.083333333333334 8.401041666666666 0 + 1 14 0 0 + 1 + 1 14 1 0 +8.5 8.25 + 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 diff --git a/anno3/vpc/consegne/3/analisi.org b/anno3/vpc/consegne/3/analisi.org index b35fade..aebf098 100644 --- a/anno3/vpc/consegne/3/analisi.org +++ b/anno3/vpc/consegne/3/analisi.org @@ -32,6 +32,10 @@ Nella tabella mostriamo i risultati ottenuti - [ ] 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? +- [ ] 3.6, perche` Amparore ha detto che deadlock: AG(EF(#critical_P == 1)) ?? + +NOTA: nel caso di Ampararore, la formula: +| da qualsiasi stato e` sempre possibile arrivare a critical_P == 1 * TODO Proprieta` del modello