44 lines
1,000 B
Markdown
44 lines
1,000 B
Markdown
|
# 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.
|