7 Dec
2024
7 Dec
'24
2:54 p.m.
Hi Laurent,
Laurent Bartholdi <laurent.bartholdi(a)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