# TP NuSMV

### Julien Doutre - Ronan Pelliard

## Exercice 3

#### Il y a toujours p: `G p`
#### Il y a p une infinité de fois : `G(F p)`
#### Il n'y a jamais p et q simultanément: `G(!(p&q))`

Ces trois propriétés sont vérifiées par le modèle suivant :

MODULE main

VAR
    p: boolean;
    q: boolean;

ASSIGN
    init(p) := TRUE;
    init(q) := FALSE;

    next(p) := TRUE;
    next(q) := FALSE;

LTLSPEC G p;
LTLSPEC G(F p);
LTLSPEC G(!(p&q));

#### Après chaque occurence de p il y a une occurence de `q` : `p => F q`

MODULE main
VAR
    p : boolean ;
    q : boolean ;
ASSIGN
    init(p) := TRUE;
    init(q) := TRUE;

    next(p) := p;
    next(q) := q;

LTLSPEC G(p -> F q)

représente un automate à quatre états (produits cartésien de deux variables booléennes `p` et `q`). Son état initial ne mène que vers lui même et ce faisant si p vrai, q sera vrai à l'état suivant.

#### S’il y a une infinité de p1 et une infinité de p2 alors toute occurrence de q1 est suivie d’une occurrence de q2 : `G(F p1) & G(F p2) -> G(q1 -> F q2)`

MODULE main

VAR
    p1: boolean;
    p2: boolean;
    q1: boolean;
    q2: boolean;

ASSIGN
    init(p1) := TRUE;
    init(p2) := TRUE;
    init(q1) := TRUE;
    init(q2) := FALSE;

    next(p1) := TRUE;
    next(p2) := TRUE;
    next(q1) := !q1;
    next(q2) := !q2;

LTLSPEC G(F p1) & G(F p2) -> G(q1 -> F q2);

On a toujours `p1` et `p2`, `q1` et `q2` qui alternent entre `true` et `false`.

#### Avant chaque occurence de p il y a au moins une occurence de q : `!(!q U p)`
Voir le modèle suivant.

#### Entre chaque paire d'occurences de p il y a qu moins une occurence de q : `p => (G !p | (Fp => (!p U q)))`

MODULE main
VAR
    p : boolean ;
    q : boolean ;
ASSIGN
    init(p) := FALSE;
    init(q) := TRUE;

    next(p) := !p;
    next(q) := !q;

LTLSPEC !(!q U p)
LTLSPEC (p -> (G !p | (F p -> (!p U q))))

représente un automate à quatre états (produits cartésien de deux variables booléennes `p` et `q`). Son état initial mène vers un autre état inversant les valeurs de `p` et `q` et dont la seule issue est l'état initial. Ainsi on a tour à tour `p` vrai et `q` faux et inversement. Il vérifie les deux dernières propriétés.

## Exercice 4

MODULE main
VAR
    l: boolean;
    m: boolean;
    s: boolean;
    b: boolean;
INIT
    l = FALSE & m = FALSE & s = FALSE & b = FALSE;
DEFINE
    l_traverse := l xor next(l);
    m_traverse := m xor next(m);
    s_traverse := s xor next(s);
TRANS
    (
        -- Personne ne peut traverser sans etre sur la meme rive que le bateau
        !(l_traverse & b != l) & !(m_traverse & b != m) & !(s_traverse & b != s)

        -- La somme des masses de ceux qui traversent doit etre entre 0 et 60
        & toint(l_traverse) * 50 + toint(m_traverse) * 30 + toint(s_traverse) * 20 > 0 
        & toint(l_traverse) * 50 + toint(m_traverse) * 30 + toint(s_traverse) * 20 <= 60

        -- Le bateau change de rive à chaque transition
        & b != next(b)
    );

SPEC EF(l & m & s & b);

Cet automate tire profit de la définition d'automates par contraintes. Les variables représentent chaque entité et sa position par rapport à la rivière (`FALSE` si elle sur la rive gauche, et `TRUE` si elle est sur la rive droite).

L'état initial impose que tous soient sur la rive gauche.

La seule contrainte imposée sur les trajets en bateau est que la somme des masses des entités qui voyagent ne dépasse pas `60` mais soit non nulle (pour forcer un déplacement). On remarque que `e xor next(e)` est vraie uniquement si `e` a changé de rive. Donc on peut calculer la somme pondérée des voyageurs et imposer que sa valeur soit inférieure au seuil autorisé.

*In fine*, on vérifie qu'il existe une branche qui mène à l'état où toutes les entités sont sur la rive droite. La spécification est vérifiée donc le problème admet une solution.

## Exercice 5

