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`.

After applying the alphabet abstraction `a=>p\/q` GOAL computes:

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.