Dear Spot devs,
Is there a way for Spot to perform the alphabet abstraction available in GOAL as triggered with the `-a` switch when invoking the `alphabet` command? I paste the GOAL documentation about it below.
Thank you, Pierre.
- Alphabet -NAMEalphabet - Manipulate the alphabet of an automaton or a game.SYNOPSISalphabet -s [ -ap ] FILE_OR_LVALalphabet -e EXPR [ -ap ] FILE_OR_LVALalphabet -c EXPR [ -ap ] FILE_OR_LVALalphabet -r EXPR [ -ap ] FILE_OR_LVALalphabet -a EXPR [-R | -A | -S EXPR | -P EXPR | -ap ] FILE_OR_LVALDESCRIPTIONManipulate the alphabet of an automaton (or a game). This operation is directly applied to the input automaton. The returned value is always the new alphabet of the automaton (or the new atomic propositions if -ap is present).
-s Simply return the alphabet of the input automaton or game. -ap Return the atomic propositions (or classical symbols) instead of the alphabet. -e Expand the alphabet by a list of propositions. -c Contract the alphabet by removing a list of propositions. -r Rename the propositions based on a map from a proposition to its new name. -a Abstract the alphabet based on a map from a predicate to its definition. -R Retain the transition symbols in alphabet abstraction. -A Only annotate the transitions with properties specified by -S and -P. -S Specify the name of the property that will store the symbols on the transitions in alphabet abstraction. -P Specify the name of the property that will store the evaluations of the predicates in alphabet abstraction. EXAMPLE
alphabet -e "r" aut.gff alphabet -c "p" aut.gff alphabet -r "p=>r,q=>s" aut.gff alphabet -a "r=>p/\q" aut.gff alphabet -a "r=>p/\q" -A -P "Predicates" aut.gff