B.2 Définitions préliminaires

B.2.1 Types de slots

Un slot structurellement mutable ou s-mutable est un slot pour lequel l'attribut s-mutable = vrai. Un slot t-mutable est un slot pour lequel t-mutable = vrai, et un slot absent est un slot pour lequel absent = vrai.

Les slots s-mutables sont uniquement définis par leur parent, leur nom, leur sens et leur type. Les slots absents sont uniquement définis par leur parent, leur nom, et leur sens.

Un slot ne peut pas être simultanément s-mutable et t-mutable. En outre, un slot déclencheur ne peut pas être s-mutable.

B.2.2 Identifiants et valuations

Les définitions qui suivent s'appliquent à tout dispositif, qu'il soit mutable ou non.

$\bullet$ L'identifiant $V(S)$ d'un slot $S$ de dispositif est un couple formé de la valeur de ses attributs nom et sens, permettant de caractériser de façon unique ce slot sur son dispositif parent :

$V(S) = \langle S.nom, S.sens \rangle$

Tout couple de la forme $\langle nom, sens \rangle$ dont les éléments constitutifs ont pour types respectifs ceux des attributs de slots nom et sens est un identifiant de slot. Un identifiant de slot $\langle nom, sens \rangle$ désigne le slot $S$ ssi $V(S)= \langle nom,sens \rangle$.

Soient $a1, \dots ,an$ des attributs de slots distincts, et différents des attributs nom et sens.

$\bullet$ La valuation $V_{a_1, \dots ,a_n}(S)$ d'un slot de dispositif $S$ est un n-uplet comportant l'identifiant de $S$ et les valeurs de ses attributs $a_1, \dots, a_n$ :

$V_{a_1, \dots ,a_n}(S) = \langle S.nom, S.sens, S.a_1, \dots, S.a_n \rangle$

Tout n-uplet de la forme $\langle nom, sens, a_1, \dots, a_n \rangle$, dont les éléments constitutifs ont pour types respectifs ceux des attributs de slots nom, sens, $a_1$, ..., $a_n$, est une valuation de slot, notée $V_{a_1, \dots ,a_n}$. Le couple $\langle nom, sens \rangle$ en constitue l'identifiant. Nous dirons qu'une valuation de slot désigne le slot $S$ ssi son identifiant désigne le slot $S$.

De façon analogue, pour les paramètres :

$\bullet$ L'identifiant $V(P)$ d'un paramètre $P$ est la valeur de son attribut nom, et la valuation $V_{valeur}(P)$ de ce paramètre est le couple formé par la valeur de ses attributs nom et valeur.

B.2.3 Paramétrages et m-paramétrages de dispositifs

Les définitions qui suivent s'appliquent à tout dispositif, qu'il soit mutable ou non.

$\bullet$ Le paramétrage d'un dispositif $d$ est le couple :

$\Pi(d) = \langle V_{Pd}, V_{Sd} \rangle$

où $V_{Pd}$ est l'ensemble des valuations $V_{valeur}$ des paramètres de $d$:

$V_{Pd} = \{ \langle P_1.nom, P_1.valeur \rangle , \dots, \langle P_n.nom, P_n.valeur \rangle \}_{P_i \in d.parametres}$

et $V_{Sd}$ est l'ensemble des valuations $V_{connecte, typeConnecte}$ des slots déclencheurs de $d$ :

$V_{Sd} = \{ \langle S_1.nom, S_1.sens, S_1.connecte, S_1.typeConnecte \rangle... ... S_{n'}.typeConnecte \rangle \} _{S_i \in d.slots ~et~ S_i.declencheur = vrai}$

$\bullet$ Le m-paramétrage d'un dispositif $d$ est le couple:

$\Pi_m(d) = \langle V_{Ss}, V_{St} \rangle$

où $V_{Ss}$ est l'ensemble de valuations $V_{type}$ des slots s-mutables de $d$:

$V_{Ss} = \{ \langle S_1.nom, S_1.sens, S_1.type \rangle, \dots, \\ \langle S_... ...''}.sens, S_{n''}.type \rangle \} _{S_i \in d.slots ~et~ S_i.s-mutable = vrai}$

et $V_{St}$ est l'ensemble de valuations $V_{type}$ des slots t-mutables de $d$:

$V_{Ss} = \{ \langle S_1.nom, S_1.sens, S_1.type \rangle, \dots, \\ \langle S_... ...'}.sens, S_{n'''}.type \rangle \} _{S_i \in d.slots ~et~ S_i.t-mutable = vrai}$

$\bullet$ Un m-paramétrage valide pour un dispositif $d$ est un couple de la forme :

$\Pi_m = \langle V_{Ss}, V_{St} \rangle$

où $V_{Ss}$ est un ensemble de valuations $V_{type}$:

$V_{Ss} = \{ \langle nom_1, sens_1, type_1 \rangle, \dots, \langle nom_{n''}, sens_{n''}, typen_{n''} \rangle \}$

dont les identifiants sont distincts et ne désignent pas de slot présent non s-mutable de $d$ (slots pour lesquels $absent=faux$ et s-mutable$=faux$).

et $V_{St}$ est un ensemble de valuations $V_{type}$:

$V_{St} = \{ \langle nom_1, sens_1, type_1 \rangle, \dots, \langle nom_{n'''}, sens_{n'''}, typen_{n'''} \rangle \}$

dont les identifiants sont distincts et désignent tous des slots t-mutables de $d$. En outre, chaque élément $\langle nom, sens, type \rangle$ de $V_{St}$ identifiant $S$ vérifie $type \leqslant S.supertype$.

Notons qu'un slot s-mutable étant entièrement défini par ses attributs parent, nom, sens et type, un ensemble de valuations $V_{type}$ suffit bien à décrire l'ensemble des slots s-mutables d'un dispositif.

B.2.4 Fonction de mutation et consistance

Les définitions qui suivent s'appliquent à tout dispositif, qu'il soit mutable ou non.

Soit $d$ un dispositif, $\mathcal{P}$ l'ensemble de ses paramétrages possibles, et $\mathcal{P}_m$ l'ensemble de ses m-paramétrages valides.

Le dispositif $d$ comporte une fonction de mutation $\mu$, qui à chaque paramétrage $\Pi$ de $\mathcal{P}$ associe un m-paramétrage $\Pi _m$ de $\mathcal{P}_m$:

$\mu: \left\vert\begin{array}{l} \mathcal{P} \rightarrow \mathcal{P}_m \\ \Pi \mapsto \Pi_m \end{array}\right.$

$\bullet$ Un dispositif est dans un état consistant ssi il est non mutable, ou s'il satisfait à sa fonction de mutation:

$\Pi_m(d) = \mu(\Pi(d))$