In questa formula abbiamo 2 volte EG.

• E -> esiste un cammino
• G -> globally

Intuizione

Dobbiamo controllare se esiste un un percorso in cui (right -> EG(left)) è vera. Iniziamo il controllo elencando alcuni dei possibili percorsi:

1. S0, S1, S2, S0, S1 ....
2. S0, S0, S1, S2, S0, S1 ....
3. S0, S0, S0, ...., S0 , ....

Path 1

Al passo 1 possiamo calcolare direttamenete il risultato infatti se l'altecedente è falso la formula è vera.

Per calcolare al passo 2 se la formula è vera dobbiamo calcolare EG(Left). Dobbiamo vedere se nel futuro left è sempre vera. Questo non è il caso infatti nello stato S2 e nello stato S0 left è falsa

Come ulteriore esempio se eseguiamo solamente right-> EG(Left) modificando le variabili e partendo dallo stato S1

Abbiamo quindi compreso che nello stato S1 la formula è falsa.

Path 2

Nel secondo path, come nel precendete si incontra lo stato S1 quindi la formula è falsa.

Path 3

Nel terzo path il nostro stato è sempre lo stato S0. Come abbiamo visto nel path1 nello stato S0 la formula è vera. Abbiamo trovato un path per cui la formula EG(right -> EG(left)) è sempre vera.

Grazie a NuSMV riusciamo a dimostrare, che EG(right -> EG(left)) soddisfa il modello.

[Partendo dallo stato S1 al posto dello stato S0 la formula è falsa.]

Algoritmo di labeling

[teoria]

Per dimostrare se la formula EG è vera usiamo una equivalenza: 𝐸𝐺𝜑 ≡ 𝜑 ∧ 𝐸𝑋(𝐸𝐺𝜑)

Questo ci permette di usare riscrivere la formula e usare il connettivo 𝐸𝑋.

Successivamente si può usare la definizione 𝑃𝑟𝑒[𝜑] = 𝐸𝑋[𝜑]  per poter riscrivere la formula come:

[𝐸𝐺(𝜑)] = [𝜑] ∩ 𝑃𝑟𝑒([𝐸𝐺𝜑])

• [𝜑] gli stati dove la formula [𝜑] è vera INTERSEZIONE ∩
• la pre-immagine di [𝐸𝐺𝜑] <- (loop)

Si ricorsivamente calcolare X:= [EG𝜑] nel seguente modo:

passo 1  X1 := [𝜑]  ---> tutti gli stati dove la formula 𝜑 è vera.

passo 2 X2 := X1 ∩ INTERSEZIONE PreImage(X1)  ---> calcolo tutti gli stati che mi riescono a portare negli stati contenuti nelll'insieme X1

passo 3 Xc := X2 ∩ INTERSEZIONE PreImage(X2)  ---> calcolo tutti gli stati che mi riescono a portare negli stati contenuti nelll'insieme X2

passo n Xn := X_n+1 ∩ INTERSEZIONE PreImage(X_n+1)  ---> calcolo tutti gli stati che mi riescono a portare negli stati contenuti nelll'insieme X_n+1

Quando il passo successivo è uguale al passo precendente --> si è raggiunto un "punto fisso" e quindi è possibile fermarsi

[svolgimento]

La prima operazione da svolgere è riscrivere la formula usando l'equivalenza che utilizza la funzione pre-image

Ricorsivamente si possono calcolare i passi successivi

Bisogna successivamente calcolare la pre-image

Si devono trovare gli stati in cui [EG(p)] è vero

Si può riscrivere l'implicazione con dei connettivi booleani

L'intersezione ci permette di trovare lo stato in cui la formula è vera: {S0}

In questa formula:

• E -> esiste un cammino
• F -> finally, nel futuro
• G -> globally, sempre nel futuro

Intuizione

La formula 𝜑 è la composizione di 2 formule EF(right) ed EG(left)

EF(right) controlla che nel futuro right diventi vera almeno una volta.

EG(left) controlla che nel futuro left sia sempre vera. Questo è sempre falso.

• se percorriamo sempre il grafo S0, S0, S0, S0, S0, ... abbiamo che la prima parte dell'implicazione EF(right) è sempre falsa e quindi che la formula 𝜑 è sempre vera
• se percorriamo il percorso S0,S1,S2,S0, ... EF(right) diventa vera ma poichè EG(left) è sempre falsa, la formula 𝜑 è sempre falsa

Quando eseguiamo l'esercizio il programma restituisce che la formula è falsa.

Algoritmo di labeling

[teoria]

Possiamo riscrivere EF(𝜑) come E(true UNTILL 𝜑)

Visto che true è ovviamente sempre vero si riesce ad esprimere che la formula 𝜑 sarà vera nel futuro

Per calcolare tutti i passaggi usiamo la seguente equivalenza:

𝐸(𝜑 𝑈 𝜓 ) ≡ 𝜓 ∨ ( 𝜑 ∧ 𝐸𝑋(𝐸 𝜑𝑈𝜓 ))  ----> phi untill psi