1. Le protocole permet de simuler la propagation d'une valeur de plus en plus grande modulo K dans le sens des processus d'index croissant. Prenons un exemple. On note `p[i]` la valeur de la variable *drapeau* du process `i`. Soit un état initial où tous les `p[i]` valent `0`. Alors le process `0` est en état critique (car `p[0] == p[N-1]`) et aucun autre (car `p[k] == p[k - 1]` pour tout les autres `k`). Dans ce cas `p[0]` est mis à jour à `1`. Le processus `0` n'est plus en état critique. Par contre on a désormais `p[0] != p[1]`, donc le processus `1` est en état critique. Sa valeur doit être mise à jour à celle de `p[0]`. Cela le stabilise mais déclenche la section critique du processus `2`, et ainsi de suite... Tous les processus vont ainsi passer dans leur état critique jusqu'à atteindre le dernier qui en changeant de valeur va redéclencher la criticité de `0`, incrémentant sa valeur de `1` et relançant un nouveau cycle avec cette nouvelle valeur.

2. Ce systè vérifie la propriété suivante :
* chaque processus est le seul à être dans un état critique une infinité de fois

3. Voici une proposition de modèle d'automate implémentant ce protocole pour $K = 4$ et $N = 3$. Les variables stockent les valeurs des drapeaux.

MODULE MAIN
VAR
    d_0: 0..4;
    d_1: 0..4;
    d_2: 0..4;
ASSIGN
    init(d_0) := 0;
    init(d_1) := 0;
    init(d_2) := 0;

    next(d_0) := case
        d_0 = d_2: (d_0 + 1) mod 5;
        TRUE: d_0;
    esac;

    next(d_1) := case
        d_0 != d_1: d_0;
        TRUE: d_1;
    esac;

    next(d_2) := case
        d_1 != d_2: d_1;
        TRUE: d_2;
    esac;
    
-- Le processus 0 sera seul processus critique une infinité de fois  
LTLSPEC G F (d_0 = d_2 & d_1 = d_0 & d_2 = d_1)
-- Le processus 1 sera seul processus critique une infinité de fois  
LTLSPEC G F (d_0 != d_2 & d_1 != d_0 & d_2 = d_1)
-- Le processus 2 sera seul processus critique une infinité de fois  
LTLSPEC G F (d_0 != d_2 & d_1 = d_0 & d_2 != d_1)

4. Si on considère $K < N$ on pourra pour certaines conditions initiales obtenir un système dans lequel deux processus ne sont jamais critiques seuls.

## Exercice 6

Le modèle suivant implémente le protocole DKR. Chaque noeud est représenté par un module, caractérisé par son `id` (constante au fil du temps), un flag `active` décrivant son mode, la valeur du leader retenu par le noeud `val`, et les valeurs reçues par les noeuds prédécesseurs `val1` et `val2`.

On considère le sens de l'anneau de P0 vers P5. L'initialisation permet d'attribuer des ids exclusifs mais aléatoires à chaque noeud, les marque comme actifs et avec `val` valant leur `id`.

Les transformations possibles suivent le protocole décrit dans l'énoncé.

MODULE ring(nxt)
VAR
  id: 0..5;
  active: boolean;
  val: 0..5;
  val1: 0..5;
  val2: 0..5;


MODULE main
VAR
  P0: ring(P1);
  P1: ring(P2);
  P2: ring(P3);
  P3: ring(P4);
  P4: ring(P5);
  P5: ring(P0);
INIT
  P0.id != P1.id &
  P0.id != P2.id &
  P0.id != P3.id &
  P0.id != P4.id &
  P0.id != P5.id &
  P1.id != P2.id &
  P1.id != P3.id &
  P1.id != P4.id &
  P1.id != P5.id &
  P2.id != P3.id &
  P2.id != P4.id &
  P2.id != P5.id &
  P3.id != P4.id &
  P3.id != P5.id &
  P4.id != P5.id &

  P0.active = TRUE &
  P1.active = TRUE &
  P2.active = TRUE &
  P3.active = TRUE &
  P4.active = TRUE &
  P5.active = TRUE &

  P0.val = P0.id &
  P1.val = P1.id &
  P2.val = P2.id &
  P3.val = P3.id &
  P4.val = P4.id &
  P5.val = P5.id;

