Laurent Bartholdi <laurent.bartholdi(a)gmail.com> writes:
> Ah, OK, thanks.
> Is there a good reason to do the log-encoding, or is it actually fine
> to have a classical alphabet a,b,c, ... and encode each letter as (a
> & !b & !c, !a & b & !c, !a & !b & c, ...)?
It all depends on what operations you plan to do on those automata.
Some operations are exponential in the number of atomic propositions, so
it is often best to have fewer of those.
If you only plan to two intersections and emptiness checks, a one-hot
encoding (what you suggested) is probably fine.
If you need to work with complete automata at some point (e.g., maybe
for complementation), one-hot encoding will be hard to work with. You
want the disjunction of the encodings of all letters in your alphabet to
be equal to true, so that completing an automaton does not "invent"
encodings that correspond to no letters.
Bonjour,
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?
Merci beaucoup d'avance, Laurent
