C   Machines

C.1   Signalisation

1. Compléter la machine de carrefour avec un invariant, une initialisation en mode non régulé et une opération start qui passe le carrefour d'un mode non régulé dans un mode régulé quelconque.
2. Écrire les obligations de preuves qui doivent être vérifiées pour que l'invariant soit établi à l'initialisation et préservé par l'opération.
3. Pour modéliser la suite des changements d'états du carrefour, on introduit de plus dans la machine une constante suivant qui fait passer d'un état à l'autre suivant le cycle :
   cross ® cross_end® stop ® stop_end ® cross
   Cette fonction n'est pas amenée à être modifiée dans la machine, il n'est donc pas nécessaire de la mettre en variable, par contre elle ne va pas être représentée telle quelle dans l'implantation, qui reposera sur les changements d'états des feux. On l'introduit dans une clause ABSTRACT_CONSTANTS qui déclare des constantes qui pourront être raffinées, l'invariant de liaison apparaissant alors dans la clause PROPERTIES.
   On écrit donc :

   ABSTRACT_CONSTANT  suivant PROPERTIES  ...

   Compléter la clause PROPERTIES pour préciser les propriétés de la fonction suivant (type et valeurs) et ajouter à la machine une opération change qui change l'état des routes en suivant le cycle autorisé.
4. Dans l'objectif de raffiner le carrefour, on introduit une machine correspondant au contrôleur des feux. L'état d'un feu est repéré par un état {s₀,s₁,s₂,s₃,s₄} qui correspond à l'état de la route {off, cross, cross_end, stop, stop_end} . Le lien entre les états des feux et des routes est établi par une constante convention qui est une bijection entre l'état d'une route et l'état d'un feu, on introduit également une fonction feu_suivant qui définit le cycle de fonctionnement du feu.
   
   Écrire une machine Contrôleur correspondant au contrôleur des feux en introduisant les constantes convention et feu_suivant avec leurs propriétés, deux variables feuA et feuB correspondant aux deux états des feux des routes A et B, l'initialisation (feu non régulés), une opération start_feu qui s'applique à des feux non régulés et prend en argument l'état de la route A qu'il faut réaliser et enfin une opération change_feu.
5. Écrire une machine qui implante le carrefour en important la machine Contrôleur. Expliciter la propriété qui lie la constante suivant de la machine Route aux constantes feu_suivant et convention de la machine Contrôleur et l'invariant qui lie routeA et routeB aux variables feuA et feuB.
6. La machine Contrôleur est alors raffinée en une machine Contrôleur2 pour faire intervenir la couleur du feu. L'ensemble COULEUR des couleurs est :
   {vert,orange,rouge,orange_clignotant,noir,rouge_et_jaune} Une fonction couleur est introduite qui associe à chaque état du feu une couleur (la fonction dépend du code de la route des différents pays). Dans cette machine on ajoute aux variables feuA et feuB les variables couleurA et couleurB.
   1. Que peut-on dire des propriétés de la fonction couleur (partielle, totale, injective, surjective) ?
   2. Quel invariant lie les variables ?
7. On se donne les machines suivantes pour représenter l'état et la couleur d'un feu :

   MACHINE  Etat_feu SETS  ETATFEU = {s0,s1,s2,s3,s4} VARIABLES  etat INVARIANT  etat Î ETATFEU INITIALISATION   etat:=s0 OPERATIONS set(v)  =  PRE  v ÎETATFEU THEN etat:=v END; r ¬¾ valeur  =  BEGIN r:=etat END END

   MACHINE  Couleur_feu SETS    COULEUR = {vert,orange,rouge,orange_clignotant,noir,rouge_et_jaune} VARIABLES  couleur INVARIANT  couleur Î COULEUR INITIALISATION   couleur:=noir OPERATIONS set(v)  =  PRE  v ÎCOULEUR THEN couleur:=v END; r ¬¾ valeur  =  BEGIN r:=couleur END END

   Pour réaliser un croisement français, on implante le contrôleur de feux (raffiné) à l'aide d'une variable d'état et de deux variables de couleur. Le squelette de la machine s'écrit :

   IMPLEMENTATION  Controleur_francais REFINES  Controleur2 INCLUDES  Route IMPORTS  Etat_feu, A.Couleur_feu,B.Couleur_feu VALUES  convention={cross|® s1,cross_end|® s2, stop|® s3, stop_end|® s4, off|® s0}; feu_suivant = { s1|® s2, s2 |® s3, s3 |® s4, s4|® s1, s0|® s0}; color={ s1|® vert, s2 |® orange, s3 |® rouge, s4|® rouge, s0|® orange_clignotant} INVARIANT ... INITIALISATION ... ... END

   Compléter l'initialisation et l'invariant. Écrire la propriété qui doit être vérifiée pour que l'initialisation respecte l'invariant.
8. La machine Couleur_feu peut elle-même être implantée en utilisant trois instances d'une machine Lampe modélisant l'état d'une lampe qui peut être allumée, éteinte ou clignotante.
   Écrire la spécification de la machine Lampe ainsi qu'une implantation de la machine Couleur_feu utilisant trois lampes.
9. Dessiner le graphe de dépendance entre les machines de ce système en indiquant les liens de raffinement, d'inclusion et d'importation.