From cfa80ed842f90e1cfb6edb5bae16e63f60a38d22 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 25 Sep 2017 10:54:09 +0200 Subject: [PATCH] tests: avoid some superfluous calls to remove_alternation() * tests/python/toweak.py: Here. --- tests/python/toweak.py | 32 ++++++++++---------------------- 1 file changed, 10 insertions(+), 22 deletions(-) diff --git a/tests/python/toweak.py b/tests/python/toweak.py index c1b3ade93..b21827a83 100644 --- a/tests/python/toweak.py +++ b/tests/python/toweak.py @@ -30,30 +30,20 @@ GF!b (b & GF!b) | (!b & FGb) b | (a & XF(b R a)) | (!a & XG(!b U !a))""" -phi1 = phi1.split('\n') - -bdddict = spot.make_bdd_dict() - def equivalent(a, phi): - negphi = spot.formula.Not(phi) - nega = spot.dualize(a) - a2 = spot.translate(phi, 'TGBA', 'SBAcc' ) - nega2 = spot.translate(negphi, 'TGBA', 'SBAcc') - 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() + negphi = spot.formula.Not(phi) + nega = spot.dualize(a) + return not (spot.translate(negphi).intersects(a) + or spot.translate(phi).intersects(nega)) def test_phi(phi): - a = spot.translate(phi, 'TGBA', 'SBAcc') - a0 = spot.dualize(a) - - res = spot.to_weak_alternating(a0) - assert equivalent(res, spot.formula.Not(spot.formula(phi))) - -for p in phi1: - test_phi(p) + a = spot.translate(phi, 'TGBA', 'SBAcc') + res = spot.to_weak_alternating(spot.dualize(a)) + assert equivalent(res, spot.formula.Not(spot.formula(phi))) +for p in phi1.split('\n'): + print(p) + test_phi(p) phi2 = spot.formula("(G((F a) U b)) W a") a2 = spot.automaton(""" @@ -99,5 +89,3 @@ State: 6 """) a2 = spot.to_weak_alternating(a2) assert equivalent(a2, phi2) - -