Modélisation par automates communicants 
========================================

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

Tau (Tiny Automata) est une interface graphique qui permet d'éditer 
des automates communicants puis de simuler visuelement leur comportement.
Les automates réalisés avec Tau sont décrit formellement par un
modèle Promela, et qui permet de bénéficier de tous les outils
de vérifications associés à ce langage, en particulier la génération
d'un vérificateur exhaustif des clauses d'assertions.


## Installation de Tau sous Linux

1. Récupérer la dernière version Tau içi : https://hepia.infolibre.ch/reseauxI-2019-2020/tau_v03.tar.gz

2. Décompresser l'archive et suivre la procédure d'installation.


3. S'assurer que vous avez rajouté 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.

4. Vérifier que la GUI s'éxecute correctement avec en lançant la commande Tau Examples/hello.tau

5. (optionnel si erreur avec t2s ), remplacer t2s par cette version https://hepia.infolibre.ch/reseauxI-2019-2020/t2s

5. (optionnel si erreur avec tau.tcl ), remplacer tau.tcl par cette version https://hepia.infolibre.ch/reseauxI-2019-2020/tau.tcl



## Exercice 1 : Modélisation de feu de signalisation de trafic

Le feu de signalisation routière suisse fonctionne en alternant entre l'état 'ROUGE' ou 'VERT'
en passant toujours par l'état 'ORANGE'. Le feu de signalisation français alterne aussi entre
les deux états 'ROUGE' et 'VERT', mais passe par contre de l'état 'ROUGE' à l'état 'VERT' directement,
sans passer par l'état 'ORANGE'.

Modéliser avec Tau le comportement des feux de signalisation suisses et français par 
une machine à état. Générer un vérificateur à l'aide du modèle proméla générée par Tau
et démontrer à l'aide du vérificateur qu'il est impossible que le feu suisse passe 
directement de l'état 'ROUGE' à l'état 'VERT'. De même, démontrer qu'il est impossible
qu'un feu français passe de l'état 'ROUGE' à l'état 'VERT' en passant par l'état orange.


## Exercice 2 : Feux de signalisation communicants

Modéliser cette fois-ci deux feux Suisses représentées par deux machines à état communicantes
Les contraintes des deux feux seront les suivantes : 

- Lorsque l'un des deux feux est 'VERT' ou bien 'ORANGE', l'autre feu sera nécessairement et toujours 'ROUGE',
  c'est à dire que les deux feux ne sont jamais 'VERT' en même temps ou bien 'VERT' et 'ORANGE' en même
  temps.

- Il est possible d'avoir les deux feux à 'ROUGE' pendant une durée déterminée, mais celà ne doit jamais
  être un état final.

## Exercice 3 : Modélisation du protocole 2 vu en cours.

Modéliser le protocole 2 vu en cours (https://hepia.infolibre.ch/reseauxI-2019-2020/reseaux_et_app_cours_A.pdf)
par deux machines à état communicantes. Démontrer qu'avec un canal qui introduit des pertes de données, 
il y a possibilité d'interblocage (aucune des deux machines à état ne peux plus avancer, car l'une 
attends l'autre).