From 3d79022abb7d16229fdf73f8e7b453e0b2c91a99 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 29 Jun 2021 23:16:40 +0200 Subject: [PATCH] adjust some python tests to work with PyPy Part of #467. * tests/python/bdddict.py, tests/python/ltl2tgba.py, tests/python/ltlparse.py, tests/python/ltlsimple.py, tests/python/sccinfo.py, tests/python/simstate.py, tests/python/split.py, tests/python/tra2tba.py: Adjust to deal with a non-refcounted Python implementation. --- tests/python/bdddict.py | 20 +++++++++++++- tests/python/ltl2tgba.py | 14 +++++++--- tests/python/ltlparse.py | 8 +++++- tests/python/ltlsimple.py | 13 ++++++--- tests/python/sccinfo.py | 8 +++--- tests/python/simstate.py | 21 +++++++++++++++ tests/python/split.py | 27 ++++++++++++++++++- tests/python/tra2tba.py | 55 +++++++++++++++++++++++++++++++-------- 8 files changed, 141 insertions(+), 25 deletions(-) diff --git a/tests/python/bdddict.py b/tests/python/bdddict.py index bdb5fc2df..d6222b58f 100644 --- a/tests/python/bdddict.py +++ b/tests/python/bdddict.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2019 Laboratoire de Recherche et Développement de l'Epita +# Copyright (C) 2019, 2021 Laboratoire de Recherche et Développement de l'Epita # (LRDE). # # This file is part of Spot, a model checking library. @@ -20,6 +20,17 @@ # Make sure we can leep track of BDD association in Python using bdd_dict, as # discussed in issue #372. +# CPython use reference counting, so that automata are destructed +# when we expect them to be. However other implementations like +# PyPy may call destructors latter, causing different output. +from platform import python_implementation +if python_implementation() == 'CPython': + def gcollect(): + pass +else: + import gc + def gcollect(): + gc.collect() import spot @@ -88,18 +99,22 @@ debug("h2") check_ok() del aut +gcollect() debug("-aut") check_ok() del word +gcollect() debug("-word") check_ok() del h +gcollect() debug("-h") check_ok() del h2 +gcollect() debug("-h2") check_nok() @@ -110,9 +125,11 @@ var = bdict.register_anonymous_variables(1, h3) debug("h3") assert var == 2 del h2 +gcollect() debug("-h2") check_ok() del h3 +gcollect() debug("-h3") check_nok() @@ -121,4 +138,5 @@ debug("h2") bdict.unregister_variable(bdict.varnum("b"), h2) bdict.unregister_variable(bdict.varnum("a"), h2) debug("-b,-a") +gcollect() check_nok() diff --git a/tests/python/ltl2tgba.py b/tests/python/ltl2tgba.py index 6f2dfdd49..25fff4566 100755 --- a/tests/python/ltl2tgba.py +++ b/tests/python/ltl2tgba.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2012, 2014, 2015, 2016 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2009, 2010, 2012, 2014-2016, 2021 Laboratoire de Recherche +# et Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. @@ -28,7 +28,6 @@ import sys import getopt import spot - def usage(prog): sys.stderr.write("""Usage: %s [OPTIONS...] formula @@ -131,4 +130,11 @@ else: del pf del dict -assert spot.fnode_instances_check() + + +# In CPython, reference counting will cause the above del() +# to actually destruct the above formulas. However that is +# not necessary in other implementations. +from platform import python_implementation +if python_implementation() == 'CPython': + assert spot.fnode_instances_check() diff --git a/tests/python/ltlparse.py b/tests/python/ltlparse.py index f0dbc373f..98562743c 100755 --- a/tests/python/ltlparse.py +++ b/tests/python/ltlparse.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2009-2012, 2014-2017, 2019 Laboratoire de Recherche et +# Copyright (C) 2009-2012, 2014-2017, 2019, 2021 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -199,6 +199,12 @@ for (x, msg) in [('a->', "missing right operand for \"implication operator\""), assert msg in err del f9 +# force GC before fnode_instances_check(), unless it's CPython +from platform import python_implementation +if python_implementation() != 'CPython': + import gc + gc.collect() + assert spot.fnode_instances_check() f = spot.formula_F(2, 4, spot.formula_ap("a")) diff --git a/tests/python/ltlsimple.py b/tests/python/ltlsimple.py index ac9e3c426..7b88f07dc 100755 --- a/tests/python/ltlsimple.py +++ b/tests/python/ltlsimple.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2012, 2015, 2018 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2009, 2010, 2012, 2015, 2018, 2021 Laboratoire de +# Recherche et Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systemes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. @@ -23,6 +23,12 @@ import spot import sys +# Some of the tests here assume timely destructor calls, as they occur +# in the the reference-counted CPython implementation. Other +# implementation such as PyPy, should skip those tests. +from platform import python_implementation +is_cpython = python_implementation() == 'CPython' + # ---------------------------------------------------------------------- a = spot.formula.ap('a') b = spot.formula.ap('b') @@ -71,7 +77,8 @@ f5 = spot.formula.Xor(F, c) del a, b, c, T, F, f1, f2, f4, f5 -assert spot.fnode_instances_check() +if is_cpython: + assert spot.fnode_instances_check() # ---------------------------------------------------------------------- assert str([str(x) for x in spot.formula('a &b & c')]) == "['a', 'b', 'c']" diff --git a/tests/python/sccinfo.py b/tests/python/sccinfo.py index fc6eeeea3..0ac645726 100644 --- a/tests/python/sccinfo.py +++ b/tests/python/sccinfo.py @@ -59,7 +59,7 @@ l = sorted(list(l0) + list(l1) + list(l2) + list(l3)) assert l == [0, 1, 2, 3, 4] i = si.initial() -todo = {i} +todo = [i] seen = {i} trans = [] transi = [] @@ -72,13 +72,13 @@ while todo: for s in si.succ(e): if s not in seen: seen.add(s) - todo.add(s) + todo.append(s) assert seen == {0, 1, 2, 3} assert trans == [(0, 0), (0, 1), (0, 2), (0, 3), (2, 0), (2, 1), (2, 2), (2, 4), - (1, 1), (4, 1), (4, 4), (3, 3)] + (3, 3), (4, 1), (4, 4), (1, 1)] assert transi == [(0, 0, 1), (0, 2, 3), (2, 0, 6), - (2, 2, 8), (1, 1, 5), (4, 4, 12), (3, 3, 10)] + (2, 2, 8), (3, 3, 10), (4, 4, 12), (1, 1, 5)] assert not spot.is_weak_automaton(a, si) diff --git a/tests/python/simstate.py b/tests/python/simstate.py index 278e05045..6c2ca8bc3 100644 --- a/tests/python/simstate.py +++ b/tests/python/simstate.py @@ -20,6 +20,18 @@ import spot from sys import exit +# CPython use reference counting, so that automata are destructed +# when we expect them to be. However other implementations like +# PyPy may call destructors latter, causing different output. +from platform import python_implementation +if python_implementation() == 'CPython': + def gcollect(): + pass +else: + import gc + def gcollect(): + gc.collect() + aut = spot.automaton(""" HOA: v1 States: 2 @@ -63,6 +75,10 @@ State: 0 "[0,1]" {0} [t] 0 --END--""" +del aut +del aut2 +gcollect() + aut = spot.translate('GF((p0 -> Gp0) R p1)') daut = spot.tgba_determinize(aut, True) @@ -92,6 +108,10 @@ State: 2 "{₀[0]₀}{₁[1]₁}" [0&1] 1 {2} --END--""" +del aut +del daut +gcollect() + aut = spot.automaton(""" HOA: v1 States: 2 @@ -175,6 +195,7 @@ assert b.num_states() == 3 b.set_init_state(1) b.purge_unreachable_states() b.copy_state_names_from(a) + assert b.to_str() == """HOA: v1 States: 1 Start: 0 diff --git a/tests/python/split.py b/tests/python/split.py index 2f7d8c756..d604df855 100644 --- a/tests/python/split.py +++ b/tests/python/split.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2018-2020 Laboratoire de Recherche et +# Copyright (C) 2018-2021 Laboratoire de Recherche et # Développement de l'Epita # # This file is part of Spot, a model checking library. @@ -19,6 +19,19 @@ import spot +# CPython use reference counting, so that automata are destructed +# when we expect them to be. However other implementations like +# PyPy may call destructors latter, causing different output. +from platform import python_implementation +if python_implementation() == 'CPython': + def gcollect(): + pass +else: + import gc + def gcollect(): + gc.collect() + + def incl(a, b): return not b.intersects(spot.dualize(spot.tgba_determinize(a))) @@ -50,6 +63,10 @@ def str_diff(expect, obtained): aut, s = do_split('(FG !a) <-> (GF b)', ['a'], ['b']) assert equiv(aut, spot.unsplit_2step(s)) +del aut +del s +gcollect() + aut, s = do_split('GFa && GFb', ['a'], ['b']) assert equiv(aut, spot.unsplit_2step(s)) assert str_diff("""HOA: v1 @@ -73,6 +90,10 @@ State: 2 [1] 0 {1} --END--""", s.to_str() ) +del aut +del s +gcollect() + aut, s = do_split('! ((G (req -> (F ack))) && (G (go -> (F grant))))', ['go', 'req'], ['ack']) assert equiv(aut, spot.unsplit_2step(s)) @@ -113,6 +134,10 @@ assert equiv(aut, spot.unsplit_2step(s)) # [!3] 2 # --END--""" +del aut +del s +gcollect() + aut, s = do_split('((G (((! g_0) || (! g_1)) && ((r_0 && (X r_1)) -> (F (g_0 \ && g_1))))) && (G (r_0 -> F g_0))) && (G (r_1 -> F g_1))', ['r_0', 'r_1'], ['g_0', 'g_1']) diff --git a/tests/python/tra2tba.py b/tests/python/tra2tba.py index c0efd6f0f..b303c010b 100644 --- a/tests/python/tra2tba.py +++ b/tests/python/tra2tba.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016-2018, 2020 Laboratoire de Recherche et Développement -# de l'Epita +# Copyright (C) 2016-2018, 2020-2021 Laboratoire de Recherche +# et Développement de l'Epita # # This file is part of Spot, a model checking library. # @@ -19,6 +19,12 @@ import spot +# CPython use reference counting, so that automata are destructed +# when we expect them to be. However other implementations like +# PyPy may call destructors latter, causing different output. +from platform import python_implementation +is_cpython = python_implementation() == 'CPython' + # Test 1. aut = spot.automaton(""" HOA: v1 @@ -365,7 +371,10 @@ State: 7 --END--""" res = spot.remove_fin(aut) -assert(res.to_str('hoa') == exp) +if is_cpython: + assert(res.to_str('hoa') == exp) +else: + assert(res.equivalent_to(spot.automaton(exp))) # Test 9. aut = spot.automaton(""" @@ -401,7 +410,10 @@ State: 1 --END--""" res = spot.remove_fin(aut) -assert(res.to_str('hoa') == exp) +if is_cpython: + assert(res.to_str('hoa') == exp) +else: + assert(res.equivalent_to(spot.automaton(exp))) # Test 10. aut = spot.automaton(""" @@ -440,7 +452,10 @@ State: 2 {0} --END--""" res = spot.remove_fin(aut) -assert(res.to_str('hoa') == exp) +if is_cpython: + assert(res.to_str('hoa') == exp) +else: + assert(res.equivalent_to(spot.automaton(exp))) # Test 11. aut = spot.automaton(""" @@ -477,7 +492,10 @@ State: 1 --END--""" res = spot.remove_fin(aut) -assert(res.to_str('hoa') == exp) +if is_cpython: + assert(res.to_str('hoa') == exp) +else: + assert(res.equivalent_to(spot.automaton(exp))) # Different order for rabin_to_buchi_if_realizable() due to merge_edges() not # being called. This is on purpose: the edge order should match exactly the @@ -499,7 +517,10 @@ State: 1 [!0] 0 {0} --END--""" res = spot.rabin_to_buchi_if_realizable(aut) -assert(res.to_str('hoa') == exp2) +if is_cpython: + assert(res.to_str('hoa') == exp2) +else: + assert(res.equivalent_to(spot.automaton(exp2))) # Test 12. aut = spot.automaton(""" @@ -543,7 +564,10 @@ State: 3 {0} --END--""" res = spot.remove_fin(aut) -assert(res.to_str('hoa') == exp) +if is_cpython: + assert(res.to_str('hoa') == exp) +else: + assert(res.equivalent_to(spot.automaton(exp))) # Test 13. aut = spot.automaton(""" @@ -590,7 +614,10 @@ State: 1 --END--""" res = spot.remove_fin(aut) -assert(res.to_str('hoa') == exp) +if is_cpython: + assert(res.to_str('hoa') == exp) +else: + assert(res.equivalent_to(spot.automaton(exp))) # rabin_to_buchi_if_realizable() does not call merge_edges() on purpose: the # edge order should match exactly the original automaton. @@ -616,7 +643,10 @@ State: 1 --END--""" res = spot.rabin_to_buchi_if_realizable(aut) -assert(res.to_str('hoa') == exp2) +if is_cpython: + assert(res.to_str('hoa') == exp2) +else: + assert(res.equivalent_to(spot.automaton(exp2))) # Test 14. aut = spot.automaton(""" @@ -650,5 +680,8 @@ State: 1 --END--""" res = spot.remove_fin(aut) -assert(res.to_str('hoa') == exp) +if is_cpython: + assert(res.to_str('hoa') == exp) +else: + assert(res.equivalent_to(spot.automaton(exp))) assert spot.rabin_to_buchi_if_realizable(aut) is None