diff --git a/anno3/vpc/consegne/3/analisi.org b/anno3/vpc/consegne/3/analisi.org index 768d0fa..c636992 100644 --- a/anno3/vpc/consegne/3/analisi.org +++ b/anno3/vpc/consegne/3/analisi.org @@ -938,9 +938,36 @@ NuSMV non possiamo rispettare il requisito di fairness. | Assenza di deadlock | true | false | | No Starvation | true | false | -* Confronto 3.2 e 3.6 +* Bisimulazione Precedentemente abbiamo modellato usando l'algebra dei processi l'algoritmo 3.2 e l'algoritmo 3.6. Entrambi hanno le seguenti azioni: | S = {localₚ, criticalₚ, local_{q}, critical_{q}} ∪ {τ} - +Si applica l'algoritmo del partizionamento per verificare +l'equivalenza tramite bisimulazione. +Questo lo stato iniziale +| {S0, R0}, {S1, S2, S3, S4, S5, S6, S7, S8, S9, S10, S11, S12, S13, S14 +| R1, R2, R2, R3, R4, R5, R6, R7, R8, R9, R10, R11, R12, R13, R14, R15, +| R16, R17, R18, R19, R20, R21, R22, R23, R24} +Applico lo split considerando l'azione /criticalₚ/ +| {S0, R0}, {S4, S5, R4, R14, R18, R19, R24} +| {S1, S2, S3, S6, S7, S8, S9, S10, S11, S12, S13, R1, R2, R3, R5, R6, +| R7, R8, R9, R10, R11, R12, R13, R15, R16, R17, R20, R21, R22, R23} +Applico lo split considerando l'azione /critical_{q}/ +| {S0, R0}, {S4, S5, R4, R14, R19, R24}, {R18}, {S11, S14, R9, R11, R16, R22} +| {S1, S2, S3, S6, S7, S8, S9, S10, S12, S13, R1, R2, R3, R5, R6, +| R7, R8, R10, R12, R13, R15, R17, R20, R21, R23} +Notiamo che R18 compare come unico elemento di un insieme. Benche` +l'algoritmo non sia terminato, questo ci basta per concludere che non +c'e` bisimulazione fra i due algoritmi. Nell'algoritmo 3.2 non compare +nessuno stato da cui e` possibile effettuare l'azione /criticalₚ/ o +l'azione /critical_{q}/. Questo risultato si poteva dedurre dal fatto +che l'algoritmo 3.6 a differenza del 3.2 non rispetta la mutua +esclusione e quindi vi sono degli stati non rappresentabili nel +modello dell'algoritmo 3.2. Si noti che non e` strettamente necessario +mascherare le azioni /isₚ/, /is_/q/, /setₚ/, set_/q/ in quanto +presenti in entrambi i modelli. Nel caso di bisimulazione fra due +modelli, l'algoritmo raggiunge la terminazione quando non e` piu` +possibile partizionare gli insieme in base alle azioni comuni e +abbiamo come risultato che in ogni set compare uno stato di un modello +insieme ad uno o piu` stati dell'altro.