Hi Alexandre, Thank you for your explanations. If I understand correctly the relabeling, it does not match what I want. Let me give a visual example from GOAL. 1. Original BA with two AP `p` and `q`. [image: original.png] After applying the alphabet abstraction `a=>p\/q` GOAL computes: [image: abstracted.png] My particular use case is the following: I have a Kripke structure with APs saying "Process 1 is in the critical section" "Process 2 is in the critical section" ... It happens that I don't care exactly which process is in the critical section and so I want to abstract all the previous APs into one AP saying "some process is in the critical section". I think I achieve this by using the abstraction of GOAL as shown in the example. At the moment I don't see how the relabelling you showed could be used to achieve the same result with SPOT. Is there a way? Thank you, Pierre. On Wed, 1 Jun 2022 at 18:19, Alexandre Duret-Lutz <adl@lrde.epita.fr> wrote:
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.
