rapport.txt

Exercice 2:

Utilisation de 4 automates différents :
	Utilisateur : typiquement le conducteur de la voiture, avec deux possibilités, celle de freiner et de ne pas freiner.
	Electrovannes : un automate qui comprend toutes les electrovannes et permettant de savoir combien sont ouvertes
	Roue : automate représentant la roue, son blocage non déterministe en fonction du freinage, ainsi que son déblocage
			éventuel en fonction du nombre d'électrovannes ouvertes puis son retour à un état normal d'utilisation après
			arrêt du freinage.
	ABS : représente le système ABS qui s'active dès que la roue est bloquée puis décide de fermer les électrovannes ou de
			les ouvrir indépendemment les unes des autres.
			
T0D0: commenter les automates

3) Ajout d'un automate observateur (ObservateurQ3) avec deux transitions, une pour le blocage de la roue après 20s et une autre pour 30s
   pour vérifier : E<> ObservateurQ3.Block20s
			E<> ObservateurQ3.Block30s

4) On ne peut pas calculer directement cette valeur mais il est possible de l'estimer. Il suffit de faire un automate
   avec deux transition, une qui rentre dans un état quand la roue est bloquée et une autre qui en sort quand elle
   est débloquée. Un rajoute un timer sur l'état central et on vérifie sa valeur en la bornant. (ObservateurQ4)
   Le mieux serait de générer la trace la plus longue avec passage sur l'état où la roue se débloque mais cela ne semble
   pas possible avec UppAal.

5)