Guide de survie avec CADP

CADP est un boîte à outils pour la spécification et la vérification formelle de systèmes finis concurrents. Pour avoir plus d'informations, visitez le site web de l'outil qui est très bien documenté!

Installation

CADP est installé sur les machines miniMac de la salle E et sur le serveur floreal.

Pour l'utiliser, il faut configurer les variables d'environnement suivantes:

la variable $CADP doit être affectée au répertoire d'installation de CADP qui est /usr/local/cadp. Par exemple sous bash:
```
export CADP=/usr/local/cadp
```
la variable $CADP_CC doit être affectée au compilateur de C utilisé. Sous floreal, il faut utiliser GCC version 4.0. Par exemple sous bash:
```
export CADP_CC=/usr/bin/gcc-4.0
```
la variable $CADP_ARCH doit être affectée à l'architecture de la machine qui est mac86 pour floreal. Par exemple sous bash:
```
export CADP_ARCH=mac86
```
la variable $PATH doit include les être affectée aux répertoires contenant les binaires de CADP. Par exemple sous bash:
```
export PATH=$PATH:$CADP/com:$CADP/bin.$CADP_ARCH
```

Pour avoir ces variables à chaque connexion, utiliser le fichier de configuration de votre shell qui, pour bash est $HOME/.bashrc, et inclure les lignes suivantes:

CADP=/usr/local/cadp
CADP_CC=/usr/bin/gcc-4.0
CADP_ARCH=mac86 
PATH=$PATH:$CADP/com:$CADP/bin.$CADP_ARCH
export CADP CADP_CC CADP_ARCH PATH

Pour lire les commande du fichier $HOME/.bashrc après sa modification, faire:

bash> source  $HOME/.bashrc

Utilisation de CAESAR.ADT

Pour la compilation des types abstraits de donnés écrits en ACT ONE, il faut suivre les pas suivants:

Utiliser un fichier LOTOS pour générique qui inclut les spécifications des types abstraits écrits dans des fichiers séparés. Ce fichier nomée spec.lotos contient le code suivant:
```
specification TDA : noexit
   (* import of the data type definitions *)
   library
      TDA1, ..., TDAn
   endlib
behaviour
  stop
endspec
```
où TDA1.lib,..., TDAn.lib sont les fichiers contenant les spécifications des types abstraits à compiler.
Spécifier les TDA dans des fichiers avec l'extension .lib. Par rapport à la syntaxe utilisée en cours, il faut faire les changements suivants:
- commenter les mots clés suivants: imports et extends,
- introduire des commentaires spéciaux pour indiquer les constructeurs du TDA ainsi:
```
type LIST 
   ...
  opns
    nil  (*! constructor *) : -> list
    cons (*! constructor *) : elem, list -> list
  ...
endtype
```
  Les autres opérations (inspecteur, observateur) n'ont pas besoin d'être annotées.
Appeler caesar.adt sur le fichier spec.lotos dans le répertoire qui contient la spécification ainsi:
```
bash> caesar.adt -indent spec.lotos
```

Des exemples de spécifications de TDA se trouvent dans le répertoire $CADP/lib.

Utilisation de SVL

A VENIR...