Modélisation
Exemple
S = (P_{1} \| P_{2} \| B)_{T}
Table de synchronisation
| Act_{B} \cup {-} | Act_{P_{1}} \cup {-} | Act_{P_{2}} \cup {-} | Act_{S} \cup {\tau} |
|---|---|---|---|
| isTrue | - | isTrue | \tau |
| isFalse | isFalse | - | \tau |
| setTrue | setTrue | - | \tau |
| setFalse | - | setFalse | \tau |
| - | wr | - | \omega |
| - | - | rd | r |
 |
LTE
-
S \vDash written \RA (XX read)
-
S \nvDash G (written \RA (XX read))
-
S \vDash G (written \RA F read) : propriété de réponse (propriété importante dans les systèmes réactifs)
On recherche de la fairness (càd un équilibre entre les lectures et écritures) ; ces propriétés ne spécifient pas la fairness.
Graphes de programmes
Définition
Syntaxe
Un graphe de programme est un tuple
< L, l_{0}, \longleftrightarrow, Val_{0}> sur un ensemble de variables
Var = EVar \cup BVar
- EVar ensemble fini de variables entières
- BVar ensemble fini de variable booléennes
- L ensemble d’états de contrôle (locationss)
- l_{0} \in L initial location (location d’états de contrôle initial)
- \hookrightarrow \subseteq L \times \mathscr{C}(Var) \times \text{Op}(Var) \times L (\mathscr{C} les conditions et \text{Op} les opérations)
- Val_{0} (définition formelle) : …
- EVal (évaluation d’une variable entière) : Evar \ra \Z
- BVal (évaluation d’un booléen) : BVar \ra \mathbb{B}
- Val(x) = \begin{cases}\text{Eval}(x) & \text{si } x \in \text{EVar} \\\\ \text{Bval}(x) & \text{si } x \in \text{BVar}\end{cases}
- Val_{0}(x) est Val(x) à l’état initial
Sémantique
Rappel : \wedge = ET
La sémantique d’un graphe de programme < L, l_{0}, \longleftrightarrow, Val_{0}> sur Var est donné par un STE < Q, q_{0}, Act, \rightarrow, AP, \mathcal{L}> tel que :
- Q = L \times Val
- q_{0} = (l_{0}, Val_{0})
- Act = {\tau}
- \rightarrow : (l, v) \xrightarrow{\tau}(l', v') ssi l \hookrightarrow l' \wedge v \vDash c \wedge v' = Op(v)
- (propositions atomiques) AP = L \times \mathscr{C}(Var)
- \mathcal{L} : Q \ra AP tel que q : q = (l, v) \rightarrow \mathcal{L}(q) = (l, C) \wedge v \vDash C (avec C la condition)
Produit
- g_{1} = <L_{1}, l_{0}^{1}, \hookrightarrow_{1}, Val_{0}^{1}> sur Var_{1}c
- g_{2} = <L_{2}, l_{0}^{2}, \hookrightarrow_{2}, Val_{0}^{2}> sur Var_{1}c
Le produit \mathbb{P}(g_{1,}g_{2}) = g_{1}||| g_{2} (||| = interleaving, aka pas de synchronisation, chacun fait un pas après le tour de l’autre)
Syntaxe de \mathbb{P}(g_{1,}g_{2}) = <L_{1 \times}L_{2}, (l_{0^{1},}l_{0}^{2}), \hookrightarrow, Val_{0}> sur Var_{1} \cup Var_{2}
\mathbb{P}(g_{1,}g_{2}) est défini ssi \forall x \in Var_{1} \cap Var_{2} : Val_{0}^{1}(x) = Val_{0}^{2}(x)
- \hookrightarrow :(l_{1}, l_{2}) \ra (l_{1}', l_{2}') ssi \begin{cases} l_{1} = l_{1}' et l_{2} \hookrightarrow_{2} l_{2}' \\\\ l_{2} = l_{2}' et l_{1} \hookrightarrow_{1} l_{1}' \end{cases}