diff --git a/.editorconfig b/.editorconfig index 4e6b3a0..2d227d8 100644 --- a/.editorconfig +++ b/.editorconfig @@ -8,5 +8,5 @@ charset = utf-8 trim_trailing_whitespace = true insert_final_newline = true -[*.{yaml,yml,toml,html,svelte,xtext,game}] +[*.{yaml,yml,toml,html,svelte,xtext,game,md}] indent_size = 2 diff --git a/docs/choix.md b/docs/choix.md deleted file mode 100755 index 7cd4a78..0000000 --- a/docs/choix.md +++ /dev/null @@ -1,10 +0,0 @@ -# Choix d'implantations a justifier - -### Les chemins - -Les chemins sont bi-directionnels. - - -### Objets et Connaissances - -Lorsque le joueur prend un objet (ou une connaissance) en passant par un chemin ou lorsuq'il est dans un lieu, celui-ci est transféré et non dupliqué. \ No newline at end of file diff --git a/docs/rendu1.md b/docs/rendu1.md new file mode 100644 index 0000000..7dcfd6b --- /dev/null +++ b/docs/rendu1.md @@ -0,0 +1,69 @@ +# 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 :) diff --git a/docs/uml.plantuml b/docs/uml.plantuml index 0635fa1..395ba20 100755 --- a/docs/uml.plantuml +++ b/docs/uml.plantuml @@ -1,139 +1,58 @@ -@startuml jeu +@startuml game -abstract class Objet -{ +' Classes +class Jeu { + +} + +class Explorateur { - taille : int - - consomable : Condition - - transmissible : Condition } -class Connaissance -{ - - transmissible : Condition +class Territoire { + } -class Lieu -{ - - exploré : bool +class Lieux { + - nom : String - déposable : Condition + - départ : Condition + - fin : Condition } -class Jeu{} - -class Territoire{} - -class Chemin -{ +class Chemin { - ouvert : Condition - visible : Condition - obligatoire : Condition } -class Explorateur{} +class Objet { + - nom : String + - taille : int + - visible : Condition +} -class Personne -{ +class Transformation { + - condition : Condition +} + +class Connaissance { + - nom : String + - visible : Condition +} + +class Personne { + - nom : String + - visible : Condition - obligatoire : Condition } -class Depart{} - -class Fin{} - -interface Cachable -{ - - caché : Condition +class Interaction { + - visible : Condition } -class Interraction -{ - - disponible : Condition -} - -class Choix{} - -class Action -{ - - proposable : Condition - - finInterraction : Condition -} - -class Description -{ - - textes : String - - conditions : Condition -} - -class Condition{} - -class ConditionOU{} - -class ConditionET{} - -class Test{} - -class TestObjet -{ - - nombre : int - - supérieurEgale : bool -} - -class TestConnaissance{} - - ' Links -Condition "1" -down- "0..*" ConditionOU -ConditionOU "1" -down- "1..*" ConditionET -ConditionET "1" -down- "1..*" Test - -Test <|-down- TestConnaissance -Test <|-down- TestObjet - -TestConnaissance "0..1" -up- "1" Connaissance -TestObjet "0..1" -up- "1" Objet - -Cachable <|-down- Connaissance -Cachable <|-down- Objet -Cachable <|-down- Personne - -Depart -up-|> Lieu -Fin -up-|> Lieu - -Jeu "1" *-- "1" Explorateur -Jeu "1" *-- "1" Territoire - -Territoire "1" *-- "1" Depart -Territoire "1" *-- "1" Fin -Territoire "1" *-- "1..*" Lieu -Territoire "1" *-- "0..*" Chemin - -Lieu "1" -- "0..*" Chemin -Lieu "1" -- "0..*" Chemin -Lieu "1" -- "0..*" Connaissance -Lieu "0..1" -- "0..*" Objet -Lieu "1" -- "0..*" Personne -Lieu "1" -- "1" Description - -Chemin "0..1" -left- "0..*" Connaissance : transmettre - -Chemin "0..1" -- "0..*" Objet : transmettre -Chemin "0..1" -- "0..*" Objet : consommer -Chemin "1" -- "1" Description - Explorateur "0..1" -- "0..*" Connaissance Explorateur "0..1" -- "0..*" Objet -Explorateur "0..1" -- "1" Lieu - -Personne "1" -- "1.." Interraction - -Objet "1" -- "1" Description - -Connaissance "1" -- "1" Description - -Interraction "0..1" -- "0..*" Objet -Interraction "0..1" -- "0..*" Connaissance -Interraction "1" -- "1" Choix - -Choix "1" -- "1..*" Action @enduml \ No newline at end of file diff --git a/test.game b/test.game deleted file mode 100644 index 7e9429f..0000000 --- a/test.game +++ /dev/null @@ -1,154 +0,0 @@ -{ - "Explorateur": { - "taille": 3, - "connaissances": [], - "objets": [ - "tentative", - "tentative", - "tentative" - ] - }, - "Territoire": { - "Lieux": [ - { - "nom": "Énigme", - "descriptions": [ - { - "nom": "lieu de départ", - "condition": "(true)" - } - ], - "deposable": "(false)", - "depart": "(true)", - "fin": "(false)", - "connaissances": [], - "personnes": [ - "Sphinx" - ], - "objets": [] - }, - { - "nom": "Succès", - "description": [ - { - "nom": "lieu succès", - "condition": "(true)" - } - ], - "deposable": "(false)", - "depart": "(false)", - "fin": "(true)", - "connaissances": [], - "personnes": [], - "objets": [] - }, - { - "nom": "Échec", - "description": [ - { - "nom": "lieu échec", - "condition": "(true)" - } - ], - "deposable": "(false)", - "depart": "(false)", - "fin": "(true)", - "connaissances": [], - "personnes": [], - "objets": [] - } - ], - "Chemins": [ - { - "lieu_in": "Énigme", - "lieu_out": "Succès", - "ouvert": "(true)", - "visible": "(Réussite==1)", - "obligatoire": "(false)", - "connaissances_gift": [], - "objets_gift": [], - "objets_conso": [], - "descriptions": [ - { - "texte": "Le chemin de la victoire !", - "condition": "(true)" - } - ] - }, - { - "lieu_in": "Énigme", - "lieu_out": "Échec", - "ouvert": "(true)", - "visible": "(tentatives==0)", - "obligatoire": "(false)", - "connaissances": [], - "objets_recus": [], - "objets_conso": [], - "descriptions": [ - { - "texte": "Le chemin de la loose !", - "condition": "(true)" - } - ] - } - ] - }, - "Objets": [ - { - "nom": "tentative", - "taille": 1, - "visible": "(true)", - "descriptions": [ - { - "texte": "permet répondre une question du sphinx", - "condition": "(true)" - } - ] - } - ], - "Connaissances": [ - { - "nom": "Réussite", - "visible": "(true)", - "descriptions": [ - { - "nom": "Permet de se casser de là", - "condition": "(true)" - } - ] - } - ], - "Personnes": [ - { - "nom": "Sphinx", - "visible": "(true)", - "obligatoire": "(true)", - "interactions": [ - { - "visible": "(true)", - "connaissances": [], - "objets_recus": [], - "actions": [ - { - "visible": "(true)", - "connaissances": [ - "Réussite" - ], - "objets_gift": [], - "objets_conso": [] - }, - { - "visible": "(true)", - "connaissances": [], - "objets_recus": [], - "objets_conso": [ - "tentative" - ] - } - ] - } - ] - } - ], - "Transformations": [] -} diff --git a/workspace/game/bin/xtext/Game.xtext b/workspace/game/bin/xtext/Game.xtext index bc9269a..1b89c8c 100644 --- a/workspace/game/bin/xtext/Game.xtext +++ b/workspace/game/bin/xtext/Game.xtext @@ -103,7 +103,7 @@ Interaction: Action: '{' - '"Description"' ':' '[' descriptions+=Description (descriptions+=Description)* ']' ',' + '"Description"' ':' '[' descriptions+=Description (descriptions+=Description)* ']' ',' '"visible"' ':' visible=Condition ',' '"connaissances"' ':' '[' (connaissances+=Nom (connaissances+=Nom)*)? ']' ',' '"objets_recus"' ':' '[' (objetsRecus+=Nom (objetsRecus+=Nom)*)? ']' ',' diff --git a/workspace/game/src/xtext/Game.xtext b/workspace/game/src/xtext/Game.xtext index bc9269a..1b89c8c 100644 --- a/workspace/game/src/xtext/Game.xtext +++ b/workspace/game/src/xtext/Game.xtext @@ -103,7 +103,7 @@ Interaction: Action: '{' - '"Description"' ':' '[' descriptions+=Description (descriptions+=Description)* ']' ',' + '"Description"' ':' '[' descriptions+=Description (descriptions+=Description)* ']' ',' '"visible"' ':' visible=Condition ',' '"connaissances"' ':' '[' (connaissances+=Nom (connaissances+=Nom)*)? ']' ',' '"objets_recus"' ':' '[' (objetsRecus+=Nom (objetsRecus+=Nom)*)? ']' ','