From 512a04eb541fe696871b23e669f124b8e1dacb26 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?S=C3=A9bastien=20PONT?= <seba12.04@orange.fr>
Date: Wed, 1 Dec 2021 10:15:44 +0100
Subject: [PATCH 1/2] feat: :sparkles: add ltl property for enigme.net

---
 enigme.ktz | Bin 0 -> 303 bytes
 enigme.ltl |   4 ++++
 enigme.scn |   0
 3 files changed, 4 insertions(+)
 create mode 100644 enigme.ktz
 create mode 100644 enigme.ltl
 create mode 100644 enigme.scn

diff --git a/enigme.ktz b/enigme.ktz
new file mode 100644
index 0000000000000000000000000000000000000000..32ed5c2c27cc566bf6d7de287b928b7983b7ace7
GIT binary patch
literal 303
zcmV+~0nq**iwFP!000003tf+0Ps1P>g?XWc)@}X<e!)U#tZ{dKEN1Z|#xC*FAbZns
zAu}yq^xylkO)n%64(FUF!2PN*rmEOsoF4ZHE&k6-I~;Xh-*jjruJtReTXfn~+FZ^}
zJwLzDGc&97`?p>#pRV){yWVeuKAYB4!?Wmv<?z5j^v*%UihSWV=;R{!_5+I-9Qxiz
z9RG^9fURskH$HsHW^fMsa)lw<=yy2zQ>g{8V7a*726<=OfZb>rB6ikAx?MfmVP}0W
zpRrqaDA)uP&zMjk1QTowD$D7_1$jV|)IQ`Cj-aF}R|S0@l#mpVdjcgP<fe?yf?8tV
zq5>-uqZm&Nxlj^D8R;T%DLHa^;`YtNsl&4h5cC|DB`#&8B`8P<V?Q3gm+`Uz004eS
BjT-;}

literal 0
HcmV?d00001

diff --git a/enigme.ltl b/enigme.ltl
new file mode 100644
index 0000000..089f027
--- /dev/null
+++ b/enigme.ltl
@@ -0,0 +1,4 @@
+op finished = Echec \/ Succes;
+
+[] (finished => dead);
+[] <> finished ;
diff --git a/enigme.scn b/enigme.scn
new file mode 100644
index 0000000..e69de29

From 7560b5a402168914be4302ad634c01329d81825d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?S=C3=A9bastien=20PONT?= <seba12.04@orange.fr>
Date: Wed, 1 Dec 2021 10:25:23 +0100
Subject: [PATCH 2/2] docs: :memo: create doc about ltl properties

---
 docs/ltl.md | 43 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)
 create mode 100644 docs/ltl.md

diff --git a/docs/ltl.md b/docs/ltl.md
new file mode 100644
index 0000000..59d4928
--- /dev/null
+++ b/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.