M2 Info Paris 7
Modélisation - Examen 2020-2021
Éléments de corrections (non officiels)

[Partie Spécification]

== Exercice 1 ==
=== Question 1 ===

Remarque : Cet exercice ressemble beaucoup à l'exercice 3 du partiel, certaines réponses sont presque des copier/coller

1) aUb
Faux
Traduction de la formule LTL : Dans toutes les exécutions, on va avoir un jour B, et jusque-là on a toujours des A
Justification : Faux car il existe une exécution dans laquelle on n'a jamais B : q0-q3- q0-q3- q0-q3-... 

2) aWb
Vrai
Rappel : aWb est une abréviation pour "aUb ∨ Ga"
Traduction de la formule LTL : Dans toutes les exécutions, soit on va avoir un jour B et jusque-là toujours des A, soit toujours A
Justification : Vrai car aUb est vrai dans toutes les exécutions sauf celle où on reste toujours sur q0 et q3, dans laquelle Ga est vrai

3) G(a ⇒ X(a∨b))
Vrai
Traduction de la formule LTL : Dans toutes les exécutions, chaque fois qu'on a un A, on a forcément A ou B le lendemain
Justification :
	Les états qui portent un A sont q0, q3 et q4, on doit donc vérifier la seconde partie de la formule pour ces états
	Depuis q0, on lit forcément un A le lendemain (on va en q3)
	Depuis q3, on lit forcément un A le lendemain (on va en q0 ou en q4)
	Depuis q4, on lit forcément un B le lendemain (on va en q2)
	C'est donc Vrai : chaque fois qu'on a un A, on a bien un A ou un B le lendemain
	
4) (GFb) ⇒ (GFc)
Faux
Traduction de la formule LTL : Toutes les exécutions qui ont une infinité de B ont aussi une infinité de C
Justification : Faux car les exécutions qui bouclent à l'infini entre q4 et q1 ont bien une infinité de B, mais pas une infinité de C
Remarque : Quand on a une infinité de B, on est même certain de ne pas avoir une infinité de C, et inversement.

5) (¬GFa) ⇒ (FGc)
Vrai
Traduction de la formule LTL : Dans toutes les exécutions qui ont un nombre fini de A, on a forcément toujours C à partir d'un certain jour
Justification : Vrai car si on a un nombre fini de A, c'est forcément qu'on est parti un jour boucler en q2, et à partir de ce jour, on a toujours C
Justification + développée :
	On peut diviser les exécutions en 3 types :
		(1) Celle qui reste boucler à l'infini entre q0 et q3 (il n'y en a qu'une seule : q0-q3- q0-q3- q0-q3-... )
		(2) Celles qui vont boucler à l'infini entre q4 et q1 (il y en a une infinité, car on peut d'abord boucler très longtemps entre q0 et q3)
		(3) Celles qui vont boucler à l'infini en q2 (il y en a une infinité, car on peut d'abord boucler très longtemps entre q0 et q3, et entre q4 et q1)
		Dans le cas (1) et les cas (2), on lit un nombre infini de A ("(¬GFa)" est Faux) ce qui valide d'office l'implication sans qu'on ait besoin de regarder la seconde partie
		Dans les cas (3), on lit un nombre fini de A ("(¬GFa)" est Vrai), mais seconde partie de l'implication est Vraie aussi, puisqu'il y a bien un jour où on lira toujours C (le jour où on arrivera en q2)


=== Question 2 ===

Remarque :
	L'énoncé demande la valeur de chaque sous-formule pour chaque état, mais il y a peut-être une erreur, car ça ferait environ 50 réponses à donner (5 états * 5 formules * environ 2 sous-formules dans chaque formule).
	Ce qui serait cher payé pour une question à 2 points.
	Ou peut-être qu'aucune justification n'était attendue, mais juste un grand tableau de 5 colonnes et d'environ 10 lignes, à remplir avec des V/F.
	Ici, on va plutôt donner la réponse pour chaque formule à l'état initial q0, en justifiant brièvement.

1) EaUb
Vrai
Traduction de la formule LTL : Il existe une exécution, dans laquelle on aura B un jour, et jusque-là toujours des A
Justification :
	Vrai, cette exécution existe.
	Par exemple, toute exécution qui commence par : q0-q3-q4-q1-....
Remarque : Cette exécution est respectée par toutes les exécutions qui passent un jour par q1, et seulement par ces exécutions

2) AG(EaUb)
Faux
Traduction de la formule LTL : Dans tous les états, il existera un chemin qui mène vers B, avec toujours des A jusque-là
Justification : Faux, car dès qu'on arrive en q2 on n'a plus de chemin qui mène vers un B ("EaUb" devient Faux)
Remarque :
	"AG" veut dire "dans toutes les exécutions, toujours", mais ici je traduits par "Dans tous les états" pour simplifier la phrase.
	Si ce qui suit "AG" doit être vrai dans toujours et dans toutes les exécutions, ça revient à dire qu'il doit être vrai dans tous les états accessible depuis l'état initial.
	Evidemment cette interprétation ne fonctionne que pour le premier "AG" de la formule.

