Hi Laurent,

Laurent Bartholdi laurent.bartholdi@gmail.com writes:

J'aimerais utiliser spot pour manipuler des automates de Buchi, parité,... en librairie (pour l'intégrer en fait à du code déjà existant). Il semble que c'est possible, mais mes automates devraient avoir un alphabet de la forme {0,...,n} ou {1,...,n}, et pas un BDD. Comment puis-je faire ? Ou, plus généralement, comment avoir accès à une documentation complète qui ne passe pas par doxygen?

(Switching to English for the subscribers of this mailing list.)

Unfortunately, Spot only supports propositional alphabets.

For classical alphabets, the usual workaround is to log-encode each letter over a set of propositions. For input/output, there is a feature of the HOA format called "alias" that can make this more readable. See https://spot.lre.epita.fr/ipynb/aliases.html

Regarding the documentation, our only sources of documentation are those listed on front page of the web site.

Alexandre