Qu’est-ce qu’un invariant en TLA+ ?
Un invariant est une condition qui doit rester vraie dans tous les états d’un système. TLA+ (logique temporelle des actions) décrit un système par ses états et ses pas, et son vérificateur TLC cherche un état qui viole l’invariant.
Une salle de travaux dirigés a 3 places. Le système de comptage laisse entrer tant qu’il y a moins de 5 personnes. Combien de pas faut-il pour dépasser la salle ?
À la fin de cette leçon
Remarque
Je peux écrire un invariant et lire le contre-exemple que TLC donne quand il est violé.
Mots-clés
| Mot | Ce que ça veut dire | Exemple |
|---|---|---|
| État | la valeur de toutes les variables à un instant | presents = 2 |
| Pas | un changement permis d’un état à un autre | |
| Spécification | la description d’un système par ses états de départ et ses pas | |
| Invariant | une condition vraie dans tous les états atteignables | |
| TLC | le programme qui essaie tous les états d’une spécification | |
| Contre-exemple | la suite d’états qui mène à la violation |
Les cellules que les étudiants remplissent restent vides dans cet aperçu.
Un système est fait d’états et de pas
La spécification de la salle a une variable, presents. Elle commence à 0. Deux pas sont permis. Entrer ajoute 1 si presents est sous 5. Sortir retire 1 si presents est au-dessus de 0.
Le symbole /\ veut dire « et », et \/ veut dire « ou ». Une apostrophe, presents', désigne la valeur après le pas. Les trois Runs écrivent la spécification et ses réglages dans essais.
La spécification de la salle
---- MODULE Salle ----
EXTENDS Naturals
VARIABLE presents
Init == presents = 0
Entrer == presents < 5 /\ presents' = presents + 1
Sortir == presents > 0 /\ presents' = presents - 1
Next == Entrer \/ Sortir
Spec == Init /\ [][Next]_presents
Capacite == presents <= 3
====Créer un dossier pour vos essais
mkdir -p essaisAffichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Écrire la spécification
printf '%s\n' '---- MODULE Salle ----' 'EXTENDS Naturals' 'VARIABLE presents' 'Init == presents = 0' "Entrer == presents < 5 /\ presents' = presents + 1" "Sortir == presents > 0 /\ presents' = presents - 1" 'Next == Entrer \/ Sortir' 'Spec == Init /\ [][Next]_presents' 'Capacite == presents <= 3' '====' > essais/Salle.tlaAffichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Dire à TLC quoi vérifier
printf '%s\n' 'SPECIFICATION Spec' 'INVARIANT Capacite' > essais/Salle.cfgAffichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
TLC cherche un état qui viole l’invariant
L’invariant Capacite dit que presents ne dépasse jamais 3. TLC part de l’état de départ et essaie tous les pas, état après état, en commençant par les chemins les plus courts.
Dès qu’il trouve un état où l’invariant est faux, il s’arrête et affiche le chemin qui y mène. Le Run garde les lignes utiles : la phrase de violation, puis presents à chaque état.
Lancer TLC sur la salle
tlc essais/Salle | grep -E "violated|presents ="Affichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Exemple travaillé : le chemin vers 4 personnes
| État | Pas | presents | Capacite (presents <= 3) |
|---|---|---|---|
| 1 | départ | 0 | vrai |
| 2 | Entrer | 1 | vrai |
| 3 | Entrer | 2 | vrai |
| 4 | Entrer | 3 | vrai |
| 5 | Entrer | 4 | faux : l’invariant est violé |
Les cellules que les étudiants remplissent restent vides dans cet aperçu.
On corrige le pas, pas l’invariant
Le contre-exemple montre le coupable : Entrer laisse entrer jusqu’à 5, alors que la salle a 3 places. Il faut changer le garde du pas, presents < 5, en presents < 3.
Les deux Runs font la correction avec sed, puis relancent TLC. Il n’affiche plus qu’une phrase : aucune erreur.
Corriger le garde du pas Entrer
sed -i 's/presents < 5/presents < 3/' essais/Salle.tlaAffichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Relancer TLC
tlc essais/Salle | grep "No error"Affichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Erreur fréquente
Attention
Beaucoup de gens pensent qu’on corrige une violation en changeant l’invariant, par exemple en écrivant presents <= 5. L’invariant dit ce que le système doit garantir : une salle de 3 places. Quand TLC le trouve violé, on répare le pas fautif. On ne change l’invariant que s’il ne disait pas ce qu’on voulait.
Pour aller plus loin
Gardez la spécification corrigée et passez la capacité à 2 : dans Salle.tla, changez presents <= 3 en presents <= 2 avec sed. Relancez tlc essais/Salle.
Prévoyez le nombre d’états du contre-exemple avant de lancer, puis comparez avec ce que TLC affiche.