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
