content/conception_formelle/2_verification/index.md

@@ -16,14 +16,14 @@ devenir un système réel. Mais alors **comment décider qu'un modèle est valid
 Il doit satisfaire toutes des propriétés qui définissent un bon candidat, mais 
 une liste de telles propriétés n'existe pas. Uen liste minimale de propriétés
 dépends avant tout du type d'application. Pour la validation, les outils de
-simulation (jouer des scénario pour observer) sont consiérés comme adaptés.
+simulation (jper des scénario pour observer) sont consiérés comme adaptés.
 
 la Validation permet donc de s'assurer **d'avoir construit quelque chose
 d'adapté**
 
 ### Vérification
 
-Le modèle doit vérifier tous les pré-requis décrits dans les spécifications.
+Le modèle doit vérifier tous les pré-requis  décrits dans les spécifications.
 Nous vérifions alors que le modèle satisfasse toutes les exigences du cahier des
 charges.
 
@@ -47,16 +47,17 @@ la vérification de modèle (*model checking*) est un bon moyen de vérification
 \\)
 
 En entrée nous avons notre modèle \\(M\\) et notre spécification \\(\varphi\\),
-nous devons alors vérifier que \\(M\\) modélise \\(\varphi\\).
+nous devons alors vérifier que \\(M\\) modélise  \\(\varphi\\).
 
 ### Deux classes de propriété
 
 #### Sureté
 
 Quelque chose **est impossible**, une configuration est inaccessible par
-exemple. À la suite d'un événement, un autre ne peut être atteint. Si une
+exemple. À la suite d'un événement, un autre ne peut être atteint.
-propriété de sureté est non-satisfaite, alors le contre exemple est un scénario
+
-fini.
+Si une propriété de sureté est non-satisfaite, alors le contre exemple est un
+scénario fini.
 
 **Il faut s'assurer que quelque chose de mauvais n'arrive jamais**
 
@@ -141,7 +142,7 @@ D'après le graphe, trouvons les états:
 
 
 Il est question de logique comportementale : on s'intéresse au comportement
-d'un système. Une propriété logique est un ensemble de conditions, dans notre
+d'un système. Une propriété logique est un ensemble de conditions, Dans notre
 exemple la preuve que `c.a` est possible. Comment vérifier, calculer ces
 propriétés? Par un **algorithme de parcours de graphes** avec une complexité
 linéaire.
@@ -170,21 +171,12 @@ Et un ensemble de transitions `self`, `epsilon`, `self-epsilon` : boucles sur
 les états.
 
 Il est possible de calculer des expressions élémentaires via des variables, par
-exemple \\([ s \\% 2 = 0 ]\\).
+exemple:
+
+\\([ s \\% 2 = 0 ]\\)
 
 Permet de trouver les états pairs.
 
-### Les calculs
-
-Il est possible de calculer des sets d'états et de transitions. 
-
-Les sets d'états : \\([expr]\\) où `expr` est un expression, par exemple 
-`[light.on]` donne les états ou la lumière est allumée.
-
-Les sets de transitions \\(\text{label expr}\\) où `expr` est une expression, par
-exemple `label button.push` donne les transitons qui porte sur l'évènement
-`push`.
-
 ### Opérateurs ensemblistes
 
 Il est possible d'utiliser des opérateurs ensemblistes comme l'union et
@@ -192,57 +184,47 @@ l'intersection
 
 Soit \\(F_1\\) et \\(F_2\\) deux formules du même type:
 
