[Spot] Re: Alphabet abstraction

Hi Pierre, Pierre <pierreganty@gmail.com> writes:

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?

-a Abstract the alphabet based on a map from a predicate to its definition. EXAMPLE alphabet -a "r=>p/\q" aut.gff

I'm not sure what "abstract the alphabet" means. The example seems to suggests it's some kind of renaming? We have the function relabel_here(aut, relabeling_map) that can replace atomic propositions appearing in aut by any Boolean formula as specified in the relabeling_map.