Introduction au language Promela et à spin
==========================================

Cette page est beaucoup plus jolie avec un plugin d'affichage
markdown installé dans votre navitateur comme par exemple https://chrome.google.com/webstore/detail/markdown-preview-plus/febilkbfcbhebfnokafefeacimjdckgl

## Installation de Spin/iSpin sous Linux

1. Cloner le dépot git suivant : https://github.com/nimble-code/Spin.git

2. Aller dans le répertoire Spin/Bin

3. Décompresser tous les fichiers qui terminent par .gz avec gunzip

4. Créer un lien symbolique s'appellant "spin" qui pointe vers la version
   qui correspond à votre système (spin650_linux64 sur les postes Linux à HEPIA)

5. Rajouter le path absolu du répertoire Spin/Bin dans votre $PATH :
   => export PATH=$PATH:~/Spin/Bin si vous avez cloné le dépôt dans votre
      répertoire de travail.

6. Aller dans le répertoire "Examples" et taper la commande "spin hello.pml"
   pour vérifier que l'interpréteur fonctionne. "Passed first test!" devrait
   s'afficher sur votre terminal.

7. Rajouter le path absolu du répertoire Spin/optional_gui dans votre $PATH

8. Vérifier que la GUI s'éxecute correctement avec la commante ispin.tcl

## Exercice 1 : Prise en main

Ecrire un programme en promela qui exécute deux
processus P1 et P2 : 

- P1 affiche les lettres de l'alphabet
en minuscule dans l'ordre en partant de 'a' 
jusqu'à 'z'.

- P2 affiche les lettres de l'alphabet dans 
l'ordre inverse en partant de 'z' jusqu'à 'a'.

P1 et P2 doivent afficher les lettres de manière concurrente.
Exécuter votre programme avec l'interpréteur 
spin et observer que l'ordonancement de l'exécution
des instructions des processus est non-déterministe.

A quoi servent les options -n et -u de l'interpréteur 
spin ? observez leur impact sur le comportement
de la simulation.
 


## Exercice 2 : Echange de message par le type chan

Ecrire une variante du programme de l'exercice précédent
dans laquelle P1 et P2 sont reliés par deux canaux (un par direction)
transportant des messages structurés par un type de message sur 8 bits,
suivi de la donnée qui est un caractère de 8 bits. La taille
du canal sera limitée à 1 message.

- Chaque lettre sera transporté par un type 'ctrl'

P1 affichera les lettres envoyées depuis P2 sur un canal et 
inversement.

A quoi sert l'option -c de l'interpréteur spin ? Observer
son effet sur la simulation des échanges de messages
entre P1 et P2.

## Exercice 3 : Introduction d'un canal modélisant le bruit

Modifier le programme de l'exercice 2 pour relier P1 et P2
par un troisième processus CHANNEL, qui simulera aléatoirement une
corruption de message en changeant le type du message retransmis
entre P1 et P2 en type 'err'.

- Lorsqu'un message de type 'err' arrive sur P1 ou P2, il ne
  sera pas affiché.

- Utilisez la GUI de ispin.tcl pour visualiser l'échange
  de messages entre P1 et P2.

A quoi servent les options -r et -s de l'interpréteur
de spin ? Utiliser ces options pour n'afficher que les
messages reçus par P1, puis que les message envoyés par P1.
Faites de même pour P2.

## Exercice 4 : Modélisation du protocole de Lynch

Sur la base des exercices 1 à 3, modélisez le protocole 
de Lynch vu en cours. A l'aide des instructions assert, 
montrez avez Spin qu'une duplication de message peut-être introduite
par le service offert par ce protocole.

Pour le démarrage du transfert, on enverra un message de
type 'err' sur le canal entre P1 et P2 dès le début 
de la simulation.