#### Maylis de Talhouet et Paco Pompeani
# TP Machine Croisement

## Machine abstraite

Pour la machine abstraite, nous avons décidé de créer deux SETS. Le premier représentant les couleurs et le second l'état du système.

### Variables
Nous avons ensuite déclaré les variables nous étant utiles : une nommée `etat` pour représenter l'état de fonctionnement des feux. Les variables`feuA` et `feuB` représentent les couleurs des feux.

### Invariant
Il va donc de soi que les variables `feuA` et `feuB` prennent des valeurs dans `Couleurs` et `etat` dans `Etats`.
Pour compléter l'invariant, nous imposons la couleurs des feux A et B lorsque le système est en service ou non. S'il est **hors service**, **les deux feux doivent être orange**.
De manière identique, si **le système fonctionne** (etat = EnService), il faut alors toujours **un des deux feux qui soit rouge** et assurer que les feux n'aient pas la même couleur. En effet, si les deux sont verts, des voitures risquent de se croiser.
Ces conditions se trouvent dans l'invariant car elles doivent toujours être validées.

### Opérations
Pour les opérations, nous avons décidé de définir chaque changement de couleur pour chacun des feux. Il y a donc 4 opérations pour **Vert->Orange** et **Orange->Rouge** pour **`feuA` et `feuB`**.
**Le passage de rouge à vert** est géré par les opérations de Orange -> Rouge: lorsqu'un feu passe à rouge, l'autre feu passe au vert.
En plus, deux opérations ont été écrites afin de faire la mise en service ou hors service.
Pour la mise en service, les feux passent de orange à rouge pour l'un et vert pour l'autre. L'état passe à `EnService`.
Pour la mise hors service, les deux feux passent à orange et l'état à `HorsService`.

### Obligations de Preuve
La machine abstraite nous a permis de générer 30 obligations de preuve : elles contiennent les PO d'initialisation et d'opérations. Toutes ont été prouvées automatiquement par atelier B.

## Raffinement

Nous avons decidé de faire deux raffinements. Un premier où seulement les variables sont raffinées et un second afin de raffiner les opérations.

### Raffinement des variables
Il s'agit ici de passer de variables abstraites à variables concrètes.

Ainsi, elles ne prennent plus des valeurs dans des ensembles abstraits. Nous avons décidé de décrire les couleurs à l'aide de nombres entiers. Vert devient 1, Orange 2 et Rouge 3. Pour la variable `etat`, 1 représente l'état en service et 0 l'état hors service.

Pour les opérations, il faut donc les écrire avec les variables concrètes définies au début du rafinement.

Atelier B génère 65 PO sur notre raffinement, dont 100% ont été automatiquement prouvées.

### Raffinement des opérations
Pour cette étape, nous devons rapproché les opérations de l'implantation. Pour cela, les `PRE` deviennent des `IF`. Les affectations de valeurs à des variables sont faites successivement : Elles étaient parallèle avant ce raffinement.

Atelier B génère 12 PO.Toutes sont prouvées par atelier B.

## Implantation
Cette étape permet de générer le code C.

Nous avons pour l'implantation 12 PO dont 10 sont prouvées.
Pourquoi ne le sont-elle pas ?
Voici ce que nous dit Atelier B :

"Valuation is correct" => Couleurs: FIN(NATURAL*{Couleurs.enum}) & not(Couleurs = {}) 
--------------------
"Valuation is correct" => Etats: FIN(NATURAL*{Etats.enum}) & not(Etats = {}) 

Il n'arrive pas à prouver que les ensembles Etats & Couleurs ne sont pas finis, mais nous pouvons le voir par nous-mêmes.
Ces POs sont donc prouvées *à la main*.

Le code C généré est 100% sûr, chaque étape générant des obligations de preuves toutes validées.

## Problèmes rencontrés à l'utilisation de l'Atelier B

Fort malheureusement, Atelier B a planté des choux pendant le raffinement, sur l'ordinateur de Maylis puis sur celui de Paco.
Les tâches qu'on lançait se mettaient pour une raison encore inconnue à ce jour en "Attente", et ce, pendant une durée plus ou moins infinie.
Ceci explique partiellement le retard de notre rendu.
Nous avons travaillé quelques jours à vue, sans pouvoir tester quoi que ce soit, nos Ateliers B s'étant mis au jardinage.

Pour la postérité, voici les étapes à réaliser pour régler ce problème :
- Fermer Atelier B
- Ouvrir Atelier B
- Créer un nouveau projet
- Recréer chaque composant et copier/coller les anciens contenus

Il semblerait que le problème soit lié au fait de lancer une deuxième tâche pendant qu'une autre est en cours, mais nous avons préféré ne pas nous en assurer.