MSO vers automates

Outil Mona

Entrée : écrire une formule MSO dans Mona

Voici un exemple d'entrée (une formule de MSO) de l'outil Mona.

pred first(var1 x) = ~ex1 y: y + 1 = x;
pred last(var1 x) = ~ex1 y: x + 1 = y;

var2 Pa, Pb;
(ex1 x: first(x) & x in Pa) & (ex1 x: x in Pb) & (Pa inter Pb= {});

Les prédicats first et last correspondent respectivement au début de mot et fin de mot. Les prédicats Pa et Pb correspondent au fait que le curseur est sous un a ou un b. Comme l'outil est général, on doit spécifier qu'on ne peut pas avoir un a et un b en même temps. C'est fait grâce à (Pa inter Pb= {}). La formule ci-dessus spécifie le langage des mots qui commencent par un a et contiennent un b.

Sortie : un automate

Choisir "Output whole automaton in Graphviz format (linear mode only)". Dans l'automate, on ne représente pas les lettres mais des vecteurs. Avec l'exemple au dessus, (1, 0) (en vertical) c'est a et (0, 1) c'est b. (0, 0) c'est une autre lettre. Et (1, 1) c'est à la fois a et b (inconsistent avec notre spécification). (0, X) signifie (0, 0) ou (0, 1). Le (X, X) initial correspond au début du mot.