Merge branch 'master' of git.inpt.fr:tocard-inc/enseeiht/gls/projet

docs/ltl.md

@@ -0,0 +1,43 @@
+# 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.

enigme.ltl

@@ -0,0 +1,4 @@
+op finished = Echec \/ Succes;
+
+[] (finished => dead);
+[] <> finished ;