Re'sume' de cours
=================
se'quence = cours1 + tp1 + cours2 + td + tp2
1. Exemple du Veilleur
----------------------
1.1. E'nonce'
Un ordinateur envoie des ordres a` une machine.
Le veilleur est charge' de ve'rifier que la machine
exe'cute ces ordres dans un certain de'lai (nombre de tops).
Pour cela, l'ordinateur envoie une copie de la commande au veilleur,
et la machine envoie au veilleur un signal indiquant qu'elle a
termine' l'exe'cution.
Une alarme doit e^tre de'clenche'e si le de'lai est de'passe'.
+----------+
COMMANDE --> |
| Veilleur --> ALARME
TERMINEE --> |
+----^-----+
|
TOP
1.2. Stucture du programme
% veilleur.SIG %
process veilleur =
{ integer DELAI % parametre %
}
( ? event TOP; % entrees %
integer COMMANDE;
event TERMINEE
! event ALARME % sortie %
)
(| ... % equations/contraintes sur les signaux %
| ...
| ...
| ...
|)
where
... % declarations locales %
end
1.3. Parametre DELAI
ordre non indifferent
==> fichier veilleur.par
5
1.4. Entrees/sorties et declarations locales
ordre indifferent (mais entrees avant sorties)
1.5. Corps du programme
ordre indifferent ==> declaratif
1.6. integer compteur
constant integer REPOS := -1;
repos ==> compteur vaut REPOS
COMMANDE ==> compteur vaut DELAI
TERMINEE ==> repos
en attente de TERMINEE ==> compteur := compteur - 1
( DELAI DELAI-1 ... 2 1 0 -1)
compteur = 0 ==> ALARME
1.7. compteur ^= TOP
mais COMMANDE ou TERMINEE pas forcement synchrones avec TOP
==> compteur ^= TOP ^+ ^COMMANDE ^+ TERMINEE
1.8. compteur := DELAI when ^COMMANDE
default REPOS when TERMINEE
default precedent-1 when precedent>=0
default REPOS
1.9. integer precedent
precedent := compteur $ 1
==> integer precedent init REPOS
1.10. ALARME := when cpt = 0
1.11. Chronogramme
TOP : t t t t t t t t t t t t t t t t t t
COMMANDE : 7 8 9
TERMINEE : t t t
compteur : -1 5 4 3 -1 -1 5 4 3 2 1 0 -1 -1 -1 -1 5 4 -1 -1
precedent : -1 -1 5 4 3 -1 -1 5 4 3 2 1 0 -1 -1 -1 -1 5 4 -1
ALARME : t
1.12. Programme final
% veilleur.SIG %
process veilleur =
{ integer DELAI; % parametre %
}
( ? event TOP; % entrees %
integer COMMANDE;
event TERMINEE;
! event ALARME; % sortie %
)
(| compteur ^= ^COMMANDE ^+ TERMINEE ^+ TOP
| compteur := DELAI when ^COMMANDE
default REPOS when TERMINEE
default precedent-1 when precedent>=0
default REPOS
| precedent := compteur $ 1
| ALARME := when compteur = 0
|)
where
integer compteur, precedent init REPOS;
constant integer REPOS := -1;
end
1.13. Les points-virgules
- notez les ; a` la fin de chaque de'claration
(qu'elle soit locale, de parame`tre, de signal d'entre'e ou de sortie)
2. Types
--------
2.1. event
* toujours la valeur vrai, mais a quels instants ?
* operateur ^ (extrait l'horloge du signal)
^E est e'quivalent a` E=E ou a` event(E)
E 1 2 3 4 5
^E T T T T T
* operateur ^+ (union des instants de deux horloges)
E1 T T T T
E2 T T T S ^= E1 ^+ E2
S T T T T T T
* operateur ^* (intersection des instants de deux horloges)
E1 T T T T
E2 T T T S ^= E1 ^* E2
S T
* operateur ^- (exclusion des instants de la deuxie`me horloge)
E1 T T T T
E2 T T T S ^= E1 ^- E2
S T T T
* contraintes sur des horloges :
- H1 ^= H2 (les deux horloges doivent e^tre identiques)
- H1 ^< H2 (H1 doit e^tre incluse dans H2, au sens large)
- H1 ^# H2 (les deux horloges ne doivent avoir aucun instant en commun)
2.2. boolean
* constantes: true et false (1 et 0 dans les fichiers de donne'es)
* resultat de comparaison: < <= > >= = /=
* operateurs logiques: not and or xor
* operateur when (extrait les instants vrais de la condition)
==> B boolean, when B est e'quivalent a` ^B when B
B T F T T F T S ^= when B
S T T T T
* signal de type event est aussi un boolean
2.3. integer
* constantes litte'rales: 1654 +287 -39
* constantes nomme'es: (dans la partie where)
constant integer TAILLE := 10;
* constantes calcule'es: constant integer Z = X + Y;
X et Y force'ment constantes ou parame`tres
* attention! les constantes n'ont pas d'horloge et
sont implicitement toujours pre'sentes
* operateurs unaires: + -
* operateurs binaires: + - * / (entie`re) modulo ** (entie`re)
2.4. real
* constantes litte'rales: 3.14 .2 2.5e-3 1e6
* me^mes constantes nomme'es et calcule'es
* me^mes operateurs, mais division re'elle, donc pas de modulo
* conversions: real(I) integer(R)
* type dreal
double precision: 'd' a la place de 'e', et obligatoire
* fonctions: (dans la partie where)
function sin = ( ? dreal X ! dreal S )
utilisation: A := 0.5 * sin( B ) + 3.14159265358979
2.5. complex
* constantes: 0.0@1.0 2.5@4e-3 1.0@(-1.0)
* type dcomplex
2 dreal au lieu de 2 real
* complex(R) e'quivalent a` R@0.0
2.6. character
* constantes: 'a' '8' '\000'
2.7. string
* constantes: "une phrase" ""
* pas de conversion vers string
2.8. enum
* definition: type color = enum ( rouge, orange, vert );
* constantes: #rouge #orange #vert
* ambiguite': type fruit = enum ( pomme, poire, orange );
fruit#orange ou color#orange
* valeurs entie`res: integer(#rouge) = 0
3. Les 4 ope'rations fondamentales
----------------------------------
3.1 La fonction imme'diate
Y := A+B ou C := A and B ou Y := X ** 2
==> synchronise Y, A, et B ou C, A, et B ou Y et X
A T F T T F F T T T
B F F T F F T F F T
A and B F F T F F F F F T
3.2 Le retard
Xprec := X$1 ou ZX := X$3
==> integer Xprec init -1 ou integer ZX init [ {to 3} : 0 ]
==> Xprec et X ou ZX et X ont la me^me horloge
X 9 8 7 6 5 pour Xprec := X$1
Xprec -1 9 8 7 6 et integer Xprec init -1;
3.3 Le sous-e'chantillonnage
Y := A when B
==> Y et A sont de me^me type, et B boolean (ou event)
==> Y n'a de valeurs que lorsque B est pre'sent et vrai
A 1 2 3 4 5 6 7 8 9
B T F T T F T
A when B 2 5 6 9
3.4 Le me'lange prioritaire
Y := A default B
==> Y, A, et B sont de me^me type
==> l'horloge de Y est l'union des horloges de A et de B
==> A est prioritaire sur B, donc Y diffe'rent de B default A
==> B peut e^tre une constante si l'horloge de Y est
de'termine'e par ailleurs;
sinon, l'horloge de B doit e^tre de'termine'e
A 11 13 14 16 18
B 22 23 25 26 27 28
A default B 11 22 13 14 25 16 27 18
B default A 11 22 23 14 25 26 27 28
3.5 En bonus : la me'morisation
Y := A cell B init V
==> B boolean (ou event)
==> Y vaut A quand A est pre'sent
==> Y vaut A$1 quand A est absent et B est vrai
==> V est utile quand B est vrai avant la premie`re valeur de A
A 1 2 3 4 5 6
B T F T F T T F T
A cell B init -1 -1 1 2 2 2 3 4 5 5 6
>>> Exercice: Comment e'crire cell s'il n'existait pas ?