1,000 B
1,000 B
Propriétés LTL
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;
- L'état
finished
est bien l'état final :
[] (finished => dead);
- 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
- Générer le fichier
.ktz
à partir de tina
tina .\enigme.net .\enigme.ktz
- 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.