Questa uguaglianza si può riassumere come:

𝜓 deve essere vera nello stato in cui stiamo partendo OR

𝜑 deve essere vera nello stato in cui stiamo partendo AND nello stato successivo dobbiamo controllare ancora che 𝐸 ( 𝜑 𝑈 𝜓) <-- loop

Possiamo definirre [𝐸 ( 𝜑 𝑈 𝜓)]  come

[𝜓] ∪ ( [𝜑] ∩ PRE-IMAGES( [(𝐸(𝜑𝑈𝜓))

• stati in cui 𝜓 è vera UNIONE
• stati in cui 𝜑 è vera INTERSEZIONE
• PRE-IMAGES [𝐸(𝜑𝑈𝜓)]

Si riesce a calcolare X:= [𝐸 ( 𝜑 𝑈 𝜓)] con l'induzione

• X₁ := [𝜓]   ---> iniziamo calcolando gli stati in cui 𝜓 è vera, AGGIUNGIAMO
• 𝑋₂ ∶= 𝑋₁ ∪ ( [𝜑] ∩ 𝑃𝑟𝑒 (𝑋₁) )  X1 AGGIUNGIAMO stati in cui ( 𝜑 è vera INTERSEZIONE pre-images X₁ )
• 𝑋₃ ∶= 𝑋₂ ∪ ( [𝜑] ∩ 𝑃𝑟𝑒 (𝑋₂))
• 𝑋_n+1 ∶= 𝑋_n ∪ ( [𝜑] ∩ 𝑃𝑟𝑒 (𝑋_n))

Quando Xn+1 è uguale a X_n allora si è raggiunto un punto di uscita nell'algoritmo.

[svolgimento]

La prima espressione da calcolare è EF(right). Può essere scritta anche in quest'altro modo:

Ricorsivamente si possono calcolare i passi successivi. Nel primo passo {S1,S2} soddisfa la formula RIGHT e si "salvano" in X1

Nel passo successivo si calcolano i passi precendenti a {S1,S2}. L'insieme finale è {S0,S1,S2}

Si può riscrivere l'implicazione e quindi calcolare gli stati dove la formula è vera

Non ci sono stati, e quindi la formula è sempre falsa

In questa formula:

• E -> esiste un cammino
• F -> finally, nel futuro

Intuizione

La formula 𝜑 vuole scoprire se nel futuro è possibile che ci sia uno stato in cui right e left sono veri

Quando eseguiamo l'esercizio il programma restituisce che la formula è vera.

Algoritmo di labeling

[teoria]

Come nell'esempio di prima 111

[svolgimento]

Il primo passo è da calcolare è EF(right AND left). Può essere scritta anche in quest'altro modo:

Ricorsivamente si possono calcolare i passi successivi. Nel primo passo solo S2 soddisfa la formula

Nel secondo passo si trova il passo precedente che porta ad S2 ovvero S1. L'insieme delle soluzioni è {S2,S1}

Il passo successivo è aggiungere gli stati che possono portare a {S2,21}

{S0,S1,S2} soddisfano la forumula, che quindi in ogni stato è vera

A partire da un modello di transizione 𝑀 = (𝑆, →, 𝐿) possiamo codificare ogni stato in base ai valori delle variabili che lo compongono. Nel nostro esercizio il primo valore rappresenta la variabile right la seconda la variabile left. Avendo solo 2 variabili sono sufficienti 2 cifre.

Quindi 01 vuol dire che right è falso mentre left è vero.

Una volta fissato l'ordine delle variabili si può rappresentare il modello anche in un quest'altro modo.

Con questa codifica ogni stato può essere rappresentato da una formula:

Viene indicata con e(s) la formula associata ad uno stato. Ogni insieme di stati Q ⊆ 𝑆 può quindi essere associato alla formula.

Nel nostro esercizio abbiamo:

Per rappresentare le transizioni del modello si inizia creado n uteriori variabili. Le nuove variabili saranno tante quante sono le variabili nel nel sistema.

La prima operazione è la costruzione di una tabella. Ogni arco nel sistema è rappresentato da una riga in tabella.

Leggendo la riga la prima metà delle colonne codifica lo stato dove sono, la seconda metà delle colonne codifica lo stato successivo.

Nel nostro esercizio avvremmo la seguente tabella:

Una volta creata la tabella possiamo scrivere la formula in DNS. 

Prendiamo il valore negato se la variabile è false mentre invece prendiamo il valore non negato se la variabile è positiva.

La formula risultate sarà vera se almeno una "riga" sarà vera. Nel nostro esempio la formula sarà:

Un altro metodo per scrivere la formula è partire direttamente dal programma scritto in NuSMV.

Una volta ottenuta la formula possiamo analizzare il grafo OBDD associato:

Il grafo è costruito collegando le varie variabili tra di loro. L'ordine delle variabili è fondamentale per crere il grafo infatti cambiando l'ordine cambia anche il grafo.

L'ordine che è stato seguito in questo caso è stato X₁, X₂, X₁', X₂'