- \\(
+\\(
 [\\![ F_1  \text{ et } F_2 ]\\!] = [\\![ F_1 \\&\\&  F_2 ]\\!] = [\\![ F_1  \cap F_2 ]\\!] 
 \\\
 [\\![ F_1  \text{ ou } F_2 ]\\!] = [\\![ F_1 \\|  F_2 ]\\!] = [\\![ F_1  \cup F_2 ]\\!] 
 \\)
 
- Soit \\(S\\) une formule d'états et \\(T\\) une formule de transitions :
-
- \\(
-[\\![not S]\\!] = [\\![any_s]\\!] \setminus [\\![S]\\!]
-\\\
-[\\![not T]\\!] = [\\![any_t]\\!] \setminus [\\![T]\\!]  
-\\)
-
- ici \\(\setminus\\) représente une différence ensembliste.
-
 ### Opérateur source, destination
 
 Soit \\(T\\) une formule de transitions
 
- * \\(\text{src}(T)\\) représente l'ensemble **des états source** d'au moins une 
+ * \\(\text{src}(T)\\) représente l'ensemble des états source d'au moins une 
    transition de \\(T\\)
- * \\(\text{tgt}(T)\\) représente l'ensemble **des états destination** d'au 
+ * \\(\text{tgt}(T)\\) représente l'ensemble des états  destination d'au moins
-   moins une transition de \\(T\\)
+   une transition de \\(T\\)
 
 Soit \\(S\\) une formule d'état
 
- * \\(\text{rsrc}(S)\\) représente les **transitions qui ont leurs source** dans 
+ * \\(\text{rsrc}(S)\\) représente les transitions qui ont leurs source dans au
-   au moins un état de \\(S\\)
+   moins un état de \\(S\\)
- * \\(\text{rtgt}(S)\\) représente les **transitions qui ont leurs destination** 
+ * \\(\text{rtgt}(S)\\) représente les transitions qui ont leurs destination 
    dans au moins un état de \\(S\\)
 
-#### Exemples
+### Exemples
 
 \\(\text{any_s} - \text{src}(\text{any_t})\\) rerésente les états qui sont
 source d'aucune transition, dont on ne peut pas sortir (état puit)
 
-\\(\text{src}(\text{rtgt}(S) \cap T)\\) représente les états utilisant les
+\\(\text{src}(\text{rtgt}(S) \cap T)\\) représente les états sources de
-transitions \\(T\\) pour mener à \\(S\\). 
+transitions vers \\(D\\) (**à vérifier**)
 
 ### Reach, coreach et loop
 
 Ces opérateurs permettent de calculer des formules, dans les explications
-suivantes \\(S\\) est une formule d'état et \\(T, T_1, T_2\\) des formules de
+suivantes \\(S\\) est une formule d'état et \\(T, T_1, T_2\\) des formulesde
 transitions:
 
  * \\(\text{reach}(S,T)\\) représente tous les états au départ de \\(S\\) avec
    \\(T\\) comme transitions
- * \\(\text{coreach}(S,T)\\) représente tous les états avec comme destination
+ * \\(\text{coreach}(S,T)\\) représente tous les états avec comme destnation
    \\(S\\) et utilisants \\(T\\) comme transitions.
- * \\(\text{loop}(T_1,T_2)\\) calcule des transitions, elle représente les
+ * \\(\text{loop}(T_1,T_2)\\) calcule des transition, elle représente les
    *Strongly Connected Components* (SCC). C'est une formule de transition tel
    que \\(T_3 \subseteq T_2\\) et \\(T_3 \cap T_1 \neq \emptyset\\). Ces *SCC*
    déterminent toutes situations permettant de revenir à la situation initiale.
@@ -256,9 +238,9 @@ transitions:
 En plus des propriétés heritées de la logique de *Dicky*, il existe dans ARC les
 propriété calculées suivantes pour chaque nœud:
 
- * `epsilon` : ensemble de transitons etiquetées \((\epsilon\\).
+ * `epsilon` :
  * `self` : transitions dont la source est la destination sont égaux
- * `self-epsilon`L définis par \\(epsilon \cap \text{self} \\)
+ * `self-epsilon`L définis par \\(epsilon \cap self \\)
  * `not_deterministic`: ensemble de transition non déterministe definies plus
    formellement par
    \\(\\{(s,e,t_1) \in E | \exists t_2 /in V, (s,e,t_2) \in  E\\}\\)
@@ -267,39 +249,24 @@ propriété calculées suivantes pour chaque nœud:
 
 ```
 with Switch, CircuitV1, Scheduler do
-    // deadlock:  états puit
     deadlock := any_s - src(any_t - self_epsilon);
-
+    notSCC := any_t - loop(any_t, any_t);
-    // notResetable : on ne peut pas revenir à l'état initial
-    notResettable := any_t - coreach(initial, any_t);
 done
-
 with CircuitV1, CircuitV2, CircuitV1_OK do
-    bug := any_s & [L.on & ~L.ok];
+    bug := [L.on & ~L.ok];
-    action := any_t & (label S.push | label G.failure | label G.repair);
+    notControl := (label G.failure | label L.reaction | epsilon) - self_epsilon;
-    reaction := any_t & ((label L.reaction | epsilon) − self_epsilon);
     
-    CFC_reaction := rsrc(reach(any_s & tgt(reaction),reaction) 
+    // IR means infinite reactions
-        & coreach(any_s & src(reaction),reaction)) & rtgt(reach(any_s 
+    IR := loop(notControl, notControl);
-        & tgt(reaction),reaction) 
-        & coreach(any_s & src(reaction),reaction)) 
-        & reaction;
-done
-
-with SchedulerRandom, SchedulerPriority, Scheduler do
-    bug := (label PJ[1].get & rsrc([PJ[0].nbJobs>0])) 
-        | (label PJ[2].get & rsrc([PJ[0].nbJobs>0 
-        | PJ[1].nbJobs>0]));
 done
 ```
-
 ### Les opérateurs
 
 En plus des oérateurs disponibles dnas la logique de Dicky, ARC implémente les
 opérateurs suivants:
 
  * \\(trace(S_1, T, S_2)\\) : ensemble de transitions représentant le chemin le
-   plus court de \\(S_1\\) vers \\(S_2\\) en utilisant les transitions\\(T\\).
+   plus long de \\(S_1\\) vers \\(S_2\\) en utilisant les transitions\\(T\\).
  * \\(project(S,T, 'newNodeName', boolean, aNode)\\) : construit une nouveau
    nœud AltaRica avec toutes les transitions \\(T\\) prenant leurs origines dans
    \\(S\\) en restectant les déclarations de \\(aNode\\) (cette déclaration est
@@ -308,38 +275,9 @@ opérateurs suivants:
 `trace` nous sera utile pour trouver des contre-exemple et `project` pour
 calculer des contrôleurs pour notre système.
 
-
-Voici un exemple de commandes `ARC`:
-
-```
-with Switch, CircuitV1, Scheduler do
-    show(all)               > ’$NODENAME.prop’;
-    test(deadlock,0)        > ’$NODENAME.res’;
-    test(notResettable,0)   >> ’$NODENAME.res’;
-done
-
-with CircuitV1, CircuitV2, CircuitV1_OK do
-    quot() > ’$NODENAME.dot’;
-    tr_CFC_reaction := trace(initial,any_t,src(CFC_reaction));
-    ce_CFC_reaction := reach(src(tr_CFC_reaction), tr_CFC_reaction 
-        | CFC_reaction);
-    dot(ce_CFC_reaction, tr_CFC_reaction|CFC_reaction) > ’$NODENAME−CFC_reaction.dot’;
-    show(tr_CFC_reaction, ce_CFC_reaction) >> ’$NODENAME.prop’;
-done
-```
-Ce qui donnera en sortie :
-
-```
-TEST(deadlock, 0)                               [PASSED]
-TEST(notResettable, 0)
-[FAILED] (!= 6)
-TEST(syst_instable, 0)
-[FAILED] (!= 4)
-```
-
 ### Methodologie
 
-nous allons utiliser cet outils comme un **déboggeur de modèle**, en respectant
+nous allons utiliser cet outils ocmme un **déboggeur de modèle**, en respectant
 les étapes suivantes:
 
  1. identifier les composants de base
@@ -357,7 +295,7 @@ les étapes suivantes:
  4. visualisation de petits composants
  5. simutation
 
-les étapes 1 et 2 sont à répéter jusqu'à obtention d'un modèle valide.
+les étapes 1 et deux sont à répéter jusqu'à obtention d'un modèle valide.
 
 ### Vérification du modèle
 

content/conception_formelle/3_extention_logique/index.md

@@ -1,145 +0,0 @@
----
-title: "Conception formelle : Extention de la logique"
-date: 2023-01-20
-tags: ["Bugs", "model-checking"]
-categories: ["Conception formelle", "Cours"]
-mathjax: true
----
-
-## Rappel mathématique
-
-Soit \\(E\\) un ensemble dictret, \\(f\\) une fonction tel que \\(f: E \to E \\)
-et \\(E_1 \subseteq E_2\\) et \\(E_2 \subseteq E\\) :
-
- * \\(f\\) est *monotone*  si et seulement si \\(E_1 \subseteq E_2) \implies
-   f(E_1) \subseteq f(E_2)\\)
- * \\(f\\) est **antimonotone* si et seulement si \\(E_1 \subseteq E_2) \implies
-   f(E_1) \supseteq f(E_2)\\)
- * \\(f\\) est augmentée si et seulement si \\(E_1 \subseteq f(E_1)\\)
- * \\(f\\) est reduite siet seulement si \\(E_1) \supseteq f(E_2)\\)
-
-Soit \\(f_1, f_2: E \to E\\) deux fonctions monotones et \\(g_1, g_2: E \to E\\)
-deux fonctions antimonotone :
-
- * \\(f_1(f_2(X))\\) est monotone
- * \\(f_1(f_2(X))\\) est antimonotone
- * \\(g_1(f_2(X))\\) est antimonotone
- * \\(g_1(g_2(X))\\) est monotone
-
-### Propriété (fonction monotone croissante)
-
-Soit \\(f: E \to E\\) une fonction monotone croissante tel que \\(\emptyset 
-\subseteq f(\emptyset) \subseteq f^2(\emptyset) \subseteq ... \subseteq 
-f^n(\emptyset) \subseteq ... \subseteq E\\) avec \\(E\\) ensemble finis et
-discret : \\(\exists i / \forall n \le i; f^n(\emptyset) = f^i(\emptyset) \\)
-alors \\(f^i(\emptyset)\\) est la plus petite solution à l'équation \\(X = f(X)
-\\).
-
-Alors si \\(E\\) est un ensemble fini et discret et que \\(f: E \to E\\) est
-une fonction monotone croissante alors \\(X=f(X)\\) est **plus petit point fixe
-obtenu par itération**. \\(f(E) = E\\) alors \\(E\\) est aussi une solution de \\(
-X = f(X)\\)
-
-### Propriété (fonction monotone décroissante)
-
-Soit \\(f: E \to E\\) une fonction monotone décroissante tel que \\(E \supseteq
-f(E) \supseteq f^2(E) \subseteq ... \subseteq f^n(E) \subseteq ... \subseteq
-\emptyset\\) avec \\(E\\) ensemble finis et discret : \\(\exists i / \forall n
-\le i; f^n(\emptyset) = f^i(\emptyset) \\) alors \\(f^i(\emptyset)\\) est la
-plus petite solution à l'équation \\(X = f(X) \\).
-
-Et si \\(f: E \to E\\) est une fonction monotone décroissante, alors \\(X=f(X)
-\\) est **plus grand point fixe obtenu par itération**.\\(f(\emptyset) = 
-\emptyset\\) alors \\(\emptyset\\) est aussi une solution de \\(
-X = f(X)\\)
-
-## Extension de la logique de Dicky
-
-Soit : 
-
- * \\(A\\) un graphe \\(G(S,T)\\)
- * \\(f(X)\\) une formule logique sur \\(S\\) (*state*) ou \\(T\\) 
-   (*transition*)
- * \\(S_1 \subseteq S\\) et \\(S_2 \subseteq S\\)
- * \\(T_1 \subseteq S\\) et \\(T_2 \subseteq S\\)
- * \\(X_1 \subseteq X\\) et \\(X_2 \subseteq X\\) avec \\(X = S\\) ou 
-   \\(X = T\\)
- * \\(Y_1 \subseteq Y\\) et \\(Y_2 \subseteq Y\\) avec \\(Y = S\\) ou 
-   \\(Y = T\\)
-
-### Constantes et proposition élémentaires
-
-\\(F(X)\\) est une formule avec seulement \\(\emptyset_S, \emptyset_T, any_s,
-any_t, initial, ...\\). Si \\(f\\) est une constante et \\(f^2(X) = f(X)\\) 
-alors \\(f(X)\\) est la solution.
-
-### Les opérateurs logiques
-
-Soit \\(f(X)\\) une formule avec aussi `src`, `tgt`, `rsrc`, `rtgt` et \\(T\\),
-\\(S\\) tel que
-
- * \\(T_1 \subseteq T_2 \implies src(T_1) \subseteq src(T_2)\\)
- * \\(T_1 \subseteq T_2 \implies tgt(T_1) \subseteq tgt(T_2)\\)
- * \\(S_1 \subseteq S_2 \implies rsrc(S_1) \subseteq rsrc(S_2)\\)
- * \\(S_1 \subseteq S_2 \implies rtgt(S_1) \subseteq rtgt(S_2)\\)
-
-\\(f\\) est monotone alors la solution de \\(X = f(X)\\) peut être calculée par
-itération.
-
-### Opérateurs d'ensembles
-
-Soit \\(f(X)\\) une formule avec aussi \\( \cup, \cap, \setminus \\)
-(soustraction d'ensemble) :
-
- * \\(X_1 \subseteq X_2, Y_1 \subseteq Y_2 \implies X_1 \cup Y_1 \subseteq X_2
-   \cup Y_2\\) (formule monotone)
- * \\(X_1 \subseteq X_2, Y_1 \subseteq Y_2 \implies X_1 \cap Y_1 \subseteq X_2
-   \cap Y_2\\) (formule monotone)
- * \\(X_1 \subseteq X_2, Y_1 \subseteq Y_2 \implies X_1 \setminus Y_1 ?
-   X_2  \setminus Y_2\\) ici deux cas de figures:
-   * \\(X_1 \subseteq X_2 \implies X_1 \setminus Y_1 \subseteq X_2 \setminus
-     Y_1\\) est une formule monotone.
-   * \\(Y_1 \subseteq Y_2 \implies X_1 \setminus X_2 \supseteq X_2 \setminus
-     Y_2\\) est une formule anti monotone.
-
-
-### Résultat
-
-Soit \\(f(X)\\) une formule. Si \\(X\\) apparaît derrière un nombre pair de
-soustrtactions, **alors \\(f\\) est monotone et \\(f(X)\\)** peut être calculé
-par itération :
-
- * Si elle est croissante nous pouvons calculer le plus petit point fixe
- * Si elle est décroissante nous pouvons caluler le plus grand point fixe
-
-Sinon **elle est antimonotone** et ne peut être calculée par itération. Alors
-nous ne pouvons pas savoir s'il existe une solution à \\(X = f(X)\\).
-
-### Exemple
-
-Prenons la formule \\(F(X) = dead_0 \ cup (src(rtgt(X)) \setminus src(rtgt(any_s
-\setminus X)))\\) :
-
- * nous avons trois occurences de \\(X\\) après 0,0 et deux soustractions dans
-   l'expression, donc \\(f\\) est monotone.
- * \\(f\\) est une fonction croissante, nous pouvons alos calculer le plus petit
-   point fixe par l'itération de \\(f^i(\emptyset_s)\\).
-
-La solution de cette équation représente le plus petit ensemble de
-configurations qu mène à un état puit.
-
-## Sur *ARC*
-
-\\( X -= f(X)\\) calcule le plus grand point fixe et \\( X += f(X)\\) le plus
-petit point fixe. Voici un exemple :
-
-``````
-with MyComponent do
-    // calculer les états puit 
-    dead := any_s - src(any_t - self_epsilon);
-
-    // trouver les transitions qui mène ces états : calcul du plus
-    // petit point fixe
-    deadlock += dead | (src(rtgt(deadlock)) - src(rtgt(any_s - deadlock)));
-done
-```