bparodi/UniTO
1
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

bisimulazione

Browse source
This commit is contained in:
Francesco Mecca 2020-05-21 20:42:06 +02:00
parent 31dba96560
commit d8099c689b
1 changed files with 29 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
anno3/vpc/consegne/3/analisi.org
View file

@ -938,9 +938,36 @@ NuSMV non possiamo rispettare il requisito di fairness.
| Assenza di deadlock | true | false | | Assenza di deadlock | true | false |
| No Starvation | true | false | | No Starvation | true | false |
* Confronto 3.2 e 3.6 * Bisimulazione
Precedentemente abbiamo modellato usando l'algebra dei processi Precedentemente abbiamo modellato usando l'algebra dei processi
l'algoritmo 3.2 e l'algoritmo 3.6. l'algoritmo 3.2 e l'algoritmo 3.6.
Entrambi hanno le seguenti azioni: Entrambi hanno le seguenti azioni:
| S = {localₚ, criticalₚ, local_{q}, critical_{q}} ∪ {τ} | 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.