alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

python: fix return of is_rabin_like() and is_streett_like()

Browse source 
* python/spot/impl.i: Fix instantiation of vector_rs_pairs.
* tests/python/setacc.py: Add test cases.
* NEWS: Mention the bugs.
This commit is contained in:
Alexandre Duret-Lutz 2018-10-31 19:43:26 +01:00
parent 266581b272
commit 5bb9c87d4c
3 changed files with 25 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

19
tests/python/setacc.py
View file

@ -36,3 +36,22 @@ assert 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]
# 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]
(b, v) = spot.acc_cond("(Fin(0)|Inf(1))&(Fin(2)|Inf(0))").is_rabin_like()
assert b == False
assert len(v) == 0
(b, v) = spot.acc_cond("(Fin(0)|Inf(1))&(Fin(2)|Inf(0))").is_streett_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]