Rendu 1 : 2021-12-01

Xtext

Nous avons choisi de suivre une grammaire proche du JSON, simplement car de nombreux outils de formattages automatiques sont disponibles.

Le fichier enigme.game est le modèle "Enigme" de l'énoncé représenté par la grammaire Xtext citée précédemment.

UML

Le diagramme UML que l'on présente dans le fichier game.png n'est pas le diagramme généré par Xtext mais il reprend la même architecture que celle générée par le Xtext (aux quelques retards de mise a jour près).

TINA

enigme.net est une traduction manuelle du modèle "Enigme" et permet via les invariants LTL de vérifier sa finitude.

Que vérifions-nous ?

On définit d'abord l'état finished comme l'état Succès ou l'état Echec :

op finished = Echec \/ Succes;

L'état finished est bien l'état final :

[] (finished => dead);

On arrivera toujours soit dans l'état échec, soit dans l'état succes :

[] <> finished ;

Vérifier les propriétés

Comment vérifier la terminaison du processus à partir d'un fichier .net et d'un fichier .ltl

Générer le fichier .ktz à partir de tina

tina .\enigme.net .\enigme.ktz

Vérifier les propriétés à l'aide de selt

selt -p -S enigme.scn enigme.ktz -prelude .\enigme.ltl

Le fichier "enigme.scn" est généré à partir de cette commande. Je ne sais pas à quoi il sert, car il semble vide, mais il est utile.

Traduction dans le langage de programmation

Pour la traduction manuelle du modèle enigme.game vers notre code java, nous avaons 18 classe (Action.java Chemin.java Condition.java ConditionBoolean.java ConditionConnaissance.java ConditionEt.java ConditionObjet.java ConditionTest.java Connaissance.java Description.java Explorateur.java Interaction.java Jeu.java Lieu.java Objet.java Personne.java Territoire.java Transformation.java) La méthode main se trouve dans la classe Jeu

Pour compiler : javac *.java Pour lancer la partie : java Jeu

Le code n'est pas encore robuste donc il faut jouer dans les règles de l'art :)

2.3 KiB Raw Blame History