TRANS
    (
        --- Cas ou le noeud est inactif
        (!P0.active -> (
            next(P0.val) = next(P5.val) &
            next(P0.val1) = next(P5.val1) &
            next(P0.val2) = next(P5.val2)
        )) & (
        
        --- Cas ou le noeud est actif
        P0.active -> (
        
            --- On propage la valeur du noeud précédent dans val1
            next(P0.val1) = P5.val &
            
            --- Si les valeurs concordent, on la garde
            (
                next(P0.val1) = P0.val -> next(P1.val) = P0.val
            ) & 
            
            --- Si les valeurs ne sont pas les memes,
            --- on regarde si val1 est le minimum
            (
                next(P0.val1) != P0.val & 
                next(P0.val2) = P4.val & (
                    (
                        next(P0.val1) < next(P0.val2) &
                        next(P0.val1) < P0.val
                    ) -> next(P0.val) = next(P0.val1) 
                ) & (
                    (
                        next(P0.val1) >= next(P0.val2) |
                        next(P0.val1) >= P0.val
                    ) -> next(P0.active = FALSE)
                )
            )    
        )
        )
    ) &
    (
        (!P1.active -> (
            next(P1.val) = next(P0.val) &
            next(P1.val1) = next(P0.val1) &
            next(P1.val2) = next(P0.val2)
        )) & (
        P1.active -> (
            next(P1.val1) = P0.val &
            (
                next(P1.val1) = P1.val -> next(P1.val) = P1.val
            ) & (
                next(P1.val1) != P1.val & 
                next(P1.val2) = P5.val & (
                    (
                        next(P1.val1) < next(P1.val2) &
                        next(P1.val1) < P1.val
                    ) -> next(P1.val) = next(P1.val1) 
                ) & (
                    (
                        next(P1.val1) >= next(P1.val2) |
                        next(P1.val1) >= P1.val
                    ) -> next(P1.active = FALSE)
                )
            )    
        )
        )
    ) & (
        (!P2.active -> (
            next(P2.val) = next(P1.val) &
            next(P2.val1) = next(P1.val1) &
            next(P2.val2) = next(P1.val2)
        )) & (
        P2.active -> (
            next(P2.val1) = P1.val &
            (
                next(P2.val1) = P2.val -> next(P1.val) = P2.val
            ) & (
                next(P2.val1) != P2.val &
                next(P2.val2) = P5.val & (
                    (
                        next(P2.val1) < next(P2.val2) &
                        next(P2.val1) < P2.val
                    ) -> next(P2.val) = next(P2.val1)
                ) & (
                    (
                        next(P2.val1) >= next(P2.val2) |
                        next(P2.val1) >= P2.val
                    ) -> next(P2.active = FALSE)
                )
            )
        )
        )
    ) & (
        (!P3.active -> (
            next(P3.val) = next(P2.val) &
            next(P3.val1) = next(P2.val1) &
            next(P3.val2) = next(P2.val2)
        )) & (
        P3.active -> (
            next(P3.val1) = P2.val &
            (
                next(P3.val1) = P3.val -> next(P3.val) = P3.val
            ) & (
                next(P3.val1) != P3.val & 
                next(P3.val2) = P1.val & (
                    (
                        next(P3.val1) < next(P3.val2) &
                        next(P3.val1) < P3.val
                    ) -> next(P3.val) = next(P3.val1) 
                ) & (
                    (
                        next(P3.val1) >= next(P3.val2) |
                        next(P3.val1) >= P3.val
                    ) -> next(P3.active = FALSE)
                )
            )    
        )
        )
    ) & (
        (!P4.active -> (
            next(P4.val) = next(P3.val) &
            next(P4.val1) = next(P3.val1) &
            next(P4.val2) = next(P3.val2)
        )) & (
        P4.active -> (
            next(P4.val1) = P3.val &
            (
                next(P4.val1) = P4.val -> next(P3.val) = P4.val
            ) & (
                next(P4.val1) != P4.val &
                next(P4.val2) = P2.val & (
                    (
                        next(P4.val1) < next(P4.val2) &
                        next(P4.val1) < P4.val
                    ) -> next(P4.val) = next(P4.val1)
                ) & (
                    (
                        next(P4.val1) >= next(P4.val2) |
                        next(P4.val1) >= P4.val
                    ) -> next(P4.active = FALSE)
                )
            )
        )
        )
    ) & (
        (!P5.active -> (
            next(P5.val) = next(P4.val) &
            next(P5.val1) = next(P4.val1) &
            next(P5.val2) = next(P4.val2)
        )) & (
        P5.active -> (
            next(P5.val1) = P4.val &
            (
                next(P5.val1) = P5.val -> next(P5.val) = P5.val
            ) & (
                next(P5.val1) != P5.val & 
                next(P5.val2) = P3.val & (
                    (
                        next(P5.val1) < next(P5.val2) &
                        next(P5.val1) < P5.val
                    ) -> next(P5.val) = next(P5.val1) 
                ) & (
                    (
                        next(P5.val1) >= next(P5.val2) |
                        next(P5.val1) >= P5.val
                    ) -> next(P5.active = FALSE)
                )
            )    
        )
    )
);
    
--- Verifie qu'on aboutit toujours à une election de leader
SPEC EF (P0.val = P1.val & P0.val = P2.val & P0.val = P3.val & P0.val = P4.val & P0.val = P5.val);

--- Verifie qu'on a jamais au plus un noeud actif et des valeurs de leader discordantes
SPEC !EF (
    (
        toint(P0.active) +
        toint(P1.active) +
        toint(P2.active) +
        toint(P3.active) +
        toint(P4.active) +
        toint(P5.active)
        <= 1
    ) 
& 
    (
        P0.val != P1.val |
        P0.val != P2.val |
        P0.val != P3.val |
        P0.val != P4.val |
        P0.val != P5.val 
    )
);