3) AG(b ⇒ EXc)
Vrai
Traduction de la formule LTL : Dans tous les états, si on a un B, alors il existe un chemin qui mène vers un A le lendemain
Justification : Vrai, car le seul état qui porte un B est q1, et depuis q1 il existe bien un chemin qui mène vers un C le lendemain (transition vers q2)

4) AG(c ⇒ AGc)
Vrai
Traduction de la formule LTL : Dans tous les états, si on a un C, alors à partir de là, on aura forcément toujours C
Justification : Vrai, car le seul état qui porte un C est q2, et depuis q2 il est vrai qu'on aura forcément toujours C.

5) AG(b ⇒ AXc)
Faux
Traduction de la formule LTL : Dans tous les états, si on a un B, alors on aura forcément C le lendemain
Justification : Faux, car dans q1 on a B, mais on n'a pas forcément C le lendemain (on peut aussi aller en q4)


== Exercice 2 ==

1) (Fa ∧ Fb) ⇒ Fc

2) G(b ⇒ X¬a)
Autre solution, si les "^-1" sont autorisés : G(a ⇒ (X^-1 b))

3) (GFa) ⇒ (¬GFb)

4) Il y avait plusieurs façons d'interpréter cette phrases, et donc plusieurs réponses possibles, probablement toutes acceptées.
Voici 2 interprétations possibles :
* G(a => bUc) si on suppose que le C peut arriver le jour même, et que dans le cas contraire, le B est obligatoire le jour même.
* G(a => X(bUc)) si on suppose que le C doit arriver à partir du lendemain (s'il y a un C le jour même, il ne compte pas) et que le B n'est obligatoire qu'à partir du lendemain.


== Exercice 3 ==

=== S1 et S2 ===
* En CTL
Ils ne sont pas bissimilaires, car dans S2, il existe un chemin (de r0 à r3) qui va lire un B le lendemain et qui ne pourra lire que un A le jour suivant.
Ce chemin n'existe pas dans S1.
Donc on peut distinguer S1 et S2 avec la formule CTL suivante (qui est fausse pour S1 et vraie pour S2) : EX(b ∧ (AXa))

* En LTL (non demandé dans cet examen)
On ne peut pas distinguer S1 et S2, car ils lisent exactement les mêmes mots : (_ b b^* a)^w + [(_ b b^* a)^* _ b^w]
Explication :
	(_ b b^* a)^w = le cas où on tourne à l'infini (dans un triangle)
	(_ b b^* a)^* _ b^w = le cas où on va un jour rester et boucler à l'infini en q1 (ou r1)

=== S1 et S3 ===
* En CTL
Dans S3, les état 1 et 3 sont clairement identiques, car ils portent tous les deux un B, et peuvent tous les deux au choix, rester sur eux-même (rester sur l'ensemble d'état [1,3]) ou aller dans l'état 2.
Donc, dans S3 on peut fusionner les états 1 et 3 sans changer le comportement du STE, ce qui donnerait le STE S1.
Ils sont donc bissimilaires (= aucune formule CTL ne peut les distinguer).
On peut les relier avec la bissimulation suivantes (les états entre les mêmes parenthèses sont équivalents) : {(q0,s0), (q1,s1,s3), (q2,s2)}

* En LTL (non demandé dans cet examen)
Si les STE ne sont pas distinguables en CTL, ils ne sont pas non plus distinguables en LTL.

=== S2 et S3 ===
* En CTL
Comme on l'a vu plus haut, S1 et S2 sont distinguables, mais S1 et S3 sont équivalents. 
Donc S2 peut se distinguer de S3 de la même façon que de S1.
Donc on peut distinguer S2 et S3 avec la formule CTL suivante (qui est fausse pour S3 et vraie pour S2) : EX(b ∧ (AXa))

* En LTL (non demandé dans cet examen)
Comme pour S1 et S2 : on ne peut pas distinguer S2 et S3, car ils lisent exactement les mêmes mots : (_ b b^* a)^w + [(_ b b^* a)^* _ b^w]

=== S4 vs Le reste du Monde ===
* En CTL
S4 est très différent des 3 autres STE, il est par exemple le seul à pouvoir lire un B juste après un A (les autres sont obligés de repasser par l'état vide après un A).
Par exemple, il est le seul à pouvoir lire des mots commençants par "_bab".
On peut donc distinguer S4 de tous les autres en CTL avec la formule suivante (qui est vraie pour S4 et fausse pour tous les autres) : EX(b ∧ EX(a ∧ EXb))

* En LTL (non demandé dans cet examen)
Comme ils ne lisent pas les mêmes mots, S4 est facile à distinguer des autres en LTL.
Par exemple avec la formule LTL suivante (fausse pour S4 et vraie pour tous les autres) : G(a ⇒ X¬b)
("quand on lit un A, on ne peut pas lire de B le lendemain")