projet-genie-logiciel-systeme/docs/rapport.md

Rapport de projet d'ingénieurie dirigée par les modèles

Xtext

Nous avons choisi de suivre une grammaire proche du YAML, puisque cela nous offre une grammaire simple et formatable par de nombreux outils.

Le fichier enigme.game est le modèle Enigme de l'énoncé représenté par la grammaire Xtext citée précédemment. Nous avons de même créé de nombreux autres modèles pour tester nos transformations.

TINA

Pour nous permettre de vérifier la terminaison de notre jeu, nous devons dans un premier temps créer une transformaion de notre métamodèle Game vers le métamodèle Petrinet vu dans le mini-projet.

A l'aide d'ATL, nous avons réalisé cette transformation modèle a modèle de la manière suivante :

• Les lieux et les personnes sont réprésentés par des places.
• Les chemins, les interractions et les places sont représentés par des transitions.
• Le joueur est représenté par une place taille qui est la taille de sont inventaire.
• Les objets et connaissances possédés par l'explorateur sont représentés par deux places : Une place qui indique le nombre et une place qui indique la quantité maximum que peut avoir l'explorateur moins son nombre actuel.
• Les objets consommés/reçus et les connaissance données par une interaction/action/chemin sont des arcs qui relie les objets/connaissances et objet_neg/connaissance_neg.
• Les conditions sont exprimé sous forme de read arc attaché à un transition tel que pour chaque ConditionOu, on duplique la transition concernée. En fonction du type de condition on a :
  • Les testes égalité du nombre d'objet : un read arc de l'objet avec un read arc de l'objet_neg avec des poids de n et n_{max} - n.
  • Les testes de supériorité strict du nombre d'objet : un read arc de l'objet avec un poids de n+1
  • ...

Schema illustrant une transformation d'un chemin

Propriétés LTL

Les propritétés LTL s'appliquent sur le modèle de réseau de pétri precedemment généré, et nous permettent de vérifier certaines propriétés, telle que la terminaison de notre jeu.

On définit d'abord l'état finished comme la réunion de toutes les places correspondant à des lieux où fin=true, dans le cas de notre exemple Enigme, on a alors:

op finished = lieu_Echec \/ lieu_Succes;

On vérifie alors qu'il existe un état de notre jeu tel que finished soit vrai.

[] <> finished ;

Vérifier les propriétés

Pour générer ces propriétés automatiquement à partir d'un modèle Game, nous utilison acceleo. Ensuite pour obtenir le rapport de terminaison, nous executons els commandes suivantes:

tina enigme.net enigme.ktz
selt -p -S enigme.scn enigme.ktz -prelude enigme.ltl

Traduction dans le langage de programmation

Pour tester le fun de notre jeu, nous pouvons le transformer en un prototype Java textuel. Ainsi, nous avons créé les 18 classes: 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 et Transformation.java correspondants aux classes de notre métamodèle Game. Lors de la transformation nous crééons Prototype.java instanciant tous les objets du modèle Game via leurs classes java correpondantes. Ensuite nous appelons simplement Jeu.jouer qui vient s'occuper d'executer la partie via l'état des différents objets.

Pour compiler :

javac *.java

Pour lancer la partie:

java Prototype

Pour la génération d'un modèle à texte, nous gardons cette structure. En effet, d'un modèle a l'autre, seul l'architecture initiale évolue donc les classes qui permettent le dérulement du jeu n'évolue pas en fonction du modèle. C'est donc le fichier NomDuJeu.java qui va dépendre du modèle.

Dans cette classe, qui fait appèle aux autres, nous allons initialiser le jeu en générant les objets correspondant au modèle. La transcription du modèle est donc uniquement présente dans ce petit bout du code.

Ainsi, nous avons une séparation entre le texte généré depuis le modèle et le code exécutant le jeu. On peut donc facilement modifier l'un sans modifier l'autre. Changer la facon dont est exécuté le code n'affectera pas la fçon dont on doit générer le code lié au modèle et vis versa.