PROJETS I

1. Modélisez une porte logique ayant deux entrées et comme sortie le maximum (donc le ou logique) des deux entrées. Ajoutez et faites vérifier les propriétés suivantes.
   1. Si à un moment quelconque l'une des entrées est vraie, au cycle suivant la sortie sera aussi vraie.
   2. Si à un moment quelconque les deux entrées sont fausses, au cycle suivant la sortie sera aussi fausse.
2. Refaites la même modélisation, mais cette fois avec deux entrées entières et une sortie qui est le maximum des deux entrées. Ajouter et faire vérifier les propriétés suivantes.
   1. Si à un moment quelconque la première entrée est plus grande ou égale à l'autre, au cycle suivant la sortie sera égale à la valeur que cette première entrée avait au cycle précédent.
   2. Même propriété, mais avec l'autre entrée.
3. Nous allons maintenant modéliser un système dynamique des plus simples, soit un automate cellulaire de dimension 1. Il s'agit d'une suite de cinq positions, chacune pouvant être soit occupée (représenté par un X) soit vide (représenté par un O). À chaque étape une nouvelle valeur pour une case C est calculée à partir des valeurs des trois cases suivantes : celle qui précède C (dénotée P), C elle-même et finalement celle qui suit C (dénotée S). Les transformations se font simultanément sur toutes les cases.
   • On calcule donc simultanément les nouvelles valeurs des cases à partir des valeurs anciennes selon les règles suivantes (exemple tiré de Wikipedia).
     • Initialement, seule la case du milieu est occupée. On a donc la configuration OOXOO.
     • La règle de transformation utilisée à chaque étape est donnée par le tableau suivant.

       anciennes valeurs de PCS	XXX	XXO	XOX	XOO	OXX	OXO	OOX	OOO
       nouvelle valeur de C	O	O	O	X	X	X	X	O

   • Exprimez et vérifier les propriétés suivantes à l'aide de l'outil.
     1. Peut-on obtenir XXXXX ?
     2. Peut-on obtenir XOXOX ?
     3. Peut-on ne jamais obtenir XOXOX ? Comment peut-on utiliser la réponse à cette question pour trouver une trace permettant d'obtenir ce motif ?
4. Modéliser l'exécution du code C suivant à l'aide de l'outil.

       /* va(x) retourne la valeur absolue de x.*/
   1   int va(int x){
   2     if (x<0)
   3       return -x;
   4     else
   5       return x;
   6   }
   

   • Il est nécessaire de définir dans le modèle une variable contenant le numéro de la ligne en cours d'exécution (program counter).
   • Dans le modèle, une valeur quelconque doit être affectée à la variable x à l'initialisation et si l'on veut à chaque retour (ceci permettra d'enchaîner plusieurs exécutions). La variable x doit néanmoins rester constante durant l'exécution de la fonction pour qu'on puisse y faire référence.
   • Exprimez et vérifier les propriétés suivantes à l'aide de l'outil.
     1. Vérifier que si x est inférieure ou égale à 0, la valeur de retour sera -x.
     2. Vérifier que si x est supérieure à 0, la valeur de retour sera x.

Pour tout commentaire, vous adresser à