PROJETS II

1. On considère un système qui possède deux variables d'entrée booléennes e1,e1 et une variable d'état (variable usuelle) s représentant la sortie. Donnez des formules LTL qui représentent les énoncés suivants.
   1. Initialement la sortie est vraie.
   2. Quelles que soient les valeurs des entrées, au cycle suivant la sortie sera égale au ou-exclusif de ces deux valeurs.
   3. Quelles que soient les valeurs des entrées, deux cycles plus tard la sortie sera égale au ou-exclusif de ces deux valeurs.
   4. Quelles que soient les valeurs des entrées, il y a un moment plus tard où la sortie sera égale au ou-exclusif de ces deux valeurs.
   5. Quelles que soient les valeurs des entrées, il y a un moment plus tard où la sortie sera égale au ou-exclusif de ces deux valeurs et entre les deux la sortie ne changera pas de valeur.
2. Considérons un système formé de cinq variables t[1],t[2],t[3],t[4],t[5] représentant la configuration d'un automate cellulaire à une dimension. Une valeur vraie représentant une case occupée et une valeur fausse une case vide. Donnez des formules LTL qui représentent les énoncés suivants.
   1. Initialement, seule la case du milieu est occupée. On a donc la configuration OOXOO.
   2. La première case t[0] suit les règles de transformation suivantes. Attention, il est plus facile de décomposer et de tout d'abord donner une formule pour chacune des règles avant de les combiner.

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

   3. Exprimez par une formule LTL que si l'état initial correspond à la configuration OOXOO, alors on ne peut pas obtenir XXXXX.
   4. Le tableau ne reste jamais constant, c.-à-d. qu'à l'état suivant il y a toujours au moins une entrée du tableau contenant une valeur différente de celle qu'elle avait au cycle précédent.
3. Considérons un système contenant les variables suivantes : pc représentant le compteur de programme (une variable contenant le numéro de la ligne à exécuter), x représentant la variable du programme du même nom et finalement une variable retour représentant la valeur de retour du programme suivant.

       /* 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   }
   

   Exprimer par des formules LTL les énoncés suivants.
   1. Si x est inférieure ou égale à 0 au début du programme, la valeur de retour sera -x (à la fin de l'exécution du programme).
   2. La variable x ne change pas de valeur durant l'exécution du programme.
   3. La valeur suivante de pc est toujours un de plus, sauf lorsque pc est égale à 2 ou 3 (et éventuellement 5, si vous voulez).

Pour tout commentaire, vous adresser à