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.
This commit is contained in:
parent
47348a9755
commit
3d79022abb
8 changed files with 141 additions and 25 deletions
|
|
@ -1,5 +1,5 @@
|
||||||
# -*- mode: python; coding: utf-8 -*-
|
# -*- 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).
|
# (LRDE).
|
||||||
#
|
#
|
||||||
# This file is part of Spot, a model checking library.
|
# 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
|
# Make sure we can leep track of BDD association in Python using bdd_dict, as
|
||||||
# discussed in issue #372.
|
# 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
|
import spot
|
||||||
|
|
||||||
|
|
@ -88,18 +99,22 @@ debug("h2")
|
||||||
check_ok()
|
check_ok()
|
||||||
|
|
||||||
del aut
|
del aut
|
||||||
|
gcollect()
|
||||||
debug("-aut")
|
debug("-aut")
|
||||||
check_ok()
|
check_ok()
|
||||||
|
|
||||||
del word
|
del word
|
||||||
|
gcollect()
|
||||||
debug("-word")
|
debug("-word")
|
||||||
check_ok()
|
check_ok()
|
||||||
|
|
||||||
del h
|
del h
|
||||||
|
gcollect()
|
||||||
debug("-h")
|
debug("-h")
|
||||||
check_ok()
|
check_ok()
|
||||||
|
|
||||||
del h2
|
del h2
|
||||||
|
gcollect()
|
||||||
debug("-h2")
|
debug("-h2")
|
||||||
check_nok()
|
check_nok()
|
||||||
|
|
||||||
|
|
@ -110,9 +125,11 @@ var = bdict.register_anonymous_variables(1, h3)
|
||||||
debug("h3")
|
debug("h3")
|
||||||
assert var == 2
|
assert var == 2
|
||||||
del h2
|
del h2
|
||||||
|
gcollect()
|
||||||
debug("-h2")
|
debug("-h2")
|
||||||
check_ok()
|
check_ok()
|
||||||
del h3
|
del h3
|
||||||
|
gcollect()
|
||||||
debug("-h3")
|
debug("-h3")
|
||||||
check_nok()
|
check_nok()
|
||||||
|
|
||||||
|
|
@ -121,4 +138,5 @@ debug("h2")
|
||||||
bdict.unregister_variable(bdict.varnum("b"), h2)
|
bdict.unregister_variable(bdict.varnum("b"), h2)
|
||||||
bdict.unregister_variable(bdict.varnum("a"), h2)
|
bdict.unregister_variable(bdict.varnum("a"), h2)
|
||||||
debug("-b,-a")
|
debug("-b,-a")
|
||||||
|
gcollect()
|
||||||
check_nok()
|
check_nok()
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
# -*- mode: python; coding: utf-8 -*-
|
# -*- mode: python; coding: utf-8 -*-
|
||||||
# Copyright (C) 2009, 2010, 2012, 2014, 2015, 2016 Laboratoire de Recherche et
|
# Copyright (C) 2009, 2010, 2012, 2014-2016, 2021 Laboratoire de Recherche
|
||||||
# Développement de l'Epita (LRDE).
|
# et Développement de l'Epita (LRDE).
|
||||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||||
# et Marie Curie.
|
# et Marie Curie.
|
||||||
|
|
@ -28,7 +28,6 @@ import sys
|
||||||
import getopt
|
import getopt
|
||||||
import spot
|
import spot
|
||||||
|
|
||||||
|
|
||||||
def usage(prog):
|
def usage(prog):
|
||||||
sys.stderr.write("""Usage: %s [OPTIONS...] formula
|
sys.stderr.write("""Usage: %s [OPTIONS...] formula
|
||||||
|
|
||||||
|
|
@ -131,4 +130,11 @@ else:
|
||||||
|
|
||||||
del pf
|
del pf
|
||||||
del dict
|
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()
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
# -*- mode: python; coding: utf-8 -*-
|
# -*- 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).
|
# Développement de l'Epita (LRDE).
|
||||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
# 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
|
assert msg in err
|
||||||
del f9
|
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()
|
assert spot.fnode_instances_check()
|
||||||
|
|
||||||
f = spot.formula_F(2, 4, spot.formula_ap("a"))
|
f = spot.formula_F(2, 4, spot.formula_ap("a"))
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
# -*- mode: python; coding: utf-8 -*-
|
# -*- mode: python; coding: utf-8 -*-
|
||||||
# Copyright (C) 2009, 2010, 2012, 2015, 2018 Laboratoire de Recherche et
|
# Copyright (C) 2009, 2010, 2012, 2015, 2018, 2021 Laboratoire de
|
||||||
# Développement de l'Epita (LRDE).
|
# Recherche et Développement de l'Epita (LRDE).
|
||||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||||
# département Systemes Répartis Coopératifs (SRC), Université Pierre
|
# département Systemes Répartis Coopératifs (SRC), Université Pierre
|
||||||
# et Marie Curie.
|
# et Marie Curie.
|
||||||
|
|
@ -23,6 +23,12 @@
|
||||||
import spot
|
import spot
|
||||||
import sys
|
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')
|
a = spot.formula.ap('a')
|
||||||
b = spot.formula.ap('b')
|
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
|
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']"
|
assert str([str(x) for x in spot.formula('a &b & c')]) == "['a', 'b', 'c']"
|
||||||
|
|
|
||||||
|
|
@ -59,7 +59,7 @@ l = sorted(list(l0) + list(l1) + list(l2) + list(l3))
|
||||||
assert l == [0, 1, 2, 3, 4]
|
assert l == [0, 1, 2, 3, 4]
|
||||||
|
|
||||||
i = si.initial()
|
i = si.initial()
|
||||||
todo = {i}
|
todo = [i]
|
||||||
seen = {i}
|
seen = {i}
|
||||||
trans = []
|
trans = []
|
||||||
transi = []
|
transi = []
|
||||||
|
|
@ -72,13 +72,13 @@ while todo:
|
||||||
for s in si.succ(e):
|
for s in si.succ(e):
|
||||||
if s not in seen:
|
if s not in seen:
|
||||||
seen.add(s)
|
seen.add(s)
|
||||||
todo.add(s)
|
todo.append(s)
|
||||||
assert seen == {0, 1, 2, 3}
|
assert seen == {0, 1, 2, 3}
|
||||||
assert trans == [(0, 0), (0, 1), (0, 2), (0, 3),
|
assert trans == [(0, 0), (0, 1), (0, 2), (0, 3),
|
||||||
(2, 0), (2, 1), (2, 2), (2, 4),
|
(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),
|
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)
|
assert not spot.is_weak_automaton(a, si)
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -20,6 +20,18 @@
|
||||||
import spot
|
import spot
|
||||||
from sys import exit
|
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("""
|
aut = spot.automaton("""
|
||||||
HOA: v1
|
HOA: v1
|
||||||
States: 2
|
States: 2
|
||||||
|
|
@ -63,6 +75,10 @@ State: 0 "[0,1]" {0}
|
||||||
[t] 0
|
[t] 0
|
||||||
--END--"""
|
--END--"""
|
||||||
|
|
||||||
|
del aut
|
||||||
|
del aut2
|
||||||
|
gcollect()
|
||||||
|
|
||||||
aut = spot.translate('GF((p0 -> Gp0) R p1)')
|
aut = spot.translate('GF((p0 -> Gp0) R p1)')
|
||||||
|
|
||||||
daut = spot.tgba_determinize(aut, True)
|
daut = spot.tgba_determinize(aut, True)
|
||||||
|
|
@ -92,6 +108,10 @@ State: 2 "{₀[0]₀}{₁[1]₁}"
|
||||||
[0&1] 1 {2}
|
[0&1] 1 {2}
|
||||||
--END--"""
|
--END--"""
|
||||||
|
|
||||||
|
del aut
|
||||||
|
del daut
|
||||||
|
gcollect()
|
||||||
|
|
||||||
aut = spot.automaton("""
|
aut = spot.automaton("""
|
||||||
HOA: v1
|
HOA: v1
|
||||||
States: 2
|
States: 2
|
||||||
|
|
@ -175,6 +195,7 @@ assert b.num_states() == 3
|
||||||
b.set_init_state(1)
|
b.set_init_state(1)
|
||||||
b.purge_unreachable_states()
|
b.purge_unreachable_states()
|
||||||
b.copy_state_names_from(a)
|
b.copy_state_names_from(a)
|
||||||
|
|
||||||
assert b.to_str() == """HOA: v1
|
assert b.to_str() == """HOA: v1
|
||||||
States: 1
|
States: 1
|
||||||
Start: 0
|
Start: 0
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
# -*- mode: python; coding: utf-8 -*-
|
# -*- 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
|
# Développement de l'Epita
|
||||||
#
|
#
|
||||||
# This file is part of Spot, a model checking library.
|
# This file is part of Spot, a model checking library.
|
||||||
|
|
@ -19,6 +19,19 @@
|
||||||
|
|
||||||
import spot
|
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):
|
def incl(a, b):
|
||||||
return not b.intersects(spot.dualize(spot.tgba_determinize(a)))
|
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'])
|
aut, s = do_split('(FG !a) <-> (GF b)', ['a'], ['b'])
|
||||||
assert equiv(aut, spot.unsplit_2step(s))
|
assert equiv(aut, spot.unsplit_2step(s))
|
||||||
|
|
||||||
|
del aut
|
||||||
|
del s
|
||||||
|
gcollect()
|
||||||
|
|
||||||
aut, s = do_split('GFa && GFb', ['a'], ['b'])
|
aut, s = do_split('GFa && GFb', ['a'], ['b'])
|
||||||
assert equiv(aut, spot.unsplit_2step(s))
|
assert equiv(aut, spot.unsplit_2step(s))
|
||||||
assert str_diff("""HOA: v1
|
assert str_diff("""HOA: v1
|
||||||
|
|
@ -73,6 +90,10 @@ State: 2
|
||||||
[1] 0 {1}
|
[1] 0 {1}
|
||||||
--END--""", s.to_str() )
|
--END--""", s.to_str() )
|
||||||
|
|
||||||
|
del aut
|
||||||
|
del s
|
||||||
|
gcollect()
|
||||||
|
|
||||||
aut, s = do_split('! ((G (req -> (F ack))) && (G (go -> (F grant))))',
|
aut, s = do_split('! ((G (req -> (F ack))) && (G (go -> (F grant))))',
|
||||||
['go', 'req'], ['ack'])
|
['go', 'req'], ['ack'])
|
||||||
assert equiv(aut, spot.unsplit_2step(s))
|
assert equiv(aut, spot.unsplit_2step(s))
|
||||||
|
|
@ -113,6 +134,10 @@ assert equiv(aut, spot.unsplit_2step(s))
|
||||||
# [!3] 2
|
# [!3] 2
|
||||||
# --END--"""
|
# --END--"""
|
||||||
|
|
||||||
|
del aut
|
||||||
|
del s
|
||||||
|
gcollect()
|
||||||
|
|
||||||
aut, s = do_split('((G (((! g_0) || (! g_1)) && ((r_0 && (X r_1)) -> (F (g_0 \
|
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))',
|
&& g_1))))) && (G (r_0 -> F g_0))) && (G (r_1 -> F g_1))',
|
||||||
['r_0', 'r_1'], ['g_0', 'g_1'])
|
['r_0', 'r_1'], ['g_0', 'g_1'])
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
# -*- mode: python; coding: utf-8 -*-
|
# -*- mode: python; coding: utf-8 -*-
|
||||||
# Copyright (C) 2016-2018, 2020 Laboratoire de Recherche et Développement
|
# Copyright (C) 2016-2018, 2020-2021 Laboratoire de Recherche
|
||||||
# de l'Epita
|
# et Développement de l'Epita
|
||||||
#
|
#
|
||||||
# This file is part of Spot, a model checking library.
|
# This file is part of Spot, a model checking library.
|
||||||
#
|
#
|
||||||
|
|
@ -19,6 +19,12 @@
|
||||||
|
|
||||||
import spot
|
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.
|
# Test 1.
|
||||||
aut = spot.automaton("""
|
aut = spot.automaton("""
|
||||||
HOA: v1
|
HOA: v1
|
||||||
|
|
@ -365,7 +371,10 @@ State: 7
|
||||||
--END--"""
|
--END--"""
|
||||||
|
|
||||||
res = spot.remove_fin(aut)
|
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.
|
# Test 9.
|
||||||
aut = spot.automaton("""
|
aut = spot.automaton("""
|
||||||
|
|
@ -401,7 +410,10 @@ State: 1
|
||||||
--END--"""
|
--END--"""
|
||||||
|
|
||||||
res = spot.remove_fin(aut)
|
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.
|
# Test 10.
|
||||||
aut = spot.automaton("""
|
aut = spot.automaton("""
|
||||||
|
|
@ -440,7 +452,10 @@ State: 2 {0}
|
||||||
--END--"""
|
--END--"""
|
||||||
|
|
||||||
res = spot.remove_fin(aut)
|
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.
|
# Test 11.
|
||||||
aut = spot.automaton("""
|
aut = spot.automaton("""
|
||||||
|
|
@ -477,7 +492,10 @@ State: 1
|
||||||
--END--"""
|
--END--"""
|
||||||
|
|
||||||
res = spot.remove_fin(aut)
|
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
|
# 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
|
# being called. This is on purpose: the edge order should match exactly the
|
||||||
|
|
@ -499,7 +517,10 @@ State: 1
|
||||||
[!0] 0 {0}
|
[!0] 0 {0}
|
||||||
--END--"""
|
--END--"""
|
||||||
res = spot.rabin_to_buchi_if_realizable(aut)
|
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.
|
# Test 12.
|
||||||
aut = spot.automaton("""
|
aut = spot.automaton("""
|
||||||
|
|
@ -543,7 +564,10 @@ State: 3 {0}
|
||||||
--END--"""
|
--END--"""
|
||||||
|
|
||||||
res = spot.remove_fin(aut)
|
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.
|
# Test 13.
|
||||||
aut = spot.automaton("""
|
aut = spot.automaton("""
|
||||||
|
|
@ -590,7 +614,10 @@ State: 1
|
||||||
--END--"""
|
--END--"""
|
||||||
|
|
||||||
res = spot.remove_fin(aut)
|
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
|
# rabin_to_buchi_if_realizable() does not call merge_edges() on purpose: the
|
||||||
# edge order should match exactly the original automaton.
|
# edge order should match exactly the original automaton.
|
||||||
|
|
@ -616,7 +643,10 @@ State: 1
|
||||||
--END--"""
|
--END--"""
|
||||||
|
|
||||||
res = spot.rabin_to_buchi_if_realizable(aut)
|
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.
|
# Test 14.
|
||||||
aut = spot.automaton("""
|
aut = spot.automaton("""
|
||||||
|
|
@ -650,5 +680,8 @@ State: 1
|
||||||
--END--"""
|
--END--"""
|
||||||
|
|
||||||
res = spot.remove_fin(aut)
|
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
|
assert spot.rabin_to_buchi_if_realizable(aut) is None
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue