More doc : command lien options;

1 files changed, 223 insertions, 22 deletions

diff --git a/readme.tm b/readme.tm
index c7a0b2f..0d6388c 100644
--- a/readme.tm
+++ b/readme.tm
@@ -1443,7 +1443,185 @@
 
   <section|Implémentation>
 
-  \;
+  Le projet scade-analyzer propose une implémentation simple des composants
+  suivants :
+
+  <\itemize>
+    <item>parser, lexer, typeur pour notre sous-ensemble de SCADE (source des
+    fichiers dans <verbatim|frontend/>)
+
+    <item>interprète pour la sémantique cocnrète
+    (<verbatim|interpret/interpret.ml>)
+
+    <item>implémentation de la transformation d'un programme en formule
+    logique ; quelques simplifications sur les formules logiques
+    (<verbatim|abstract/formula.ml>, <verbatim|abstract/transform.ml>).
+
+    <item>domaine numérique non-relationnel basé sur les intervalles ;
+    domaine relationnel basé sur la bibliothèque externe Apron
+    (<verbatim|abstract/num_domain.ml>, <verbatim|abstract/nonrelational.ml>,
+    <verbatim|abstract/apron_domain.ml>, ...)
+
+    <item>deux domaines abstraits et analyseur statique correspondant
+    (<verbatim|abstract/abs_interp.ml>, <verbatim|abstract/abs_interp_edd.ml>)
+  </itemize>
+
+  En nous basant sur les options de la ligne de commande, nous allons
+  maintenant décrire les différentes fonctionnalités.
+
+  <subsection|Parsing et affichage de programmes SCADE>
+
+  <\itemize>
+    <item><verbatim|--dump> : parse un fichier SCADE et le ré-affiche en
+    sortie
+
+    <item><verbatim|--dump-rn> : parse un fichier SCADE et le ré-affiche en
+    sortie, après une étape de renommage qui consiste à rendre les noms
+    unique au sein d'un noeud. Cette passe est implémentée dans
+    <verbatim|frontend/rename.ml>.
+  </itemize>
+
+  <subsection|Interprète SCADE>
+
+  <\itemize>
+    <item><verbatim|--test> : execute le programme SCADE donné en argument,
+    avec l'interprète <verbatim|interpret/interpret.ml> basé sur la
+    sémantique à réduction. Le programme doit satisfaire la spécification
+    suivante : avoir un noeud <verbatim|test> qui servira de racine, ce noeud
+    devant prendre une unique entrée, <verbatim|i>, qui est un compteur
+    incrémenté à chaque cycle, et renvoyant trois entiers, <verbatim|a>,
+    <verbatim|b> et <verbatim|c> (qui seront affichés en sortie), ainsi qu'un
+    booleen <verbatim|exit> qui indiquera que l'interprète doit terminer. Cf
+    fichiers dans <verbatim|tests/source/*.scade> pour des exemples.
+
+    <item><verbatim|--vtest> : pareil mais affiche plus de détails (tout le
+    contenu de la mémoire est affiché à chaque cycle).
+  </itemize>
+
+  <subsection|Analyse statique par interprétation abstraite>
+
+  <subsubsection|Domaine à disjonctions simples>
+
+  Cette analyse est implémentée dans <verbatim|abstract/abs_interp.ml>.
+
+  <paragraph|Modes d'analyse>
+
+  <\itemize>
+    <item><verbatim|--ai-itv> : fait une passe d'analyse statique par
+    interprétation abstraite utilisant le domaine à disjonctions simples, et
+    en s'appuyant sur le domaine non-relationnel à base d'intervalles pour la
+    partie numérique
+
+    <item><verbatim|--ai-rel> : de même mais utilise le domaine abstrait
+    relationnel basé sur Apron (polyèdres) pour la partie numérique
+  </itemize>
+
+  <paragraph|Options de l'analyse>
+
+  <\itemize>
+    <item><verbatim|--root \<less\>noeud\<gtr\>> : spécifie le noeud racine
+    dont on veut faire l'analyse (par défaut : <verbatim|test>)
+
+    <item><verbatim|--ai-vci> : affiche des détails sur le contenu de
+    l'accumulateur à chaque itération
+
+    <item><verbatim|--ai-vvci> : affiche encore plus de détails
+
+    <item><verbatim|--ai-wd \<less\>n\<gtr\>> : définit un délai pour les
+    opérations de widening (par défaut 5)
+
+    <item><verbatim|--disj \<less\>vars\<gtr\>> : variables à utiliser comme
+    variables de disjonction (par défaut : aucune)
+
+    <item><verbatim|--no-time \<less\>scopes\<gtr\>> : donne un certain
+    nombre de scopes pour lesquels ne pas introduire de variable
+    <verbatim|time> (par défaut <verbatim|all>, c'est-à-dire que
+    <verbatim|time> n'est jamais introduite). Lorsqu'une variable
+    <verbatim|time> est introduite, on génère les équations qui font en sorte
+    que <verbatim|time> soit égal au numéro du cycle depuis le début de
+    l'exécution du programme.
+
+    <item><verbatim|--init \<less\>scopes\<gtr\>> : donne un certain nombre
+    de scopes pour lesquels introduire une variable <verbatim|init> (par
+    défaut <verbatim|all>). Il est envisageable de remplacer la variable
+    <verbatim|init> de chaque scope par une variable <verbatim|time>, les
+    disjonctions de cas init/non init se feront alors selon la condition
+    <math|time=0> ou <math|time\<geqslant\>1>. En ne générant ni variable
+    <verbatim|time> ni variable <verbatim|init>, la disjonction n'est pas
+    faite.
+  </itemize>
+
+  <subsubsection|Domaine à disjonction par graphe de décision>
+
+  Cette analyse est implémentée dans <verbatim|abstract/abs_interp_edd.ml>.
+
+  <paragraph|Modes d'analyse>
+
+  <\itemize>
+    <item><verbatim|--ai-itv-edd> : fait une passe d'analyse statique
+    utilisant le domaine à base d'EDD et en utilisant les intervalles comme
+    domaine de valeurs numériques
+
+    <item><verbatim|--ai-rel-edd> : de même mais utilise le domaine abstrait
+    relationnel basé sur Apron (polyèdres) pour la partie numérique
+  </itemize>
+
+  <paragraph|Options de l'analyse>
+
+  <\itemize>
+    <item><verbatim|--root>
+
+    <item><verbatim|--ai-vci>, <verbatim|--ai-vvci>
+
+    <item><verbatim|--ai-wd>
+
+    <item><verbatim|--no-time>, <verbatim|--init>
+
+    <item>Non implémenté : paramètre <verbatim|--disj> pouvant intervenir sur
+    le choix des variables à considérer dans le graphe de décision
+    (actuellement toutes sont nécessairement considérées).
+  </itemize>
+
+  <subsubsection|Analyse par partitionnement dynamique>
+
+  Une troisième forme d'analyse, basée sur un partitionnement dynamique de
+  <math|S<rsup|#>> a été tentée. Celle-ci n'a pas donné de très bons
+  résultats, mais nous indiquons néanmoins son existence ici.
+  L'implémentation existe dans <verbatim|abstract/abs_interp_dynpart.ml>.
+
+  <paragraph|Modes d'analyse>
+
+  <\itemize>
+    <item><verbatim|--ai-s-itv-dp> : analyse par partitionnement dynamique,
+    utilise un domaine simple non-relationnel pour les valeurs énumérées et
+    les intervalles pour la partie numérique
+
+    <item><verbatim|--ai-edd-itv-dp> : analyse par partitionnement dynamique,
+    utilise des graphes de décision pour représenter les conditions sur les
+    énumérées et les intervalles pour la partie numérique
+
+    <item><verbatim|--ai-s-rel-dp>
+
+    <item><verbatim|--ai-edd-rel-dp>
+  </itemize>
+
+  <paragraph|Paramètres de l'analyse>
+
+  <\itemize>
+    <item><verbatim|--root>
+
+    <item><verbatim|--ai-wd>
+
+    <item><verbatim|--ai-vci>, <verbatim|--ai-vvci>
+
+    <item><verbatim|--no-time>, <verbatim|--init>
+
+    <item><verbatim|--ai-max-dp-depth> : profondeur maximale de
+    partitionnement
+
+    <item><verbatim|--ai-max-dp-width> : largeur maximale de partitionnement
+    (ie nombre maximal de parties à considérer)
+  </itemize>
 </body>
 
 <\initial>
@@ -1461,31 +1639,43 @@
     <associate|auto-13|<tuple|2.4|6>>
     <associate|auto-14|<tuple|2.4.1|6>>
     <associate|auto-15|<tuple|2.4.2|7>>
-    <associate|auto-16|<tuple|3|8>>
+    <associate|auto-16|<tuple|3|7>>
     <associate|auto-17|<tuple|4|8>>
     <associate|auto-18|<tuple|4.1|8>>
     <associate|auto-19|<tuple|4.1.1|8>>
     <associate|auto-2|<tuple|2|1>>
     <associate|auto-20|<tuple|4.1.2|9>>
-    <associate|auto-21|<tuple|4.2|10>>
+    <associate|auto-21|<tuple|4.2|9>>
     <associate|auto-22|<tuple|5|11>>
     <associate|auto-23|<tuple|5.1|11>>
     <associate|auto-24|<tuple|5.2|13>>
-    <associate|auto-25|<tuple|5.2.1|13>>
-    <associate|auto-26|<tuple|5.2.2|13>>
-    <associate|auto-27|<tuple|5.2.3|13>>
+    <associate|auto-25|<tuple|5.2.1|14>>
+    <associate|auto-26|<tuple|5.2.2|14>>
+    <associate|auto-27|<tuple|5.2.3|14>>
     <associate|auto-28|<tuple|5.2.4|15>>
-    <associate|auto-29|<tuple|5.2.5|15>>
+    <associate|auto-29|<tuple|5.2.5|16>>
     <associate|auto-3|<tuple|2.1|1>>
     <associate|auto-30|<tuple|5.2.3.3|?>>
-    <associate|auto-31|<tuple|5.2.5.2|?>>
-    <associate|auto-32|<tuple|6|?>>
+    <associate|auto-31|<tuple|5.2.5.2|16>>
+    <associate|auto-32|<tuple|6|16>>
+    <associate|auto-33|<tuple|6.1|?>>
+    <associate|auto-34|<tuple|6.2|?>>
+    <associate|auto-35|<tuple|6.3|?>>
+    <associate|auto-36|<tuple|6.3.1|?>>
+    <associate|auto-37|<tuple|6.3.1.1|?>>
+    <associate|auto-38|<tuple|6.3.1.2|?>>
+    <associate|auto-39|<tuple|6.3.2|?>>
     <associate|auto-4|<tuple|2.2|2>>
-    <associate|auto-5|<tuple|2.3|2>>
+    <associate|auto-40|<tuple|6.3.2.1|?>>
+    <associate|auto-41|<tuple|6.3.2.2|?>>
+    <associate|auto-42|<tuple|6.3.3|?>>
+    <associate|auto-43|<tuple|6.3.3.1|?>>
+    <associate|auto-44|<tuple|6.3.3.2|?>>
+    <associate|auto-5|<tuple|2.3|3>>
     <associate|auto-6|<tuple|2.3.1|3>>
     <associate|auto-7|<tuple|2.3.2|3>>
     <associate|auto-8|<tuple|2.3.3|3>>
-    <associate|auto-9|<tuple|2.3.4|3>>
+    <associate|auto-9|<tuple|2.3.4|4>>
   </collection>
 </references>
 
@@ -1584,29 +1774,40 @@
       simple <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
       <no-break><pageref|auto-23>>
 
-      <with|par-left|<quote|1.5fn>|5.2<space|2spc>Domaine à arbre de
-      disjonctions <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <with|par-left|<quote|1.5fn>|5.2<space|2spc>Domaine à graphe de
+      décision <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
       <no-break><pageref|auto-24>>
 
-      <with|par-left|<quote|6fn>|Variables et contraintes.
+      <with|par-left|<quote|3fn>|5.2.1<space|2spc>Variables et contraintes
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-25><vspace|0.15fn>>
+      <no-break><pageref|auto-25>>
 
-      <with|par-left|<quote|6fn>|Domaine numérique.
+      <with|par-left|<quote|3fn>|5.2.2<space|2spc>Domaine numérique
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-26><vspace|0.15fn>>
+      <no-break><pageref|auto-26>>
 
-      <with|par-left|<quote|6fn>|Les EDD.
+      <with|par-left|<quote|3fn>|5.2.3<space|2spc>Les EDD
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-27><vspace|0.15fn>>
+      <no-break><pageref|auto-27>>
 
-      <with|par-left|<quote|6fn>|Opérateur de widening.
+      <with|par-left|<quote|3fn>|5.2.4<space|2spc>Opérateur de widening
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-28><vspace|0.15fn>>
+      <no-break><pageref|auto-28>>
+
+      <with|par-left|<quote|3fn>|5.2.5<space|2spc><assign|paragraph-numbered|<quote|false>><assign|paragraph-prefix|<quote|<macro|<compound|the-paragraph>.>>><assign|paragraph-nr|<quote|1>><hidden|<tuple>><assign|subparagraph-nr|<quote|0>><flag|table
+      des matières|dark green|what><assign|auto-nr|<quote|30>><label|auto-30><write|toc|<with|par-left|<quote|6fn>|Itérations
+      chaotiques. <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-30><vspace|0.15fn>>><no-indent><with|math-font-series|<quote|bold>|font-series|<quote|bold>|<vspace*|0.5fn>Itérations
+      chaotiques.<space|2spc>> <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-30>>
 
       <with|par-left|<quote|6fn>|Itérations chaotiques.
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-29><vspace|0.15fn>>
+      <no-break><pageref|auto-31><vspace|0.15fn>>
+
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|6<space|2spc>Implémentation>
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-32><vspace|0.5fn>
     </associate>
   </collection>
 </auxiliary>
\ No newline at end of file