Read Me

Contenu de l'archive:
--------------------
AHAH!
--------------------


- fichiers 'var_module.tla' et 'run_module.tla':
  pour la vérification de la correction d'un module

- fichiers 'var_raffinement.tla' et 'run_raffinement.tla'
  pour la vérification du raffinement entre deux modules

- répertoire 'tree':
  - fichier 'tree.tla':
    module contenant les opérations 'create' et 'get' permettant
    de créer des arbres et de parcourir leurs branches
  - fichier 'run_tree.tla':
    module principal pour lancer la vérification du module tree
  - fichier 'run_tree.cfg':
    fichier de configuration contenant les paramètres instanciés 
    du module tree, notamment l'ensemble des noeuds NODES et 
    le nombre maximal de fils de chaque noeud WIDTH
  - autres liens symboliques vers des fichiers définis ailleurs

- répertoire 'graph':
  - fichier 'graph.tla':
    module introduisant l'opération supplémentaire 'set' permettant 
    la création de graphes
  - fichiers 'run_graph.tla' et 'run_graph.cfg'
    pour vérifier la correction du module 'graph'
  - fichiers 'run_raffinement.tla' et 'run_raffinement.cfg'
    pour vérifier le raffinement du module 'tree' par le module 'graph'

- répertoire 'memory':
  - fichier 'memory.tla':
    module raffinant les opérations 'create' et 'get' à l'aide d'une 
    représentation mémoire classique (à base de pointeurs)
  - fichiers 'run_memory.tla' et 'run_memory.cfg'
    pour vérifier la correction du module 'memory'
  - fichiers 'run_raffinement.tla' et 'run_raffinement.cfg'
    pour vérifier le raffinement du module 'tree' par le module 'memory'

Travail à effectuer:
-------------------

- améliorer éventuellement les invariants des modules donnés. Attention, 
  les temps de calcul augmentent considérablement suivant le nombre et 
  la complexité des propriétés à vérifier

- définir un raffinement du module 'memory' afin de prendre en compte 
  les graphes (en définissant l'opération 'set')

- proposer des raffinements (au moins un) permettant d'autres représentations
  plus compactes/efficaces des arbres, puis des graphes

Conseils:
--------

- couramment un graphe est défini comme un arbre + une relation d'équivalence 
  entre noeuds. Cette relation permet d'associer à chaque noeud le noeud 
  vers lequel il 'pointe', i.e. son représentant dans sa classe d'équivalence, 
  ce qui permet de définir des graphes arbitraires, un noeud pouvant pointer 
  sur n'importe quel autre noeud

- les valeurs actuelles des paramètres utilisés pour la vérification des 
  modules (correction ou raffinement) sont parfois trop grands pour les 
  capacités de votre machine (ou votre patience). Par exemple, la correction 
  du module 'graphe' nécessite le parcours de près de 300 millions d'états, 
  ce qui peut nécessiter typiquement 10h de calculs (ou plus, suivant votre 
  machine) et 1Go de mémoire...

- ne restez pas bloqué, et n'hésitez pas à me poser des questions. 
  Par contre, si vous voulez des réponses, il me faut un diagnostic précis
  et compréhensible...

IMPORTANT: Changement dans le raffinement:
-----------------------------------------

- pour des raisons d'efficacité, le raffinement a du être (un peu) modifié.

- ainsi, le prédicat de liaison: 'Liaison(etatA, etatC)'
  devient une fonction de liaison: 'Liaison(etatC)' qui à tout etat concret
  donne l'ensemble des états abstraits lui correspondant.

- Par conséquent, les définitions ETATA et ETATC (permettant une forme de 
  typage des modules) ne sont plus nécessaires dans la définition du 
  raffinement.

- on peut retrouver l'ancienne forme où on avait:
  'etatA \in ETATA' en invariant abstrait
  'etatC \in ETATC' en invariant concret
  'Liaison(etatA,etatC) == def' en prédicat de liaison

  en définissant à la place:
  'Liaison(etatC) == { etatA \in ETATA : def }'

  dans cette forme, il faut d'abord calculer ETATA (énorme ensemble), pour 
  ne garder que les valeurs satisfaisant 'def'
 
- l'avantage de la nouvelle forme est que l'on peut beaucoup mieux préciser 
  les états abstraits valides, ce qui évite des calculs:
  par exemple, pour le raffinement entre les arbres et les graphes, 
  au lieu de la solution attendue:
        Liaison(etatA, etatC) == etatA = etatC
  (i.e. un graphe construit sans utiliser l'opération 'set' est un arbre)
  avec etatA\in ETATA en invariant (i.e. etatA est un arbre)
  ce qui correspondrait dans le nouveau codage à:
        Liaison(etatC) == { etatA\in ETATA : etatC = etatA }

  on peut directement écrire:
        Liaison(etatC) == { etatC }
  (i.e. etatA est une valeur à choisir dans ce singleton)