70 lines
2.3 KiB
Markdown
70 lines
2.3 KiB
Markdown
# 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.
|
|
|
|
### Propriétés LTL
|
|
|
|
- [Propriétés LTL](#propriétés-ltl)
|
|
- [Que vérifions-nous ?](#que-vérifions-nous-?)
|
|
- [Vérifier les propriétés](#vérifier-les-propriétés)
|
|
|
|
### Que vérifions-nous ?
|
|
|
|
On définit d'abord l'état finished comme l'état Succès ou l'état Echec :
|
|
|
|
```ltl
|
|
op finished = Echec \/ Succes;
|
|
```
|
|
|
|
1. L'état `finished` est bien l'état final :
|
|
|
|
```ltl
|
|
[] (finished => dead);
|
|
```
|
|
|
|
2. On arrivera toujours soit dans l'état échec, soit dans l'état succes :
|
|
|
|
```ltl
|
|
[] <> finished ;
|
|
```
|
|
|
|
### Vérifier les propriétés
|
|
|
|
Comment vérifier la terminaison du processus à partir d'un fichier `.net` et d'un fichier `.ltl`
|
|
|
|
1. Générer le fichier `.ktz` à partir de tina
|
|
|
|
```console
|
|
tina .\enigme.net .\enigme.ktz
|
|
```
|
|
|
|
2. Vérifier les propriétés à l'aide de selt
|
|
|
|
```console
|
|
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 :)
|