Pierre <pierreganty(a)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