projet-genie-logiciel-systeme/docs/ltl.md

Propriétés LTL

• Propriétés LTL
  • Que vérifions-nous ?
  • 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 :

op finished = Echec \/ Succes;

1. L'état finished est bien l'état final :

[] (finished => dead);

2. On arrivera toujours soit dans l'état échec, soit dans l'état succes :

[] <> 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

tina .\enigme.net .\enigme.ktz

2. Vérifier les propriétés à l'aide de selt

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.