2 Jun
2022
2 Jun
'22
3:49 p.m.
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(a)lrde.epita.fr> wrote:
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.
