Re'sume' de cours (suite)
=================
se'quence = cours1 + td + tp1 + cours2 + tp2
4. Calculs d'horloge (vu en td)
--------------------
4.1 Notation
4.2 Re`gles
4.3 Exemple : Abs
process Abs = {}
( ? integer E ! integer S )
(| N := E<0 % e1: P(N) = P(E) %
| M := -E when N % e2: P(M) = P(-E).T(N) = P(E).T(N) %
% e3: T(N)<=P(N) & e1 => T(N)<=P(E) %
% e4: e2&e3&2a => P(M) = T(N) %
| S := M default E % e5: P(S) = P(M)+P(E) = T(N)+P(E) %
|) % e6: e3&e5&2b => P(S) = P(E) %
where
boolean N;
integer M;
end
4.4 Autres cas
Si la de'monstration aboutit a` :
* P(S)>=X ou P(S)<=X
l'horloge de S n'est que partiellement de'termine'e
il faut ajouter une e'quation d'horloge S ^= ...
* P(S)=P(S)
l'horloge de S est inde'termine'e
il faut ajouter une e'quation d'horloge S ^= ...
* P(S)=X+Y et P(S)<=X (par exemple)
les contraintes d'horloge sont incompatibles
il faut modifier les e'quations de signaux et/ou d'horloge
4.5 Conseils
- de'composer au maximum (un seul ope'rateur par e'quation)
et ne pas he'siter a` cre'er des signaux interme'diaires
- traiter le cas le plus particulier d'abord
(notamment pas de constante apre`s un default)
- e'crire les e'quations d'horloge en commentaire dans les .SIG
- nume'roter les e'quations d'horloge
5. Modularite' (sous-processus)
-------------------------------
5.1 De'claration
where
process moy = ( ? dreal X1, X2 ! dreal M )
(| M := ( X1 + X2 ) / 2.0 |)
end
5.2 Appel
C := moy( A, B )
e'quivalent a` C := ( A + B ) / 2.0
5.3 Exemple avec un parame`tre et avec plusieurs sorties
De'claration:
where
process proc = {integer P1, P2} ( ? integer E1, E2 ! integer S1, S2 )
(| S1 := E1 + P1 | S2 := E2 - P2 |)
end
Appel: (Res1, Res2) := proc{Param1, Param2} (Donnee1, Donnee2)
5.4 Exemple de programme complet
% MAIN.SIG %
process MAIN = ( ? integer E1,E2 ! integer S1,S2 )
(| S1 := INC( E1 ) | S2 := INC( E2 ) |)
where
process INC = ( ? integer E ! integer S )
(| S := E + 1 |)
end
5.5 Multi-fichiers
% MAIN.SIG %
process MAIN =
( ? integer E1,E2 ! integer S1,S2 )
(| S1 := INC( E1 ) | S2 := INC( E2 ) |)
where
use mINC;
end;
% mINC.SIG %
module mINC =
process INC =
( ? integer E ! integer S )
(| S := E + 1 |)
end;
6. Tableaux
-----------
* e'le'ments de me^me type (ni event ni tableau)
* taille constante, indices commencent a` 0
* plusieurs dimensions
* tous les e'le'ments sont synchrones
6.1. De'claration
[taille] type nom
[3,3] integer Masque
type Tab = [3,3] integer; Tab Masque;
6.2. Utilisation
X := Masque[0,0]
M := Masque default Masque2
M := Masque + Masque2
6.3. E'nume'ration
Tab := [ [0]:10, [1]:20, [2]:30 ]
Tab := [ {to 2}:0, [1]:1 ]
M := [ {to 2, to 2}:0, {i to 2}:[i,i]:1 ]
{indice in debut to fin step pas}
6.4. Concatenation
Tab := { T1 || T2 }
6.5. Fene^tre glissante
* W1 := X window 3
[3] integer W1 init [ [0]:-2, [1]:-1 ]
* W2 := X $ 2 window 3
[3] integer W2 init [ {to 3}:0 ]
* chronogramme:
X 1 2 3 4 5
W1 [-2,-1,1] [-1,1,2] [1,2,3] [2,3,4] [3,4,5]
W2 [ 0,0,0 ] [ 0,0,0] [0,0,1] [0,1,2] [1,2,3]
zeros 1 2 3 2 3 4 3 4 4
* ==> initialisation: (taille+retard-1) valeurs
6.6. Tableaux constants
* constante nomme'e:
constant [3,3] integer IDENTITE = [ [1,0,0], [0,1,0], [0,0,1] ];
* fichier de parame`tres
process proc = { integer N; [N] real TC }
proc.par:
3, [ [0]:2.5, [1]:1.5, [2]:0.5 ]
7. Processus particuliers
-------------------------
7.1. Le portier
* Compter le nombre de PRESents dans une piece a partir de signaux
d'ENTRant et de SORTant.
* - process portier1 = ( ? event ENTR, SORT ! integer PRES )
- NE := NEprec+1 when ENTR default NEprec
NEprec := NE $ 1
NS := NSprec+1 when SORT default NSprec
NSprec := NS $ 1
PRES := NE - NS
- where integer NE, NEprec init 0, NS, NSprec init 0
- horloge partiellement de'termine'e => PRES ^= ENTR ^+ SORT
- beaucoup de signaux; et au bout d'un certain temps ...
- auto-test ==>
sortie supplementaire: event DEF
DEF := when PRES < 0
* - process portier2 =
( ? event ENTR, SORT ! integer PRES; event DEF )
- me^me e'quation d'horloge
- PRES := PRESprec+1 when ENTR
default PRESprec-1 when SORT
PRESprec := PRES $ 1
- where integer PRESprec init 0
- que se passe-t-il si ENTR et SORT simultane's ?
* - si ENTR alors
si SORT alors
ne rien changer
sinon, donc uniquement ENTR
ajouter 1
finsi
sinon, donc uniquement SORT
enlever 1
- PRES := ( PRESprec when SORT default PRESprec + 1)
when ENTR
default PRESprec - 1
7.2. Duree separant deux evenements
* Compter le nombre de TOP d'horloge separant les
evenements DEBUT et FIN.
* - process duree =
( ? event TOP, DEBUT, FIN ! integer DUREE )
- N := 0 when DEBUT default Nprec + 1
Nprec := N $ 1
N ^= DEBUT ^+ FIN ^+ TOP }
DUREE := N when FIN
- where integer N, Nprec init 0 end
7.3. Presence entre deux evenements
* Tester si un evenement E est survenu entre les
evenements DEBUT et FIN.
* - process dansfo =
( ? event E, DEBUT, FIN ! boolean DANS )
- S := DEBUT % true when DEBUT %
default not FIN % false when FIN %
default Sprec
Sprec := S $ 1
DANS := S when E
S ^= DEBUT ^+ FIN ^+ E
- where boolean S, Sprec init false end
- et si E quand DEBUT ? et si E quand FIN ?
==> [DEBUT,FIN[
* - process dansof (solution inelegante)
DANS := (not DEBUT default FIN default S) when E
* - process dansoo (solution inelegante)
DANS := (not DEBUT default not FIN default S) when E
* - process dansff (solution inelegante)
DANS := (DEBUT default FIN default S) when E
7.4. Automate
* Un automate reagit a un certain nombre d'evenements; son etat doit
donc evoluer a chaque fois qu'un de ces evenements se produit :
S ^= A ^+ B ^+ ...
* La reaction a un evenement depend de l'etat precedent :
S := ( 2 when event A
default 3 when event B
default ... ) when Sprec = 1
default ( 3 when event B ) when Sprec = 2
default ...
default Sprec % pas d'evt ==> bouclage sur etat courant %
Sprec := S $ 1
* % Actions sur transitions %
X := 0 when Sprec=1 and S=2
default Xprec+1 when event B
default ...
* where integer S, Sprec init 1 end
7.5. Synchronisation sur l'horloge des sorties
* process capteur = ( ? integer A ! integer S )
(| ES := event S | S := (A cell ES) when ES |)
where event ES end
* ==> horloge de S doit etre fixee par l'exterieur
* when ES car S ne doit pas etre present aux instants de A
7.6. Sur-echantillonnage
* process sur = ( ? integer E ! integer S )
BASC := not BASCprec
BASCprec := BASC $ 1
S ^= BASC % sortie 2 fois plus %
E ^= when BASC % frequente que l'entree %
where BASC, BASCprec init false end % 1er instant true %
* BASC t f t f t f t f
P(S) t t t t t t t t
P(E) t t t t