alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

tests: avoid some superfluous calls to remove_alternation()

Browse source 
* tests/python/toweak.py: Here.
This commit is contained in:
Alexandre Duret-Lutz 2017-09-25 10:54:09 +02:00
parent f45112a235
commit cfa80ed842
1 changed files with 10 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

22
tests/python/toweak.py
View file

@ -30,31 +30,21 @@ GF!b
(b & GF!b) | (!b & FGb) (b & GF!b) | (!b & FGb)
b | (a & XF(b R a)) | (!a & XG(!b U !a))""" b | (a & XF(b R a)) | (!a & XG(!b U !a))"""
phi1 = phi1.split('\n')
bdddict = spot.make_bdd_dict()
def equivalent(a, phi): def equivalent(a, phi):
negphi = spot.formula.Not(phi) negphi = spot.formula.Not(phi)
nega = spot.dualize(a) nega = spot.dualize(a)
a2 = spot.translate(phi, 'TGBA', 'SBAcc' ) return not (spot.translate(negphi).intersects(a)
nega2 = spot.translate(negphi, 'TGBA', 'SBAcc') or spot.translate(phi).intersects(nega))
ra = spot.remove_alternation(a)
ran = spot.remove_alternation(nega)
return spot.product(spot.remove_alternation(a), nega2).is_empty()\
and spot.product(spot.remove_alternation(nega), a2).is_empty()
def test_phi(phi): def test_phi(phi):
a = spot.translate(phi, 'TGBA', 'SBAcc') a = spot.translate(phi, 'TGBA', 'SBAcc')
a0 = spot.dualize(a) res = spot.to_weak_alternating(spot.dualize(a))
res = spot.to_weak_alternating(a0)
assert equivalent(res, spot.formula.Not(spot.formula(phi))) assert equivalent(res, spot.formula.Not(spot.formula(phi)))
for p in phi1: for p in phi1.split('\n'):
print(p)
test_phi(p) test_phi(p)
phi2 = spot.formula("(G((F a) U b)) W a") phi2 = spot.formula("(G((F a) U b)) W a")
a2 = spot.automaton(""" a2 = spot.automaton("""
HOA: v1 HOA: v1
@ -99,5 +89,3 @@ State: 6
""") """)
a2 = spot.to_weak_alternating(a2) a2 = spot.to_weak_alternating(a2)
assert equivalent(a2, phi2) assert equivalent(a2, phi2)