629 lines
24 KiB
Org Mode
629 lines
24 KiB
Org Mode
#+TITLE: Programmation synchrone 2025/2026 -- Journal du cours
|
|
#+AUTHOR: Adrien Guatto
|
|
#+EMAIL: guatto@irif.org
|
|
#+LANGUAGE: fr
|
|
#+OPTIONS: ^:nil p:nil
|
|
#+LATEX_CLASS: article
|
|
#+LATEX_CLASS_OPTIONS: [a4paper,11pt]
|
|
#+LATEX_HEADER: \usepackage{a4wide}
|
|
#+LATEX_HEADER: \usepackage{microtype}
|
|
#+LATEX_HEADER: \hypersetup{hidelinks}
|
|
#+LATEX_HEADER: \usepackage[french]{babel}
|
|
# (org-latex-export-to-pdf)
|
|
|
|
* Cours 01 <2025-09-29>
|
|
On lit le syllabus ainsi que le début des notes.
|
|
|
|
Le manuel d'Heptagon peut être trouvé sur le dépôt git du projet. On peut
|
|
cliquer sur le bouton /download/ pour télécharger une copie PDF.
|
|
|
|
https://gitlab.inria.fr/synchrone/heptagon/-/blob/ec26be27b91f3e601b98b8b7e15e8d56d4b9afc7/manual/heptagon-manual.pdf
|
|
* Cours 02 <2025-10-06>
|
|
On traite des constructions de base du langage.
|
|
* Cours 03 <2025-10-13>
|
|
On traite des horloges et automates.
|
|
* Cours 04 <2025-10-20>
|
|
On traite des automates et tableaux.
|
|
* Cours 05 <2025-10-27>
|
|
** Programmation Heptagon
|
|
On traite des tableaux.
|
|
** Exemples
|
|
On traite la génération d'échantillons audios, disponbile dans son
|
|
[dossier](audio/).
|
|
* Cours 06 <2025-11-04>
|
|
** Projet
|
|
On traite du fonctionnement du projet.
|
|
* Cours 07 <2025-11-10>
|
|
** Exemples
|
|
On traite l'exemple du pendule inversé, disponible dans son
|
|
[dossier](inverted-pendulum/).
|
|
** Implémentation des langages synchrones
|
|
On commence à expliquer la compilation d'Heptagon, avec l'explication de
|
|
MiniLS vers Obc jusqu'au traitement des horloges *exclu*.
|
|
* Cours 08 <2025-11-17>
|
|
** Implémentation des langages synchrones
|
|
On discute de la compilation des horloges en MiniLS, de la traduction des
|
|
automates et des structures de contrôle plus simples (notamment ~switch~) en
|
|
Heptagon. On présente l'analyse d'initialisation.
|
|
* Cours 09 <2025-11-24>
|
|
** Implémentation des langages synchrones
|
|
On termine la partie concernant l'implémentation des langages synchrones.
|
|
** Vérification automatique
|
|
L'outil Kind2 est un vérificateur de modèle (/model checker/) pour un langage
|
|
proche d'Heptagon développé à l'université de l'Iowa.
|
|
|
|
https://kind.cs.uiowa.edu
|
|
|
|
Un tel outil est une des justifications pour l'emploi d'un langage très
|
|
limité comme Heptagon, SCADE et leurs variantes. La vérification automatique
|
|
est beaucoup plus difficile lorsque le langage d'entrée est un langage
|
|
généraliste comme C, Python ou OCaml.
|
|
*** Introduction
|
|
Le langage accepté par Kind2 est une variante d'Heptagon beaucoup plus
|
|
proche de son ancêtre Lustre. Les différences sont assez mineures mais
|
|
peuvent rendre l'écriture du code désagréable lorsqu'on est habitué aux
|
|
constructions d'Heptagon.
|
|
|
|
Par exemple, le langage ne propose pas l'opérateur ~fby~, uniquement ~pre~
|
|
et ~->~. Notre classique compteur doit donc être écrit comme suit.
|
|
|
|
#+BEGIN_SRC
|
|
node counter() returns (o : int)
|
|
let
|
|
o = 0 -> (pre o + 1);
|
|
tel
|
|
#+END_SRC
|
|
|
|
Kind2 est capable de traduire ce programme vers du code impératif, jouant
|
|
ainsi le même rôle que le compilateur ~heptc~ pour Heptagon. Plutôt que de
|
|
générer du code C, Kind2 produit du code Rust.
|
|
|
|
#+BEGIN_SRC
|
|
$ kind2 --compile true ex0.lus
|
|
kind2 v1.1.0-16-g9572d9b
|
|
|
|
<Note> System counter has no property, skipping verification step.
|
|
|
|
--------------------------------------------------------------------------------
|
|
Post-analysis: rust generation
|
|
|
|
<Note> Compilation to Rust is still a rather experimental feature:
|
|
in particular, arrays are not supported.
|
|
|
|
Compiling node "counter" to Rust in `ex0.lus.out/counter/implem`.
|
|
|
|
Done compiling.
|
|
|
|
--------------------------------------------------------------------------------
|
|
$ wc -l ex0.lus.out/counter/implem/src/main.rs
|
|
366 ex0.lus.out/counter/implem/src/main.rs
|
|
#+END_SRC
|
|
|
|
L'intérêt principal de Kind2 est ailleurs : il est capable de /vérifier
|
|
formellement/ des propriétés. Par opposition au test, la vérification
|
|
formelle permet de vérifier qu'une propriété est vraie pour *toute* entrée,
|
|
plutôt que pour une entrée particulière. De plus, dans le cas des langages
|
|
synchrones, les entrées sont des suites infinies, dont on ne peut tester
|
|
qu'un préfixe fini. La vérification formelle, elle, considère des entrées de
|
|
longueur infinie.
|
|
|
|
Lorsqu'on découvre un outil de vérification formelle, un des premières
|
|
questions à se poser est celle du langage dans lequel les propriétés sont
|
|
écrites. Certains outils de vérification offrent un langage spécialisé pour
|
|
ce faire, par exemple une logique temporelle pour le model-checker PRISM.
|
|
Les outils de vérification de langages synchrones comme Kind2 font un choix
|
|
un peu différent. Le langage des propriétés est le même que celui des
|
|
programmes, et la propriété à vérifier est exprimée par un flot booléen
|
|
désigné par l'utilisateur doit toujours être vrai. Avec cette approche, on
|
|
va avoir tendance à écrire des /observateurs synchrones/, c'est-à-dire des
|
|
noeuds qui sont utilisés uniquement pour vérifier que le noeud qui va être
|
|
déployé sur le système embarqué final va respecter certaines propriétés,
|
|
éventuellement sous certaines hypothèses concernant ses entrées.
|
|
|
|
#+BEGIN_SRC
|
|
node top() returns (ok : bool)
|
|
var o : int;
|
|
let
|
|
o = counter();
|
|
ok = o >= 0;
|
|
--%PROPERTY ok;
|
|
tel
|
|
#+END_SRC
|
|
|
|
En lançant Kind2 sur ce fichier, on lui demande de vérifier que le flot ~ok~
|
|
est toujours vrai. Il est capable de vérifier que c'est le cas, même si ~ok~
|
|
contient une infinité de valeurs.
|
|
|
|
#+BEGIN_SRC
|
|
$ kind2 ex0.lus
|
|
kind2 v1.6.0
|
|
|
|
====================================================================================================================
|
|
Analyzing top
|
|
with First top: 'top'
|
|
subsystems
|
|
| concrete: counter
|
|
|
|
<Success> Property ok is valid by property directed reachability after 0.148s.
|
|
|
|
--------------------------------------------------------------------------------------------------------------------
|
|
Summary of properties:
|
|
--------------------------------------------------------------------------------------------------------------------
|
|
ok: valid (at 1)
|
|
====================================================================================================================
|
|
#+END_SRC
|
|
|
|
(Cet exemple montre que Kind2 suppose que la sémantique du type ~int~ de
|
|
Lustre est celle des entiers relatifs, sans limite de taille. Pourquoi ?
|
|
Remarquons que jusqu'ici on avait supposé que les types des langages
|
|
synchrones étaient tous finis, ce qui assurait la finitude de la mémoire.
|
|
Comme on le décrira plus bas, ce choix n'est pas sans conséquences
|
|
théoriques et pratiques.)
|
|
|
|
Cet exemple laisse aussi deviner que la vérification est un processus
|
|
coûteux, beaucoup plus coûteux que la compilation. Ce fichier étant écrit
|
|
dans le sous-ensemble commun à Heptagon et Lustre, on peut le compiler avec
|
|
~heptc~ et comparer le temps de compilation au temps de vérification.
|
|
|
|
#+BEGIN_SRC
|
|
$ time heptc -target c ex0.lus
|
|
real 0m0,026s
|
|
user 0m0,013s
|
|
sys 0m0,013s
|
|
#+END_SRC
|
|
|
|
On peut montrer des propriétés un peu plus intéressantes, par exemple en
|
|
écrivant une variante du compteur avec une valeur d'initialisation.
|
|
|
|
#+BEGIN_SRC
|
|
node counterini(ini : int) returns (o : int)
|
|
let
|
|
o = ini -> (pre o + 1);
|
|
tel
|
|
|
|
node top(ini : int) returns (ok : bool)
|
|
var o : int;
|
|
let
|
|
o = counterini(ini);
|
|
ok = o >= 0;
|
|
check ok;
|
|
tel
|
|
#+END_SRC
|
|
|
|
Cet exemple est plus intéressant que le précédent en ce que le noeud ~top~
|
|
dispose désormais d'une entrée. Kind2 va donc essayer de vérifier que toutes
|
|
les valeurs de la suite ~ok~ sont vraies et ce /pour toutes les suites
|
|
d'entrée ~ini~/. Va-t-il réussir ?
|
|
|
|
#+BEGIN_SRC shell
|
|
$ kind2 ex0.lus
|
|
kind2 v1.6.0
|
|
|
|
====================================================================================================================
|
|
Analyzing top
|
|
with First top: 'top'
|
|
subsystems
|
|
| concrete: counterini
|
|
|
|
<Failure> Property ok is invalid by bounded model checking for k=0 after 0.041s.
|
|
|
|
Counterexample:
|
|
Node top ()
|
|
== Inputs ==
|
|
ini -1
|
|
== Outputs ==
|
|
ok false
|
|
== Locals ==
|
|
o -1
|
|
|
|
Node counterini (top[l14c7])
|
|
== Inputs ==
|
|
ini -1
|
|
== Outputs ==
|
|
o -1
|
|
|
|
|
|
--------------------------------------------------------------------------------------------------------------------
|
|
Summary of properties:
|
|
--------------------------------------------------------------------------------------------------------------------
|
|
ok: invalid after 0 steps
|
|
====================================================================================================================
|
|
#+END_SRC
|
|
|
|
La vérification a échoué, mais Kind2 nous a fourni un contre-exemple sous la
|
|
forme d'une séquence d'entrées qui falsifie la propriété. Il suffit bien sûr
|
|
de donner un ~ini~ strictement négatif au premier instant !
|
|
|
|
Notre propriété est donc fausse. Peut-on exprimer que le flot ~o~ est
|
|
toujours vrai mais *à condition* que la première valeur de ~ini~ soit
|
|
positive ? Oui, en utilisant l'opérateur booléen d'implication pour exprimer
|
|
une /précondition/ (hypothèse) sur l'entrée ~ini~.
|
|
|
|
(Remarque : l'implication dont il s'agit ici n'est que l'opérateur
|
|
combinatoire sur les flots défini par ~x => y = not x or y~, rien de plus.
|
|
En particulier, Kind2 n'a aucun traitement spécifique de cet opérateur.)
|
|
|
|
Un premier essai pourrait ressembler à ce qui suit.
|
|
|
|
#+BEGIN_SRC
|
|
node top(ini : int) returns (ok : bool)
|
|
var o : int;
|
|
let
|
|
o = counterini(ini);
|
|
ok = ((ini >= 0) -> true) => (o >= 0);
|
|
check ok;
|
|
tel
|
|
#+END_SRC
|
|
|
|
La vérification échoue encore, avec le contre-exemple qui suit.
|
|
|
|
#+BEGIN_VERBATIM
|
|
Counterexample:
|
|
Node top ()
|
|
== Inputs ==
|
|
ini -2 0
|
|
== Outputs ==
|
|
ok true false
|
|
== Locals ==
|
|
o -2 -1
|
|
|
|
Node counterini (top[l19c7])
|
|
== Inputs ==
|
|
ini -2 0
|
|
== Outputs ==
|
|
o -2 -1
|
|
#+END_VERBATIM
|
|
|
|
Comment comprendre ce contre-exemple ? Au premier instant, ~i~ vaut ~-2~ et
|
|
la précondition sur ~ini~ est fausse, donc l'implication est vraie. Au
|
|
deuxième instant, la précondition sur ini est vraie, donc l'implication
|
|
prend la valeur de ~o >= 0~, qui se trouve fausse.
|
|
|
|
Quel est le problème ? Ce que nous avions en tête n'est pas ce que nous
|
|
avons écrit. On aurait voulu dire "si ~ini < 0~ au premier instant, la
|
|
précondition est fausse pour toujours", mais on a écrit "si ~ini < 0~ au
|
|
premier instant, la précondition est fausse /au premier instant/". On peut
|
|
régler le problème en introduisant un noeud ~always~ dont la sortie devient
|
|
fausse pour toujours dès que son entrée est fausse.
|
|
|
|
#+BEGIN_SRC
|
|
node always(b : bool) returns (o : bool)
|
|
let
|
|
o = (true -> pre o) and b;
|
|
tel
|
|
|
|
node top(ini : int) returns (ok : bool)
|
|
var o : int;
|
|
let
|
|
o = counterini(ini);
|
|
ok = always((ini >= 0) -> true) => (o >= 0);
|
|
check ok;
|
|
tel
|
|
#+END_SRC
|
|
|
|
La vérification réussit. En particulier, le contre-exemple précédent n'est
|
|
plus valide. Si la valeur initiale de ~ini~ est ~-2~, la valeur de
|
|
~always((ini >= 0) -> true)~ sera toujours fausse, et donc la vérité de
|
|
l'implication dépendra de ~o >= 0~, toujours vraie.
|
|
|
|
Le fait d'exprimer une précondition sur les entrées est très fréquent, et
|
|
Kind2 propose une syntaxe un peu plus agréable pour ce faire.
|
|
|
|
#+BEGIN_SRC
|
|
node top(ini : int) returns (ok : bool)
|
|
var o : int;
|
|
let
|
|
o = counterini(ini);
|
|
ok = o >= 0;
|
|
check ok provided always((ini >= 0) -> true);
|
|
tel
|
|
#+END_SRC
|
|
*** Comparaison de noeuds
|
|
On peut utiliser le principe des observateurs synchrones pour comparer le
|
|
comportement de deux noeuds, et éventuellement tester leur équivalence.
|
|
|
|
Par exemple, comment quelle relation voyez vous entre notre premier noeud
|
|
~counter~ et le noeud ~counterini~ ? Et comment la feriez-vous vérifier par
|
|
Kind2 ?
|
|
|
|
Le lien est essentiellement qu'ajouter la première valeur de ~ini~ à la
|
|
sortie de ~counter~ donne celle de ~counterini~. La tentative donnée
|
|
ci-dessous est trop naïve puisqu'il ne faut prendre en compte ~ini~
|
|
uniquement au premier instant.
|
|
|
|
#+BEGIN_SRC
|
|
node compare(ini : int) returns (ok : bool)
|
|
let
|
|
ok = counter() + ini = counterini(ini);
|
|
check ok;
|
|
tel
|
|
#+END_SRC
|
|
|
|
On peut utiliser un noeud ~constant~ qui maintient la valeur reçue au
|
|
premier instant. On obtient le noeud suivant, dont la propriété est
|
|
vérifiée.
|
|
|
|
#+BEGIN_SRC
|
|
node constant(ini : int) returns (o : bool)
|
|
let
|
|
o = ini -> pre o;
|
|
tel
|
|
|
|
node compare(ini : int) returns (ok : bool)
|
|
let
|
|
ok = counter() + constant(ini) = counterini(ini);
|
|
check ok;
|
|
tel
|
|
#+END_SRC
|
|
*** Les contrats
|
|
Les propriétés qu'on a vérifié jusqu'ici sont des propriétés globales du
|
|
système. Il s'agit certainement d'une approche utile, mais elle n'est pas
|
|
tout à fait convaincante du point de vue du génie logiciel. On aimerait
|
|
plutôt vérifier chaque noeud indépendamment. Kind2 le permet via l'écriture
|
|
de /contrats/ qui permettent à chaque noeud de documenter ses attentes
|
|
vis-à-vis de ses appelants (mot-clef /assume/) et ses garanties (mot-clef
|
|
/guarantee/).
|
|
|
|
#+BEGIN_SRC
|
|
node counterini(ini : int) returns (o : int)
|
|
(*@contract
|
|
assume (ini >= 0) -> true;
|
|
guarantee o >= 0;
|
|
*)
|
|
let
|
|
o = ini -> (pre o + 1);
|
|
tel
|
|
#+END_SRC
|
|
|
|
Notez que Kind2 assure la bonne sémantique pour l'hypothèse (/assume/),
|
|
c'est-à-dire qu'elle doit être valide de toute la séquence d'entrées, et ce
|
|
sans avoir à utiliser une noeud comme ~always~. (Pour ceux et celles d'entre
|
|
vous qui connaissent la logique temporelle, si $A$ est la formule booléenne
|
|
des hypothèses et $G$ est la formule booléenne des garanties, la formule que
|
|
l'outil cherche à démontrer est $\square A \Rightarrow \square G$ plutôt que
|
|
$\square A \Rightarrow \square G$.
|
|
|
|
Je finis cette partie pratique par une difficulté à laquelle tous les
|
|
utilisateurs de vérification formelle finissent par se heurter un jour ou
|
|
l'autre : des hypothèses trop fortes rendent la garantie triviale. Voir
|
|
ci-dessous pour un exemple caricatural ; /garbage in, garbage out/.
|
|
|
|
#+BEGIN_SRC
|
|
node counterini(ini : int) returns (o : int)
|
|
(*@contract
|
|
assume false;
|
|
guarantee (o = constant(o));
|
|
*)
|
|
let
|
|
o = ini -> (pre o + 1);
|
|
tel
|
|
#+END_SRC
|
|
|
|
Cependant, Kind2 aide à détecter le problème. L'outil va chercher à vérifier
|
|
que tout appelant à ce ~counterini~ satisfait aux hypothèses, ce qui ici est
|
|
impossible... Sauf si l'appelant a lui-même fait des hypothèses
|
|
contradictoires sur ses entrées, bien entendu !
|
|
* Cours 10 <2025-12-01>
|
|
** Vérification automatique, suite
|
|
*** Exemples
|
|
**** Compteurs
|
|
On va s'intéresser à la vérification d'équivalence entre compteurs
|
|
périodiques de 0 à 3, formulé avec des entiers, puis en codage binaire,
|
|
classique puis de Gray.
|
|
|
|
On commence par écrire le compteur sur deux bits avec un entier
|
|
|
|
#+BEGIN_SRC
|
|
node intcounter (rst : bool; const max : int) returns (out : bool);
|
|
var t : int;
|
|
let
|
|
t = 0 -> if rst or pre t = max then 0 else pre t + 1;
|
|
out = t = 3;
|
|
tel
|
|
|
|
node graycounter (rst : bool) returns (out : bool);
|
|
var a, b : bool;
|
|
let
|
|
a = false -> (not rst and not pre b);
|
|
b = false -> (not rst and pre a);
|
|
out = not a and b;
|
|
tel
|
|
|
|
node bincounter (rst : bool) returns (out : bool);
|
|
var a, b : bool;
|
|
let
|
|
a = false -> (not rst and (pre a <> pre b));
|
|
b = false -> (not rst and not pre b);
|
|
out = a and b;
|
|
tel
|
|
|
|
node top (rst : bool) returns ();
|
|
var grayc, binc, intc : bool;
|
|
let
|
|
grayc = graycounter(rst);
|
|
intc = intcounter(rst, 3);
|
|
binc = bincounter(rst);
|
|
check binc = intc;
|
|
check grayc = intc;
|
|
tel
|
|
#+END_SRC
|
|
*** Les bases de l'algorithmique de la vérification
|
|
Les données du problème sont :
|
|
|
|
1. un programme synchrone à vérifier,
|
|
|
|
2. un /observateur/ pour la propriété à démontrer (~check ok~),
|
|
|
|
3. un /observateur/ pour l'hypothèse supposée (~assert hyp~).
|
|
|
|
L'objectif d'un vérificateur de modèle pour un programme synchrone à flots
|
|
de données est de démontrer :
|
|
|
|
~always(so_far(hyp) => ok)~.
|
|
|
|
Notons qu'on ne traite que les propriétés de sûreté (``quelque-chose de
|
|
mauvais n'arrive toujours'') et pas de vivacité (``quelque-chose de bon
|
|
finit toujours par arriver''), comme expliqué au cours précédent.
|
|
|
|
On va s'intéresser à ce problème dans le cas *purement booléen*,
|
|
c'est-à-dire où toutes les variables manipulées sont des suites de
|
|
booléens. Notre description est basée sur le rapport de recherche de Pascal
|
|
Raymond disponible à
|
|
[[https://www.di.ens.fr/~pouzet/cours/mpri/bib/lesar-rapport.pdf][cette
|
|
adresse]].
|
|
|
|
Si $X$ est un ensemble, on écrit $\overline{X}$ pour les fonctions de $X$
|
|
dans $\mathbb{B}$, qui sont en bijection avec les parties de $X$. On
|
|
identifiera librement les sous-ensembles et leurs fonctions
|
|
charactéristiques dans ce qui suit.
|
|
|
|
Les données du problème sont les n-uplets ($V$, $S$, $I \subseteq
|
|
\overline{S}$, $g : \overline{S} \times \overline{V} \to \overline{S}$, $H
|
|
\subseteq \overline{S} \times \overline{V}$, $\Phi \overline{S} \times
|
|
\overline{V}$), où :
|
|
|
|
- $S$ et $V$ sont des ensembles *finis* dont les éléments sont
|
|
respectivement les variables d'état de d'entrée du programme,
|
|
|
|
- $I$ est l'ensemble des états initiaux,
|
|
|
|
- $H$ est l'hypothèse,
|
|
|
|
- $\Phi$ est la propriété à démontrer.
|
|
|
|
On écrira $q \to^v q'$ pour $q' = g(q, v)$ avec $q,q' \in \overline{S}$ et
|
|
$v \in \overline{V}$.
|
|
|
|
On définit les états successeur/prédécesseurs d'un état $q$ ou d'un
|
|
ensemble d'états~$X$ par :
|
|
|
|
\begin{align*}
|
|
post_H(q) & = \{ q' \mid \exists v \in q \to_v q' \wedge H(q, v) \}
|
|
\\
|
|
pre_H(q) & = \{ q' \mid \exists v \in q' \to_v q \wedge H(q', v) \}
|
|
\\
|
|
POST_H(X) & = \bigcup_{q \in X} post_H(q)
|
|
\\
|
|
PRE_H(X) & = \bigcup_{q \in X} pre_H(q)
|
|
\end{align*}
|
|
|
|
L'ensemble des états d'erreurs immédiate sont ceux qui satisfont
|
|
l'hypothèse mais pas la propriété à démontrer.
|
|
|
|
\[
|
|
Err = \{ q \mid \exists v, H(q, v) \wedge \neg \Phi(q, v) \}
|
|
\]
|
|
|
|
On définit maintenant l'ensemble $Acc$ des états accessibles du programme
|
|
et l'ensemble $Bad$ des mauvais états par un plus petit point fixe
|
|
ensembliste : $\mu X . F(X)$ désigne le plus petit ensemble $Y$ tel que
|
|
$F(Y) \subseteq Y$ ; son existence est garantie dès lors que $F$ est
|
|
croissante pour l'inclusion.
|
|
|
|
\begin{align*}
|
|
Acc & = \mu X. (I \cup POST_H(X))
|
|
\\
|
|
Err & = \{ q \mid \exists v, H(q, v) \wedge \neg \Phi(q, v) \}
|
|
\\
|
|
Bad & = \mu X . (Err \cup PRE_H(X))
|
|
\end{align*}
|
|
|
|
L'objectif est maintenant de démontrer que le système est *sûr*,
|
|
c'est-à-dire que $Acc \cap Bad = \emptyset$. Autrement dit, aucun état
|
|
accessible du système n'est un état d'erreur.
|
|
|
|
Pour ce faire, il existe deux grandes méthodes :
|
|
|
|
- l'exploration en *avant* : on démontre $Acc \cap Err = \emptyset$,
|
|
|
|
- l'exploration en *arrière* : on démontre $Bad \cap I = \emptyset$.
|
|
|
|
L'approche la plus simple pour ce faire est une approche énumérative : on
|
|
explore explicitement l'automate induit par le programme, en imitant le
|
|
calcul du plus petit point fixe correspondant à $Acc$ ou $Bad$.
|
|
|
|
#+BEGIN_SRC
|
|
Known := I; Explored := {}
|
|
while there is q in Known \ Explored:
|
|
for all q' in post(q):
|
|
if q' in Err:
|
|
return FAILURE
|
|
move q' to Known
|
|
move q to Explored
|
|
}
|
|
return SUCCESS
|
|
#+END_SRC
|
|
|
|
Cet algorithme peut être implémenté et termine puisque tous les ensembles
|
|
manipules sont finis, les prédicats calculables, tout comme la fonction de
|
|
transition du programme. En particulier, vous pouvez implémenter les
|
|
ensembles ~Known~ et ~Explored~ par votre structure d'ensemble fini
|
|
favorite, et énumérer les valeurs possibles pour calculer ~post(q)~. Il
|
|
s'agit donc en somme d'exécuter le programme sur toutes les entrées
|
|
possibles ; on voit que c'est très inefficace.
|
|
|
|
On peut aussi implémenter une version en arrière.
|
|
|
|
#+BEGIN_SRC
|
|
Known := Err; Explored := {}
|
|
while there is q in Known \ Explored:
|
|
for all q' in pre(q):
|
|
if q' in I:
|
|
return FAILURE
|
|
move q' to Known
|
|
move q to Explored
|
|
}
|
|
return SUCCESS
|
|
#+END_SRC
|
|
|
|
Les deux algorithmes sont très inefficaces, tellement qu'ils en deviennent
|
|
inutilisables en pratique. En effet, les structures de données
|
|
représentant les ensembles d'état ou d'entrées deviendront très grosses,
|
|
et les calculs attenants (différence ensembliste, ajout, choix d'un
|
|
élément...) coûteux à réaliser.
|
|
|
|
Notons que le second algorithme est encore moins efficace que le
|
|
premier. Voyez-vous pourquoi ? Le calcul de ~pre(q)~ est encore plus
|
|
coûteux, puisqu'il faut calculer l'image inverse de la fonction de
|
|
transition $g$, c'est-à-dire trouver l'ensemble des $q'$ tel que $g(q', v)
|
|
= q$ pour $v$ et $q$ fixés.
|
|
|
|
Depuis les années 1990, on utilise plutôt des méthodes dites
|
|
*symboliques*. L'idée générale est de représenter les ensembles finis par
|
|
des formules logiques plutôt que par des énumérations explicites. Par
|
|
exemple, on pourrait représenter l'ensemble $\{ (x, y, z) \mid x
|
|
\overline{y} + z = 1 \}$ directement par le *code* de sa fonction
|
|
caractéristique $f(x, y, z) = x \overline{y} + z$ plutôt qu'explicitement
|
|
par l'ensemble de triplets $\{ (1, 0, 0), (1, 0, 1), (0, 0, 1), (0, 1, 1),
|
|
(1, 1, 1) \}$. Les méthodes symboliques sont donc un exemple de compromis
|
|
temps-espace : on y gagne une représentation nettement plus succincte des
|
|
données que la représentation explicite, en contrepartie de quoi les
|
|
opérations (notamment test d'égalité, du vide, d'inclusion, etc.) seront
|
|
plus coûteuses.
|
|
|
|
Il existe deux grandes méthodes d'implémentation pour exprimer les
|
|
opérations et les tests :
|
|
|
|
1. On peut représenter les formules directement par leur code et utiliser
|
|
un solveur SAT général pour répondre aux questions intéressantes pour
|
|
la vérification. Par exemple, l'ensemble $\{ \vec{x} \mid \phi(\vec{x})
|
|
\}$ est inclus dans l'ensemble $\{ vec{x} \mid \psi(\vec{x}) \}$ si et
|
|
seulement si $\forall \vec{x}, \phi(\vec{x}) \implies \psi(\vec{x})$,
|
|
question à laquelle un solveur SAT peut répondre, y compris pour de
|
|
très grosses formules $\phi$ et $\psi$. D'autres questions, comme par
|
|
exemple l'énumération des valeurs appartenant à un ensemble, sont d'un
|
|
traitement moins direct mais peuvent être gérée avec un peu de
|
|
réflexion et d'effort.
|
|
|
|
2. On peut utiliser une représentation canonique des formules booléennes,
|
|
par exemple les /diagrammes de décision binaire/ (ou /binary decision
|
|
diagrams/ en anglais, BDD). Ici, toutes les formules équivalentes sont
|
|
représentées par la même structure de données. La construction de cette
|
|
représentation est donc forcément coûteuse, mais une fois construite on
|
|
peut l'utiliser pour répondre efficaement à beaucoup de questions. C'est
|
|
cette approche qui est très bien exposée dans le rapport de P. Raymond
|
|
cité plus haut.
|
|
|
|
Le principe des diagrammes de décision binaire a été brièvement expliqué en
|
|
cours mais ne sera pas détaillé dans ces notes.
|