Navigation lights

Les feux de navigation (navigation lights)
Version n° 1 du 17-05-2005
Rédigé par H. Habrias
____________________________________________________

Les aéronefs doivent avoir des feux de navigation dont les " Right-of-Way lights".
Un feu rouge est monté sur le côté gauche de l’aéronef et un feu vert sur son côté
droit. Ils servent quand deux aéronefs ont une direction qui les conduit à une
collision : si un pilote voit un aéronef sur une route qui croise la sienne, il
verra soit son feu rouge soit son feu vert. Si il voit le vert, il sait que c’est à
lui de passer. Si il voit le rouge, il sait que c’est à l’autre de passer.
On suppose qu'un avion ne voit qu'un des feux de l'autre avion et que quand l'un
voit un feu de l'autre, l'autre voit le feu du premier.

Vous considérerez deux aéronefs et spécifierez le comportement de ceux-ci tel que
décrit ci-dessus. Vous utilisez LTSA.

1) Dans une première spécification, vous utiliserez le renommage des actions
2) Dans une deuxième spécification, vous utiliserez le renommage des processus et
des actions



AVION1= (av1VoitRouge -> av1_laissePasser -> AVION1 | av1VoitVert -> av1_passe ->
AVION1).
AVION2 = (av2VoitRouge -> av2_laissePasser -> AVION2 | av2VoitVert -> av2_passe ->
AVION2).
||AV1_AV2 = (AVION1 || AVION2)/ {av2VoitRouge / av1VoitVert, aV2VoitVert/av1VoitRouge,
av2_laissePasser/ av1_passe,av2_passe/av1_laissePasser}.


AVION = (voitRouge -> laissePasser -> AVION | voitVert -> passe -> AVION).
||DEUX_AVIONS = (a:AVION || b:AVION||{a,b}::AVION)/{b.voitRouge/a.voitVert,
b.voitVert/a.voitRouge, b.laissePasser/a.passe, b.passe/a.laissePasser}.