From e52aa8f9eb0b97b512b284573589f41693ad4f8c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 30 Jul 2019 15:34:46 +0200 Subject: [PATCH] * tests/python/sum.py: Simplify code. --- tests/python/sum.py | 28 ++++++++-------------------- 1 file changed, 8 insertions(+), 20 deletions(-) diff --git a/tests/python/sum.py b/tests/python/sum.py index af59e1a44..7e2e74220 100644 --- a/tests/python/sum.py +++ b/tests/python/sum.py @@ -1,5 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de l'Epita +# Copyright (C) 2017-2019 Laboratoire de Recherche et Développement +# de l'Epita # # This file is part of Spot, a model checking library. # @@ -58,27 +59,14 @@ def produce_phi(rg, n): phi1 = produce_phi(rg, 1000) phi2 = produce_phi(rg, 1000) -inputres = [] -aut = [] for p in zip(phi1, phi2): - inputres.append(spot.formula.Or(p)) a1 = spot.ltl_to_tgba_fm(p[0], dict) a2 = spot.ltl_to_tgba_fm(p[1], dict) - aut.append(spot.to_generalized_buchi( - spot.remove_alternation(spot.sum(a1, a2), True))) -for p in zip(aut, inputres): - assert p[0].equivalent_to(p[1]) + p0orp1 = spot.formula.Or(p) + a1ora2 = spot.remove_alternation(spot.sum(a1, a2), True) + assert p0orp1.equivalent_to(a1ora2) -aut = [] -inputres = [] - -for p in zip(phi1, phi2): - inputres.append(spot.formula.And(p)) - a1 = spot.ltl_to_tgba_fm(p[0], dict) - a2 = spot.ltl_to_tgba_fm(p[1], dict) - aut.append(spot.to_generalized_buchi( - spot.remove_alternation(spot.sum_and(a1, a2), True))) - -for p in zip(aut, inputres): - assert p[0].equivalent_to(p[1]) + p0andp1 = spot.formula.And(p) + a1anda2 = spot.remove_alternation(spot.sum_and(a1, a2), True) + assert p0andp1.equivalent_to(a1anda2)