À quoi sert Alloy ?
Alloy est un langage pour décrire un système avec des ensembles et des relations. Son outil cherche un exemple ou un contre-exemple de petite taille. Quand une propriété est fausse, il montre la situation qui la contredit.
Dans une entreprise, chaque personne a au plus un chef. On affirme que personne n’est son propre chef, même de loin. Alloy cherche un groupe où ce n’est pas vrai.
À la fin de cette leçon
Remarque
Je peux lire un contre-exemple d’Alloy, dessiné comme des personnes et leurs liens.
Mots-clés
| Mot | Ce que ça veut dire | Exemple |
|---|---|---|
| Ensemble (sig) | un genre de choses du modèle | Personne |
| Relation | des liens entre les éléments de deux ensembles | chef |
| Fait (fact) | une règle que tout exemple doit respecter | |
| Assertion | une propriété qu’on veut vérifier | |
| Instance | un exemple concret : des éléments et leurs liens | |
| Portée | le nombre maximal d’éléments que l’outil essaie | for 4 |
Les cellules que les étudiants remplissent restent vides dans cet aperçu.
Un modèle est fait d’ensembles et de relations
Le modèle a un ensemble, Personne, et une relation, chef. Le mot lone veut dire « zéro ou un » : une personne a au plus un chef.
Un fait écarte les exemples qu’on refuse. Ici, personne n’est directement son propre chef. Les deux Runs écrivent le modèle dans essais.
Le modèle des personnes et de leur chef
sig Personne { chef: lone Personne }
fact pas_son_propre_chef { no p: Personne | p.chef = p }
assert pas_de_boucle { no p: Personne | p in p.^chef }
check pas_de_boucle for 4
run exemple { some chef } for 3Cré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 le modèle dans un fichier
printf '%s\n' 'sig Personne { chef: lone Personne }' 'fact pas_son_propre_chef { no p: Personne | p.chef = p }' 'assert pas_de_boucle { no p: Personne | p in p.^chef }' 'check pas_de_boucle for 4' 'run exemple { some chef } for 3' > essais/chefs.alsAffiché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.
Une vérification cherche un contre-exemple
L’assertion dit que personne n’est son propre chef, même par plusieurs chefs de suite : p.^chef est tous les chefs de p, directs ou lointains. check demande à Alloy de chercher un contre-exemple avec au plus 4 personnes.
Pour un check, SAT veut dire qu’un contre-exemple existe, et UNSAT qu’il n’y en a pas. run cherche un simple exemple.
Lancer Alloy sur le modèle
alloy essais/chefs.alsAffiché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 contre-exemple d’Alloy
| Personne | A pour chef | Que se passe-t-il ? |
|---|---|---|
| Personne$0 | Personne$2 | Le fait est respecté : personne n’est son propre chef direct |
| Personne$1 | Personne$0 | Le chef de Personne$1 est Personne$0 |
| Personne$2 | Personne$1 | La boucle est fermée : Personne$0 est son propre chef de loin |
Les cellules que les étudiants remplissent restent vides dans cet aperçu.
Un fait plus fort écarte le contre-exemple
Le fait était trop faible. Il faut interdire les boucles de toute longueur : une personne ne doit pas se trouver parmi ses propres chefs, p in p.^chef.
Le Run remplace la règle du fait avec sed. Alors Alloy répond UNSAT pour le check : plus de contre-exemple. Le run répond toujours SAT.
Renforcer le fait
sed -i 's/p.chef = p/p in p.^chef/' essais/chefs.alsAffiché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 Alloy et lire les deux résultats
alloy essais/chefs.als | head -n 2Affiché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 que UNSAT prouve la propriété pour toute taille de groupe. Alloy ne cherche que jusqu’à la portée donnée, ici 4 personnes. UNSAT dit qu’il n’y a pas de contre-exemple de 4 personnes ou moins. Il reste vrai qu’un fait qui répète l’assertion rend la vérification inutile.
Pour aller plus loin
Faites une copie du modèle de départ, avec le fait p.chef = p, et changez check pas_de_boucle for 4 en check pas_de_boucle for 1. Lancez alloy sur la copie.
Dites ce que répond Alloy pour le check, puis pourquoi cette réponse ne prouve pas que la propriété est vraie.