Dear Spot devs,
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? I paste the GOAL documentation about it below.
Thank you, Pierre.
- Alphabet -NAMEalphabet - Manipulate the alphabet of an automaton or a game.SYNOPSISalphabet -s [ -ap ] FILE_OR_LVALalphabet -e EXPR [ -ap ] FILE_OR_LVALalphabet -c EXPR [ -ap ] FILE_OR_LVALalphabet -r EXPR [ -ap ] FILE_OR_LVALalphabet -a EXPR [-R | -A | -S EXPR | -P EXPR | -ap ] FILE_OR_LVALDESCRIPTIONManipulate the alphabet of an automaton (or a game). This operation is directly applied to the input automaton. The returned value is always the new alphabet of the automaton (or the new atomic propositions if -ap is present).
-s Simply return the alphabet of the input automaton or game. -ap Return the atomic propositions (or classical symbols) instead of the alphabet. -e Expand the alphabet by a list of propositions. -c Contract the alphabet by removing a list of propositions. -r Rename the propositions based on a map from a proposition to its new name. -a Abstract the alphabet based on a map from a predicate to its definition. -R Retain the transition symbols in alphabet abstraction. -A Only annotate the transitions with properties specified by -S and -P. -S Specify the name of the property that will store the symbols on the transitions in alphabet abstraction. -P Specify the name of the property that will store the evaluations of the predicates in alphabet abstraction. EXAMPLE
alphabet -e "r" aut.gff alphabet -c "p" aut.gff alphabet -r "p=>r,q=>s" aut.gff alphabet -a "r=>p/\q" aut.gff alphabet -a "r=>p/\q" -A -P "Predicates" aut.gff
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.
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.
Pierre pierreganty@gmail.com writes:
If I understand correctly the relabeling, it does not match what I want.
What Spot has is a way to replace any atomic proposition by a Boolean formula. But you are asking for something that goes in the other direction, somehow.
If I understand correctly the example, given the rule a=>f you want that any label ℓ is replaced by ℓ' computed as follow:
1. ℓ' = false 2. if (ℓ & f != false) then ℓ' |= a 3. if (ℓ & !f != false) then ℓ' |= !a
do I get this right?
Here is a quick & dirty Python function that does it:
import spot from buddy import bdd_ithvar, bddfalse
def abstract(repl, match, aut): repl = spot.formula(repl) assert repl._is(spot.op_ap) match = spot.formula(match) assert match.is_boolean() # Not going to simplify anything, but tl_simplifier # has a convenient transformation from formula to BDD. tls = spot.tl_simplifier(aut.get_dict()) match = tls.as_bdd(match) nmatch = -match repl = bdd_ithvar(aut.register_ap(repl)) nrepl = -repl for e in aut.edges(): l = bddfalse if (e.cond & match != bddfalse): l |= repl if (e.cond & nmatch != bddfalse): l |= nrepl e.cond = l aut.remove_unused_ap() return aut
-
Alexandre Duret-Lutz -
Pierre