diff --git a/HACKING b/HACKING
index 8841b033c..c6e127a70 100644
--- a/HACKING
+++ b/HACKING
@@ -290,8 +290,8 @@ would understand with:
make check LOG_DRIVER=$PWD/tools/test-driver-teamcity
-Coding conventions
-==================
+C++ Coding conventions
+======================
Here some of the conventions we follow in Spot, so that the code looks
homogeneous. Please follow these strictly. Since this is free
@@ -682,3 +682,43 @@ Other style recommandations
* Always code as if the person who ends up maintaining your code is
a violent psychopath who knows where you live.
+
+
+Coding conventions for Python Tests
+===================================
+
+Unless you have some specific reason to write test cases in C++ (for
+instance do test some specific C++ constructions, or to use valgrind),
+prefer writing test cases in Python. Writing test cases in C++
+requires some compilation, which slows down the test suite. Doing the
+same test in Python is therefore faster, and it has the added benefit
+of ensuring that the Python bindings works.
+
+We have two types of Python tests: Python scripts or jupyter
+notebooks. Jupyter notebooks are usually used for a sequence of
+examples and comments that can also serve as part of the
+documentation. Such jupyter notebooks should be added to the list of
+code examples in doc/org/tut.org. Testing a notebook is done by the
+tests/python/ipnbdoctest.py scripts, which evaluate each cells, and
+checks that the obtainted result is equivalent to the result saved in
+the notebook. The process is a bit slow, so plain Python scripts
+should be prefered for most tests.
+
+If you do need a notebook to tests Jupyter-specific code but this
+notebook should not be shown in the documentation, use a filename
+starting with '_'.
+
+Tests written as Python scripts should follow the same convention as
+shell scripts: exit 0 for PASS, exit 77 for SKIP, and any other exit
+code for FAIL.
+
+Do not use assert() in those scripts, as (1) asserts can be disabled,
+and (2) they provide poor insights in case of failures. Instead do
+
+ from unittest import TestCase
+ tc = TestCase()
+
+and then use tc.assertTrue(...), tc.assertEqual(..., ...),
+tc.assertIn(..., ...), etc. In case of failures, those will print
+useful messages in the trace of the tests. For instance multiline
+strings that should have been equal will be presented with a diff.
diff --git a/tests/python/298.py b/tests/python/298.py
index d4865c440..89ddbdb0c 100644
--- a/tests/python/298.py
+++ b/tests/python/298.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -20,21 +20,23 @@
# Test for parts of Issue #298.
import spot
+from unittest import TestCase
+tc = TestCase()
a1 = spot.automaton("""genltl --dac=51 | ltl2tgba --med |""")
a1 = spot.degeneralize_tba(a1)
r1 = spot.tgba_determinize(a1, True, False, False)
-assert r1.num_sets() == 3
-assert a1.prop_complete().is_false();
+tc.assertEqual(r1.num_sets(), 3)
+tc.assertTrue(a1.prop_complete().is_false())
# This used to fail in 2.9.5 and earlier.
-assert r1.prop_complete().is_maybe();
-assert spot.is_complete(r1)
+tc.assertTrue(r1.prop_complete().is_maybe())
+tc.assertTrue(spot.is_complete(r1))
a2 = spot.automaton("""genltl --dac=51 | ltl2tgba --high |""")
a2 = spot.degeneralize_tba(a2)
r2 = spot.tgba_determinize(a2, True, False, False)
# This used to fail in 2.9.5 and earlier.
-assert r2.num_sets() == 3
-assert a2.prop_complete().is_false();
-assert r2.prop_complete().is_maybe();
-assert spot.is_complete(r2)
+tc.assertEqual(r2.num_sets(), 3)
+tc.assertTrue(a2.prop_complete().is_false())
+tc.assertTrue(r2.prop_complete().is_maybe())
+tc.assertTrue(spot.is_complete(r2))
diff --git a/tests/python/341.py b/tests/python/341.py
index 4c5937149..e828ab07c 100644
--- a/tests/python/341.py
+++ b/tests/python/341.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -19,7 +19,8 @@
import spot
from subprocess import _active
-
+from unittest import TestCase
+tc = TestCase()
def two_intersecting_automata():
"""return two random automata with a non-empty intersection"""
@@ -34,4 +35,4 @@ for i in range(5):
n = len(_active)
print(n, "active processes")
-assert(n == 0)
+tc.assertEqual(n, 0)
diff --git a/tests/python/471.py b/tests/python/471.py
index 6fee3a2d3..0fe180554 100644
--- a/tests/python/471.py
+++ b/tests/python/471.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2021 Laboratoire de Recherche et Développement de l'Epita
+# Copyright (C) 2021, 2022 Laboratoire de Recherche et Développement de l'Epita
# (LRDE).
#
# This file is part of Spot, a model checking library.
@@ -20,9 +20,12 @@
# Test for Issue #471.
import spot
+from unittest import TestCase
+tc = TestCase()
+
a = spot.translate('Fa')
a = spot.to_generalized_rabin(a, False)
r1 = a.intersecting_run(a)
r2 = a.accepting_run()
-assert str(r1) == str(r2)
-assert a.prop_weak().is_true()
+tc.assertEqual(str(r1), str(r2))
+tc.assertTrue(a.prop_weak().is_true())
diff --git a/tests/python/accparse2.py b/tests/python/accparse2.py
index 4e6eb1cb3..d9c7274a0 100644
--- a/tests/python/accparse2.py
+++ b/tests/python/accparse2.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2015, 2017-2018 Laboratoire de Recherche et Développement
+# Copyright (C) 2015, 2017-2018, 2022 Laboratoire de Recherche et Développement
# de l'Epita
#
# This file is part of Spot, a model checking library.
@@ -18,99 +18,101 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
a = spot.acc_cond(5)
a.set_acceptance(spot.acc_code('parity min odd 5'))
-assert(a.is_parity() == [True, False, True])
+tc.assertEqual(a.is_parity(), [True, False, True])
a.set_acceptance('parity max even 5')
-assert(a.is_parity() == [True, True, False])
+tc.assertEqual(a.is_parity(), [True, True, False])
a.set_acceptance('generalized-Buchi 5')
-assert(a.is_parity()[0] == False)
-assert(a.is_parity(True)[0] == False)
+tc.assertEqual(a.is_parity()[0], False)
+tc.assertEqual(a.is_parity(True)[0], False)
a.set_acceptance('Inf(4) | (Fin(3)&Inf(2)) | (Fin(3)&Fin(1)&Inf(0))')
-assert(a.is_parity()[0] == False)
-assert(a.is_parity(True) == [True, True, False])
+tc.assertEqual(a.is_parity()[0], False)
+tc.assertEqual(a.is_parity(True), [True, True, False])
-assert a.maybe_accepting([1, 2, 3], [0, 4]).is_true()
-assert a.maybe_accepting([0], []).is_true()
-assert a.maybe_accepting([0], [3]).is_false()
-assert a.maybe_accepting([0, 3], []).is_maybe()
-assert a.maybe_accepting([2, 3], [3]).is_false()
-assert a.maybe_accepting([2, 3], []).is_maybe()
-assert a.maybe_accepting([2], []).is_true()
-assert a.maybe_accepting([0, 1], []).is_maybe()
-assert a.maybe_accepting([0, 1], [1]).is_false()
+tc.assertTrue(a.maybe_accepting([1, 2, 3], [0, 4]).is_true())
+tc.assertTrue(a.maybe_accepting([0], []).is_true())
+tc.assertTrue(a.maybe_accepting([0], [3]).is_false())
+tc.assertTrue(a.maybe_accepting([0, 3], []).is_maybe())
+tc.assertTrue(a.maybe_accepting([2, 3], [3]).is_false())
+tc.assertTrue(a.maybe_accepting([2, 3], []).is_maybe())
+tc.assertTrue(a.maybe_accepting([2], []).is_true())
+tc.assertTrue(a.maybe_accepting([0, 1], []).is_maybe())
+tc.assertTrue(a.maybe_accepting([0, 1], [1]).is_false())
a.set_acceptance('Fin(0)|Fin(1)')
-assert a.maybe_accepting([0, 1], [1]).is_maybe()
-assert a.maybe_accepting([0, 1], [0, 1]).is_false()
-assert a.maybe_accepting([0], []).is_true()
-assert a.maybe_accepting([], [0]).is_true()
+tc.assertTrue(a.maybe_accepting([0, 1], [1]).is_maybe())
+tc.assertTrue(a.maybe_accepting([0, 1], [0, 1]).is_false())
+tc.assertTrue(a.maybe_accepting([0], []).is_true())
+tc.assertTrue(a.maybe_accepting([], [0]).is_true())
a = spot.acc_cond(0)
a.set_acceptance('all')
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == 0)
-assert(a.is_parity() == [True, True, True])
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), 0)
+tc.assertEqual(a.is_parity(), [True, True, True])
a.set_acceptance('none')
-assert(a.is_rabin() == 0)
-assert(a.is_streett() == -1)
-assert(a.is_parity() == [True, True, False])
+tc.assertEqual(a.is_rabin(), 0)
+tc.assertEqual(a.is_streett(), -1)
+tc.assertEqual(a.is_parity(), [True, True, False])
a = spot.acc_cond('(Fin(0)&Inf(1))')
-assert(a.is_rabin() == 1)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), 1)
+tc.assertEqual(a.is_streett(), -1)
a.set_acceptance('Inf(1)&Fin(0)')
-assert(a.is_rabin() == 1)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), 1)
+tc.assertEqual(a.is_streett(), -1)
a.set_acceptance('(Fin(0)|Inf(1))')
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == 1)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), 1)
a.set_acceptance('Inf(1)|Fin(0)')
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == 1)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), 1)
a = spot.acc_cond('(Fin(0)&Inf(1))|(Fin(2)&Inf(3))')
-assert(a.is_rabin() == 2)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), 2)
+tc.assertEqual(a.is_streett(), -1)
a.set_acceptance(spot.acc_code('(Inf(3)&Fin(2))|(Fin(0)&Inf(1))'))
-assert(a.is_rabin() == 2)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), 2)
+tc.assertEqual(a.is_streett(), -1)
a.set_acceptance(spot.acc_code('(Inf(2)&Fin(3))|(Fin(0)&Inf(1))'))
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), -1)
a.set_acceptance(spot.acc_code('(Inf(3)&Fin(2))|(Fin(2)&Inf(1))'))
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), -1)
a.set_acceptance(spot.acc_code('(Inf(1)&Fin(0))|(Fin(0)&Inf(1))'))
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), -1)
a.set_acceptance('(Fin(0)&Inf(1))|(Inf(1)&Fin(0))|(Inf(3)&Fin(2))')
-assert(a.is_rabin() == 2)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), 2)
+tc.assertEqual(a.is_streett(), -1)
a.set_acceptance('(Fin(0)|Inf(1))&(Fin(2)|Inf(3))')
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == 2)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), 2)
a.set_acceptance('(Inf(3)|Fin(2))&(Fin(0)|Inf(1))')
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == 2)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), 2)
a.set_acceptance('(Inf(2)|Fin(3))&(Fin(0)|Inf(1))')
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), -1)
a.set_acceptance('(Inf(3)|Fin(2))&(Fin(2)|Inf(1))')
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), -1)
a.set_acceptance('(Inf(1)|Fin(0))&(Fin(0)|Inf(1))')
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), -1)
a.set_acceptance('(Fin(0)|Inf(1))&(Inf(1)|Fin(0))&(Inf(3)|Fin(2))')
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == 2)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), 2)
a = spot.acc_code('Inf(0)&Inf(1)&Inf(3) | Fin(0)&(Fin(1)|Fin(3))')
u = a.symmetries()
-assert u[0] == 0
-assert u[1] == 1
-assert u[2] == 2
-assert u[3] == 1
+tc.assertEqual(u[0], 0)
+tc.assertEqual(u[1], 1)
+tc.assertEqual(u[2], 2)
+tc.assertEqual(u[3], 1)
diff --git a/tests/python/aiger.py b/tests/python/aiger.py
index 5148fef5f..f490465b0 100644
--- a/tests/python/aiger.py
+++ b/tests/python/aiger.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2021 Laboratoire de Recherche et
+# Copyright (C) 2021, 2022 Laboratoire de Recherche et
# Développement de l'Epita
#
# This file is part of Spot, a model checking library.
@@ -18,6 +18,8 @@
# along with this program. If not, see .
import spot, buddy
+from unittest import TestCase
+tc = TestCase()
strats = (("""HOA: v1
States: 4
@@ -3346,7 +3348,7 @@ for strat_string, (ins_str, outs_str) in strats:
print(f"Mode is {m+ss+ddx+uud}")
print(f"""Strat is \n{strat_s.to_str("hoa")}""")
print(f"""Aig as aut is \n{strat2_s.to_str("hoa")}""")
- assert 0
+ raise AssertionError("not a specialization")
# Check stepwise simulation
@@ -3386,7 +3388,7 @@ for (i, e_latch) in zip(ins, exp_latches):
# Variable names
-assert(spot.aiger_circuit("""aag 2 2 0 2 0
+tc.assertEqual(spot.aiger_circuit("""aag 2 2 0 2 0
2
4
2
@@ -3394,9 +3396,9 @@ assert(spot.aiger_circuit("""aag 2 2 0 2 0
i0 a
i1 b c
c
-""").to_str() == 'aag 2 2 0 2 0\n2\n4\n2\n1\ni0 a\ni1 b c\no0 o0\no1 o1')
+""").to_str(), 'aag 2 2 0 2 0\n2\n4\n2\n1\ni0 a\ni1 b c\no0 o0\no1 o1')
-assert(spot.aiger_circuit("""aag 2 2 0 2 0
+tc.assertEqual(spot.aiger_circuit("""aag 2 2 0 2 0
2
4
2
@@ -3404,7 +3406,7 @@ assert(spot.aiger_circuit("""aag 2 2 0 2 0
o0 x
o1 y
c
-""").to_str() == 'aag 2 2 0 2 0\n2\n4\n2\n1\ni0 i0\ni1 i1\no0 x\no1 y')
+""").to_str(), 'aag 2 2 0 2 0\n2\n4\n2\n1\ni0 i0\ni1 i1\no0 x\no1 y')
def report_missing_exception():
@@ -3415,7 +3417,7 @@ try:
0
""")
except SyntaxError as e:
- assert str(e) == "\n:1: invalid header line"
+ tc.assertEqual(str(e), "\n:1: invalid header line")
else:
report_missing_exception()
@@ -3423,14 +3425,15 @@ try:
spot.aiger_circuit("""aag 2 2 3 2 0
""")
except SyntaxError as e:
- assert str(e) == "\n:1: more variables than indicated by max var"
+ tc.assertEqual(str(e),
+ "\n:1: more variables than indicated by max var")
else:
report_missing_exception()
try:
spot.aiger_circuit("""aag 2 2 0 2 0\n""")
except SyntaxError as e:
- assert str(e) == "\n:2: expecting input number 2"
+ tc.assertEqual(str(e), "\n:2: expecting input number 2")
else:
report_missing_exception()
@@ -3439,7 +3442,7 @@ try:
3
""")
except SyntaxError as e:
- assert str(e) == "\n:2: expecting input number 2"
+ tc.assertEqual(str(e), "\n:2: expecting input number 2")
else:
report_missing_exception()
@@ -3448,7 +3451,7 @@ try:
3 4 5
""")
except SyntaxError as e:
- assert str(e) == "\n:2: invalid format for an input"
+ tc.assertEqual(str(e), "\n:2: invalid format for an input")
else:
report_missing_exception()
@@ -3457,7 +3460,7 @@ try:
2
""")
except SyntaxError as e:
- assert str(e) == "\n:3: expecting input number 4"
+ tc.assertEqual(str(e), "\n:3: expecting input number 4")
else:
report_missing_exception()
@@ -3468,7 +3471,7 @@ try:
1
""")
except SyntaxError as e:
- assert str(e) == "\n:4: invalid format for a latch"
+ tc.assertEqual(str(e), "\n:4: invalid format for a latch")
else:
report_missing_exception()
@@ -3479,7 +3482,7 @@ try:
1 1
""")
except SyntaxError as e:
- assert str(e) == "\n:4: expecting latch number 6"
+ tc.assertEqual(str(e), "\n:4: expecting latch number 6")
else:
report_missing_exception()
@@ -3490,7 +3493,7 @@ try:
6 1
""")
except SyntaxError as e:
- assert str(e) == "\n:5: expecting latch number 8"
+ tc.assertEqual(str(e), "\n:5: expecting latch number 8")
else:
report_missing_exception()
@@ -3502,7 +3505,7 @@ try:
8 7
""")
except SyntaxError as e:
- assert str(e) == "\n:6: expecting an output"
+ tc.assertEqual(str(e), "\n:6: expecting an output")
else:
report_missing_exception()
@@ -3515,7 +3518,7 @@ try:
9 9 9
""")
except SyntaxError as e:
- assert str(e) == "\n:6: invalid format for an output"
+ tc.assertEqual(str(e), "\n:6: invalid format for an output")
else:
report_missing_exception()
@@ -3528,7 +3531,7 @@ try:
9 9 9
""")
except SyntaxError as e:
- assert str(e) == "\n:6: invalid format for an output"
+ tc.assertEqual(str(e), "\n:6: invalid format for an output")
else:
report_missing_exception()
@@ -3541,7 +3544,7 @@ try:
9
""")
except SyntaxError as e:
- assert str(e) == "\n:7: expecting AND gate number 10"
+ tc.assertEqual(str(e), "\n:7: expecting AND gate number 10")
else:
report_missing_exception()
@@ -3555,7 +3558,7 @@ try:
10 3 8 9
""")
except SyntaxError as e:
- assert str(e) == "\n:7: invalid format for an AND gate"
+ tc.assertEqual(str(e), "\n:7: invalid format for an AND gate")
else:
report_missing_exception()
@@ -3569,7 +3572,7 @@ try:
10 3
""")
except SyntaxError as e:
- assert str(e) == "\n:7: invalid format for an AND gate"
+ tc.assertEqual(str(e), "\n:7: invalid format for an AND gate")
else:
report_missing_exception()
@@ -3583,7 +3586,7 @@ try:
10 3 8
""")
except SyntaxError as e:
- assert str(e) == "\n:8: expecting AND gate number 12"
+ tc.assertEqual(str(e), "\n:8: expecting AND gate number 12")
else:
report_missing_exception()
@@ -3599,7 +3602,7 @@ try:
i0
""")
except SyntaxError as e:
- assert str(e) == "\n:9: could not parse as input name"
+ tc.assertEqual(str(e), "\n:9: could not parse as input name")
else:
report_missing_exception()
@@ -3616,7 +3619,7 @@ i0 foo
i3 bar
""")
except SyntaxError as e:
- assert str(e) == "\n:10: value 3 exceeds input count"
+ tc.assertEqual(str(e), "\n:10: value 3 exceeds input count")
else:
report_missing_exception()
@@ -3633,7 +3636,7 @@ i1 bar
i0 foo
""")
except SyntaxError as e:
- assert str(e) == "\n:9: expecting name for input 0"
+ tc.assertEqual(str(e), "\n:9: expecting name for input 0")
else:
report_missing_exception()
@@ -3650,8 +3653,8 @@ i0 name with spaces
i1 name with spaces
""")
except SyntaxError as e:
- assert str(e) == \
- "\n:10: name 'name with spaces' already used"
+ tc.assertEqual(str(e), \
+ "\n:10: name 'name with spaces' already used")
else:
report_missing_exception()
@@ -3669,7 +3672,7 @@ i1 bar
o0
""")
except SyntaxError as e:
- assert str(e) == "\n:11: could not parse as output name"
+ tc.assertEqual(str(e), "\n:11: could not parse as output name")
else:
report_missing_exception()
@@ -3689,7 +3692,7 @@ o1 hmm
o0 foo bar baz
""")
except SyntaxError as e:
- assert str(e) == "\n:12: expecting name for output 0"
+ tc.assertEqual(str(e), "\n:12: expecting name for output 0")
else:
report_missing_exception()
@@ -3709,7 +3712,7 @@ o0 hmm
o2 foo bar baz
""")
except SyntaxError as e:
- assert str(e) == "\n:13: value 2 exceeds output count"
+ tc.assertEqual(str(e), "\n:13: value 2 exceeds output count")
else:
report_missing_exception()
@@ -3729,7 +3732,7 @@ o0 foo
o1 foo
""")
except SyntaxError as e:
- assert str(e) == "\n:13: name 'foo' already used"
+ tc.assertEqual(str(e), "\n:13: name 'foo' already used")
else:
report_missing_exception()
@@ -3749,7 +3752,7 @@ o0 foo
o1 bar
""")
except SyntaxError as e:
- assert str(e) == "\n:13: name 'bar' already used"
+ tc.assertEqual(str(e), "\n:13: name 'bar' already used")
else:
report_missing_exception()
@@ -3770,7 +3773,7 @@ o1 baz
this is a bug
""")
except SyntaxError as e:
- assert str(e) == "\n:14: unsupported line type"
+ tc.assertEqual(str(e), "\n:14: unsupported line type")
else:
report_missing_exception()
@@ -3791,8 +3794,8 @@ c
this is not a bug
""")
except SyntaxError as e:
- assert str(e) == \
- "\n:10: either all or none of the inputs should be named"
+ tc.assertEqual(str(e), \
+ "\n:10: either all or none of the inputs should be named")
else:
report_missing_exception()
@@ -3815,8 +3818,8 @@ c
this is not a bug
""")
except SyntaxError as e:
- assert str(e) == \
- "\n:11-12: either all or none of the inputs should be named"
+ tc.assertEqual(str(e), \
+ "\n:11-12: either all or none of the inputs should be named")
else:
report_missing_exception()
@@ -3841,8 +3844,8 @@ c
this is not a bug
""")
except SyntaxError as e:
- assert str(e) == \
- "\n:14-16: either all or none of the outputs should be named"
+ tc.assertEqual(str(e), \
+ "\n:14-16: either all or none of the outputs should be named")
else:
report_missing_exception()
@@ -3866,4 +3869,4 @@ o2 bar
c
this is not a bug
""").to_str()
-assert x == spot.aiger_circuit(x).to_str()
+tc.assertEqual(x, spot.aiger_circuit(x).to_str())
diff --git a/tests/python/aliases.py b/tests/python/aliases.py
index 6f861a880..40dd4d0ec 100644
--- a/tests/python/aliases.py
+++ b/tests/python/aliases.py
@@ -20,6 +20,8 @@
# Test for parts of Issue #497.
import spot
+from unittest import TestCase
+tc = TestCase()
aut = spot.automaton("""
HOA: v1
@@ -63,11 +65,11 @@ State: 0
--END--""")
s = aut.to_str('hoa')
aut2 = spot.automaton(s)
-assert aut.equivalent_to(aut2)
+tc.assertTrue(aut.equivalent_to(aut2))
s2 = aut.to_str('hoa')
-assert s == s2
+tc.assertEqual(s, s2)
-assert s == """HOA: v1
+tc.assertEqual(s, """HOA: v1
States: 1
Start: 0
AP: 3 "x" "y" "z"
@@ -105,7 +107,7 @@ State: 0
[@a&2 | @p1&@p0&2] 0
[@a&2] 0
[@p0&2 | @p1&2] 0
---END--"""
+--END--""")
# Check what happens to aliases when an AP has been removed, but
# the aliases have been preserved...
@@ -115,7 +117,7 @@ aut3 = rem.strip(aut)
spot.set_aliases(aut3, spot.get_aliases(aut))
s2 = aut3.to_str('hoa')
# Aliases based on "x" should have disappeared.
-assert(s2 == """HOA: v1
+tc.assertEqual(s2, """HOA: v1
States: 1
Start: 0
AP: 2 "y" "z"
diff --git a/tests/python/alternating.py b/tests/python/alternating.py
index 7b3a5d713..5b38ca378 100755
--- a/tests/python/alternating.py
+++ b/tests/python/alternating.py
@@ -1,7 +1,7 @@
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016, 2017, 2021 Laboratoire de Recherche et Développement de
-# l'EPITA.
+# Copyright (C) 2016-2017, 2021-2022 Laboratoire de Recherche
+# et Développement de l'EPITA.
#
# This file is part of Spot, a model checking library.
#
@@ -20,6 +20,8 @@
import spot
import buddy
+from unittest import TestCase
+tc = TestCase()
aut = spot.make_twa_graph(spot._bdd_dict)
@@ -38,9 +40,8 @@ aut.new_edge(2, 2, p1 | p2)
tr = [(s, [[x for x in aut.univ_dests(i)] for i in aut.out(s)])
for s in range(3)]
-print(tr)
-assert [(0, [[1, 2], [0, 1]]), (1, [[0, 2, 1]]), (2, [[2]])] == tr
-assert not aut.is_existential()
+tc.assertEqual([(0, [[1, 2], [0, 1]]), (1, [[0, 2, 1]]), (2, [[2]])], tr)
+tc.assertFalse(aut.is_existential())
received = False
try:
@@ -49,11 +50,10 @@ try:
pass
except RuntimeError:
received = True
-assert received
+tc.assertTrue(received)
h = aut.to_str('hoa')
-print(h)
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
States: 3
Start: 0
AP: 2 "p1" "p2"
@@ -68,22 +68,20 @@ State: 1
[0&1] 0&2&1
State: 2
[0 | 1] 2
---END--"""
+--END--""")
aut2 = spot.automaton(h)
h2 = aut2.to_str('hoa')
-print(h2)
-assert h != h2
+tc.assertNotEqual(h, h2)
# This will sort destination groups
aut.merge_univ_dests()
h = aut.to_str('hoa')
-assert h == h2
+tc.assertEqual(h, h2)
aut2.set_univ_init_state([0, 1])
h3 = aut2.to_str('hoa')
-print(h3)
-assert h3 == """HOA: v1
+tc.assertEqual(h3, """HOA: v1
States: 3
Start: 0&1
AP: 2 "p1" "p2"
@@ -98,23 +96,22 @@ State: 1
[0&1] 0&1&2
State: 2
[0 | 1] 2
---END--"""
+--END--""")
st = spot.states_and(aut, [0, 2])
st2 = spot.states_and(aut, [1, st])
st3 = spot.states_and(aut, [0, 1, 2])
-assert (st, st2, st3) == (3, 4, 5)
+tc.assertEqual((st, st2, st3), (3, 4, 5))
received = False
try:
st4 = spot.states_and(aut, [])
except RuntimeError:
received = True
-assert received
+tc.assertTrue(received)
h = aut.to_str('hoa')
-print(h)
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
States: 6
Start: 0
AP: 2 "p1" "p2"
@@ -136,11 +133,10 @@ State: 4
[0&1] 0&1&2
State: 5
[0&1] 0&1&2
---END--"""
+--END--""")
h = spot.split_edges(aut).to_str('hoa')
-print(h)
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
States: 6
Start: 0
AP: 2 "p1" "p2"
@@ -168,7 +164,7 @@ State: 4
[0&1] 0&1&2
State: 5
[0&1] 0&1&2
---END--"""
+--END--""")
# remove_univ_otf
@@ -206,11 +202,11 @@ State: 2
--END--"""
desalt = spot.remove_univ_otf(aut)
-assert(desalt.to_str('hoa') == out)
+tc.assertEqual(desalt.to_str('hoa'), out)
-assert aut.num_states() == 3
-assert aut.num_edges() == 3
+tc.assertEqual(aut.num_states(), 3)
+tc.assertEqual(aut.num_edges(), 3)
aut.edge_storage(3).cond = buddy.bddfalse
aut.purge_dead_states()
-assert aut.num_states() == 1
-assert aut.num_edges() == 0
+tc.assertEqual(aut.num_states(), 1)
+tc.assertEqual(aut.num_edges(), 0)
diff --git a/tests/python/bdddict.py b/tests/python/bdddict.py
index d6222b58f..0172bd050 100644
--- a/tests/python/bdddict.py
+++ b/tests/python/bdddict.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2019, 2021 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2019, 2021, 2022 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -33,6 +33,8 @@ else:
gc.collect()
import spot
+from unittest import TestCase
+tc = TestCase()
class bdd_holder:
@@ -64,7 +66,7 @@ class bdd_holder3:
def check_ok():
- assert type(bdict.varnum(spot.formula.ap("a"))) is int
+ tc.assertIs(type(bdict.varnum(spot.formula.ap("a"))), int)
def check_nok():
@@ -123,7 +125,7 @@ debug("h2")
h3 = bdd_holder3(h2)
var = bdict.register_anonymous_variables(1, h3)
debug("h3")
-assert var == 2
+tc.assertEqual(var, 2)
del h2
gcollect()
debug("-h2")
diff --git a/tests/python/bdditer.py b/tests/python/bdditer.py
index 3d3bb7894..95cc441b3 100644
--- a/tests/python/bdditer.py
+++ b/tests/python/bdditer.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017, 2018, 2021 Laboratoire de Recherche et
+# Copyright (C) 2017, 2018, 2021, 2022 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@@ -24,11 +24,13 @@
import spot
import buddy
import sys
+from unittest import TestCase
+tc = TestCase()
run = spot.translate('a & !b').accepting_run()
b = run.prefix[0].label
c = buddy.bdd_satone(b)
-assert c != buddy.bddfalse
+tc.assertNotEqual(c, buddy.bddfalse)
res = []
while c != buddy.bddtrue:
var = buddy.bdd_var(c)
@@ -40,23 +42,23 @@ while c != buddy.bddtrue:
res.append(var)
c = h
-assert res == [0, -1]
+tc.assertEqual(res, [0, -1])
res2 = []
for i in run.aut.ap():
res2.append((str(i), run.aut.register_ap(i)))
-assert str(res2) == "[('a', 0), ('b', 1)]"
+tc.assertEqual(str(res2), "[('a', 0), ('b', 1)]")
f = spot.bdd_to_formula(b)
-assert f._is(spot.op_And)
-assert f[0]._is(spot.op_ap)
-assert f[1]._is(spot.op_Not)
-assert f[1][0]._is(spot.op_ap)
-assert str(f) == 'a & !b'
+tc.assertTrue(f._is(spot.op_And))
+tc.assertTrue(f[0]._is(spot.op_ap))
+tc.assertTrue(f[1]._is(spot.op_Not))
+tc.assertTrue(f[1][0]._is(spot.op_ap))
+tc.assertEqual(str(f), 'a & !b')
try:
f = spot.bdd_to_formula(b, spot.make_bdd_dict())
sys.exit(2)
except RuntimeError as e:
- assert "not in the dictionary" in str(e)
+ tc.assertIn("not in the dictionary", str(e))
diff --git a/tests/python/bugdet.py b/tests/python/bugdet.py
index 9e06e0db3..19434c967 100644
--- a/tests/python/bugdet.py
+++ b/tests/python/bugdet.py
@@ -1,7 +1,7 @@
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016 Laboratoire de Recherche et Développement de
-# l'EPITA.
+# Copyright (C) 2016, 2022 Laboratoire de Recherche et Développement
+# de l'EPITA.
#
# This file is part of Spot, a model checking library.
#
@@ -22,6 +22,8 @@
# sent to the Spot mailing list on 2016-10-31.
import spot
+from unittest import TestCase
+tc = TestCase()
a = spot.automaton("""
HOA: v1
@@ -80,12 +82,12 @@ State: 7 {0}
# was fine.
print("use_simulation=True")
b1 = spot.tgba_determinize(b, False, True, True, True)
-assert b1.num_states() == 5
+tc.assertEqual(b1.num_states(), 5)
b1 = spot.remove_fin(spot.dualize(b1))
-assert not a.intersects(b1)
+tc.assertFalse(a.intersects(b1))
print("\nuse_simulation=False")
b2 = spot.tgba_determinize(b, False, True, False, True)
-assert b2.num_states() == 5
+tc.assertEqual(b2.num_states(), 5)
b2 = spot.remove_fin(spot.dualize(b2))
-assert not a.intersects(b2)
+tc.assertFalse(a.intersects(b2))
diff --git a/tests/python/complement_semidet.py b/tests/python/complement_semidet.py
index 5ab4557bc..da06749a3 100644
--- a/tests/python/complement_semidet.py
+++ b/tests/python/complement_semidet.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018 Laboratoire de Recherche et Développement de
+# Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@@ -19,6 +19,8 @@
import spot
import buddy
+from unittest import TestCase
+tc = TestCase()
def complement(aut):
@@ -35,4 +37,4 @@ for aut in spot.automata(
comp = complement(aut)
semidet_comp = spot.complement_semidet(aut, True)
- assert(comp.equivalent_to(semidet_comp))
+ tc.assertTrue(comp.equivalent_to(semidet_comp))
diff --git a/tests/python/declenv.py b/tests/python/declenv.py
index 868f6ca1d..3ab47736b 100644
--- a/tests/python/declenv.py
+++ b/tests/python/declenv.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -21,6 +21,8 @@
# This file tests various error conditions on the twa API
import spot
+from unittest import TestCase
+tc = TestCase()
env = spot.declarative_environment()
env.declare("a")
@@ -28,26 +30,27 @@ env.declare("b")
f1a = spot.parse_infix_psl("a U b")
f1b = spot.parse_infix_psl("a U b", env)
-assert not f1a.errors
-assert not f1b.errors
+tc.assertFalse(f1a.errors)
+tc.assertFalse(f1b.errors)
+
# In the past, atomic propositions requires via different environments were
# never equal, but this feature was never used and we changed that in Spot 2.0
# for the sake of simplicity.
-assert f1a.f == f1b.f
+tc.assertEqual(f1a.f, f1b.f)
f2 = spot.parse_infix_psl("(a U b) U c", env)
-assert f2.errors
+tc.assertTrue(f2.errors)
ostr = spot.ostringstream()
f2.format_errors(ostr)
err = ostr.str()
-assert "unknown atomic proposition `c'" in err
+tc.assertIn("unknown atomic proposition `c'", err)
f3 = spot.parse_prefix_ltl("R a d", env)
-assert f3.errors
+tc.assertTrue(f3.errors)
ostr = spot.ostringstream()
f3.format_errors(ostr)
err = ostr.str()
-assert "unknown atomic proposition `d'" in err
+tc.assertIn("unknown atomic proposition `d'", err)
f4 = spot.parse_prefix_ltl("R a b", env)
-assert not f4.errors
+tc.assertFalse(f4.errors)
diff --git a/tests/python/decompose_scc.py b/tests/python/decompose_scc.py
index 5f6ad46cb..47741fb72 100644
--- a/tests/python/decompose_scc.py
+++ b/tests/python/decompose_scc.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017, 2021 Laboratoire de Recherche et
+# Copyright (C) 2017, 2021, 2022 Laboratoire de Recherche et
# Développement de l'Epita
#
# This file is part of Spot, a model checking library.
@@ -18,6 +18,8 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
aut = spot.translate('(Ga -> Gb) W c')
si = spot.scc_info(aut)
@@ -26,10 +28,10 @@ si = spot.scc_info(aut)
# if the generation of the automaton changes, so just scan
# for it.
rej = [j for j in range(si.scc_count()) if si.is_rejecting_scc(j)]
-assert len(rej) == 1
+tc.assertEqual(len(rej), 1)
s = spot.decompose_scc(si, rej[0]).to_str('hoa', '1.1')
-assert (s == """HOA: v1.1
+tc.assertEqual(s, """HOA: v1.1
States: 3
Start: 0
AP: 3 "b" "a" "c"
@@ -56,7 +58,8 @@ except RuntimeError:
else:
raise AssertionError
-assert (spot.decompose_scc(si, 0, True).to_str('hoa', '1.1') == """HOA: v1.1
+tc.assertEqual(spot.decompose_scc(si, 0, True).to_str('hoa', '1.1'),
+"""HOA: v1.1
States: 4
Start: 0
AP: 3 "b" "a" "c"
@@ -81,7 +84,8 @@ State: 3
[1] 3
--END--""")
-assert (spot.decompose_scc(si, 2, True).to_str('hoa', '1.1') == """HOA: v1.1
+tc.assertEqual(spot.decompose_scc(si, 2, True).to_str('hoa', '1.1'),
+"""HOA: v1.1
States: 2
Start: 0
AP: 3 "b" "a" "c"
@@ -103,4 +107,4 @@ try:
except RuntimeError:
pass
else:
- raise AssertionError
+ raise AssertionError("missing exception")
diff --git a/tests/python/det.py b/tests/python/det.py
index 03f07c096..36fa31ff3 100644
--- a/tests/python/det.py
+++ b/tests/python/det.py
@@ -1,6 +1,6 @@
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2021 Laboratoire de Recherche et Développement de
+# Copyright (C) 2021, 2022 Laboratoire de Recherche et Développement de
# l'EPITA.
#
# This file is part of Spot, a model checking library.
@@ -19,6 +19,8 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
a = spot.translate('FGa | FGb')
@@ -26,10 +28,10 @@ a = spot.translate('FGa | FGb')
d = spot.tgba_determinize(a, False, True, True, True,
None, -1, True)
cld = list(d.get_original_classes())
-assert [0, 1, 2, 3, 3] == cld
+tc.assertEqual([0, 1, 2, 3, 3], cld)
e = spot.sbacc(d)
-assert e.get_original_states() is None
+tc.assertIsNone(e.get_original_states())
cle = list(e.get_original_classes())
-assert len(cle) == e.num_states()
-assert set(cle) == set(cld)
+tc.assertEqual(len(cle), e.num_states())
+tc.assertEqual(set(cle), set(cld))
diff --git a/tests/python/dualize.py b/tests/python/dualize.py
index 81d2a2b23..b870e1e5e 100755
--- a/tests/python/dualize.py
+++ b/tests/python/dualize.py
@@ -1,7 +1,7 @@
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017-2019, 2021 Laboratoire de Recherche et Développement de
-# l'EPITA.
+# Copyright (C) 2017-2019, 2021-2022 Laboratoire de Recherche et
+# Développement de l'EPITA.
#
# This file is part of Spot, a model checking library.
#
@@ -20,6 +20,8 @@
import spot
import buddy
+from unittest import TestCase
+tc = TestCase()
match_strings = [('is_buchi', 'is_co_buchi'),
('is_generalized_buchi', 'is_generalized_co_buchi'),
@@ -79,19 +81,19 @@ def test_aut(aut, d=None):
def test_complement(aut):
- assert aut.is_deterministic()
+ tc.assertTrue(aut.is_deterministic())
d = spot.dualize(aut)
s = spot.product_or(aut, d)
- assert spot.dualize(s).is_empty()
+ tc.assertTrue(spot.dualize(s).is_empty())
def test_assert(a, d=None):
t = test_aut(a, d)
if not t[0]:
- print (t[1])
- print (a.to_str('hoa'))
- print (spot.dualize(a).to_str('hoa'))
- assert False
+ print(t[1])
+ print(a.to_str('hoa'))
+ print(spot.dualize(a).to_str('hoa'))
+ tc.assertTrue(t[0])
aut = spot.translate('a')
@@ -101,7 +103,7 @@ test_assert(aut)
dual = spot.dualize(aut)
h = dual.to_str('hoa')
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
States: 3
Start: 1
AP: 1 "a"
@@ -117,7 +119,7 @@ State: 1
[!0] 2
State: 2
[t] 2
---END--"""
+--END--""")
aut = spot.automaton("""
HOA: v1
@@ -141,7 +143,7 @@ test_assert(aut)
dual = spot.dualize(aut)
h = dual.to_str('hoa')
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
States: 4
Start: 0
AP: 2 "a" "b"
@@ -161,7 +163,7 @@ State: 2 {0}
[!1] 3
State: 3
[t] 3
---END--"""
+--END--""")
aut = spot.automaton("""
HOA: v1
@@ -186,7 +188,7 @@ test_assert(aut)
dual = spot.dualize(aut)
h = dual.to_str('hoa')
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
States: 2
Start: 1
AP: 2 "a" "b"
@@ -198,7 +200,7 @@ State: 0
[t] 0
State: 1
[!0 | !1] 0
---END--"""
+--END--""")
aut = spot.automaton("""
HOA: v1
@@ -219,10 +221,10 @@ State: 3 {1}
--END--""")
dual = spot.dualize(aut)
-assert dualtype(aut, dual)
+tc.assertTrue(dualtype(aut, dual))
h = dual.to_str('hoa')
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
States: 2
Start: 1
AP: 2 "a" "b"
@@ -234,7 +236,7 @@ State: 0
[t] 0
State: 1
[!0 | !1] 0
---END--"""
+--END--""")
aut = spot.automaton("""
HOA: v1
@@ -255,10 +257,10 @@ State: 3 {0}
--END--""")
dual = spot.dualize(aut)
-assert dualtype(aut, dual)
+tc.assertTrue(dualtype(aut, dual))
h = dual.to_str('hoa')
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
States: 5
Start: 0
AP: 2 "a" "b"
@@ -280,7 +282,7 @@ State: 3 {0}
[t] 3
State: 4
[t] 4
---END--"""
+--END--""")
aut = spot.automaton("""
HOA: v1
@@ -302,10 +304,10 @@ State: 2
--END--""")
dual = spot.dualize(aut)
-assert dualtype(aut, dual)
+tc.assertTrue(dualtype(aut, dual))
h = dual.to_str('hoa')
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
States: 4
Start: 0
AP: 2 "a" "b"
@@ -327,7 +329,7 @@ State: 2
[!0&!1] 0&2
State: 3
[t] 3
---END--"""
+--END--""")
aut = spot.automaton("""
HOA: v1
@@ -348,10 +350,10 @@ State: 2
--END--""")
dual = spot.dualize(aut)
-assert dualtype(aut, dual)
+tc.assertTrue(dualtype(aut, dual))
h = dual.to_str('hoa')
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
States: 1
Start: 0
AP: 1 "a"
@@ -362,7 +364,7 @@ properties: deterministic terminal
--BODY--
State: 0
[t] 0
---END--"""
+--END--""")
aut = spot.automaton("""
HOA: v1
@@ -382,10 +384,10 @@ State: 2
--END--""")
dual = spot.dualize(aut)
-assert dualtype(aut, dual)
+tc.assertTrue(dualtype(aut, dual))
h = dual.to_str('hoa')
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
States: 1
Start: 0
AP: 1 "a"
@@ -396,7 +398,7 @@ properties: deterministic terminal
--BODY--
State: 0
[t] 0
---END--"""
+--END--""")
aut = spot.automaton("""
HOA: v1
@@ -419,7 +421,7 @@ State: 2
dual = spot.dualize(aut)
h = dual.to_str('hoa')
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
@@ -435,7 +437,7 @@ State: 1 {0}
[t] 1
State: 2
[t] 2
---END--"""
+--END--""")
aut = spot.automaton("""
HOA: v1
@@ -456,10 +458,10 @@ State: 2
dual = spot.dualize(aut)
-assert dualtype(aut, dual)
+tc.assertTrue(dualtype(aut, dual))
h = dual.to_str('hoa')
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
States: 2
Start: 0
AP: 1 "a"
@@ -471,7 +473,7 @@ State: 0
[!0] 1
State: 1 {0}
[t] 1
---END--"""
+--END--""")
aut = spot.automaton("""
HOA: v1
@@ -495,10 +497,10 @@ State: 3 {0}
--END--""")
dual = spot.dualize(aut)
-assert dualtype(aut, dual)
+tc.assertTrue(dualtype(aut, dual))
h = dual.to_str('hoa')
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
States: 3
Start: 0
AP: 1 "a"
@@ -515,7 +517,7 @@ State: 1
[0] 2
State: 2 {0}
[t] 2
---END--"""
+--END--""")
aut = spot.automaton("""
HOA: v1
@@ -536,10 +538,10 @@ State: 2
--END--""")
dual = spot.dualize(aut)
-assert dualtype(aut, dual)
+tc.assertTrue(dualtype(aut, dual))
h = dual.to_str('hoa')
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
States: 3
Start: 0
AP: 1 "a"
@@ -555,14 +557,14 @@ State: 1 {0}
[t] 0
State: 2 {1}
[t] 0
---END--"""
+--END--""")
aut = spot.translate('G!a R XFb')
test_assert(aut)
dual = spot.dualize(aut)
h = dual.to_str('hoa')
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
States: 5
Start: 0
AP: 2 "a" "b"
@@ -589,7 +591,7 @@ State: 3 {0}
[0] 4
State: 4
[t] 4
---END--"""
+--END--""")
opts = spot.option_map()
opts.set('output', spot.randltlgenerator.LTL)
diff --git a/tests/python/ecfalse.py b/tests/python/ecfalse.py
index 36301914b..ccbaa2693 100644
--- a/tests/python/ecfalse.py
+++ b/tests/python/ecfalse.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -19,6 +19,8 @@
import spot
from buddy import bddfalse, bddtrue
+from unittest import TestCase
+tc = TestCase()
a = spot.automaton("""
HOA: v1
@@ -43,8 +45,8 @@ for e in a.out(1):
if e.dst == 0:
e.cond = bddfalse
-assert a.accepting_run() is None
-assert a.is_empty()
+tc.assertIsNone(a.accepting_run())
+tc.assertTrue(a.is_empty())
for name in ['SE05', 'CVWY90', 'GV04', 'Cou99(shy)', 'Cou99', 'Tau03']:
print(name)
@@ -52,13 +54,13 @@ for name in ['SE05', 'CVWY90', 'GV04', 'Cou99(shy)', 'Cou99', 'Tau03']:
res = ec.check()
if res is not None:
print(res.accepting_run())
- assert res is None
+ tc.assertIsNone(res)
si = spot.scc_info(a)
-assert si.scc_count() == 1 # only one accessible SCC
+tc.assertEqual(si.scc_count(), 1) # only one accessible SCC
a.set_init_state(0)
si = spot.scc_info(a)
-assert si.scc_count() == 2
+tc.assertEqual(si.scc_count(), 2)
a = spot.automaton("""HOA: v1 States: 11 Start: 0 AP: 2 "a" "b" Acceptance: 8
(Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & ((Fin(4) & Inf(5)) | (Fin(6) & Inf(7)))
@@ -71,16 +73,16 @@ State: 5 State: 6 State: 7 [!0&!1] 1 {4 6 7} [!0&!1] 2 {5 6} State: 8 [!0&!1] 2
{4} State: 9 [!0&!1] 2 {0 4} [!0&!1] 4 {3 4} State: 10 --END-- """)
r = a.accepting_run()
-assert r is not None
-assert r.replay(spot.get_cout())
+tc.assertIsNotNone(r)
+tc.assertTrue(r.replay(spot.get_cout()))
for e in a.out(7):
if e.dst == 2:
e.cond = bddfalse
s = a.accepting_run()
-assert s is not None
-assert s.replay(spot.get_cout())
+tc.assertIsNotNone(s)
+tc.assertTrue(s.replay(spot.get_cout()))
for e in a.out(2):
if e.dst == 1:
e.cond = bddfalse
s = a.accepting_run()
-assert s is None
+tc.assertIsNone(s)
diff --git a/tests/python/except.py b/tests/python/except.py
index 178e419b4..76f17f76c 100644
--- a/tests/python/except.py
+++ b/tests/python/except.py
@@ -24,6 +24,8 @@
import spot
import buddy
+from unittest import TestCase
+tc = TestCase()
def report_missing_exception():
@@ -35,7 +37,7 @@ aut.set_acceptance(spot.acc_cond("parity min even 4"))
try:
spot.iar(aut)
except RuntimeError as e:
- assert 'iar() expects Rabin-like or Streett-like input' in str(e)
+ tc.assertIn('iar() expects Rabin-like or Streett-like input', str(e))
else:
report_missing_exception()
@@ -43,7 +45,7 @@ alt = spot.dualize(spot.translate('FGa | FGb'))
try:
spot.tgba_determinize(alt)
except RuntimeError as e:
- assert 'tgba_determinize() does not support alternation' in str(e)
+ tc.assertIn('tgba_determinize() does not support alternation', str(e))
else:
report_missing_exception()
@@ -52,18 +54,18 @@ aps = aut.ap()
rem = spot.remove_ap()
rem.add_ap('"a"=0,b')
aut = rem.strip(aut)
-assert aut.ap() == aps[2:]
+tc.assertEqual(aut.ap(), aps[2:])
try:
rem.add_ap('"a=0,b')
except ValueError as e:
- assert """missing closing '"'""" in str(e)
+ tc.assertIn("""missing closing '"'""", str(e))
else:
report_missing_exception()
try:
rem.add_ap('a=0=b')
except ValueError as e:
- assert """unexpected '=' at position 3""" in str(e)
+ tc.assertIn("""unexpected '=' at position 3""", str(e))
else:
report_missing_exception()
@@ -73,7 +75,7 @@ for meth in ('scc_has_rejecting_cycle', 'is_inherently_weak_scc',
try:
getattr(spot, meth)(si, 20)
except ValueError as e:
- assert "invalid SCC number" in str(e)
+ tc.assertIn("invalid SCC number", str(e))
else:
report_missing_exception()
@@ -89,14 +91,15 @@ si = spot.scc_info(alt)
try:
si.determine_unknown_acceptance()
except RuntimeError as e:
- assert "scc_info::determine_unknown_acceptance() does not supp" in str(e)
+ tc.assertIn("scc_info::determine_unknown_acceptance() does not supp",
+ str(e))
else:
report_missing_exception()
try:
alt.set_init_state(999)
except ValueError as e:
- assert "set_init_state()" in str(e)
+ tc.assertIn("set_init_state()", str(e))
else:
report_missing_exception()
@@ -107,7 +110,7 @@ alt.set_init_state(u)
try:
alt.set_init_state(u - 1)
except ValueError as e:
- assert "set_init_state()" in str(e)
+ tc.assertIn("set_init_state()", str(e))
else:
report_missing_exception()
@@ -116,21 +119,21 @@ r = spot.twa_run(aut)
try:
a = r.as_twa()
except RuntimeError as e:
- assert "empty cycle" in str(e)
+ tc.assertIn("empty cycle", str(e))
else:
report_missing_exception()
try:
a = r.replay(spot.get_cout())
except RuntimeError as e:
- assert "empty cycle" in str(e)
+ tc.assertIn("empty cycle", str(e))
else:
report_missing_exception()
try:
a = r.reduce()
except RuntimeError as e:
- assert "empty cycle" in str(e)
+ tc.assertIn("empty cycle", str(e))
else:
report_missing_exception()
@@ -138,12 +141,12 @@ a = spot.translate('Fa')
a = spot.to_generalized_rabin(a, False)
r = a.accepting_run()
r = r.reduce()
-assert r.cycle[0].acc == spot.mark_t([1])
+tc.assertEqual(r.cycle[0].acc, spot.mark_t([1]))
r.cycle[0].acc = spot.mark_t([0])
try:
r.reduce();
except RuntimeError as e:
- assert "expects an accepting cycle" in str(e)
+ tc.assertIn("expects an accepting cycle", str(e))
else:
report_missing_exception()
@@ -151,7 +154,7 @@ f = spot.formula('GF(a | Gb)')
try:
spot.gf_guarantee_to_ba(f, spot._bdd_dict)
except RuntimeError as e:
- assert "guarantee" in str(e)
+ tc.assertIn("guarantee", str(e))
else:
report_missing_exception()
@@ -159,7 +162,7 @@ f = spot.formula('FG(a | Fb)')
try:
spot.fg_safety_to_dca(f, spot._bdd_dict)
except RuntimeError as e:
- assert "safety" in str(e)
+ tc.assertIn("safety", str(e))
else:
report_missing_exception()
@@ -168,28 +171,28 @@ m = spot.mark_t([n - 1])
try:
m = spot.mark_t([0]) << n
except RuntimeError as e:
- assert "Too many acceptance sets" in str(e)
+ tc.assertIn("Too many acceptance sets", str(e))
else:
report_missing_exception()
try:
m.set(n)
except RuntimeError as e:
- assert "bit index is out of bounds" in str(e)
+ tc.assertIn("bit index is out of bounds", str(e))
else:
report_missing_exception()
try:
m = spot.mark_t([0, n, 1])
except RuntimeError as e:
- assert "Too many acceptance sets used. The limit is" in str(e)
+ tc.assertIn("Too many acceptance sets used. The limit is", str(e))
else:
report_missing_exception()
try:
spot.complement_semidet(spot.translate('Gb R a', 'ba'))
except RuntimeError as e:
- assert "requires a semi-deterministic input" in str(e)
+ tc.assertIn("requires a semi-deterministic input", str(e))
else:
report_missing_exception()
@@ -197,52 +200,55 @@ try:
spot.translate('F(G(a | !a) & ((b <-> c) W d))', 'det', 'any')
except ValueError as e:
s = str(e)
- assert 'det' in s
- assert 'any' in s
+ tc.assertIn('det', s)
+ tc.assertIn('any', s)
else:
report_missing_exception()
a1 = spot.translate('FGa')
a2 = spot.translate('Gb')
-assert not spot.is_deterministic(a1)
-assert spot.is_deterministic(a2)
+tc.assertFalse(spot.is_deterministic(a1))
+tc.assertTrue(spot.is_deterministic(a2))
try:
spot.product_xor(a1, a2)
except RuntimeError as e:
- assert "product_xor() only works with deterministic automata" in str(e)
+ tc.assertIn("product_xor() only works with deterministic automata", str(e))
else:
report_missing_exception()
try:
spot.product_xor(a2, a1)
except RuntimeError as e:
- assert "product_xor() only works with deterministic automata" in str(e)
+ tc.assertIn("product_xor() only works with deterministic automata", str(e))
else:
report_missing_exception()
try:
spot.product_xnor(a1, a2)
except RuntimeError as e:
- assert "product_xnor() only works with deterministic automata" in str(e)
+ tc.assertIn("product_xnor() only works with deterministic automata", str(e))
else:
report_missing_exception()
try:
spot.product_xnor(a2, a1)
except RuntimeError as e:
- assert "product_xnor() only works with deterministic automata" in str(e)
+ tc.assertIn("product_xnor() only works with deterministic automata", str(e))
else:
report_missing_exception()
try:
spot.solve_safety_game(a1)
except RuntimeError as e:
- assert "solve_safety_game(): arena should have true acceptance" in str(e)
+ tc.assertIn(
+ "solve_safety_game(): arena should have true acceptance",
+ str(e))
else:
report_missing_exception()
try:
spot.solve_parity_game(a1)
except RuntimeError as e:
- assert "solve_parity_game(): arena must have max-odd acceptance condition" \
- in str(e)
+ tc.assertIn(
+ "solve_parity_game(): arena must have max-odd acceptance condition",
+ str(e))
else:
report_missing_exception()
@@ -250,16 +256,16 @@ else:
try:
spot.formula_Star(spot.formula("a"), 10, 333)
except OverflowError as e:
- assert "333" in str(e)
- assert "254" in str(e)
+ tc.assertIn("333", str(e))
+ tc.assertIn("254", str(e))
else:
report_missing_exception()
try:
spot.formula_FStar(spot.formula("a"), 333, 400)
except OverflowError as e:
- assert "333" in str(e)
- assert "254" in str(e)
+ tc.assertIn("333", str(e))
+ tc.assertIn("254", str(e))
else:
report_missing_exception()
@@ -267,15 +273,15 @@ try:
spot.formula_nested_unop_range(spot.op_F, spot.op_Or, 333, 400,
spot.formula("a"))
except OverflowError as e:
- assert "333" in str(e)
- assert "254" in str(e)
+ tc.assertIn("333", str(e))
+ tc.assertIn("254", str(e))
else:
report_missing_exception()
try:
spot.formula_FStar(spot.formula("a"), 50, 40)
except OverflowError as e:
- assert "reversed" in str(e)
+ tc.assertIn("reversed", str(e))
else:
report_missing_exception()
@@ -287,5 +293,5 @@ try:
a.to_str()
except RuntimeError as e:
se = str(e)
- assert "synthesis-outputs" in se
- assert "unregistered proposition" in se
+ tc.assertIn("synthesis-outputs", se)
+ tc.assertIn("unregistered proposition", se)
diff --git a/tests/python/game.py b/tests/python/game.py
index 9d77c153d..d7aec2f38 100644
--- a/tests/python/game.py
+++ b/tests/python/game.py
@@ -1,6 +1,6 @@
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2020 Laboratoire de Recherche et Développement de
+# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement de
# l'EPITA.
#
# This file is part of Spot, a model checking library.
@@ -19,6 +19,8 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
g = spot.automaton("""HOA: v1 States: 9 Start: 0 AP: 2 "a" "b"
acc-name: Streett 1 Acceptance: 2 Fin(0) | Inf(1) properties:
@@ -27,10 +29,10 @@ trans-labels explicit-labels state-acc spot-state-player: 0 1 0 1 0 1
{1} [0] 8 State: 3 {1} [1] 4 State: 4 {1} [0] 5 State: 5 {1} [0] 6
State: 6 {1} [1] 7 State: 7 State: 8 {1} [0] 2 --END--""")
-assert spot.solve_parity_game(g) == False
+tc.assertFalse(spot.solve_parity_game(g))
s = spot.highlight_strategy(g).to_str("HOA", "1.1")
-assert s == """HOA: v1.1
+tc.assertEqual(s, """HOA: v1.1
States: 9
Start: 0
AP: 2 "a" "b"
@@ -60,4 +62,4 @@ State: 6 {1}
State: 7
State: 8 {1}
[0] 2
---END--"""
+--END--""")
diff --git a/tests/python/gen.py b/tests/python/gen.py
index dd844741c..a9fed6890 100644
--- a/tests/python/gen.py
+++ b/tests/python/gen.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017 Laboratoire de Recherche et Développement de
+# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@@ -23,63 +23,66 @@
import spot.gen as gen
from sys import exit
+from unittest import TestCase
+tc = TestCase()
k2 = gen.aut_pattern(gen.AUT_KS_NCA, 2)
-assert k2.prop_state_acc()
-assert k2.num_states() == 5
-assert k2.prop_universal().is_false()
-assert k2.prop_inherently_weak().is_false()
-assert k2.prop_stutter_invariant().is_false()
-assert k2.prop_semi_deterministic().is_false()
-assert k2.prop_deterministic().is_false()
-assert k2.prop_terminal().is_false()
+tc.assertTrue(k2.prop_state_acc())
+tc.assertEqual(k2.num_states(), 5)
+tc.assertTrue(k2.prop_universal().is_false())
+tc.assertTrue(k2.prop_inherently_weak().is_false())
+tc.assertTrue(k2.prop_stutter_invariant().is_false())
+tc.assertTrue(k2.prop_semi_deterministic().is_false())
+tc.assertTrue(k2.prop_deterministic().is_false())
+tc.assertTrue(k2.prop_terminal().is_false())
# to_str is defined in the spot package, so this makes sure
# the type returned by spot.gen.ks_nca() is the correct one.
-assert 'to_str' in dir(k2)
+tc.assertIn('to_str', dir(k2))
k3 = gen.aut_pattern(gen.AUT_L_NBA, 3)
-assert k3.num_states() == 10
-assert k3.prop_state_acc()
-assert k3.prop_universal().is_false()
-assert k3.prop_inherently_weak().is_false()
-assert k3.prop_stutter_invariant().is_false()
-assert k3.prop_semi_deterministic().is_false()
-assert k3.prop_deterministic().is_false()
-assert k3.prop_terminal().is_false()
+tc.assertEqual(k3.num_states(), 10)
+tc.assertTrue(k3.prop_state_acc())
+tc.assertTrue(k3.prop_universal().is_false())
+tc.assertTrue(k3.prop_inherently_weak().is_false())
+tc.assertTrue(k3.prop_stutter_invariant().is_false())
+tc.assertTrue(k3.prop_semi_deterministic().is_false())
+tc.assertTrue(k3.prop_deterministic().is_false())
+tc.assertTrue(k3.prop_terminal().is_false())
-assert k2.get_dict() == k3.get_dict()
+tc.assertEqual(k2.get_dict(), k3.get_dict())
try:
gen.aut_pattern(gen.AUT_KS_NCA, 0)
except RuntimeError as e:
- assert 'positive argument' in str(e)
+ tc.assertIn('positive argument', str(e))
else:
exit(2)
f = gen.ltl_pattern(gen.LTL_AND_F, 3)
-assert f.size() == 3
-assert gen.ltl_pattern_name(gen.LTL_AND_F) == "and-f"
+tc.assertEqual(f.size(), 3)
+tc.assertEqual(gen.ltl_pattern_name(gen.LTL_AND_F), "and-f")
try:
gen.ltl_pattern(1000, 3)
except RuntimeError as e:
- assert 'unsupported pattern' in str(e)
+ tc.assertIn('unsupported pattern', str(e))
else:
exit(2)
try:
gen.ltl_pattern(gen.LTL_OR_G, -10)
except RuntimeError as e:
- assert 'or-g' in str(e)
- assert 'positive' in str(e)
+ tc.assertIn('or-g', str(e))
+ tc.assertIn('positive', str(e))
else:
exit(2)
-assert 40 == sum(p.size() for p in gen.ltl_patterns((gen.LTL_OR_G, 1, 5),
- (gen.LTL_GH_Q, 3),
- gen.LTL_EH_PATTERNS))
+tc.assertEqual(40, sum(p.size()
+ for p in gen.ltl_patterns((gen.LTL_OR_G, 1, 5),
+ (gen.LTL_GH_Q, 3),
+ gen.LTL_EH_PATTERNS)))
-assert 32 == sum(p.num_states()
- for p in gen.aut_patterns((gen.AUT_L_NBA, 1, 3),
- (gen.AUT_KS_NCA, 5)))
+tc.assertEqual(32, sum(p.num_states()
+ for p in gen.aut_patterns((gen.AUT_L_NBA, 1, 3),
+ (gen.AUT_KS_NCA, 5))))
diff --git a/tests/python/genem.py b/tests/python/genem.py
index 5da9ce85c..0c9d0809a 100644
--- a/tests/python/genem.py
+++ b/tests/python/genem.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018-2022 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2018-2022 Laboratoire de Recherche et Développement de
+# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -22,6 +22,8 @@
# are usable with methods from the spot package.
import spot
+from unittest import TestCase
+tc = TestCase()
a1 = spot.automaton('''
HOA: v1 name: "aut" States: 4 Start: 0 AP: 0
@@ -179,7 +181,7 @@ def generic_emptiness2_rec(aut):
# Find some Fin set, we necessarily have one, otherwise the SCC
# would have been found to be either rejecting or accepting.
fo = acc.fin_one()
- assert fo >= 0, acc
+ tc.assertTrue(fo >= 0, acc)
for part in si.split_on_sets(scc, [fo]):
if not generic_emptiness2(part):
return False
@@ -309,10 +311,10 @@ def run_bench(automata):
+ str(res3b)[0] + str(res3c)[0] + str(res3d)[0]
+ str(res4)[0] + str(res5)[0])
print(res)
- assert res in ('TTTTTTTT', 'FFFFFFFF')
+ tc.assertIn(res, ('TTTTTTTT', 'FFFFFFFF'))
if res == 'FFFFFFFF':
run3 = spot.generic_accepting_run(aut)
- assert run3.replay(spot.get_cout()) is True
+ tc.assertTrue(run3.replay(spot.get_cout()))
run_bench([a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a360, act])
diff --git a/tests/python/implies.py b/tests/python/implies.py
index 2e4e64ddd..24d74b720 100755
--- a/tests/python/implies.py
+++ b/tests/python/implies.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2012 Laboratoire de Recherche et Développement
+# Copyright (C) 2012, 2022 Laboratoire de Recherche et Développement
# de l'EPITA.
#
# This file is part of Spot, a model checking library.
@@ -19,6 +19,8 @@
import sys
from buddy import *
+from unittest import TestCase
+tc = TestCase()
bdd_init(10000, 10000)
bdd_setvarnum(5)
@@ -33,26 +35,26 @@ e = V[1] & V[2] & -V[3] & V[4]
f = V[0] & -V[3] & V[4]
g = -V[0] | V[1]
-assert(bdd_implies(b, a))
-assert(not bdd_implies(a, b))
-assert(not bdd_implies(c, a))
-assert(bdd_implies(a, d))
-assert(bdd_implies(b, d))
-assert(bdd_implies(c, d))
-assert(bdd_implies(d, d))
-assert(not bdd_implies(e, d))
-assert(not bdd_implies(d, e))
-assert(not bdd_implies(f, e))
-assert(not bdd_implies(e, f))
-assert(bdd_implies(bddfalse, f))
-assert(not bdd_implies(bddtrue, f))
-assert(bdd_implies(f, bddtrue))
-assert(not bdd_implies(f, bddfalse))
-assert(bdd_implies(a, g))
+tc.assertTrue(bdd_implies(b, a))
+tc.assertFalse(bdd_implies(a, b))
+tc.assertFalse(bdd_implies(c, a))
+tc.assertTrue(bdd_implies(a, d))
+tc.assertTrue(bdd_implies(b, d))
+tc.assertTrue(bdd_implies(c, d))
+tc.assertTrue(bdd_implies(d, d))
+tc.assertFalse(bdd_implies(e, d))
+tc.assertFalse(bdd_implies(d, e))
+tc.assertFalse(bdd_implies(f, e))
+tc.assertFalse(bdd_implies(e, f))
+tc.assertTrue(bdd_implies(bddfalse, f))
+tc.assertFalse(bdd_implies(bddtrue, f))
+tc.assertTrue(bdd_implies(f, bddtrue))
+tc.assertFalse(bdd_implies(f, bddfalse))
+tc.assertTrue(bdd_implies(a, g))
a = (-V[2] & (-V[1] | V[0])) | (-V[0] & V[1] & V[2])
b = V[1] | -V[2]
-assert(bdd_implies(a, b))
+tc.assertTrue(bdd_implies(a, b))
# Cleanup all BDD variables before calling bdd_done(), otherwise
# bdd_delref will be called after bdd_done() and this is unsafe in
diff --git a/tests/python/intrun.py b/tests/python/intrun.py
index c86c6d643..e3b708a95 100644
--- a/tests/python/intrun.py
+++ b/tests/python/intrun.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -18,6 +18,8 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
# This issue was reported by Florian Renkin. The reduce() call used in
# intersecting_run() was bogus, and could incorrectly reduce a word
@@ -34,5 +36,5 @@ trans-labels explicit-labels trans-acc complete properties: deterministic
State: 3 [t] 1 {1 2} State: 4 [!0&1] 4 {2} [!0&!1] 3 {2} [0] 2 {0 2} --END--""")
r = b.intersecting_run(spot.complement(a));
c = spot.twa_word(r).as_automaton()
-assert c.intersects(b)
-assert not c.intersects(a)
+tc.assertTrue(c.intersects(b))
+tc.assertFalse(c.intersects(a))
diff --git a/tests/python/kripke.py b/tests/python/kripke.py
index f3ce218b2..fa92b3fa9 100644
--- a/tests/python/kripke.py
+++ b/tests/python/kripke.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2019 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2019, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -19,6 +19,9 @@
import spot
import buddy
+from unittest import TestCase
+tc = TestCase()
+
bdict = spot.make_bdd_dict()
k = spot.make_kripke_graph(bdict)
p1 = buddy.bdd_ithvar(k.register_ap("p1"))
@@ -51,25 +54,25 @@ State: [0&1] 1 "0"
State: [!0&!1] 2 "2"
2 1
--END--"""
-assert hoa == k.to_str('HOA')
-assert k.num_states() == 3
-assert k.num_edges() == 5
+tc.assertEqual(hoa, k.to_str('HOA'))
+tc.assertEqual(k.num_states(), 3)
+tc.assertEqual(k.num_edges(), 5)
res = []
for e in k.out(s1):
res.append((e.src, e.dst))
-assert res == [(1, 0), (1, 2)]
+tc.assertEqual(res, [(1, 0), (1, 2)])
res = []
for e in k.edges():
res.append((e.src, e.dst))
-assert res == [(1, 0), (0, 0), (1, 2), (2, 2), (2, 0)]
+tc.assertEqual(res, [(1, 0), (0, 0), (1, 2), (2, 2), (2, 0)])
res = []
for s in k.states():
res.append(s.cond())
-assert res == [cond1, cond2, cond3]
+tc.assertEqual(res, [cond1, cond2, cond3])
-assert k.states()[0].cond() == cond1
-assert k.states()[1].cond() == cond2
-assert k.states()[2].cond() == cond3
+tc.assertEqual(k.states()[0].cond(), cond1)
+tc.assertEqual(k.states()[1].cond(), cond2)
+tc.assertEqual(k.states()[2].cond(), cond3)
diff --git a/tests/python/langmap.py b/tests/python/langmap.py
index 6fd860986..723a5c0d5 100644
--- a/tests/python/langmap.py
+++ b/tests/python/langmap.py
@@ -1,6 +1,6 @@
# -*- coding: utf-8 -*-
-# Copyright (C) 2016, 2017, 2020 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE)
+# Copyright (C) 2016, 2017, 2020, 2022 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE)
#
# This file is part of Spot, a model checking library.
#
@@ -19,6 +19,8 @@
import spot
import sys
+from unittest import TestCase
+tc = TestCase()
def hstates(txt):
@@ -31,13 +33,10 @@ def hstates(txt):
def test(f, opt, expected):
aut = spot.translate(f, *opt, 'deterministic')
v = spot.language_map(aut)
- assert len(v) == aut.num_states()
+ tc.assertEqual(len(v), aut.num_states())
spot.highlight_languages(aut)
l = hstates(aut.to_str('hoa', '1.1'))
- if l != expected:
- print('for {}\nexpected: {}\n but got: {}'.format(f, expected, l),
- file=sys.stderr)
- exit(1)
+ tc.assertEqual(l, expected)
test('GF(a) & GFb & c', ['Buchi', 'SBAcc'], '1 0 2 0 3 0')
@@ -50,6 +49,6 @@ test('Xa', ['Buchi', 'SBAcc'], '')
try:
test('FGa', ['Buchi'], '')
except RuntimeError as e:
- assert 'language_map only works with deterministic automata'in str(e)
+ tc.assertIn('language_map only works with deterministic automata', str(e))
else:
exit(1)
diff --git a/tests/python/ltl2tgba.py b/tests/python/ltl2tgba.py
index 25fff4566..913c557be 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-2016, 2021 Laboratoire de Recherche
-# et Développement de l'Epita (LRDE).
+# Copyright (C) 2009, 2010, 2012, 2014-2016, 2021-2022 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.
@@ -98,7 +98,7 @@ if f:
elif taa_opt:
a = concrete = spot.ltl_to_taa(f, dict)
else:
- assert "unspecified translator"
+ raise RuntimeError("unspecified translator")
if wdba:
a = spot.ensure_digraph(a)
@@ -117,7 +117,7 @@ if f:
elif output == 6:
spot.print_lbtt(cout, a)
else:
- assert "unknown output option"
+ raise RuntimeError("unknown output option")
if degeneralize_opt:
del degeneralized
@@ -137,4 +137,6 @@ del dict
# not necessary in other implementations.
from platform import python_implementation
if python_implementation() == 'CPython':
- assert spot.fnode_instances_check()
+ from unittest import TestCase
+ tc = TestCase()
+ tc.assertTrue(spot.fnode_instances_check())
diff --git a/tests/python/ltlf.py b/tests/python/ltlf.py
index 5676a2a1b..b13432d3e 100644
--- a/tests/python/ltlf.py
+++ b/tests/python/ltlf.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016 Laboratoire de Recherche et Développement de
+# Copyright (C) 2016, 2022 Laboratoire de Recherche et Développement de
# l'Epita
#
# This file is part of Spot, a model checking library.
@@ -18,6 +18,8 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
lcc = spot.language_containment_checker()
@@ -43,5 +45,5 @@ for f in formulas:
f4 = spot.formula_And([spot.from_ltlf(f2), cst])
print("{}\t=>\t{}".format(f1, f3))
print("{}\t=>\t{}".format(f2, f4))
- assert lcc.equal(f3, f4)
+ tc.assertTrue(lcc.equal(f3, f4))
print()
diff --git a/tests/python/ltlparse.py b/tests/python/ltlparse.py
index 98562743c..208e0c321 100755
--- a/tests/python/ltlparse.py
+++ b/tests/python/ltlparse.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2009-2012, 2014-2017, 2019, 2021 Laboratoire de Recherche et
-# Développement de l'Epita (LRDE).
+# Copyright (C) 2009-2012, 2014-2017, 2019, 2021-2022 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.
@@ -22,6 +22,8 @@
import sys
import spot
+from unittest import TestCase
+tc = TestCase()
e = spot.default_environment.instance()
@@ -41,11 +43,11 @@ for str1, isl in l:
pf = spot.parse_infix_psl(str2, e)
if pf.format_errors(spot.get_cout()):
sys.exit(1)
- assert isl == pf.f.is_leaf()
+ tc.assertEqual(isl, pf.f.is_leaf())
del pf
-assert spot.formula('a').is_leaf()
-assert spot.formula('0').is_leaf()
+tc.assertTrue(spot.formula('a').is_leaf())
+tc.assertTrue(spot.formula('0').is_leaf())
for str1 in ['a * b', 'a xor b', 'a <-> b']:
pf = spot.parse_infix_boolean(str1, e, False)
@@ -66,21 +68,21 @@ for (x, op) in [('a* <-> b*', "`<->'"),
('a*[=2]', "[=...]"),
('a*[->2]', "[->...]")]:
f5 = spot.parse_infix_sere(x)
- assert f5.errors
+ tc.assertTrue(f5.errors)
ostr = spot.ostringstream()
f5.format_errors(ostr)
err = ostr.str()
- assert "not a Boolean expression" in err
- assert op in err
- assert "SERE" in err
+ tc.assertIn("not a Boolean expression", err)
+ tc.assertIn(op, err)
+ tc.assertIn("SERE", err)
del f5
f6 = spot.parse_infix_sere('(a <-> b -> c ^ "b\n\n\rc")[=2] & c[->2]')
-assert not f6.errors
+tc.assertFalse(f6.errors)
del f6
f6 = spot.parse_infix_sere('-')
-assert f6.errors
+tc.assertTrue(f6.errors)
del f6
for (x, msg) in [('{foo[->bug]}', "treating this goto block as [->]"),
@@ -150,12 +152,12 @@ for (x, msg) in [('{foo[->bug]}', "treating this goto block as [->]"),
('{"X}', "missing closing brace"),
]:
f7 = spot.parse_infix_psl(x)
- assert f7.errors
+ tc.assertTrue(f7.errors)
ostr = spot.ostringstream()
f7.format_errors(ostr)
err = ostr.str()
print(err)
- assert msg in err
+ tc.assertIn(msg, err)
del f7
for (x, msg) in [('a&', "missing right operand for \"and operator\""),
@@ -174,12 +176,12 @@ for (x, msg) in [('a&', "missing right operand for \"and operator\""),
('!', "missing right operand for \"not operator\""),
]:
f8 = spot.parse_infix_boolean(x)
- assert f8.errors
+ tc.assertTrue(f8.errors)
ostr = spot.ostringstream()
f8.format_errors(ostr)
err = ostr.str()
print(err)
- assert msg in err
+ tc.assertIn(msg, err)
del f8
for (x, msg) in [('a->', "missing right operand for \"implication operator\""),
@@ -191,12 +193,12 @@ for (x, msg) in [('a->', "missing right operand for \"implication operator\""),
]:
f9 = spot.parse_infix_psl(x, spot.default_environment.instance(),
False, True)
- assert f9.errors
+ tc.assertTrue(f9.errors)
ostr = spot.ostringstream()
f9.format_errors(ostr)
err = ostr.str()
print(err)
- assert msg in err
+ tc.assertIn(msg, err)
del f9
# force GC before fnode_instances_check(), unless it's CPython
@@ -205,15 +207,15 @@ if python_implementation() != 'CPython':
import gc
gc.collect()
-assert spot.fnode_instances_check()
+tc.assertTrue(spot.fnode_instances_check())
f = spot.formula_F(2, 4, spot.formula_ap("a"))
-assert f == spot.formula("XX(a | X(a | X(a)))")
+tc.assertEqual(f, spot.formula("XX(a | X(a | X(a)))"))
f = spot.formula_G(2, 4, spot.formula_ap("a"))
-assert f == spot.formula("XX(a & X(a & X(a)))")
+tc.assertEqual(f, spot.formula("XX(a & X(a & X(a)))"))
f = spot.formula_X(2, spot.formula_ap("a"))
-assert f == spot.formula("XX(a)")
+tc.assertEqual(f, spot.formula("XX(a)"))
f = spot.formula_G(2, spot.formula_unbounded(), spot.formula_ap("a"))
-assert f == spot.formula("XXG(a)")
+tc.assertEqual(f, spot.formula("XXG(a)"))
f = spot.formula_F(2, spot.formula_unbounded(), spot.formula_ap("a"))
-assert f == spot.formula("XXF(a)")
+tc.assertEqual(f, spot.formula("XXF(a)"))
diff --git a/tests/python/ltlsimple.py b/tests/python/ltlsimple.py
index 7b88f07dc..c21c3b7f1 100755
--- a/tests/python/ltlsimple.py
+++ b/tests/python/ltlsimple.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2012, 2015, 2018, 2021 Laboratoire de
+# Copyright (C) 2009, 2010, 2012, 2015, 2018, 2021-2022 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
@@ -22,6 +22,8 @@
import spot
import sys
+from unittest import TestCase
+tc = TestCase()
# Some of the tests here assume timely destructor calls, as they occur
# in the the reference-counted CPython implementation. Other
@@ -35,13 +37,13 @@ b = spot.formula.ap('b')
c = spot.formula.ap('c')
c2 = spot.formula.ap('c')
-assert c == c2
+tc.assertEqual(c, c2)
op = spot.formula.And([a, b])
op2 = spot.formula.And([op, c])
op3 = spot.formula.And([a, c, b])
-assert op2 == op3
+tc.assertEqual(op2, op3)
# The symbol for a subformula which hasn't been cloned is better
# suppressed, so we don't attempt to reuse it elsewhere.
@@ -52,12 +54,12 @@ sys.stdout.write('op2 = %s\n' % str(op2))
del a, b, c2
sys.stdout.write('op3 = %s\n' % str(op3))
-assert op2 == op3
+tc.assertEqual(op2, op3)
op4 = spot.formula.Or([op2, op3])
sys.stdout.write('op4 = %s\n' % str(op4))
-assert op4 == op2
+tc.assertEqual(op4, op2)
del op2, op3, op4
@@ -78,10 +80,11 @@ f5 = spot.formula.Xor(F, c)
del a, b, c, T, F, f1, f2, f4, f5
if is_cpython:
- assert spot.fnode_instances_check()
+ tc.assertTrue(spot.fnode_instances_check())
# ----------------------------------------------------------------------
-assert str([str(x) for x in spot.formula('a &b & c')]) == "['a', 'b', 'c']"
+tc.assertEqual(str([str(x) for x in spot.formula('a &b & c')]),
+ "['a', 'b', 'c']")
def switch_g_f(x):
@@ -93,7 +96,7 @@ def switch_g_f(x):
f = spot.formula('GFa & XFGb & Fc & G(a | b | Fd)')
-assert str(switch_g_f(f)) == 'FGa & XGFb & Gc & F(a | b | Gd)'
+tc.assertEqual(str(switch_g_f(f)), 'FGa & XGFb & Gc & F(a | b | Gd)')
x = 0
@@ -105,7 +108,7 @@ def count_g(f):
f.traverse(count_g)
-assert x == 3
+tc.assertEqual(x, 3)
# ----------------------------------------------------------------------
@@ -121,14 +124,14 @@ LBT for shell: echo {f:lq} | ...
Default for CSV: ...,{f:c},...
Wring, centered: {f:w:~^50}""".format(f=formula)
-assert res == """\
+tc.assertEqual(res, """\
Default output: a U (b U "$strange[0]=name")
Spin syntax: a U (b U ($strange[0]=name))
(Spin syntax): (a) U ((b) U ($strange[0]=name))
Default for shell: echo 'a U (b U "$strange[0]=name")' | ...
LBT for shell: echo 'U "a" U "b" "$strange[0]=name"' | ...
Default for CSV: ...,"a U (b U ""$strange[0]=name"")",...
-Wring, centered: ~~~~~(a=1) U ((b=1) U ("$strange[0]=name"=1))~~~~~"""
+Wring, centered: ~~~~~(a=1) U ((b=1) U ("$strange[0]=name"=1))~~~~~""")
opt = spot.tl_simplifier_options(False, True, True,
@@ -144,9 +147,8 @@ for (input, output) in [('(a&b)<->b', 'b->(a&b)'),
('b xor (!(a&b))', 'b->(a&b)'),
('!b xor (a&b)', 'b->(a&b)')]:
f = spot.tl_simplifier(opt).simplify(input)
- print(input, f, output)
- assert(f == output)
- assert(spot.are_equivalent(input, output))
+ tc.assertEqual(f, output)
+ tc.assertTrue(spot.are_equivalent(input, output))
def myparse(input):
@@ -157,7 +159,7 @@ def myparse(input):
# This used to fail, because myparse would return a pointer
# to pf.f inside the destroyed pf.
-assert myparse('a U b') == spot.formula('a U b')
+tc.assertEqual(myparse('a U b'), spot.formula('a U b'))
-assert spot.is_liveness('a <-> GFb')
-assert not spot.is_liveness('a & GFb')
+tc.assertTrue(spot.is_liveness('a <-> GFb'))
+tc.assertFalse(spot.is_liveness('a & GFb'))
diff --git a/tests/python/mealy.py b/tests/python/mealy.py
index da71d1bfb..71c7739f9 100644
--- a/tests/python/mealy.py
+++ b/tests/python/mealy.py
@@ -19,6 +19,8 @@
# along with this program. If not, see .
import spot, buddy
+from unittest import TestCase
+tc = TestCase()
# Testing Sat-based approach
@@ -42,8 +44,8 @@ spot.set_state_players(a, [False,True,False,True,False,True])
spot.set_synthesis_outputs(a, o1&o2)
b = spot.minimize_mealy(a)
-assert(list(spot.get_state_players(b)).count(False) == 2)
-assert(spot.is_split_mealy_specialization(a, b))
+tc.assertEqual(list(spot.get_state_players(b)).count(False), 2)
+tc.assertTrue(spot.is_split_mealy_specialization(a, b))
test_auts = [
("""HOA: v1
@@ -371,21 +373,21 @@ for (mealy_str, nenv_min) in test_auts:
elif aap.ap_name().startswith("i"):
ins = ins & buddy.bdd_ithvar(mealy.register_ap(aap.ap_name()))
else:
- assert("""Aps must start with either "i" or "o".""")
+ raise AssertionError("""Aps must start with either "i" or "o".""")
spot.set_synthesis_outputs(mealy, outs)
mealy_min_ks = spot.minimize_mealy(mealy, -1)
n_e = sum([s == 0 for s in spot.get_state_players(mealy_min_ks)])
- assert(n_e == nenv_min)
- assert(spot.is_split_mealy_specialization(mealy, mealy_min_ks))
+ tc.assertEqual(n_e, nenv_min)
+ tc.assertTrue(spot.is_split_mealy_specialization(mealy, mealy_min_ks))
# Test un- and resplit
tmp = spot.unsplit_2step(mealy_min_ks)
mealy_min_rs = spot.split_2step(tmp, spot.get_synthesis_outputs(tmp), False)
- assert(spot.is_split_mealy_specialization(mealy, mealy_min_rs, True))
- assert(spot.are_equivalent(mealy_min_ks, mealy_min_rs))
+ tc.assertTrue(spot.is_split_mealy_specialization(mealy, mealy_min_rs, True))
+ tc.assertTrue(spot.are_equivalent(mealy_min_ks, mealy_min_rs))
# Testing bisimulation (with output assignment)
@@ -515,15 +517,15 @@ spot.set_synthesis_outputs(aut,
& buddy.bdd_ithvar(
aut.register_ap("u02alarm29control0f1d2alarm29turn2off1b")))
min_equiv = spot.reduce_mealy(aut, False)
-assert min_equiv.num_states() == 6
-assert spot.are_equivalent(min_equiv, aut)
+tc.assertEqual(min_equiv.num_states(), 6)
+tc.assertTrue(spot.are_equivalent(min_equiv, aut))
# Build an automaton that recognizes a subset of the language of the original
# automaton
min_sub = spot.reduce_mealy(aut, True)
-assert min_sub.num_states() == 5
+tc.assertEqual(min_sub.num_states(), 5)
prod = spot.product(spot.complement(aut), min_sub)
-assert spot.generic_emptiness_check(prod)
+tc.assertTrue(spot.generic_emptiness_check(prod))
aut = spot.automaton("""
HOA: v1
@@ -564,7 +566,7 @@ State: 0
# An example that shows that we should not build a tree when we use inclusion.
res = spot.reduce_mealy(aut, True)
-assert res.to_str() == exp
+tc.assertEqual(res.to_str(), exp)
aut = spot.automaton("""
HOA: v1
@@ -608,4 +610,4 @@ State: 1
--END--"""
res = spot.reduce_mealy(aut, True)
-assert res.to_str() == exp
+tc.assertEqual(res.to_str(), exp)
diff --git a/tests/python/merge.py b/tests/python/merge.py
index c56d8f309..893916953 100644
--- a/tests/python/merge.py
+++ b/tests/python/merge.py
@@ -1,7 +1,7 @@
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017, 2020 Laboratoire de Recherche et Développement de
-# l'EPITA.
+# Copyright (C) 2017, 2020, 2022 Laboratoire de Recherche et
+# Développement de l'EPITA.
#
# This file is part of Spot, a model checking library.
#
@@ -19,6 +19,8 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
aut = spot.automaton("""
HOA: v1
@@ -39,7 +41,7 @@ State: 2
out = spot.simplify_acceptance(aut)
hoa = out.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
@@ -54,8 +56,8 @@ State: 1
[1] 2 {0}
State: 2
[1] 0
---END--"""
-assert spot.are_equivalent(out, aut)
+--END--""")
+tc.assertTrue(spot.are_equivalent(out, aut))
aut = spot.automaton("""HOA: v1
States: 3
@@ -75,7 +77,7 @@ State: 2
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
@@ -90,7 +92,7 @@ State: 1
[1] 2 {0}
State: 2
[1] 0
---END--"""
+--END--""")
aut = spot.automaton("""
HOA: v1
@@ -111,7 +113,7 @@ State: 2
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
@@ -126,7 +128,7 @@ State: 1
[1] 2
State: 2
[1] 0
---END--"""
+--END--""")
aut = spot.automaton("""HOA: v1
States: 3
@@ -146,7 +148,7 @@ State: 2
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
@@ -161,7 +163,7 @@ State: 1
[1] 2 {1}
State: 2
[1] 0 {0}
---END--"""
+--END--""")
aut = spot.automaton("""
HOA: v1
@@ -182,7 +184,7 @@ State: 2
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
@@ -197,7 +199,7 @@ State: 1
[1] 2
State: 2
[1] 0
---END--"""
+--END--""")
aut = spot.automaton("""HOA: v1
States: 3
@@ -217,7 +219,7 @@ State: 2
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
@@ -232,7 +234,7 @@ State: 1 {0}
[1] 2
State: 2 {0}
[1] 0
---END--"""
+--END--""")
aut = spot.automaton("""HOA: v1
States: 3
@@ -252,7 +254,7 @@ State: 2
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
@@ -267,7 +269,7 @@ State: 1 {0}
[1] 2
State: 2 {0}
[1] 0
---END--"""
+--END--""")
aut = spot.automaton("""HOA: v1
States: 3
@@ -287,7 +289,7 @@ State: 2
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
@@ -301,7 +303,7 @@ State: 1 {1}
[1] 2
State: 2
[1] 0
---END--"""
+--END--""")
aut = spot.automaton("""HOA: v1
States: 4
@@ -335,7 +337,7 @@ State: 3 {1 3}
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 4
Start: 0
AP: 2 "a" "b"
@@ -364,7 +366,7 @@ State: 3 {1}
[0&!1] 0
[!0&1] 3
[0&1] 2
---END--"""
+--END--""")
aut = spot.automaton("""HOA: v1
States: 3
@@ -388,7 +390,7 @@ State: 2
out = spot.simplify_acceptance(aut)
hoa = out.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 3
Start: 0
AP: 2 "p0" "p1"
@@ -406,8 +408,8 @@ State: 1
State: 2
[0] 2 {0}
[!0] 1 {0}
---END--"""
-assert spot.are_equivalent(out, aut)
+--END--""")
+tc.assertTrue(spot.are_equivalent(out, aut))
aut = spot.automaton("""HOA: v1
States: 4
@@ -435,7 +437,7 @@ State: 3
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 4
Start: 0
AP: 2 "p0" "p1"
@@ -457,7 +459,7 @@ State: 3
[0&1] 0 {1}
[0&!1] 3 {1 2}
[!0] 1 {3}
---END--"""
+--END--""")
aut = spot.automaton("""HOA: v1
States: 1
@@ -475,7 +477,7 @@ State: 0 {1 2}
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 1
Start: 0
AP: 2 "p0" "p1"
@@ -486,7 +488,7 @@ properties: deterministic
--BODY--
State: 0
[t] 0
---END--"""
+--END--""")
aut = spot.automaton("""HOA: v1
States: 2
@@ -506,7 +508,7 @@ State: 1
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 2
Start: 0
AP: 2 "p0" "p1"
@@ -519,7 +521,7 @@ State: 0
[!0] 1 {2}
State: 1
[t] 1 {1 2}
---END--"""
+--END--""")
aut = spot.automaton("""HOA: v1
States: 1
@@ -536,7 +538,7 @@ State: 0 {0 1 3}
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 1
Start: 0
AP: 2 "p0" "p1"
@@ -547,7 +549,7 @@ properties: deterministic
--BODY--
State: 0
[t] 0
---END--"""
+--END--""")
aut = spot.automaton("""HOA: v1
States: 2
@@ -568,7 +570,7 @@ State: 1
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 2
Start: 0
AP: 2 "p0" "p1"
@@ -583,7 +585,7 @@ State: 0
State: 1
[0] 1
[!0] 0 {1}
---END--"""
+--END--""")
aut = spot.automaton("""HOA: v1
States: 2
@@ -602,7 +604,7 @@ State: 1 {1}
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 2
Start: 0
AP: 2 "p0" "p1"
@@ -615,7 +617,7 @@ State: 0
[t] 1
State: 1
[t] 0
---END--"""
+--END--""")
aut = spot.automaton("""HOA: v1
States: 3
@@ -636,7 +638,7 @@ State: 2 {2}
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 3
Start: 0
AP: 2 "p0" "p1"
@@ -650,7 +652,7 @@ State: 1 {0}
[t] 1
State: 2 {2}
[t] 1
---END--"""
+--END--""")
aut = spot.automaton("""HOA: v1
States: 3
@@ -672,7 +674,7 @@ State: 2 {1 2 3}
out = spot.simplify_acceptance(aut)
hoa = out.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 3
Start: 0
AP: 2 "p0" "p1"
@@ -687,8 +689,8 @@ State: 1 {1}
[t] 2
State: 2 {0 1}
[t] 1
---END--"""
-assert spot.are_equivalent(out, aut)
+--END--""")
+tc.assertTrue(spot.are_equivalent(out, aut))
aut = spot.automaton("""HOA: v1
States: 2
@@ -708,7 +710,7 @@ State: 1
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 2
Start: 0
AP: 2 "p0" "p1"
@@ -722,7 +724,7 @@ State: 0
State: 1
[0] 1
[!0] 0
---END--"""
+--END--""")
aut = spot.automaton("""HOA: v1
States: 3
@@ -740,7 +742,7 @@ State: 2
--END--""")
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
@@ -755,7 +757,7 @@ State: 1
[1] 2
State: 2
[1] 0
---END--"""
+--END--""")
aut = spot.automaton("""HOA: v1
States: 3
@@ -773,7 +775,7 @@ State: 2
--END--""")
spot.simplify_acceptance_here(aut)
hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
@@ -788,4 +790,4 @@ State: 1
[1] 2
State: 2
[1] 0
---END--"""
+--END--""")
diff --git a/tests/python/mergedge.py b/tests/python/mergedge.py
index e55bdabf2..4e97abe23 100644
--- a/tests/python/mergedge.py
+++ b/tests/python/mergedge.py
@@ -1,6 +1,6 @@
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2020, 2021 Laboratoire de Recherche et Développement de
+# Copyright (C) 2020-2022 Laboratoire de Recherche et Développement de
# l'EPITA.
#
# This file is part of Spot, a model checking library.
@@ -20,12 +20,14 @@
import spot
+from unittest import TestCase
+tc = TestCase()
aut = spot.automaton("""HOA: v1 States: 1 Start: 0 AP: 1 "a"
Acceptance: 1 Inf(0) --BODY-- State: 0 [0] 0 [0] 0 {0} --END--""")
-assert aut.num_edges() == 2
+tc.assertEqual(aut.num_edges(), 2)
aut.merge_edges()
-assert aut.num_edges() == 1
+tc.assertEqual(aut.num_edges(), 1)
aut = spot.automaton("""
HOA: v1
@@ -44,15 +46,15 @@ State: 1
[0 | 1] 1
[0&!1] 1 {0}
--END--""")
-assert aut.num_edges() == 5
+tc.assertEqual(aut.num_edges(), 5)
aut.merge_edges()
-assert aut.num_edges() == 5
-assert not spot.is_deterministic(aut)
+tc.assertEqual(aut.num_edges(), 5)
+tc.assertFalse(spot.is_deterministic(aut))
aut = spot.split_edges(aut)
-assert aut.num_edges() == 9
+tc.assertEqual(aut.num_edges(), 9)
aut.merge_edges()
-assert aut.num_edges() == 5
-assert spot.is_deterministic(aut)
+tc.assertEqual(aut.num_edges(), 5)
+tc.assertTrue(spot.is_deterministic(aut))
aut = spot.automaton("""
HOA: v1
@@ -74,15 +76,15 @@ State: 2
[0] 1
--END--""")
aut.merge_states()
-assert aut.num_edges() == 4
-assert aut.num_states() == 2
-assert spot.is_deterministic(aut)
-assert aut.prop_complete()
+tc.assertEqual(aut.num_edges(), 4)
+tc.assertEqual(aut.num_states(), 2)
+tc.assertTrue(spot.is_deterministic(aut))
+tc.assertTrue(aut.prop_complete())
aut.merge_states()
-assert aut.num_edges() == 4
-assert aut.num_states() == 2
-assert spot.is_deterministic(aut)
-assert aut.prop_complete()
+tc.assertEqual(aut.num_edges(), 4)
+tc.assertEqual(aut.num_states(), 2)
+tc.assertTrue(spot.is_deterministic(aut))
+tc.assertTrue(aut.prop_complete())
aa = spot.automaton("""
diff --git a/tests/python/misc-ec.py b/tests/python/misc-ec.py
index d1234bd69..85d4aaa47 100644
--- a/tests/python/misc-ec.py
+++ b/tests/python/misc-ec.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017, 2020 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2017, 2020, 2022 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -18,6 +18,9 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
+
aut = spot.translate("G(p0 | (p0 R Xp0) | XF(!p0 & p1))", 'Buchi', 'SBAcc')
ec = spot.make_emptiness_check_instantiator('SE05')[0].instantiate(aut)
n = 0
@@ -27,7 +30,7 @@ while True:
break
print(res.accepting_run())
n += 1
-assert n == 2
+tc.assertEqual(n, 2)
for name in ['SE05', 'CVWY90', 'GV04']:
aut = spot.translate("GFa && GFb")
@@ -35,13 +38,13 @@ for name in ['SE05', 'CVWY90', 'GV04']:
ec = spot.make_emptiness_check_instantiator(name)[0].instantiate(aut)
print(ec.check().accepting_run())
except RuntimeError as e:
- assert "Büchi or weak" in str(e)
+ tc.assertIn("Büchi or weak", str(e))
aut = spot.translate("a", 'monitor')
try:
ec = spot.make_emptiness_check_instantiator('Tau03')[0].instantiate(aut)
except RuntimeError as e:
- assert "at least one" in str(e)
+ tc.assertIn("at least one", str(e))
aut = spot.translate("a", 'ba')
ec = spot.make_emptiness_check_instantiator('Tau03')[0].instantiate(aut)
diff --git a/tests/python/optionmap.py b/tests/python/optionmap.py
index 667ef0b19..ad526f510 100755
--- a/tests/python/optionmap.py
+++ b/tests/python/optionmap.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2010, 2012, 2018 Laboratoire de Recherche et Développement
-# de l'EPITA.
+# Copyright (C) 2010, 2012, 2018, 2022 Laboratoire de Recherche et
+# Développement de l'EPITA.
# Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie.
@@ -21,65 +21,67 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
o = spot.option_map()
res = o.parse_options("optA, opta=2M, optb =4 ; optB = 7\
, optC= 10")
-assert not res
+tc.assertFalse(res)
-assert o.get('optA') == 1
-assert o.get('opta') == 2*1024*1024
-assert o.get('optb') == 4
-assert o.get('optB') == 7
-assert o.get('optC') == 10
-assert o.get('none') == 0
-assert o.get('none', 16) == 16
+tc.assertEqual(o.get('optA'), 1)
+tc.assertEqual(o.get('opta'), 2*1024*1024)
+tc.assertEqual(o.get('optb'), 4)
+tc.assertEqual(o.get('optB'), 7)
+tc.assertEqual(o.get('optC'), 10)
+tc.assertEqual(o.get('none'), 0)
+tc.assertEqual(o.get('none', 16), 16)
o.set('optb', 40)
-assert o.get('optb') == 40
+tc.assertEqual(o.get('optb'), 40)
res = o.parse_options("!optA !optb optC, !optB")
-assert not res
-assert o.get('optA') == 0
-assert o.get('opta') == 2*1024*1024
-assert o.get('optb') == 0
-assert o.get('optB') == 0
-assert o.get('optC') == 1
+tc.assertFalse(res)
+tc.assertEqual(o.get('optA'), 0)
+tc.assertEqual(o.get('opta'), 2*1024*1024)
+tc.assertEqual(o.get('optb'), 0)
+tc.assertEqual(o.get('optB'), 0)
+tc.assertEqual(o.get('optC'), 1)
res = o.parse_options("!")
-assert res == "!"
+tc.assertEqual(res, "!")
res = o.parse_options("foo, !opt = 1")
-assert res == "!opt = 1"
+tc.assertEqual(res, "!opt = 1")
res = o.parse_options("foo=3, opt == 1")
-assert res == "opt == 1"
+tc.assertEqual(res, "opt == 1")
res = o.parse_options("foo=3opt == 1")
-assert res == "3opt == 1"
+tc.assertEqual(res, "3opt == 1")
aut1 = spot.translate('GF(a <-> XXa)', 'det')
-assert aut1.num_states() == 4
+tc.assertEqual(aut1.num_states(), 4)
aut2 = spot.translate('GF(a <-> XXa)', 'det', xargs='gf-guarantee=0')
-assert aut2.num_states() == 9
+tc.assertEqual(aut2.num_states(), 9)
try:
spot.translate('GF(a <-> XXa)', 'det', xargs='foobar=1')
except RuntimeError as e:
- assert "option 'foobar' was not used" in str(e)
+ tc.assertIn("option 'foobar' was not used", str(e))
else:
raise RuntimeError("missing exception")
try:
spot.translate('GF(a <-> XXa)').postprocess('det', xargs='gf-guarantee=0')
except RuntimeError as e:
- assert "option 'gf-guarantee' was not used" in str(e)
+ tc.assertIn("option 'gf-guarantee' was not used", str(e))
else:
raise RuntimeError("missing exception")
try:
spot.translate('GF(a <-> XXa)').postprocess('det', xargs='gf-guarantee=x')
except RuntimeError as e:
- assert "failed to parse option at: 'gf-guarantee=x'" in str(e)
+ tc.assertIn("failed to parse option at: 'gf-guarantee=x'", str(e))
else:
raise RuntimeError("missing exception")
diff --git a/tests/python/origstate.py b/tests/python/origstate.py
index 0ca013889..15a7ab0ad 100644
--- a/tests/python/origstate.py
+++ b/tests/python/origstate.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement
-# de l'Epita
+# Copyright (C) 2015, 2017, 2022 Laboratoire de Recherche et
+# Développement de l'Epita
#
# This file is part of Spot, a model checking library.
#
@@ -19,6 +19,8 @@
import spot
from sys import exit
+from unittest import TestCase
+tc = TestCase()
aut = spot.automaton("""
HOA: v1
@@ -38,7 +40,7 @@ State: 1
""")
aut2 = spot.degeneralize(aut)
-assert aut2.to_str() == """HOA: v1
+tc.assertEqual(aut2.to_str(), """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
@@ -56,10 +58,10 @@ State: 1
[1] 2
State: 2 {0}
[1] 2
---END--"""
+--END--""")
aut2.copy_state_names_from(aut)
-assert aut2.to_str() == """HOA: v1
+tc.assertEqual(aut2.to_str(), """HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
@@ -77,7 +79,7 @@ State: 1 "0#0"
[1] 2
State: 2 "1#1" {0}
[1] 2
---END--"""
+--END--""")
aut2.set_init_state(2)
aut2.purge_unreachable_states()
@@ -93,16 +95,16 @@ properties: deterministic
State: 0 "1#1" {0}
[1] 0
--END--"""
-assert aut2.to_str() == ref
+tc.assertEqual(aut2.to_str(), ref)
# This makes sure that the original-states vector has also been renamed.
aut2.copy_state_names_from(aut)
-assert aut2.to_str() == ref
+tc.assertEqual(aut2.to_str(), ref)
aut2 = spot.degeneralize(aut)
aut2.release_named_properties()
try:
aut2.copy_state_names_from(aut)
except RuntimeError as e:
- assert "state does not exist in source automaton" in str(e)
+ tc.assertIn("state does not exist in source automaton", str(e))
else:
exit(1)
diff --git a/tests/python/otfcrash.py b/tests/python/otfcrash.py
index 69acbcb1a..8e30cb501 100644
--- a/tests/python/otfcrash.py
+++ b/tests/python/otfcrash.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016, 2018 Laboratoire de Recherche et Développement
+# Copyright (C) 2016, 2018, 2022 Laboratoire de Recherche et Développement
# de l'Epita
#
# This file is part of Spot, a model checking library.
@@ -23,6 +23,8 @@ import spot.aux
import tempfile
import shutil
import sys
+from unittest import TestCase
+tc = TestCase()
spot.ltsmin.require('divine')
@@ -51,4 +53,4 @@ system async;
p = spot.otf_product(k, a)
return p.is_empty()
- assert(modelcheck('X "R.found"', m) == True)
+ tc.assertTrue(modelcheck('X "R.found"', m))
diff --git a/tests/python/parity.py b/tests/python/parity.py
index b0389c40e..6ced51c40 100644
--- a/tests/python/parity.py
+++ b/tests/python/parity.py
@@ -19,36 +19,38 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
max_even_5 = spot.acc_code.parity(True, False, 5)
-assert max_even_5 == spot.acc_code.parity_max_even(5)
-assert max_even_5 == spot.acc_code.parity_max(False, 5)
+tc.assertEqual(max_even_5, spot.acc_code.parity_max_even(5))
+tc.assertEqual(max_even_5, spot.acc_code.parity_max(False, 5))
min_even_5 = spot.acc_code.parity(False, False, 5)
-assert min_even_5 == spot.acc_code.parity_min_even(5)
-assert min_even_5 == spot.acc_code.parity_min(False, 5)
+tc.assertEqual(min_even_5, spot.acc_code.parity_min_even(5))
+tc.assertEqual(min_even_5, spot.acc_code.parity_min(False, 5))
max_odd_5 = spot.acc_code.parity(True, True, 5)
-assert max_odd_5 == spot.acc_code.parity_max_odd(5)
-assert max_odd_5 == spot.acc_code.parity_max(True, 5)
+tc.assertEqual(max_odd_5, spot.acc_code.parity_max_odd(5))
+tc.assertEqual(max_odd_5, spot.acc_code.parity_max(True, 5))
min_odd_5 = spot.acc_code.parity(False, True, 5)
-assert min_odd_5 == spot.acc_code.parity_min_odd(5)
-assert min_odd_5 == spot.acc_code.parity_min(True, 5)
+tc.assertEqual(min_odd_5, spot.acc_code.parity_min_odd(5))
+tc.assertEqual(min_odd_5, spot.acc_code.parity_min(True, 5))
for f in ('FGa', 'GFa & GFb & FGc', 'XXX(a U b)'):
a1 = spot.translate(f, 'parity')
- assert a1.acc().is_parity()
+ tc.assertTrue(a1.acc().is_parity())
a2 = spot.translate(f).postprocess('parity')
- assert a2.acc().is_parity()
+ tc.assertTrue(a2.acc().is_parity())
a3 = spot.translate(f, 'det').postprocess('parity', 'colored')
- assert a3.acc().is_parity()
- assert spot.is_colored(a3)
+ tc.assertTrue(a3.acc().is_parity())
+ tc.assertTrue(spot.is_colored(a3))
a = spot.translate('GFa & GFb')
try:
spot.change_parity_here(a, spot.parity_kind_same, spot.parity_style_even)
except RuntimeError as e:
- assert 'input should have parity acceptance' in str(e)
+ tc.assertIn('input should have parity acceptance', str(e))
else:
exit(2)
@@ -64,7 +66,7 @@ State: 0
--END--
""")
spot.cleanup_parity_here(a)
-assert a.to_str() == """HOA: v1
+tc.assertEqual(a.to_str(), """HOA: v1
States: 1
Start: 0
AP: 1 "a"
@@ -75,7 +77,7 @@ properties: deterministic
--BODY--
State: 0
[t] 0
---END--"""
+--END--""")
a = spot.automaton("""
HOA: v1
@@ -89,7 +91,7 @@ State: 0
--END--
""")
spot.cleanup_parity_here(a)
-assert a.to_str() == """HOA: v1
+tc.assertEqual(a.to_str(), """HOA: v1
States: 1
Start: 0
AP: 1 "a"
@@ -100,7 +102,7 @@ properties: deterministic
--BODY--
State: 0
[t] 0
---END--"""
+--END--""")
a = spot.automaton("""HOA: v1
States: 3
@@ -120,39 +122,39 @@ State: 2
try:
spot.get_state_players(a)
except RuntimeError as e:
- assert "not a game" in str(e)
+ tc.assertIn("not a game", str(e))
else:
report_missing_exception()
try:
spot.set_state_player(a, 1, True)
except RuntimeError as e:
- assert "Can only" in str(e)
+ tc.assertIn("Can only", str(e))
else:
report_missing__exception()
spot.set_state_players(a, (False, True, False))
-assert spot.get_state_player(a, 0) == False
-assert spot.get_state_player(a, 1) == True
-assert spot.get_state_player(a, 2) == False
+tc.assertEqual(spot.get_state_player(a, 0), False)
+tc.assertEqual(spot.get_state_player(a, 1), True)
+tc.assertEqual(spot.get_state_player(a, 2), False)
try:
spot.set_state_players(a, [True, False, False, False])
except RuntimeError as e:
- assert "many owners as states" in str(e)
+ tc.assertIn("many owners as states", str(e))
else:
report_missing_exception()
try:
spot.get_state_player(a, 4)
except RuntimeError as e:
- assert "invalid state number" in str(e)
+ tc.assertIn("invalid state number", str(e))
else:
report_missing_exception()
try:
spot.set_state_player(a, 4, True)
except RuntimeError as e:
- assert "invalid state number" in str(e)
+ tc.assertIn("invalid state number", str(e))
else:
report_missing_exception()
@@ -168,4 +170,4 @@ oi.erase()
# postprocess used to call reduce_parity that did not
# work correctly on automata with deleted edges.
sm = a.postprocess("gen", "small")
-assert sm.num_states() == 3
+tc.assertEqual(sm.num_states(), 3)
diff --git a/tests/python/parsetgba.py b/tests/python/parsetgba.py
index cbcacb183..038b33a19 100755
--- a/tests/python/parsetgba.py
+++ b/tests/python/parsetgba.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# Copyright (C) 2012, 2014, 2015, 2022 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -19,6 +19,8 @@
import os
import spot
+from unittest import TestCase
+tc = TestCase()
contents = '''
HOA: v1 name: "a U b" States: 2 Start: 1 AP: 2 "a" "b" acc-name: Buchi
@@ -34,7 +36,7 @@ out.close()
a = spot.parse_aut(filename, spot.make_bdd_dict())
-assert not a.errors
+tc.assertFalse(a.errors)
spot.print_dot(spot.get_cout(), a.aut)
diff --git a/tests/python/pdegen.py b/tests/python/pdegen.py
index 02150d375..12bc9e39a 100644
--- a/tests/python/pdegen.py
+++ b/tests/python/pdegen.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2019, 2020, 2021 Laboratoire de Recherche et Développement de
-# l'Epita (LRDE).
+# Copyright (C) 2019, 2020, 2021, 2022 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -23,6 +23,8 @@
import spot
+from unittest import TestCase
+tc = TestCase()
a, b, d, f = spot.automata("""
HOA: v1
@@ -73,19 +75,19 @@ State: 1
--END--
""")
-assert spot.is_partially_degeneralizable(a) == [0, 1]
+tc.assertEqual(spot.is_partially_degeneralizable(a), [0, 1])
da = spot.partial_degeneralize(a, [0, 1])
-assert da.equivalent_to(a)
-assert da.num_states() == 2
+tc.assertTrue(da.equivalent_to(a))
+tc.assertEqual(da.num_states(), 2)
-assert spot.is_partially_degeneralizable(b) == [0, 1]
+tc.assertEqual(spot.is_partially_degeneralizable(b), [0, 1])
db = spot.partial_degeneralize(b, [0, 1])
-assert db.equivalent_to(b)
-assert db.num_states() == 3
+tc.assertTrue(db.equivalent_to(b))
+tc.assertEqual(db.num_states(), 3)
db.copy_state_names_from(b)
dbhoa = db.to_str('hoa')
-assert dbhoa == """HOA: v1
+tc.assertEqual(dbhoa, """HOA: v1
States: 3
Start: 0
AP: 1 "p0"
@@ -99,28 +101,28 @@ State: 1 "0#0" {0 1}
[0] 2
State: 2 "1#0" {1}
[0] 1
---END--"""
+--END--""")
c = spot.automaton("randaut -A'(Fin(0)&Inf(1)&Inf(2))|Fin(2)' 1 |")
-assert spot.is_partially_degeneralizable(c) == [1, 2]
+tc.assertEqual(spot.is_partially_degeneralizable(c), [1, 2])
dc = spot.partial_degeneralize(c, [1, 2])
-assert dc.equivalent_to(c)
-assert str(dc.get_acceptance()) == '(Fin(0) & Inf(2)) | Fin(1)'
+tc.assertTrue(dc.equivalent_to(c))
+tc.assertEqual(str(dc.get_acceptance()), '(Fin(0) & Inf(2)) | Fin(1)')
-assert spot.is_partially_degeneralizable(d) == []
+tc.assertEqual(spot.is_partially_degeneralizable(d), [])
dd = spot.partial_degeneralize(d, [])
-assert dd.equivalent_to(d)
-assert dd.num_states() == 1
-assert str(dd.get_acceptance()) == 'Inf(1) & Fin(0)'
+tc.assertTrue(dd.equivalent_to(d))
+tc.assertEqual(dd.num_states(), 1)
+tc.assertEqual(str(dd.get_acceptance()), 'Inf(1) & Fin(0)')
e = spot.dualize(b)
de = spot.partial_degeneralize(e, [0, 1])
-assert de.equivalent_to(e)
-assert de.num_states() == 4
+tc.assertTrue(de.equivalent_to(e))
+tc.assertEqual(de.num_states(), 4)
de.copy_state_names_from(e)
dehoa = de.to_str('hoa')
-assert dehoa == """HOA: v1
+tc.assertEqual(dehoa, """HOA: v1
States: 4
Start: 0
AP: 1 "p0"
@@ -140,18 +142,18 @@ State: 2 "3#0"
State: 3 "2#0"
[0] 1 {0}
[!0] 2
---END--"""
+--END--""")
-assert spot.is_partially_degeneralizable(de) == []
+tc.assertEqual(spot.is_partially_degeneralizable(de), [])
df = spot.partial_degeneralize(f, [0, 1])
df.equivalent_to(f)
-assert str(df.acc()) == '(1, Fin(0))'
+tc.assertEqual(str(df.acc()), '(1, Fin(0))')
try:
df = spot.partial_degeneralize(f, [0, 1, 2])
except RuntimeError as e:
- assert 'partial_degeneralize(): {0,1,2} does not' in str(e)
+ tc.assertIn('partial_degeneralize(): {0,1,2} does not', str(e))
else:
raise RuntimeError("missing exception")
@@ -165,13 +167,13 @@ State: 2 [0&!1&2] 3 {1 4 9} State: 3 [0&!1&2] 4 {0 1 5 9} State: 4 [!0&!1&2] 1
State: 7 [0&!1&!2] 0 {4 7} --END--""")
daut5 = spot.degeneralize_tba(aut5)
-assert daut5.equivalent_to(aut5)
+tc.assertTrue(daut5.equivalent_to(aut5))
sets = list(range(aut5.num_sets()))
-assert spot.is_partially_degeneralizable(aut5) == sets
+tc.assertEqual(spot.is_partially_degeneralizable(aut5), sets)
pdaut5 = spot.partial_degeneralize(aut5, sets)
-assert pdaut5.equivalent_to(aut5)
-assert daut5.num_states() == 9
-assert pdaut5.num_states() == 8
+tc.assertTrue(pdaut5.equivalent_to(aut5))
+tc.assertEqual(daut5.num_states(), 9)
+tc.assertEqual(pdaut5.num_states(), 8)
aut6 = spot.automaton("""HOA: v1 States: 6 Start: 0 AP: 3 "p0" "p1" "p2"
acc-name: generalized-Buchi 3 Acceptance: 3 Inf(0)&Inf(1)&Inf(2) properties:
@@ -180,13 +182,13 @@ trans-labels explicit-labels trans-acc deterministic --BODY-- State: 0
[0&1&!2] 5 {1} State: 4 [!0&1&!2] 0 {1 2} [0&!1&!2] 3 {0} State: 5 [!0&1&2] 1
--END-- """)
daut6 = spot.degeneralize_tba(aut6)
-assert daut6.equivalent_to(aut6)
+tc.assertTrue(daut6.equivalent_to(aut6))
sets = list(range(aut6.num_sets()))
-assert spot.is_partially_degeneralizable(aut6) == sets
+tc.assertEqual(spot.is_partially_degeneralizable(aut6), sets)
pdaut6 = spot.partial_degeneralize(aut6, sets)
-assert pdaut6.equivalent_to(aut6)
-assert daut6.num_states() == 8
-assert pdaut6.num_states() == 8
+tc.assertTrue(pdaut6.equivalent_to(aut6))
+tc.assertEqual(daut6.num_states(), 8)
+tc.assertEqual(pdaut6.num_states(), 8)
aut7 = spot.automaton("""HOA: v1 States: 8 Start: 0 AP: 3 "p0" "p1" "p2"
@@ -197,13 +199,13 @@ State: 0 [0&!1&2] 1 {2 3} State: 1 [0&!1&2] 0 {0 2} [0&!1&!2] 6 State: 2
[!0&!1&!2] 3 State: 5 [0&1&!2] 0 [!0&1&2] 7 State: 6 [0&1&2] 2 {1} State: 7
[!0&!1&2] 0 {0} [!0&1&!2] 4 --END--""")
daut7 = spot.degeneralize_tba(aut7)
-assert daut7.equivalent_to(aut7)
+tc.assertTrue(daut7.equivalent_to(aut7))
sets = list(range(aut7.num_sets()))
-assert spot.is_partially_degeneralizable(aut7) == sets
+tc.assertEqual(spot.is_partially_degeneralizable(aut7), sets)
pdaut7 = spot.partial_degeneralize(aut7, sets)
-assert pdaut7.equivalent_to(aut7)
-assert daut7.num_states() == 10
-assert pdaut7.num_states() == 10
+tc.assertTrue(pdaut7.equivalent_to(aut7))
+tc.assertEqual(daut7.num_states(), 10)
+tc.assertEqual(pdaut7.num_states(), 10)
aut8 = spot.automaton("""HOA: v1 States: 8 Start: 0 AP: 3 "p0" "p1" "p2"
acc-name: generalized-Buchi 5 Acceptance: 5 Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)
@@ -213,19 +215,19 @@ State: 0 [!0&1&!2] 7 {0} State: 1 [!0&1&2] 1 {4} [0&!1&2] 6 {1 2} State: 2
5 [!0&1&!2] 0 {1 3} State: 6 [0&1&2] 4 [0&1&!2] 6 State: 7 [!0&!1&!2] 1
--END--""")
daut8 = spot.degeneralize_tba(aut8)
-assert daut8.equivalent_to(aut8)
+tc.assertTrue(daut8.equivalent_to(aut8))
sets = list(range(aut8.num_sets()))
-assert spot.is_partially_degeneralizable(aut8) == sets
+tc.assertEqual(spot.is_partially_degeneralizable(aut8), sets)
pdaut8 = spot.partial_degeneralize(aut8, sets)
-assert pdaut8.equivalent_to(aut8)
-assert daut8.num_states() == 22
-assert pdaut8.num_states() == 9
+tc.assertTrue(pdaut8.equivalent_to(aut8))
+tc.assertEqual(daut8.num_states(), 22)
+tc.assertEqual(pdaut8.num_states(), 9)
aut9 = spot.dualize(aut8)
pdaut9 = spot.partial_degeneralize(aut9, sets)
-assert pdaut9.equivalent_to(aut9)
+tc.assertTrue(pdaut9.equivalent_to(aut9))
# one more state than aut9, because dualize completed the automaton.
-assert pdaut9.num_states() == 10
+tc.assertEqual(pdaut9.num_states(), 10)
aut10 = spot.automaton("""HOA: v1
States: 3
@@ -242,10 +244,10 @@ State: 2
[0] 0 {1}
[!0] 1
--END--""")
-assert spot.is_partially_degeneralizable(aut10) == [0, 1]
+tc.assertEqual(spot.is_partially_degeneralizable(aut10), [0, 1])
pdaut10 = spot.partial_degeneralize(aut10, [0, 1])
-assert pdaut10.equivalent_to(aut10)
-assert pdaut10.to_str() == """HOA: v1
+tc.assertTrue(pdaut10.equivalent_to(aut10))
+tc.assertEqual(pdaut10.to_str(), """HOA: v1
States: 3
Start: 0
AP: 1 "p0"
@@ -260,7 +262,7 @@ State: 1
State: 2
[0] 0 {1}
[!0] 1
---END--"""
+--END--""")
aut11 = spot.automaton("""HOA: v1
States: 3
@@ -277,10 +279,10 @@ State: 2
[0] 0 {1}
[!0] 1
--END--""")
-assert spot.is_partially_degeneralizable(aut11) == [0, 1]
+tc.assertEqual(spot.is_partially_degeneralizable(aut11), [0, 1])
pdaut11 = spot.partial_degeneralize(aut11, [0, 1])
-assert pdaut11.equivalent_to(aut11)
-assert pdaut11.to_str() == """HOA: v1
+tc.assertTrue(pdaut11.equivalent_to(aut11))
+tc.assertEqual(pdaut11.to_str(), """HOA: v1
States: 3
Start: 0
AP: 1 "p0"
@@ -295,7 +297,7 @@ State: 1
State: 2
[0] 0 {2}
[!0] 1
---END--"""
+--END--""")
aut12 = spot.automaton("""HOA: v1
States: 3
@@ -313,24 +315,24 @@ State: 2
[0] 0
[!0] 1 {3}
--END--""")
-assert spot.is_partially_degeneralizable(aut12) == [0,1]
+tc.assertEqual(spot.is_partially_degeneralizable(aut12), [0,1])
aut12b = spot.partial_degeneralize(aut12, [0,1])
aut12c = spot.partial_degeneralize(aut12b, [1,2])
-assert aut12c.equivalent_to(aut12)
-assert aut12c.num_states() == 9
+tc.assertTrue(aut12c.equivalent_to(aut12))
+tc.assertEqual(aut12c.num_states(), 9)
aut12d = spot.partial_degeneralize(aut12, [0,1,3])
aut12e = spot.partial_degeneralize(aut12d, [0,1])
-assert aut12e.equivalent_to(aut12)
-assert aut12e.num_states() == 9
+tc.assertTrue(aut12e.equivalent_to(aut12))
+tc.assertEqual(aut12e.num_states(), 9)
aut12f = spot.partial_degeneralize(aut12)
-assert aut12f.equivalent_to(aut12)
-assert aut12f.num_states() == 9
+tc.assertTrue(aut12f.equivalent_to(aut12))
+tc.assertEqual(aut12f.num_states(), 9)
# Check handling of original-states
dot = aut12f.to_str('dot', 'd')
-assert dot == """digraph "" {
+tc.assertEqual(dot, """digraph "" {
rankdir=LR
label="Inf(2) | (Inf(1) & Fin(0))\\n[Rabin-like 2]"
labelloc="t"
@@ -367,10 +369,10 @@ assert dot == """digraph "" {
8 -> 4 [label="p0\\n{1,2}"]
8 -> 7 [label="p0"]
}
-"""
+""")
aut12g = spot.partial_degeneralize(aut12f)
-assert aut12f == aut12g
+tc.assertEqual(aut12f, aut12g)
aut13 = spot.automaton("""HOA: v1
States: 2
@@ -390,8 +392,8 @@ State: 1
[!0&!1&2&3] 1 {0 2}
--END--""")
aut13g = spot.partial_degeneralize(aut13)
-assert aut13g.equivalent_to(aut13)
-assert aut13g.num_states() == 3
+tc.assertTrue(aut13g.equivalent_to(aut13))
+tc.assertEqual(aut13g.num_states(), 3)
aut14 = spot.automaton("""HOA: v1
@@ -412,8 +414,8 @@ State: 1
--END--
""")
aut14g = spot.partial_degeneralize(aut14)
-assert aut14g.equivalent_to(aut14)
-assert aut14g.num_states() == 3
+tc.assertTrue(aut14g.equivalent_to(aut14))
+tc.assertEqual(aut14g.num_states(), 3)
# Extracting an SCC from this large automaton will produce an automaton A in
# which original-states refers to states larger than those in A. Some version
@@ -439,4 +441,4 @@ State: 10 [!0&1] 4 [0&1] 8 [!0&!1] 10 {0 1 2 3 5} [0&!1] 13 {1 2 3} State: 11
si = spot.scc_info(aut15)
aut15b = si.split_on_sets(2, [])[0]; d
aut15c = spot.partial_degeneralize(aut15b)
-assert aut15c.equivalent_to(aut15b)
+tc.assertTrue(aut15c.equivalent_to(aut15b))
diff --git a/tests/python/prodexpt.py b/tests/python/prodexpt.py
index 098bafb26..4d00b4dae 100644
--- a/tests/python/prodexpt.py
+++ b/tests/python/prodexpt.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016-2017, 2019-2020 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# Copyright (C) 2016-2017, 2019-2020, 2022 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -18,6 +18,8 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
# make sure that we are not allowed to build the product of two automata with
# different dictionaries.
@@ -94,14 +96,14 @@ State: 60 40 38 60 68 State: 61 40 41 57 61 State: 62 40 59 44 62 State:
State: 70 40 59 57 70 State: 71 40 63 57 71 State: 72 40 69 57 72 --END--
''')
res = spot.product(left, right)
-assert res.num_states() == 977
-assert res.num_edges() == 8554
+tc.assertEqual(res.num_states(), 977)
+tc.assertEqual(res.num_edges(), 8554)
res = spot.product(left, right, spot.output_aborter(1000, 6000))
-assert res is None
+tc.assertIsNone(res)
res = spot.product(left, right, spot.output_aborter(900, 9000))
-assert res is None
+tc.assertIsNone(res)
res = spot.product(left, right, spot.output_aborter(1000, 9000))
-assert res is not None
+tc.assertIsNotNone(res)
a, b = spot.automata("""HOA: v1 States: 1 Start: 0 AP: 0 acc-name: all
Acceptance: 0 t properties: trans-labels explicit-labels state-acc complete
@@ -110,7 +112,7 @@ properties: deterministic stutter-invariant weak --BODY-- State: 0 [t] 0
properties: trans-labels explicit-labels state-acc complete properties:
deterministic stutter-invariant weak --BODY-- State: 0 [t] 0 --END--""")
out = spot.product(a, b).to_str()
-assert out == """HOA: v1
+tc.assertEqual(out, """HOA: v1
States: 1
Start: 0
AP: 0
@@ -120,9 +122,9 @@ properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant terminal
--BODY--
State: 0
---END--"""
+--END--""")
out = spot.product_susp(a, b).to_str()
-assert out == """HOA: v1
+tc.assertEqual(out, """HOA: v1
States: 1
Start: 0
AP: 0
@@ -132,4 +134,4 @@ properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant terminal
--BODY--
State: 0
---END--"""
+--END--""")
diff --git a/tests/python/randgen.py b/tests/python/randgen.py
index 094ddcb3f..32762d02e 100755
--- a/tests/python/randgen.py
+++ b/tests/python/randgen.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2015 Laboratoire de Recherche et Développement de
-# l'Epita (LRDE).
+# Copyright (C) 2015, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -18,9 +18,11 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
o = spot.option_map()
g = spot.randltlgenerator(0, o)
-assert str(g.next()) == '1'
-assert str(g.next()) == '0'
-assert str(g.next()) == 'None'
+tc.assertEqual(str(g.next()), '1')
+tc.assertEqual(str(g.next()), '0')
+tc.assertEqual(str(g.next()), 'None')
diff --git a/tests/python/relabel.py b/tests/python/relabel.py
index 5a4a370eb..0de668b12 100644
--- a/tests/python/relabel.py
+++ b/tests/python/relabel.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2015, 2017-2019 Laboratoire de Recherche et Développement
-# de l'Epita
+# Copyright (C) 2015, 2017-2019, 2022 Laboratoire de Recherche et
+# Développement de l'Epita
#
# This file is part of Spot, a model checking library.
#
@@ -18,6 +18,8 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
f = spot.formula('GF(a & b) -> (FG(a & b) & Gc)')
m = spot.relabeling_map()
@@ -26,19 +28,18 @@ res = ""
for old, new in m.items():
res += "#define {} {}\n".format(old, new)
res += str(g)
-print(res)
-assert(res == """#define p0 a & b
+tc.assertEqual(res, """#define p0 a & b
#define p1 c
GFp0 -> (FGp0 & Gp1)""")
h = spot.relabel_apply(g, m)
-assert h == f
+tc.assertEqual(h, f)
autg = g.translate()
spot.relabel_here(autg, m)
-assert str(autg.ap()) == \
- '(spot.formula("a"), spot.formula("b"), spot.formula("c"))'
-assert spot.isomorphism_checker.are_isomorphic(autg, f.translate())
+tc.assertEqual(str(autg.ap()), \
+ '(spot.formula("a"), spot.formula("b"), spot.formula("c"))')
+tc.assertTrue(spot.isomorphism_checker.are_isomorphic(autg, f.translate()))
a = spot.formula('a')
u = spot.formula('a U b')
@@ -46,11 +47,11 @@ m[a] = u
try:
spot.relabel_here(autg, m)
except RuntimeError as e:
- assert "new labels" in str(e)
+ tc.assertIn("new labels", str(e))
m = spot.relabeling_map()
m[u] = a
try:
spot.relabel_here(autg, m)
except RuntimeError as e:
- assert "old labels" in str(e)
+ tc.assertIn("old labels", str(e))
diff --git a/tests/python/remfin.py b/tests/python/remfin.py
index 20115a14f..ffff3e22a 100644
--- a/tests/python/remfin.py
+++ b/tests/python/remfin.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2015-2018, 2020 Laboratoire de Recherche et Développement de
-# l'Epita
+# Copyright (C) 2015-2018, 2020, 2022 Laboratoire de Recherche et
+# Développement de l'Epita
#
# This file is part of Spot, a model checking library.
#
@@ -19,6 +19,8 @@
import spot
+from unittest import TestCase
+tc = TestCase()
# This test used to trigger an assertion (or a segfault)
# in scc_filter_states().
@@ -41,7 +43,7 @@ State: 2
aut.prop_inherently_weak(True)
aut = spot.dualize(aut)
aut1 = spot.scc_filter_states(aut)
-assert(aut1.to_str('hoa') == """HOA: v1
+tc.assertEqual(aut1.to_str('hoa'), """HOA: v1
States: 2
Start: 0
AP: 1 "a"
@@ -56,17 +58,17 @@ State: 1
[t] 1
--END--""")
-assert(aut.scc_filter_states().to_str() == aut1.to_str())
-assert(aut1.get_name() == None)
+tc.assertEqual(aut.scc_filter_states().to_str(), aut1.to_str())
+tc.assertIsNone(aut1.get_name())
aut1.set_name("test me")
-assert(aut1.get_name() == "test me")
+tc.assertEqual(aut1.get_name(), "test me")
# The method is the same as the function
a = spot.translate('true', 'low', 'any')
-assert(a.prop_universal().is_maybe())
-assert(a.prop_unambiguous().is_maybe())
-assert(a.is_deterministic() == True)
-assert(a.is_unambiguous() == True)
+tc.assertTrue(a.prop_universal().is_maybe())
+tc.assertTrue(a.prop_unambiguous().is_maybe())
+tc.assertTrue(a.is_deterministic())
+tc.assertTrue(a.is_unambiguous())
a = spot.automaton("""
HOA: v1
@@ -92,4 +94,4 @@ State: 2
""")
b = spot.remove_fin(a)
size = (b.num_states(), b.num_edges())
-assert size == (5, 13);
+tc.assertEqual(size, (5, 13))
diff --git a/tests/python/removeap.py b/tests/python/removeap.py
index 7a9268c85..ba656ac89 100644
--- a/tests/python/removeap.py
+++ b/tests/python/removeap.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2019 Laboratoire de Recherche et Développement
+# Copyright (C) 2019, 2022 Laboratoire de Recherche et Développement
# de l'Epita
#
# This file is part of Spot, a model checking library.
@@ -18,16 +18,18 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
aut = spot.translate('a U (c & Gb)')
-assert not spot.is_terminal_automaton(aut)
-assert aut.prop_terminal().is_false()
+tc.assertFalse(spot.is_terminal_automaton(aut))
+tc.assertTrue(aut.prop_terminal().is_false())
rem = spot.remove_ap()
rem.add_ap("b")
aut = rem.strip(aut)
-assert not aut.prop_terminal().is_false()
-assert spot.is_terminal_automaton(aut)
-assert aut.prop_terminal().is_true()
+tc.assertFalse(aut.prop_terminal().is_false())
+tc.assertTrue(spot.is_terminal_automaton(aut))
+tc.assertTrue(aut.prop_terminal().is_true())
aut = rem.strip(aut)
-assert aut.prop_terminal().is_true()
+tc.assertTrue(aut.prop_terminal().is_true())
diff --git a/tests/python/rs_like.py b/tests/python/rs_like.py
index 7b4ee75cf..669af5885 100644
--- a/tests/python/rs_like.py
+++ b/tests/python/rs_like.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017 Laboratoire de Recherche et Développement
+# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement
# de l'Epita
#
# This file is part of Spot, a model checking library.
@@ -18,6 +18,8 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
a = spot.vector_rs_pair()
@@ -30,12 +32,13 @@ mall = spot.mark_t()
def test_rs(acc, rs, expected_res, expected_pairs):
res, p = getattr(acc, 'is_' + rs + '_like')()
- assert res == expected_res
+ tc.assertEqual(res, expected_res)
if expected_res:
expected_pairs.sort()
p = sorted(p)
for a, b in zip(p, expected_pairs):
- assert a.fin == b.fin and a.inf == b.inf
+ tc.assertEqual(a.fin, b.fin)
+ tc.assertEqual(a.inf, b.inf)
def switch_pairs(pairs):
diff --git a/tests/python/satmin.py b/tests/python/satmin.py
index 2d28dd405..f9fa466f8 100644
--- a/tests/python/satmin.py
+++ b/tests/python/satmin.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2015, 2020, 2021 Laboratoire de Recherche et Développement
-# de l'Epita
+# Copyright (C) 2015, 2020, 2021, 2022 Laboratoire de Recherche et
+# Développement de l'Epita
#
# This file is part of Spot, a model checking library.
#
@@ -18,232 +18,234 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
aut = spot.translate('GFa & GFb', 'Buchi', 'SBAcc')
-assert aut.num_sets() == 1
-assert aut.num_states() == 3
-assert aut.is_deterministic()
+tc.assertEqual(aut.num_sets(), 1)
+tc.assertEqual(aut.num_states(), 3)
+tc.assertTrue(aut.is_deterministic())
min1 = spot.sat_minimize(aut, acc='Rabin 1')
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_langmap=True)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=0)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=1)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=2)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=50)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=-1)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=0)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=1)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=2)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=50)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_naive=True)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
min2 = spot.sat_minimize(aut, acc='Streett 2')
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_langmap=True)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=0)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=1)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=2)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=50)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=-1)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=0)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=1)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=2)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=50)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
min2 = spot.sat_minimize(aut, acc='Streett 2', sat_naive=True)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, sat_langmap=True)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, sat_incr=1)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, sat_incr=1,
sat_incr_steps=0)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, sat_incr=1,
sat_incr_steps=1)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, sat_incr=1,
sat_incr_steps=2)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, sat_incr=1,
sat_incr_steps=50)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, sat_incr=2)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, sat_incr=2,
sat_incr_steps=-1)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, sat_incr=2,
sat_incr_steps=0)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, sat_incr=2,
sat_incr_steps=1)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, sat_incr=2,
sat_incr_steps=2)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, sat_incr=2,
sat_incr_steps=50)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, sat_naive=True)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, sat_langmap=True)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, sat_incr=1)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, sat_incr=1, sat_incr_steps=0)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, sat_incr=1, sat_incr_steps=1)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, sat_incr=1, sat_incr_steps=2)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, sat_incr=1, sat_incr_steps=50)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, sat_incr=2)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, sat_incr=2, sat_incr_steps=-1)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, sat_incr=2, sat_incr_steps=0)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, sat_incr=2, sat_incr_steps=1)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, sat_incr=2, sat_incr_steps=2)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, sat_incr=2, sat_incr_steps=50)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, sat_naive=True)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
aut = spot.translate('GFa')
-assert aut.num_sets() == 1
-assert aut.num_states() == 1
-assert aut.is_deterministic()
+tc.assertEqual(aut.num_sets(), 1)
+tc.assertEqual(aut.num_states(), 1)
+tc.assertTrue(aut.is_deterministic())
out = spot.sat_minimize(aut, state_based=True)
-assert out.num_states() == 2
+tc.assertEqual(out.num_states(), 2)
out = spot.sat_minimize(aut, state_based=True, max_states=1)
-assert out is None
+tc.assertTrue(out is None)
diff --git a/tests/python/sbacc.py b/tests/python/sbacc.py
index 445845dbc..22d937014 100644
--- a/tests/python/sbacc.py
+++ b/tests/python/sbacc.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017-2018, 2021 Laboratoire de Recherche et
+# Copyright (C) 2017-2018, 2021, 2022 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@@ -18,13 +18,15 @@
# along with this program. If not, see .
import spot
-aut = spot.translate('GFa')
-assert aut.num_states() == 1
-assert not aut.prop_state_acc().is_true()
-aut = spot.sbacc(aut)
-assert aut.num_states() == 2
-assert aut.prop_state_acc().is_true()
+from unittest import TestCase
+tc = TestCase()
+aut = spot.translate('GFa')
+tc.assertEqual(aut.num_states(), 1)
+tc.assertFalse(aut.prop_state_acc().is_true())
+aut = spot.sbacc(aut)
+tc.assertEqual(aut.num_states(), 2)
+tc.assertTrue(aut.prop_state_acc().is_true())
aut = spot.automaton("""HOA: v1
States: 3
@@ -48,7 +50,7 @@ s = spot.sbacc(aut)
s.copy_state_names_from(aut)
h = s.to_str('hoa')
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
@@ -59,7 +61,7 @@ State: 0 "0"
[0] 1
State: 1 "2" {1}
[t] 1
---END--"""
+--END--""")
aut = spot.automaton("""HOA: v1
States: 3
@@ -83,7 +85,7 @@ d = spot.degeneralize(aut)
d.copy_state_names_from(aut)
h = d.to_str('hoa')
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
@@ -95,4 +97,4 @@ State: 0 "0#0"
[0] 1
State: 1 "2#0" {0}
[t] 1
---END--"""
+--END--""")
diff --git a/tests/python/sccfilter.py b/tests/python/sccfilter.py
index 6edd33e9f..7728b70a6 100644
--- a/tests/python/sccfilter.py
+++ b/tests/python/sccfilter.py
@@ -1,6 +1,6 @@
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016 Laboratoire de Recherche et Développement de
+# Copyright (C) 2016, 2022 Laboratoire de Recherche et Développement de
# l'EPITA.
#
# This file is part of Spot, a model checking library.
@@ -22,6 +22,8 @@
# Major)
import spot
+from unittest import TestCase
+tc = TestCase()
a = spot.automaton("""
HOA: v1.1
@@ -43,7 +45,7 @@ State: 1 "bar"
--END--
""")
-assert (spot.scc_filter(a, True).to_str('hoa', '1.1') == """HOA: v1.1
+tc.assertEqual(spot.scc_filter(a, True).to_str('hoa', '1.1'), """HOA: v1.1
States: 2
Start: 0
AP: 1 "a"
diff --git a/tests/python/sccinfo.py b/tests/python/sccinfo.py
index 0ac645726..f8ade7e4b 100644
--- a/tests/python/sccinfo.py
+++ b/tests/python/sccinfo.py
@@ -1,7 +1,7 @@
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017, 2021 Laboratoire de Recherche et Développement de
-# l'EPITA.
+# Copyright (C) 2017, 2021, 2022 Laboratoire de Recherche et
+# Développement de l'EPITA.
#
# This file is part of Spot, a model checking library.
#
@@ -19,6 +19,8 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
a = spot.translate('(Ga -> Gb) W c')
@@ -26,11 +28,11 @@ try:
si = spot.scc_info(a, 10)
exit(2)
except RuntimeError as e:
- assert "initial state does not exist" in str(e)
+ tc.assertIn("initial state does not exist", str(e))
si = spot.scc_info(a)
n = si.scc_count()
-assert n == 4
+tc.assertEqual(n, 4)
acc = 0
rej = 0
@@ -39,24 +41,24 @@ for i in range(n):
acc += si.is_accepting_scc(i)
rej += si.is_rejecting_scc(i)
triv += si.is_trivial(i)
-assert acc == 3
-assert rej == 1
-assert triv == 0
+tc.assertEqual(acc, 3)
+tc.assertEqual(rej, 1)
+tc.assertEqual(triv, 0)
for scc in si:
acc -= scc.is_accepting()
rej -= scc.is_rejecting()
triv -= scc.is_trivial()
-assert acc == 0
-assert rej == 0
-assert triv == 0
+tc.assertEqual(acc, 0)
+tc.assertEqual(rej, 0)
+tc.assertEqual(triv, 0)
l0 = si.states_of(0)
l1 = si.states_of(1)
l2 = si.states_of(2)
l3 = si.states_of(3)
l = sorted(list(l0) + list(l1) + list(l2) + list(l3))
-assert l == [0, 1, 2, 3, 4]
+tc.assertEqual(l, [0, 1, 2, 3, 4])
i = si.initial()
todo = [i]
@@ -73,14 +75,14 @@ while todo:
if s not in seen:
seen.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),
- (3, 3), (4, 1), (4, 4), (1, 1)]
-assert transi == [(0, 0, 1), (0, 2, 3), (2, 0, 6),
- (2, 2, 8), (3, 3, 10), (4, 4, 12), (1, 1, 5)]
+tc.assertEqual(seen, {0, 1, 2, 3})
+tc.assertEqual(trans, [(0, 0), (0, 1), (0, 2), (0, 3),
+ (2, 0), (2, 1), (2, 2), (2, 4),
+ (3, 3), (4, 1), (4, 4), (1, 1)])
+tc.assertEqual(transi, [(0, 0, 1), (0, 2, 3), (2, 0, 6),
+ (2, 2, 8), (3, 3, 10), (4, 4, 12), (1, 1, 5)])
-assert not spot.is_weak_automaton(a, si)
+tc.assertFalse(spot.is_weak_automaton(a, si))
a = spot.automaton("""
@@ -107,8 +109,8 @@ State: 3
""")
si = spot.scc_info(a)
si.determine_unknown_acceptance()
-assert si.scc_count() == 2
-assert si.is_accepting_scc(0)
-assert not si.is_rejecting_scc(0)
-assert si.is_rejecting_scc(1)
-assert not si.is_accepting_scc(1)
+tc.assertEqual(si.scc_count(), 2)
+tc.assertTrue(si.is_accepting_scc(0))
+tc.assertFalse(si.is_rejecting_scc(0))
+tc.assertTrue(si.is_rejecting_scc(1))
+tc.assertFalse(si.is_accepting_scc(1))
diff --git a/tests/python/sccsplit.py b/tests/python/sccsplit.py
index 9095a1a29..4a1781475 100644
--- a/tests/python/sccsplit.py
+++ b/tests/python/sccsplit.py
@@ -1,7 +1,7 @@
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018 Laboratoire de Recherche et Développement de
-# l'EPITA.
+# Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement
+# de l'EPITA.
#
# This file is part of Spot, a model checking library.
#
@@ -19,6 +19,9 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
+
aut = spot.translate('GF(a <-> Xa) & GF(b <-> XXb)')
si = spot.scc_info(aut)
@@ -27,4 +30,4 @@ for aut2 in si.split_on_sets(0, [0]):
# This call to to_str() used to fail because split_on_sets had not
# registered the atomic propositions of aut
s += aut2.to_str()
-assert spot.automaton(s).num_states() == 8
+tc.assertEqual(spot.automaton(s).num_states(), 8)
diff --git a/tests/python/semidet.py b/tests/python/semidet.py
index 856b3b7d2..9072f5917 100644
--- a/tests/python/semidet.py
+++ b/tests/python/semidet.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017 Laboratoire de Recherche et Développement de
-# l'Epita (LRDE).
+# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -18,6 +18,8 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
formulas = [('(Gp0 | Fp1) M 1', False, True),
('(!p1 U p1) U X(!p0 -> Fp1)', False, True),
@@ -31,9 +33,9 @@ for f, isd, issd in formulas:
aut = spot.translate(f)
# The formula with isd=True, issd=True is the only one
# for which both properties are already set.
- assert (aut.prop_deterministic().is_maybe() or
- aut.prop_semi_deterministic().is_maybe() or
- isd == issd)
+ tc.assertTrue(aut.prop_deterministic().is_maybe() or
+ aut.prop_semi_deterministic().is_maybe() or
+ isd == issd)
spot.check_determinism(aut)
- assert aut.prop_deterministic() == isd
- assert aut.prop_semi_deterministic() == issd
+ tc.assertEqual(aut.prop_deterministic(), isd)
+ tc.assertEqual(aut.prop_semi_deterministic(), issd)
diff --git a/tests/python/setacc.py b/tests/python/setacc.py
index 8d20b6a49..7246bf5cc 100644
--- a/tests/python/setacc.py
+++ b/tests/python/setacc.py
@@ -1,7 +1,7 @@
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016, 2018, 2021 Laboratoire de Recherche et Développement de
-# l'EPITA.
+# Copyright (C) 2016, 2018, 2021, 2022 Laboratoire de Recherche et
+# Développement de l'EPITA.
#
# This file is part of Spot, a model checking library.
#
@@ -19,54 +19,56 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
# Test case reduced from a report from Juraj Major .
a = spot.make_twa_graph(spot._bdd_dict)
a.set_acceptance(0, spot.acc_code("t"))
-assert(a.prop_state_acc() == True)
+tc.assertTrue(a.prop_state_acc())
a.set_acceptance(1, spot.acc_code("Fin(0)"))
-assert(a.prop_state_acc() == spot.trival.maybe())
+tc.assertEqual(a.prop_state_acc(), spot.trival.maybe())
# Some tests for used_inf_fin_sets(), which return a pair of mark_t.
(inf, fin) = a.get_acceptance().used_inf_fin_sets()
-assert inf == []
-assert fin == [0]
+tc.assertEqual(inf, [])
+tc.assertEqual(fin, [0])
(inf, fin) = spot.acc_code("(Fin(0)|Inf(1))&Fin(2)&Inf(0)").used_inf_fin_sets()
-assert inf == [0, 1]
-assert fin == [0, 2]
+tc.assertEqual(inf, [0, 1])
+tc.assertEqual(fin, [0, 2])
# is_rabin_like() returns (bool, [(inf, fin), ...])
(b, v) = spot.acc_cond("(Fin(0)&Inf(1))|(Fin(2)&Inf(0))").is_rabin_like()
-assert b == True
-assert len(v) == 2
-assert v[0].fin == [0]
-assert v[0].inf == [1]
-assert v[1].fin == [2]
-assert v[1].inf == [0]
+tc.assertTrue(b)
+tc.assertEqual(len(v), 2)
+tc.assertEqual(v[0].fin, [0])
+tc.assertEqual(v[0].inf, [1])
+tc.assertEqual(v[1].fin, [2])
+tc.assertEqual(v[1].inf, [0])
(b, v) = spot.acc_cond("(Fin(0)|Inf(1))&(Fin(2)|Inf(0))").is_rabin_like()
-assert b == False
-assert len(v) == 0
+tc.assertFalse(b)
+tc.assertEqual(len(v), 0)
(b, v) = spot.acc_cond("(Fin(0)|Inf(1))&(Fin(2)|Inf(0))").is_streett_like()
-assert b == True
-assert repr(v) == \
- '(spot.rs_pair(fin=[0], inf=[1]), spot.rs_pair(fin=[2], inf=[0]))'
+tc.assertTrue(b)
+tc.assertEqual(repr(v), \
+ '(spot.rs_pair(fin=[0], inf=[1]), spot.rs_pair(fin=[2], inf=[0]))')
v2 = (spot.rs_pair(fin=[0], inf=[1]), spot.rs_pair(fin=[2], inf=[0]))
-assert v == v2
+tc.assertEqual(v, v2)
acc = spot.acc_cond("generalized-Rabin 1 2")
(b, v) = acc.is_generalized_rabin()
-assert b == True
-assert v == (2,)
+tc.assertTrue(b)
+tc.assertEqual(v, (2,))
(b, v) = acc.is_generalized_streett()
-assert b == False
-assert v == ()
+tc.assertFalse(b)
+tc.assertEqual(v, ())
(b, v) = acc.is_streett_like()
-assert b == True
+tc.assertTrue(b)
ve = (spot.rs_pair([0], []), spot.rs_pair([], [1]), spot.rs_pair([], [2]))
-assert v == ve
-assert acc.name() == "generalized-Rabin 1 2"
+tc.assertEqual(v, ve)
+tc.assertEqual(acc.name(), "generalized-Rabin 1 2")
# At the time of writting, acc_cond does not yet recognize
# "generalized-Streett", as there is no definition for that in the HOA format,
@@ -74,23 +76,23 @@ assert acc.name() == "generalized-Rabin 1 2"
# being a generalized-Streett. See issue #249.
acc = spot.acc_cond("Inf(0)|Fin(1)|Fin(2)")
(b, v) = acc.is_generalized_streett()
-assert b == True
-assert v == (2,)
+tc.assertTrue(b)
+tc.assertEqual(v, (2,))
(b, v) = acc.is_generalized_rabin()
-assert b == False
-assert v == ()
+tc.assertFalse(b)
+tc.assertEqual(v, ())
# FIXME: We should have a way to disable the following output, as it is not
# part of HOA v1.
-assert acc.name() == "generalized-Streett 1 2"
+tc.assertEqual(acc.name(), "generalized-Streett 1 2")
# issue #469. This test is meaningful only if Spot is compiled with
# --enable-max-accsets=64 or more.
try:
m = spot.mark_t([33])
- assert m.lowest() == m
+ tc.assertEqual(m.lowest(), m)
n = spot.mark_t([33,34])
- assert n.lowest() == m
+ tc.assertEqual(n.lowest(), m)
except RuntimeError as e:
if "Too many acceptance sets used." in str(e):
pass
@@ -102,24 +104,24 @@ except RuntimeError as e:
from gc import collect
acc = spot.translate('a').acc()
collect()
-assert acc == spot.acc_cond('Inf(0)')
+tc.assertEqual(acc, spot.acc_cond('Inf(0)'))
acc = spot.translate('b').get_acceptance()
collect()
-assert acc == spot.acc_code('Inf(0)')
+tc.assertEqual(acc, spot.acc_code('Inf(0)'))
c = spot.acc_cond('Fin(0)&Fin(1)&(Inf(2)|Fin(3))')
m1 = c.fin_unit()
m2 = c.inf_unit()
-assert m1 == [0,1]
-assert m2 == []
+tc.assertEqual(m1, [0,1])
+tc.assertEqual(m2, [])
c = spot.acc_cond('Inf(0)&Inf(1)&(Inf(2)|Fin(3))')
m1 = c.fin_unit()
m2 = c.inf_unit()
-assert m1 == []
-assert m2 == [0,1]
+tc.assertEqual(m1, [])
+tc.assertEqual(m2, [0,1])
c = spot.acc_cond('Inf(0)&Inf(1)|(Inf(2)|Fin(3))')
m1 = c.fin_unit()
m2 = c.inf_unit()
-assert m1 == []
-assert m2 == []
+tc.assertEqual(m1, [])
+tc.assertEqual(m2, [])
diff --git a/tests/python/setxor.py b/tests/python/setxor.py
index 7cd1e5da1..2fe69cd99 100755
--- a/tests/python/setxor.py
+++ b/tests/python/setxor.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement
-# de l'EPITA.
+# Copyright (C) 2010, 2011, 2022 Laboratoire de Recherche et
+# Développement de l'EPITA.
#
# This file is part of Spot, a model checking library.
#
@@ -19,6 +19,8 @@
import sys
from buddy import *
+from unittest import TestCase
+tc = TestCase()
bdd_init(10000, 10000)
bdd_setvarnum(5)
@@ -29,18 +31,18 @@ a = V[0] & -V[1] & V[2] & -V[3]
b = V[0] & V[1] & V[2] & -V[3]
c = -V[0] & V[1] & -V[2] & -V[3]
-assert(c == bdd_setxor(a, b))
-assert(c == bdd_setxor(b, a))
-assert(a == bdd_setxor(b, c))
-assert(a == bdd_setxor(c, b))
-assert(b == bdd_setxor(a, c))
-assert(b == bdd_setxor(c, a))
+tc.assertEqual(c, bdd_setxor(a, b))
+tc.assertEqual(c, bdd_setxor(b, a))
+tc.assertEqual(a, bdd_setxor(b, c))
+tc.assertEqual(a, bdd_setxor(c, b))
+tc.assertEqual(b, bdd_setxor(a, c))
+tc.assertEqual(b, bdd_setxor(c, a))
d = V[1] & V[2] & -V[3] & V[4]
e = V[0] & V[1] & -V[2] & -V[3] & V[4]
-assert(e == bdd_setxor(a, d))
-assert(e == bdd_setxor(d, a))
+tc.assertEqual(e, bdd_setxor(a, d))
+tc.assertEqual(e, bdd_setxor(d, a))
# Cleanup all BDD variables before calling bdd_done(), otherwise
# bdd_delref will be called after bdd_done() and this is unsafe in
diff --git a/tests/python/simplacc.py b/tests/python/simplacc.py
index e742d69a4..50dc2d74a 100644
--- a/tests/python/simplacc.py
+++ b/tests/python/simplacc.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita
+# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement de l'Epita
# (LRDE).
#
# This file is part of Spot, a model checking library.
@@ -18,6 +18,8 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
auts = list(spot.automata("""
@@ -70,19 +72,19 @@ explicit-labels trans-acc deterministic --BODY-- State: 0 [0&!1] 0 {2 3}
res = []
for a in auts:
b = spot.simplify_acceptance(a)
- assert b.equivalent_to(a)
+ tc.assertTrue(b.equivalent_to(a))
res.append(str(b.get_acceptance()))
c = spot.simplify_acceptance(b)
- assert b.get_acceptance() == c.get_acceptance()
+ tc.assertEqual(b.get_acceptance(), c.get_acceptance())
a.set_acceptance(a.num_sets(), a.get_acceptance().complement())
b = spot.simplify_acceptance(a)
- assert b.equivalent_to(a)
+ tc.assertTrue(b.equivalent_to(a))
res.append(str(b.get_acceptance()))
c = spot.simplify_acceptance(b)
- assert b.get_acceptance() == c.get_acceptance()
+ tc.assertEqual(b.get_acceptance(), c.get_acceptance())
-assert res == [
+tc.assertEqual(res, [
'Inf(0)',
'Fin(0)',
'Inf(1) & Fin(0)',
@@ -101,4 +103,4 @@ assert res == [
'(Inf(0) | Fin(2)) & Inf(1)',
'(Fin(2) & (Inf(1) | Fin(0))) | (Inf(0)&Inf(2))',
'(Inf(2) | (Fin(1) & Inf(0))) & (Fin(0)|Fin(2))',
- ]
+ ])
diff --git a/tests/python/simstate.py b/tests/python/simstate.py
index 6c2ca8bc3..b0b62267d 100644
--- a/tests/python/simstate.py
+++ b/tests/python/simstate.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2015, 2017-2018, 2020-2021 Laboratoire de Recherche
+# Copyright (C) 2015, 2017-2018, 2020-2022 Laboratoire de Recherche
# et Développement de l'Epita
#
# This file is part of Spot, a model checking library.
@@ -19,6 +19,8 @@
import spot
from sys import exit
+from unittest import TestCase
+tc = TestCase()
# CPython use reference counting, so that automata are destructed
# when we expect them to be. However other implementations like
@@ -48,7 +50,7 @@ State: 1
""")
aut2 = spot.simulation(aut)
-assert aut2.to_str() == """HOA: v1
+tc.assertEqual(aut2.to_str(), """HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
@@ -59,10 +61,10 @@ properties: deterministic
--BODY--
State: 0 {0}
[t] 0
---END--"""
+--END--""")
aut2.copy_state_names_from(aut)
-assert aut2.to_str() == """HOA: v1
+tc.assertEqual(aut2.to_str(), """HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
@@ -73,7 +75,7 @@ properties: deterministic
--BODY--
State: 0 "[0,1]" {0}
[t] 0
---END--"""
+--END--""")
del aut
del aut2
@@ -82,7 +84,7 @@ gcollect()
aut = spot.translate('GF((p0 -> Gp0) R p1)')
daut = spot.tgba_determinize(aut, True)
-assert daut.to_str() == """HOA: v1
+tc.assertEqual(daut.to_str(), """HOA: v1
States: 3
Start: 0
AP: 2 "p1" "p0"
@@ -106,7 +108,7 @@ State: 2 "{₀[0]₀}{₁[1]₁}"
[!0&1] 2
[0&!1] 0 {0}
[0&1] 1 {2}
---END--"""
+--END--""")
del aut
del daut
@@ -129,7 +131,7 @@ State: 1
""")
daut = spot.tgba_determinize(aut, True)
-assert daut.to_str() == """HOA: v1
+tc.assertEqual(daut.to_str(), """HOA: v1
States: 12
Start: 0
AP: 2 "a" "b"
@@ -185,18 +187,18 @@ State: 11 "{₀[1#1]{₁[0#0,0#1]{₂[1#0]₂}₁}₀}"
[!0&1] 2 {0}
[0&!1] 6 {0}
[0&1] 9 {0}
---END--"""
+--END--""")
a = spot.translate('!Gp0 xor FG((p0 W Gp1) M p1)')
a = spot.degeneralize_tba(a)
-assert a.num_states() == 8
+tc.assertEqual(a.num_states(), 8)
b = spot.simulation(a)
-assert b.num_states() == 3
+tc.assertEqual(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
+tc.assertEqual(b.to_str(), """HOA: v1
States: 1
Start: 0
AP: 2 "p0" "p1"
@@ -208,7 +210,7 @@ properties: deterministic stutter-invariant
State: 0 "[1,7]"
[1] 0
[!1] 0 {0}
---END--"""
+--END--""")
aut = spot.automaton('''HOA: v1
States: 12
@@ -267,7 +269,7 @@ State: 11
[0&!1] 6 {0}
[0&1] 9 {0}
--END--''')
-assert spot.reduce_iterated(aut).to_str() == '''HOA: v1
+tc.assertEqual(spot.reduce_iterated(aut).to_str(), '''HOA: v1
States: 9
Start: 0
AP: 2 "a" "b"
@@ -308,7 +310,7 @@ State: 8
[0&!1] 4 {0}
[!0&1] 6
[0&1] 7
---END--'''
+--END--''')
aut = spot.automaton('''HOA: v1
States: 6
@@ -332,7 +334,7 @@ State: 4
State: 5
[0] 5
--END--''')
-assert spot.reduce_iterated(aut).to_str() == '''HOA: v1
+tc.assertEqual(spot.reduce_iterated(aut).to_str(), '''HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
@@ -347,7 +349,7 @@ State: 1
[0] 2
State: 2
[1] 2
---END--'''
+--END--''')
aut = spot.automaton('''HOA: v1
States: 5
@@ -374,7 +376,7 @@ State: 4
[0&1&!2&3] 4 {0}
--END--''')
-assert spot.reduce_direct_cosim(aut).to_str() == '''HOA: v1
+tc.assertEqual(spot.reduce_direct_cosim(aut).to_str(), '''HOA: v1
States: 5
Start: 0
AP: 4 "p0" "p2" "p3" "p1"
@@ -395,7 +397,7 @@ State: 3
[0&!1&2&3] 3 {1}
State: 4
[0&!1&2&3] 4 {0}
---END--'''
+--END--''')
aut = spot.automaton('''HOA: v1
States: 2
@@ -410,7 +412,7 @@ State: 0
State: 1
[0] 0
--END--''')
-assert spot.reduce_direct_sim(aut).to_str() == '''HOA: v1
+tc.assertEqual(spot.reduce_direct_sim(aut).to_str(), '''HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
@@ -418,7 +420,7 @@ Acceptance: 2 Fin(0) & Fin(1)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
---END--'''
+--END--''')
aut = spot.automaton('''HOA: v1
name: "(p1 U p2) U p3"
@@ -445,7 +447,7 @@ State: 3
[1] 1
[0&!1] 3
--END--''')
-assert spot.reduce_direct_cosim_sba(aut).to_str() == '''HOA: v1
+tc.assertEqual(spot.reduce_direct_cosim_sba(aut).to_str(), '''HOA: v1
States: 4
Start: 0
AP: 3 "p2" "p3" "p1"
@@ -468,7 +470,7 @@ State: 2
State: 3
[0] 1
[!0&2] 3
---END--'''
+--END--''')
aut = spot.automaton('''HOA: v1
States: 4
@@ -488,7 +490,7 @@ State: 2
State: 3 {0}
[1] 3
--END--''')
-assert spot.reduce_direct_cosim(aut).to_str() == '''HOA: v1
+tc.assertEqual(spot.reduce_direct_cosim(aut).to_str(), '''HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
@@ -502,9 +504,9 @@ State: 1
[1] 2
State: 2 {0}
[1] 2
---END--'''
+--END--''')
-assert spot.reduce_direct_sim_sba(aut).to_str() == '''HOA: v1
+tc.assertEqual(spot.reduce_direct_sim_sba(aut).to_str(), '''HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
@@ -516,7 +518,7 @@ State: 0
[0] 1
State: 1 {0}
[1] 1
---END--'''
+--END--''')
aut = spot.automaton('''HOA: v1
States: 3
@@ -532,7 +534,7 @@ State: 1
State: 2 {0}
[0] 2
--END--''')
-assert spot.reduce_iterated_sba(aut).to_str() == '''HOA: v1
+tc.assertEqual(spot.reduce_iterated_sba(aut).to_str(), '''HOA: v1
States: 1
Start: 0
AP: 1 "a"
@@ -542,7 +544,7 @@ properties: deterministic
--BODY--
State: 0 {0}
[0] 0
---END--'''
+--END--''')
aut = spot.automaton('''HOA: v1
States: 30
@@ -630,7 +632,7 @@ State: 28
State: 29
[0&!1&!2&!3] 29
--END--''')
-assert spot.reduce_iterated(a).to_str() == '''HOA: v1
+tc.assertEqual(spot.reduce_iterated(a).to_str(), '''HOA: v1
States: 8
Start: 0
AP: 2 "p0" "p1"
@@ -669,7 +671,7 @@ State: 7
[!1] 1 {0}
[0&1] 5
[1] 7
---END--'''
+--END--''')
# issue #452
@@ -707,4 +709,4 @@ State: 8
[@p] 3 {0 1}
--END--""")
aut = spot.simulation(aut)
-assert aut.num_states() == 1
+tc.assertEqual(aut.num_states(), 1)
diff --git a/tests/python/sonf.py b/tests/python/sonf.py
index 558f90c63..40af758b0 100644
--- a/tests/python/sonf.py
+++ b/tests/python/sonf.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita
+# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement de l'Epita
# (LRDE).
#
# This file is part of Spot, a model checking library.
@@ -18,6 +18,8 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
formulas = """\
{x[*]}[]-> F({y[*]}<>-> GFz)
@@ -38,4 +40,4 @@ for f1 in formulas.splitlines():
rm.add_ap(ap)
a2 = rm.strip(a2)
- assert(spot.are_equivalent(a1, a2))
+ tc.assertTrue(spot.are_equivalent(a1, a2))
diff --git a/tests/python/split.py b/tests/python/split.py
index adab5a931..b916f494f 100644
--- a/tests/python/split.py
+++ b/tests/python/split.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018-2021 Laboratoire de Recherche et
+# Copyright (C) 2018-2022 Laboratoire de Recherche et
# Développement de l'Epita
#
# This file is part of Spot, a model checking library.
@@ -19,6 +19,8 @@
import spot
import buddy
+from unittest import TestCase
+tc = TestCase()
# CPython use reference counting, so that automata are destructed
# when we expect them to be. However other implementations like
@@ -51,16 +53,17 @@ def do_split(f, out_list):
return aut, s
aut, s = do_split('(FG !a) <-> (GF b)', ['b'])
-assert equiv(aut, spot.unsplit_2step(s))
+tc.assertTrue(equiv(aut, spot.unsplit_2step(s)))
del aut
del s
gcollect()
aut, s = do_split('GFa && GFb', ['b'])
-assert equiv(aut, spot.unsplit_2step(s))
-# FIXME see below
-# assert str_diff("""HOA: v1
+tc.assertTrue(equiv(aut, spot.unsplit_2step(s)))
+# FIXME s.to_str() is NOT the same on Debian stable and on Debian unstable
+# we should investigate this. See Issue #502.
+# tc.assertEqual("""HOA: v1
# States: 3
# Start: 0
# AP: 2 "a" "b"
@@ -86,10 +89,11 @@ del s
gcollect()
aut, s = do_split('! ((G (req -> (F ack))) && (G (go -> (F grant))))', ['ack'])
-assert equiv(aut, spot.unsplit_2step(s))
+tc.assertTrue(equiv(aut, spot.unsplit_2step(s)))
+
# FIXME s.to_str() is NOT the same on Debian stable and on Debian unstable
-# we should investigate this
-# assert s.to_str() == """HOA: v1
+# we should investigate this. See Issue #502.
+# tc.assertEqual(s.to_str(), """HOA: v1
# States: 9
# Start: 0
# AP: 4 "ack" "req" "go" "grant"
@@ -122,7 +126,7 @@ assert equiv(aut, spot.unsplit_2step(s))
# [!0] 1
# State: 8 {0}
# [!3] 2
-# --END--"""
+# --END--""")
del aut
del s
@@ -131,4 +135,4 @@ 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))',
['g_0', 'g_1'])
-assert equiv(aut, spot.unsplit_2step(s))
+tc.assertTrue(equiv(aut, spot.unsplit_2step(s)))
diff --git a/tests/python/streett_totgba.py b/tests/python/streett_totgba.py
index 1c0bfc13e..8a18defbc 100644
--- a/tests/python/streett_totgba.py
+++ b/tests/python/streett_totgba.py
@@ -1,7 +1,7 @@
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017, 2018, 2021 Laboratoire de Recherche et Développement de
-# l'EPITA.
+# Copyright (C) 2017-2018, 2021-2022 Laboratoire de Recherche et
+# Développement de l'EPITA.
#
# This file is part of Spot, a model checking library.
#
@@ -22,7 +22,8 @@ import spot
import os
import shutil
import sys
-
+from unittest import TestCase
+tc = TestCase()
def tgba(a):
if not a.is_existential():
@@ -33,11 +34,11 @@ def tgba(a):
def test_aut(aut):
stgba = tgba(aut)
- assert stgba.equivalent_to(aut)
+ tc.assertTrue(stgba.equivalent_to(aut))
os.environ["SPOT_STREETT_CONV_MIN"] = '1'
sftgba = tgba(aut)
del os.environ["SPOT_STREETT_CONV_MIN"]
- assert stgba.equivalent_to(sftgba)
+ tc.assertTrue(stgba.equivalent_to(sftgba))
slike = spot.simplify_acceptance(aut)
@@ -45,8 +46,7 @@ def test_aut(aut):
os.environ["SPOT_STREETT_CONV_MIN"] = "1"
slftgba = tgba(slike)
del os.environ["SPOT_STREETT_CONV_MIN"]
- assert sltgba.equivalent_to(slftgba)
-
+ tc.assertTrue(sltgba.equivalent_to(slftgba))
if shutil.which('ltl2dstar') is None:
sys.exit(77)
diff --git a/tests/python/streett_totgba2.py b/tests/python/streett_totgba2.py
index 852eff0af..5ff97a369 100644
--- a/tests/python/streett_totgba2.py
+++ b/tests/python/streett_totgba2.py
@@ -1,7 +1,7 @@
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018 Laboratoire de Recherche et Développement de
-# l'EPITA.
+# Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement
+# de l'EPITA.
#
# This file is part of Spot, a model checking library.
#
@@ -19,6 +19,8 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
# Issue 316
a = spot.automaton("""
@@ -60,11 +62,11 @@ State: 7 {1 3 4}
""")
tgba = spot.streett_to_generalized_buchi(a)
-assert tgba.acc().is_generalized_buchi()
+tc.assertTrue(tgba.acc().is_generalized_buchi())
ba = spot.simplify_acceptance(a)
-assert ba.acc().is_buchi()
+tc.assertTrue(ba.acc().is_buchi())
nba = spot.dualize(ba.postprocess('generic', 'deterministic'))
ntgba = spot.dualize(tgba.postprocess('generic', 'deterministic'))
-assert not ba.intersects(ntgba)
-assert not tgba.intersects(nba)
+tc.assertFalse(ba.intersects(ntgba))
+tc.assertFalse(tgba.intersects(nba))
diff --git a/tests/python/stutter.py b/tests/python/stutter.py
index dafb03b7e..05c28fda9 100644
--- a/tests/python/stutter.py
+++ b/tests/python/stutter.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2019-2021 Laboratoire de Recherche et Développement de
+# Copyright (C) 2019-2022 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@@ -23,6 +23,8 @@
import spot
+from unittest import TestCase
+tc = TestCase()
def explain_stut(f):
@@ -45,20 +47,20 @@ def explain_stut(f):
# Test from issue #388
w1, w2 = explain_stut('{(a:b) | (a;b)}|->Gc')
-assert str(w1) == 'a & !b & !c; cycle{!a & b & !c}'
-assert str(w2) == 'a & !b & !c; a & !b & !c; cycle{!a & b & !c}'
+tc.assertEqual(str(w1), 'a & !b & !c; cycle{!a & b & !c}')
+tc.assertEqual(str(w2), 'a & !b & !c; a & !b & !c; cycle{!a & b & !c}')
# Test from issue #401
w1, w2 = explain_stut('G({x} |-> ({x[+]} <>-> ({Y1[+]} <>=> Y2)))')
-assert str(w1) == 'cycle{!Y1 & !Y2 & x; Y1 & Y2 & x}'
-assert str(w2) == 'cycle{!Y1 & !Y2 & x; Y1 & Y2 & x; Y1 & Y2 & x}'
+tc.assertEqual(str(w1), 'cycle{!Y1 & !Y2 & x; Y1 & Y2 & x}')
+tc.assertEqual(str(w2), 'cycle{!Y1 & !Y2 & x; Y1 & Y2 & x; Y1 & Y2 & x}')
# Related to issue #401 as well. sl() and sl2() should upgrade
# the t acceptance condition into inf(0).
pos = spot.translate('Xa & XXb')
w = pos.accepting_word().as_automaton()
-assert w.acc().is_t()
+tc.assertTrue(w.acc().is_t())
a = spot.sl2(w)
-assert a.acc().is_buchi()
+tc.assertTrue(a.acc().is_buchi())
a = spot.sl(w)
-assert a.acc().is_buchi()
+tc.assertTrue(a.acc().is_buchi())
diff --git a/tests/python/sum.py b/tests/python/sum.py
index 7e2e74220..1f7c6e0a1 100644
--- a/tests/python/sum.py
+++ b/tests/python/sum.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017-2019 Laboratoire de Recherche et Développement
-# de l'Epita
+# Copyright (C) 2017-2019, 2022 Laboratoire de Recherche et
+# Développement de l'Epita
#
# This file is part of Spot, a model checking library.
#
@@ -20,6 +20,8 @@
import spot
import sys
import itertools
+from unittest import TestCase
+tc = TestCase()
# make sure that we are not allowed to build the sum of two automata with
# different dictionaries.
@@ -65,8 +67,8 @@ for p in zip(phi1, phi2):
p0orp1 = spot.formula.Or(p)
a1ora2 = spot.remove_alternation(spot.sum(a1, a2), True)
- assert p0orp1.equivalent_to(a1ora2)
+ tc.assertTrue(p0orp1.equivalent_to(a1ora2))
p0andp1 = spot.formula.And(p)
a1anda2 = spot.remove_alternation(spot.sum_and(a1, a2), True)
- assert p0andp1.equivalent_to(a1anda2)
+ tc.assertTrue(p0andp1.equivalent_to(a1anda2))
diff --git a/tests/python/synthesis.py b/tests/python/synthesis.py
index 59022624c..e1a88650a 100644
--- a/tests/python/synthesis.py
+++ b/tests/python/synthesis.py
@@ -18,6 +18,8 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
# A shared variable caused the 2nd call to ltl_to_game to give an incorrect
# result.
@@ -25,11 +27,11 @@ for i in range(0, 2):
gi = spot.synthesis_info()
gi.s = spot.synthesis_info.algo_LAR
game = spot.ltl_to_game("(Ga) <-> (Fb)", ["b"], gi)
- assert not spot.solve_game(game)
+ tc.assertFalse(spot.solve_game(game))
# A game can have only inputs
game = spot.ltl_to_game("GFa", [])
-assert(game.to_str() == """HOA: v1
+tc.assertEqual(game.to_str(), """HOA: v1
States: 3
Start: 0
AP: 1 "a"
diff --git a/tests/python/toparity.py b/tests/python/toparity.py
index df226ebe4..37e111f9b 100644
--- a/tests/python/toparity.py
+++ b/tests/python/toparity.py
@@ -1,6 +1,6 @@
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018-2021 Laboratoire de Recherche et Développement de
+# Copyright (C) 2018-2022 Laboratoire de Recherche et Développement de
# l'EPITA.
#
# This file is part of Spot, a model checking library.
@@ -21,6 +21,8 @@
import spot
from itertools import zip_longest
from buddy import bddfalse
+from unittest import TestCase
+tc = TestCase()
# Tests for the new version of to_parity
@@ -114,17 +116,16 @@ def test(aut, expected_num_states=[], full=True):
if opt is not None and opt.parity_prefix is False:
# Reduce the number of colors to help are_equivalent
spot.reduce_parity_here(p1)
- assert spot.are_equivalent(aut, p1)
+ tc.assertTrue(spot.are_equivalent(aut, p1))
if expected_num is not None:
- # print(p1.num_states(), expected_num)
- assert p1.num_states() == expected_num
+ tc.assertEqual(p1.num_states(), expected_num)
if full and opt is not None:
# Make sure passing opt is the same as setting
# each argument individually
p2 = spot.to_parity(aut, opt)
- assert p2.num_states() == p1st
- assert p2.num_edges() == p1ed
- assert p2.num_sets() == p1se
+ tc.assertEqual(p2.num_states(), p1st)
+ tc.assertEqual(p2.num_edges(), p1ed)
+ tc.assertEqual(p2.num_sets(), p1se)
test(spot.automaton("""HOA: v1
name: "(FGp0 & ((XFp0 & F!p1) | F(Gp1 & XG!p0))) | G(F!p0 & (XFp0 | F!p1) &
@@ -351,7 +352,7 @@ State: 0
[!0&!1] 0
--END--""")
p = spot.to_parity_old(a, True)
-assert spot.are_equivalent(a, p)
+tc.assertTrue(spot.are_equivalent(a, p))
test(a)
a = spot.automaton("""
@@ -363,8 +364,8 @@ explicit-labels trans-acc --BODY-- State: 0 [0&1] 2 {4 5} [0&1] 4 {0 4}
4 [!0&!1] 1 {2 4} State: 5 [!0&1] 4 --END--
""")
p = spot.to_parity_old(a, True)
-assert p.num_states() == 22
-assert spot.are_equivalent(a, p)
+tc.assertEqual(p.num_states(), 22)
+tc.assertTrue(spot.are_equivalent(a, p))
test(a, [8, 6, 6, 6, 6, 6, 6, 6])
# Force a few edges to false, to make sure to_parity() is OK with that.
@@ -377,22 +378,22 @@ for e in a.out(3):
e.cond = bddfalse
break
p = spot.to_parity_old(a, True)
-assert p.num_states() == 22
-assert spot.are_equivalent(a, p)
+tc.assertEqual(p.num_states(), 22)
+tc.assertTrue(spot.are_equivalent(a, p))
test(a, [7, 6, 6, 6, 6, 6, 6, 6])
for f in spot.randltl(4, 400):
d = spot.translate(f, "det", "G")
p = spot.to_parity_old(d, True)
- assert spot.are_equivalent(p, d)
+ tc.assertTrue(spot.are_equivalent(p, d))
for f in spot.randltl(5, 2000):
n = spot.translate(f)
p = spot.to_parity_old(n, True)
- assert spot.are_equivalent(n, p)
+ tc.assertTrue(spot.are_equivalent(n, p))
# Issue #390.
a = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det')
b = spot.to_parity_old(a, True)
-assert a.equivalent_to(b)
+tc.assertTrue(a.equivalent_to(b))
test(a, [7, 7, 3, 7, 7, 7, 3, 3])
diff --git a/tests/python/toweak.py b/tests/python/toweak.py
index b2d908037..23dcf66fa 100644
--- a/tests/python/toweak.py
+++ b/tests/python/toweak.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017, 2018, 2020 Laboratoire de Recherche et Développement
-# de l'Epita
+# Copyright (C) 2017, 2018, 2020, 2022 Laboratoire de Recherche et
+# Développement de l'Epita
#
# This file is part of Spot, a model checking library.
#
@@ -18,6 +18,8 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
phi1 = """GFb
X(!b | GF!a)
@@ -33,7 +35,7 @@ b | (a & XF(b R a)) | (!a & XG(!b U !a))"""
def test_phi(phi):
a = spot.translate(phi, 'GeneralizedBuchi', 'SBAcc')
res = spot.to_weak_alternating(spot.dualize(a))
- assert res.equivalent_to(spot.formula.Not(spot.formula(phi)))
+ tc.assertTrue(res.equivalent_to(spot.formula.Not(spot.formula(phi))))
for p in phi1.split('\n'):
@@ -83,4 +85,4 @@ State: 6
--END--
""")
a2 = spot.to_weak_alternating(a2)
-assert a2.equivalent_to(phi2)
+tc.assertTrue(a2.equivalent_to(phi2))
diff --git a/tests/python/tra2tba.py b/tests/python/tra2tba.py
index b303c010b..354ced630 100644
--- a/tests/python/tra2tba.py
+++ b/tests/python/tra2tba.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016-2018, 2020-2021 Laboratoire de Recherche
+# Copyright (C) 2016-2018, 2020-2022 Laboratoire de Recherche
# et Développement de l'Epita
#
# This file is part of Spot, a model checking library.
@@ -18,6 +18,8 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
# CPython use reference counting, so that automata are destructed
# when we expect them to be. However other implementations like
@@ -57,7 +59,7 @@ State: 1
--END--"""
res = spot.remove_fin(aut)
-assert(res.to_str('hoa') == exp)
+tc.assertEqual(res.to_str('hoa'), exp)
# Test 2.
aut = spot.automaton("""
@@ -97,7 +99,7 @@ State: 2
--END--"""
res = spot.remove_fin(aut)
-assert(res.to_str('hoa') == exp)
+tc.assertEqual(res.to_str('hoa'), exp)
# Test 3.
aut = spot.automaton("""
@@ -128,7 +130,7 @@ State: 0
--END--"""
res = spot.remove_fin(aut)
-assert(res.to_str('hoa') == exp)
+tc.assertEqual(res.to_str('hoa'), exp)
# Test 4.
aut = spot.automaton("""
@@ -168,7 +170,7 @@ State: 2 {0}
--END--"""
res = spot.remove_fin(aut)
-assert(res.to_str('hoa') == exp)
+tc.assertEqual(res.to_str('hoa'), exp)
# Test 5.
aut = spot.automaton("""
@@ -214,7 +216,7 @@ State: 3 {0}
--END--"""
res = spot.remove_fin(aut)
-assert(res.to_str('hoa') == exp)
+tc.assertEqual(res.to_str('hoa'), exp)
# Test 6.
aut = spot.automaton("""
@@ -257,7 +259,7 @@ State: 2 {0}
--END--"""
res = spot.remove_fin(aut)
-assert(res.to_str('hoa') == exp)
+tc.assertEqual(res.to_str('hoa'), exp)
# Test 7.
aut = spot.automaton("""
@@ -292,7 +294,7 @@ State: 1 {0}
--END--"""
res = spot.remove_fin(aut)
-assert(res.to_str('hoa') == exp)
+tc.assertEqual(res.to_str('hoa'), exp)
# Test 8.
aut = spot.automaton("""
@@ -372,9 +374,9 @@ State: 7
res = spot.remove_fin(aut)
if is_cpython:
- assert(res.to_str('hoa') == exp)
+ tc.assertEqual(res.to_str('hoa'), exp)
else:
- assert(res.equivalent_to(spot.automaton(exp)))
+ tc.assertTrue(res.equivalent_to(spot.automaton(exp)))
# Test 9.
aut = spot.automaton("""
@@ -411,9 +413,9 @@ State: 1
res = spot.remove_fin(aut)
if is_cpython:
- assert(res.to_str('hoa') == exp)
+ tc.assertEqual(res.to_str('hoa'), exp)
else:
- assert(res.equivalent_to(spot.automaton(exp)))
+ tc.assertTrue(res.equivalent_to(spot.automaton(exp)))
# Test 10.
aut = spot.automaton("""
@@ -453,9 +455,9 @@ State: 2 {0}
res = spot.remove_fin(aut)
if is_cpython:
- assert(res.to_str('hoa') == exp)
+ tc.assertEqual(res.to_str('hoa'), exp)
else:
- assert(res.equivalent_to(spot.automaton(exp)))
+ tc.assertTrue(res.equivalent_to(spot.automaton(exp)))
# Test 11.
aut = spot.automaton("""
@@ -493,9 +495,9 @@ State: 1
res = spot.remove_fin(aut)
if is_cpython:
- assert(res.to_str('hoa') == exp)
+ tc.assertEqual(res.to_str('hoa'), exp)
else:
- assert(res.equivalent_to(spot.automaton(exp)))
+ tc.assertTrue(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
@@ -518,9 +520,9 @@ State: 1
--END--"""
res = spot.rabin_to_buchi_if_realizable(aut)
if is_cpython:
- assert(res.to_str('hoa') == exp2)
+ tc.assertEqual(res.to_str('hoa'), exp2)
else:
- assert(res.equivalent_to(spot.automaton(exp2)))
+ tc.assertTrue(res.equivalent_to(spot.automaton(exp2)))
# Test 12.
aut = spot.automaton("""
@@ -565,9 +567,9 @@ State: 3 {0}
res = spot.remove_fin(aut)
if is_cpython:
- assert(res.to_str('hoa') == exp)
+ tc.assertEqual(res.to_str('hoa'), exp)
else:
- assert(res.equivalent_to(spot.automaton(exp)))
+ tc.assertTrue(res.equivalent_to(spot.automaton(exp)))
# Test 13.
aut = spot.automaton("""
@@ -615,9 +617,9 @@ State: 1
res = spot.remove_fin(aut)
if is_cpython:
- assert(res.to_str('hoa') == exp)
+ tc.assertEqual(res.to_str('hoa'), exp)
else:
- assert(res.equivalent_to(spot.automaton(exp)))
+ tc.assertTrue(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.
@@ -644,9 +646,9 @@ State: 1
res = spot.rabin_to_buchi_if_realizable(aut)
if is_cpython:
- assert(res.to_str('hoa') == exp2)
+ tc.assertEqual(res.to_str('hoa'), exp2)
else:
- assert(res.equivalent_to(spot.automaton(exp2)))
+ tc.assertTrue(res.equivalent_to(spot.automaton(exp2)))
# Test 14.
aut = spot.automaton("""
@@ -681,7 +683,7 @@ State: 1
res = spot.remove_fin(aut)
if is_cpython:
- assert(res.to_str('hoa') == exp)
+ tc.assertEqual(res.to_str('hoa'), exp)
else:
- assert(res.equivalent_to(spot.automaton(exp)))
-assert spot.rabin_to_buchi_if_realizable(aut) is None
+ tc.assertTrue(res.equivalent_to(spot.automaton(exp)))
+tc.assertIsNone(spot.rabin_to_buchi_if_realizable(aut))
diff --git a/tests/python/trival.py b/tests/python/trival.py
index 8fcf6a1fa..ea844e29c 100644
--- a/tests/python/trival.py
+++ b/tests/python/trival.py
@@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016, 2018 Laboratoire de Recherche et Développement
+# Copyright (C) 2016, 2018, 2022 Laboratoire de Recherche et Développement
# de l'Epita
#
# This file is part of Spot, a model checking library.
@@ -18,30 +18,32 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
v1 = spot.trival()
v2 = spot.trival(False)
v3 = spot.trival(True)
v4 = spot.trival_maybe()
-assert v1 != v2
-assert v1 != v3
-assert v2 != v3
-assert v2 == spot.trival(spot.trival.no_value)
-assert v2 != spot.trival(spot.trival.yes_value)
-assert v4 != v2
-assert v4 != v3
-assert v2 == False
-assert True == v3
-assert v2 != True
-assert False != v3
-assert v4 == spot.trival_maybe()
-assert v4 == spot.trival(spot.trival.maybe_value)
-assert v3
-assert -v2
-assert not -v1
-assert not v1
-assert not -v3
+tc.assertNotEqual(v1, v2)
+tc.assertNotEqual(v1, v3)
+tc.assertNotEqual(v2, v3)
+tc.assertEqual(v2, spot.trival(spot.trival.no_value))
+tc.assertNotEqual(v2, spot.trival(spot.trival.yes_value))
+tc.assertNotEqual(v4, v2)
+tc.assertNotEqual(v4, v3)
+tc.assertEqual(v2, False)
+tc.assertEqual(True, v3)
+tc.assertNotEqual(v2, True)
+tc.assertNotEqual(False, v3)
+tc.assertEqual(v4, spot.trival_maybe())
+tc.assertEqual(v4, spot.trival(spot.trival.maybe_value))
+tc.assertTrue(v3)
+tc.assertTrue(-v2)
+tc.assertFalse(-v1)
+tc.assertFalse(v1)
+tc.assertFalse(-v3)
for u in (v1, v2, v3):
for v in (v1, v2, v3):
- assert (u & v) == -(-u | -v)
+ tc.assertEqual((u & v), -(-u | -v))
diff --git a/tests/python/twagraph.py b/tests/python/twagraph.py
index b8834b211..1ebcb8ac5 100644
--- a/tests/python/twagraph.py
+++ b/tests/python/twagraph.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017, 2021 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2017, 2021-2022 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -22,6 +22,8 @@
import spot
from buddy import bddtrue, bddfalse
+from unittest import TestCase
+tc = TestCase()
aut = spot.make_twa_graph(spot.make_bdd_dict())
@@ -29,98 +31,98 @@ try:
print(aut.to_str())
exit(2)
except RuntimeError as e:
- assert "no state" in str(e)
+ tc.assertIn("no state", str(e))
try:
aut.set_init_state(2)
except ValueError as e:
- assert "nonexisting" in str(e)
+ tc.assertIn("nonexisting", str(e))
try:
aut.set_univ_init_state([2, 1])
except ValueError as e:
- assert "nonexisting" in str(e)
+ tc.assertIn("nonexisting", str(e))
aut.new_states(3)
aut.set_init_state(2)
-assert aut.get_init_state_number() == 2
+tc.assertEqual(aut.get_init_state_number(), 2)
aut.set_univ_init_state([2, 1])
-assert [2, 1] == list(aut.univ_dests(aut.get_init_state_number()))
+tc.assertEqual([2, 1], list(aut.univ_dests(aut.get_init_state_number())))
try:
aut.get_init_state()
except RuntimeError as e:
s = str(e)
- assert "abstract interface" in s and "alternating automata" in s
+ tc.assertIn("abstract interface" in s and "alternating automata", s)
cpy = spot.make_twa_graph(aut, spot.twa_prop_set.all())
-assert aut.to_str() == cpy.to_str()
+tc.assertEqual(aut.to_str(), cpy.to_str())
all = aut.set_buchi()
-assert aut.to_str() != cpy.to_str()
+tc.assertNotEqual(aut.to_str(), cpy.to_str())
cpy = spot.make_twa_graph(aut, spot.twa_prop_set.all())
aut.new_acc_edge(0, 1, bddtrue, True)
-assert aut.num_edges() == 1 + cpy.num_edges()
+tc.assertEqual(aut.num_edges(), 1 + cpy.num_edges())
aut.prop_universal(True)
aut.set_name("some name")
cpy = spot.make_twa_graph(aut, spot.twa_prop_set(False, False, False,
False, False, False))
-assert cpy.prop_universal() != aut.prop_universal()
-assert cpy.prop_universal() == spot.trival.maybe()
-assert cpy.get_name() == None
+tc.assertNotEqual(cpy.prop_universal(), aut.prop_universal())
+tc.assertEqual(cpy.prop_universal(), spot.trival.maybe())
+tc.assertEqual(cpy.get_name(), None)
cpy = spot.make_twa_graph(aut, spot.twa_prop_set(False, False, False,
False, False, False), True)
-assert cpy.get_name() == "some name"
+tc.assertEqual(cpy.get_name(), "some name")
from copy import copy
cpy = copy(aut)
-assert aut.to_str() == cpy.to_str()
+tc.assertEqual(aut.to_str(), cpy.to_str())
cpy.set_init_state(1)
-assert [2, 1] == list(aut.univ_dests(aut.get_init_state_number()))
-assert cpy.get_init_state_number() == 1
-assert cpy.get_name() == "some name"
+tc.assertEqual([2, 1], list(aut.univ_dests(aut.get_init_state_number())))
+tc.assertEqual(cpy.get_init_state_number(), 1)
+tc.assertEqual(cpy.get_name(), "some name")
try:
s = aut.state_acc_sets(0)
except RuntimeError as e:
- assert "state-based acceptance" in str(e)
+ tc.assertIn("state-based acceptance", str(e))
try:
s = aut.state_is_accepting(0)
except RuntimeError as e:
- assert "state-based acceptance" in str(e)
+ tc.assertIn("state-based acceptance", str(e))
aut.prop_state_acc(True)
-assert aut.state_acc_sets(0) == all
-assert aut.state_is_accepting(0) == True
+tc.assertEqual(aut.state_acc_sets(0), all)
+tc.assertEqual(aut.state_is_accepting(0), True)
aut.set_init_state(0)
aut.purge_unreachable_states()
i = aut.get_init_state()
-assert aut.state_is_accepting(i) == True
+tc.assertEqual(aut.state_is_accepting(i), True)
it = aut.succ_iter(i)
it.first()
-assert aut.edge_number(it) == 1
-assert aut.state_number(it.dst()) == 1
-assert aut.edge_storage(it).src == 0
-assert aut.edge_storage(1).src == 0
-assert aut.edge_data(it).cond == bddtrue
-assert aut.edge_data(1).cond == bddtrue
+tc.assertEqual(aut.edge_number(it), 1)
+tc.assertEqual(aut.state_number(it.dst()), 1)
+tc.assertEqual(aut.edge_storage(it).src, 0)
+tc.assertEqual(aut.edge_storage(1).src, 0)
+tc.assertEqual(aut.edge_data(it).cond, bddtrue)
+tc.assertEqual(aut.edge_data(1).cond, bddtrue)
aut.release_iter(it)
aut.purge_dead_states()
i = aut.get_init_state()
-assert aut.state_is_accepting(i) == False
+tc.assertEqual(aut.state_is_accepting(i), False)
aut = spot.translate('FGa')
# Kill the edge between state 0 and 1
-assert aut.edge_storage(2).src == 0
-assert aut.edge_storage(2).dst == 1
+tc.assertEqual(aut.edge_storage(2).src, 0)
+tc.assertEqual(aut.edge_storage(2).dst, 1)
aut.edge_data(2).cond = bddfalse
-assert aut.num_edges() == 3
-assert aut.num_states() == 2
+tc.assertEqual(aut.num_edges(), 3)
+tc.assertEqual(aut.num_states(), 2)
aut.purge_dead_states()
-assert aut.num_edges() == 1
-assert aut.num_states() == 1
+tc.assertEqual(aut.num_edges(), 1)
+tc.assertEqual(aut.num_states(), 1)
diff --git a/tests/python/zlktree.py b/tests/python/zlktree.py
index df8fd86f0..e1b0c9e7b 100644
--- a/tests/python/zlktree.py
+++ b/tests/python/zlktree.py
@@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2021 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2021, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -18,6 +18,8 @@
# along with this program. If not, see .
import spot
+from unittest import TestCase
+tc = TestCase()
a = spot.automaton("""HOA: v1 States: 5 Start: 0 AP: 2 "p0" "p1"
Acceptance: 4 Inf(3) | Fin(3) properties: trans-labels explicit-labels
@@ -25,8 +27,8 @@ trans-acc --BODY-- State: 0 [!0&!1] 3 [!0&!1] 4 State: 1 [!0&!1] 4 {3}
[0&!1] 0 {2} [!0&1] 1 {2} State: 2 [!0&1] 0 {0 2} [!0&!1] 1 State: 3
[!0&1] 2 State: 4 [0&!1] 3 --END--""")
b = spot.zielonka_tree_transform(a)
-assert spot.are_equivalent(a, b)
-assert b.acc().is_buchi()
+tc.assertTrue(spot.are_equivalent(a, b))
+tc.assertTrue(b.acc().is_buchi())
def report_missing_exception():
raise RuntimeError("missing exception")
@@ -45,95 +47,96 @@ State: 2 [0&1] 8 {3} [0&1] 2 {1} [!0&1] 4 {3 4} [!0&!1] 3 {2 5} State:
[!0&!1] 2 {5} [!0&!1] 0 {3} [!0&!1] 5 --END--""")
aa = spot.acd(a)
try:
- assert aa.has_rabin_shape()
+ tc.assertTrue(aa.has_rabin_shape())
except RuntimeError as e:
- assert 'CHECK_RABIN' in str(e)
+ tc.assertIn('CHECK_RABIN', str(e))
else:
report_missing_exception()
try:
- assert not aa.has_streett_shape()
+ tc.assertFalse(aa.has_streett_shape())
except RuntimeError as e:
- assert 'CHECK_STREETT' in str(e)
+ tc.assertIn('CHECK_STREETT', str(e))
else:
report_missing_exception()
try:
- assert not aa.has_parity_shape()
+ tc.assertFalse(aa.has_parity_shape())
except RuntimeError as e:
- assert 'CHECK_PARITY' in str(e)
+ tc.assertIn('CHECK_PARITY', str(e))
else:
report_missing_exception()
aa = spot.acd(a, spot.acd_options_CHECK_RABIN)
-assert aa.has_rabin_shape()
-assert aa.node_count() == 13
+tc.assertTrue(aa.has_rabin_shape())
+tc.assertEqual(aa.node_count(), 13)
try:
- assert not aa.has_streett_shape()
+ tc.assertFalse(aa.has_streett_shape())
except RuntimeError as e:
- assert 'CHECK_STREETT' in str(e)
+ tc.assertIn('CHECK_STREETT', str(e))
else:
report_missing_exception()
try:
- assert aa.has_parity_shape()
+ tc.assertTrue(aa.has_parity_shape())
except RuntimeError as e:
- assert 'CHECK_PARITY' in str(e)
+ tc.assertIn('CHECK_PARITY', str(e))
else:
report_missing_exception()
aa = spot.acd(a, (spot.acd_options_CHECK_PARITY |
spot.acd_options_ABORT_WRONG_SHAPE))
-assert aa.has_rabin_shape()
-assert not aa.has_streett_shape()
-assert not aa.has_parity_shape()
-assert aa.node_count() == 0
+tc.assertTrue(aa.has_rabin_shape())
+tc.assertFalse(aa.has_streett_shape())
+tc.assertFalse(aa.has_parity_shape())
+tc.assertEqual(aa.node_count(), 0)
+
try:
aa.first_branch(0)
except RuntimeError as e:
- assert 'ABORT_WRONG_SHAPE' in str(e)
+ tc.assertIn('ABORT_WRONG_SHAPE', str(e))
else:
report_missing_exception()
try:
aa.step(0, 0)
except RuntimeError as e:
- assert 'incorrect branch number' in str(e)
+ tc.assertIn('incorrect branch number', str(e))
else:
report_missing_exception()
try:
aa.node_acceptance(0)
except RuntimeError as e:
- assert 'unknown node' in str(e)
+ tc.assertIn('unknown node', str(e))
else:
report_missing_exception()
try:
aa.edges_of_node(0)
except RuntimeError as e:
- assert 'unknown node' in str(e)
+ tc.assertIn('unknown node', str(e))
else:
report_missing_exception()
try:
aa.node_level(0)
except RuntimeError as e:
- assert 'unknown node' in str(e)
+ tc.assertIn('unknown node', str(e))
else:
report_missing_exception()
a = spot.translate('true')
a.set_acceptance(spot.acc_cond('f'))
b = spot.acd_transform(a)
-assert a.equivalent_to(b)
+tc.assertTrue(a.equivalent_to(b))
a = spot.translate('true')
a.set_acceptance(spot.acc_cond('f'))
b = spot.zielonka_tree_transform(a)
-assert a.equivalent_to(b)
+tc.assertTrue(a.equivalent_to(b))
a = spot.automaton("""HOA: v1 name: "^ G F p0 G F p1" States: 5 Start:
2 AP: 2 "a" "b" acc-name: Rabin 2 Acceptance: 4 (Fin(0) & Inf(1)) |
@@ -144,8 +147,8 @@ complete properties: deterministic --BODY-- State: 0 {0} [!0&!1] 0
2} [!0&!1] 1 [0&!1] 4 [!0&1] 3 [0&1] 2 State: 4 {0 3} [!0&!1] 0 [0&!1]
4 [!0&1] 3 [0&1] 2 --END--""")
b = spot.acd_transform_sbacc(a, True)
-assert str(b.acc()) == '(3, Fin(0) & (Inf(1) | Fin(2)))'
-assert a.equivalent_to(b)
+tc.assertEqual(str(b.acc()), '(3, Fin(0) & (Inf(1) | Fin(2)))')
+tc.assertTrue(a.equivalent_to(b))
b = spot.acd_transform_sbacc(a, False)
-assert str(b.acc()) == '(2, Fin(0) & Inf(1))'
-assert a.equivalent_to(b)
+tc.assertEqual(str(b.acc()), '(2, Fin(0) & Inf(1))')
+tc.assertTrue(a.equivalent_to(b))
diff --git a/tests/sanity/style.test b/tests/sanity/style.test
index 8f157014d..85ef359b0 100755
--- a/tests/sanity/style.test
+++ b/tests/sanity/style.test
@@ -1,6 +1,6 @@
#! /bin/sh
# -*- coding: utf-8 -*-
-# Copyright (C) 2009-2021 Laboratoire de Recherche et Développement de
+# Copyright (C) 2009-2022 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
# Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6
# (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -392,6 +392,27 @@ for dir in "${INCDIR-..}" "${INCDIR-..}/../bin" "${INCDIR-..}/../tests"; do
done || : # Make sure sh does not abort when read exits with false.
done
+# Rules for Python tests
+for dir in "${INCDIR-..}/../tests"; do
+
+ find "$dir" -name "*.py" -a -type f -a -print |
+ while read file; do
+ fail=false
+
+ # Strip comments.
+ sed 's,[ ]*#.*,,' < $file > $tmp
+
+ $GREP '[ ]$' $tmp &&
+ diag 'Trailing whitespace.'
+
+ $GREP -E '([ ]|^)assert[ (]' $tmp &&
+ diag "replace assert keywords by unittest assertion tests"
+
+ $fail && echo "$file" >>failures.style
+ done || : # Make sure sh does not abort when read exits with false.
+done
+
+
if test -f failures.style; then
echo "The following files contain style errors:"
cat failures.style