From bebab48e94ad156341f12fe90224e67e98477ca8 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Wed, 16 Jul 2014 15:50:02 +0200 Subject: More doc : command lien options; --- readme.pdf | Bin 221365 -> 236320 bytes readme.tm | 245 +++++++++++++++++++++++++++++++++++++++++++++++++++++++------ 2 files changed, 223 insertions(+), 22 deletions(-) diff --git a/readme.pdf b/readme.pdf index c97712f..4a97029 100644 Binary files a/readme.pdf and b/readme.pdf differ diff --git a/readme.tm b/readme.tm index c7a0b2f..0d6388c 100644 --- a/readme.tm +++ b/readme.tm @@ -1443,7 +1443,185 @@ - \; + Le projet scade-analyzer propose une implémentation simple des composants + suivants : + + <\itemize> + parser, lexer, typeur pour notre sous-ensemble de SCADE (source des + fichiers dans ) + + interprète pour la sémantique cocnrète + () + + implémentation de la transformation d'un programme en formule + logique ; quelques simplifications sur les formules logiques + (, ). + + domaine numérique non-relationnel basé sur les intervalles ; + domaine relationnel basé sur la bibliothèque externe Apron + (, , + , ...) + + deux domaines abstraits et analyseur statique correspondant + (, ) + + + En nous basant sur les options de la ligne de commande, nous allons + maintenant décrire les différentes fonctionnalités. + + + + <\itemize> + : parse un fichier SCADE et le ré-affiche en + sortie + + : 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 + . + + + + + <\itemize> + : execute le programme SCADE donné en argument, + avec l'interprète basé sur la + sémantique à réduction. Le programme doit satisfaire la spécification + suivante : avoir un noeud qui servira de racine, ce noeud + devant prendre une unique entrée, , qui est un compteur + incrémenté à chaque cycle, et renvoyant trois entiers, , + et (qui seront affichés en sortie), ainsi qu'un + booleen qui indiquera que l'interprète doit terminer. Cf + fichiers dans pour des exemples. + + : pareil mais affiche plus de détails (tout le + contenu de la mémoire est affiché à chaque cycle). + + + + + + + Cette analyse est implémentée dans . + + + + <\itemize> + : 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 + + : de même mais utilise le domaine abstrait + relationnel basé sur Apron (polyèdres) pour la partie numérique + + + + + <\itemize> + noeud\> : spécifie le noeud racine + dont on veut faire l'analyse (par défaut : ) + + : affiche des détails sur le contenu de + l'accumulateur à chaque itération + + : affiche encore plus de détails + + n\> : définit un délai pour les + opérations de widening (par défaut 5) + + vars\> : variables à utiliser comme + variables de disjonction (par défaut : aucune) + + scopes\> : donne un certain + nombre de scopes pour lesquels ne pas introduire de variable + (par défaut , c'est-à-dire que + n'est jamais introduite). Lorsqu'une variable + est introduite, on génère les équations qui font en sorte + que soit égal au numéro du cycle depuis le début de + l'exécution du programme. + + scopes\> : donne un certain nombre + de scopes pour lesquels introduire une variable (par + défaut ). Il est envisageable de remplacer la variable + de chaque scope par une variable , les + disjonctions de cas init/non init se feront alors selon la condition + ou 1>. En ne générant ni variable + ni variable , la disjonction n'est pas + faite. + + + + + Cette analyse est implémentée dans . + + + + <\itemize> + : fait une passe d'analyse statique + utilisant le domaine à base d'EDD et en utilisant les intervalles comme + domaine de valeurs numériques + + : de même mais utilise le domaine abstrait + relationnel basé sur Apron (polyèdres) pour la partie numérique + + + + + <\itemize> + + + , + + + + , + + Non implémenté : paramètre pouvant intervenir sur + le choix des variables à considérer dans le graphe de décision + (actuellement toutes sont nécessairement considérées). + + + + + Une troisième forme d'analyse, basée sur un partitionnement dynamique de + > 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 . + + + + <\itemize> + : analyse par partitionnement dynamique, + utilise un domaine simple non-relationnel pour les valeurs énumérées et + les intervalles pour la partie numérique + + : 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 + + + + + + + + + <\itemize> + + + + + , + + , + + : profondeur maximale de + partitionnement + + : largeur maximale de partitionnement + (ie nombre maximal de parties à considérer) + <\initial> @@ -1461,31 +1639,43 @@ > > > - > + > > > > > > - > + > > > > - > - > - > + > + > + > > - > + > > > - > - > + > + > + > + > + > + > + > + > + > > - > + > + > + > + > + > + > > > > - > + > @@ -1584,29 +1774,40 @@ simple |.>>>>|> > - |5.2Domaine à arbre de - disjonctions |.>>>>|> + |5.2Domaine à graphe de + décision |.>>>>|> > - |Variables et contraintes. + |5.2.1Variables et contraintes |.>>>>|> - > + > - |Domaine numérique. + |5.2.2Domaine numérique |.>>>>|> - > + > - |Les EDD. + |5.2.3Les EDD |.>>>>|> - > + > - |Opérateur de widening. + |5.2.4Opérateur de widening |.>>>>|> - > + > + + |5.2.5>.>>>>>>>|Itérations + chaotiques. |.>>>>|> + >>|font-series||Itérations + chaotiques.> |.>>>>|> + > |Itérations chaotiques. |.>>>>|> - > + > + + |math-font-series||6Implémentation> + |.>>>>|> + \ No newline at end of file -- cgit v1.2.3