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 -

NAME

alphabet - Manipulate the alphabet of an automaton or a game.

SYNOPSIS

alphabet -s [ -ap ] FILE_OR_LVAL

alphabet -e EXPR [ -ap ] FILE_OR_LVAL

alphabet -c EXPR [ -ap ] FILE_OR_LVAL

alphabet -r EXPR [ -ap ] FILE_OR_LVAL

alphabet -a EXPR [-R | -A | -S EXPR | -P EXPR | -ap ] FILE_OR_LVAL

DESCRIPTION

Manipulate 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