Programme

Ce programme exécute l’algorithme de raffinement de système de transitions qui permet d’obtenir la relation de bisimulation la plus grossière de ce système. À chaque étape de raffinement, le fendeur (splitter) trouvé et le nouveau partitionnement sont affichés.

Le système de transitions est codé en dur au début du programme. C’est le système de la question 1 du TD 3. Il peut bien entendu être remplacé par un autre. Note : pour la conformité avec l’énoncé du TD 3, les états sont indexés à partir de 1.

Pour exécuter le programme, on peut le compiler, ou bien l’interpréter directement :

ocaml refine.ml

Voir le code source

Résultat

{} 1 6 
{c} 14 
{a} 2 7 10 12 13 
{a,b} 3 4 5 8 9 11 

Splitter: 14 

1 6 
14 
7 10 12 13 
2 
3 4 5 8 9 11 

Splitter: 1 6 

1 6 
14 
7 10 12 13 
2 
5 
3 4 8 9 11 

Splitter: 5 

1 
6 
14 
7 10 12 13 
2 
5 
3 4 8 9 11