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
