Hi Pierre,
Pierre <pierreganty(a)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.