# 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.