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

to_weak_alternating(): fixes a bug on generalized co-Büchi automata

Browse source 
Fixes #278. Also adds a test ensuring non-regression.

* spot/twaalgos/toweak.cc: Fixes the bug.
* tests/python/toweak.py: Add a test case.
This commit is contained in:
Thomas Medioni 2017-08-16 17:06:09 +02:00
parent df04c715cf
commit 4b5606e742
2 changed files with 51 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
spot/twaalgos/toweak.cc
View file

@ -121,10 +121,11 @@ namespace spot
int curr = static_cast<int>(rank);
// We must always be able to go to the previous even rank
int lower = less_ ? ((curr - 1) & ~1) : 0;
for (int i = curr; i >= lower; --i)
for (int i = curr, start_set = st.mark.min_set() - 1;
i >= lower; --i, start_set = 0)
{
if (i % 2)
for (unsigned m = 0; m < numsets_; ++m)
for (unsigned m = start_set; m < numsets_; ++m)
levels |= state_to_var_[new_state(d, i, {m})];
else
levels |= state_to_var_[new_state(d, i, 0U)];

48
tests/python/toweak.py
View file

@ -53,3 +53,51 @@ def test_phi(phi):
for p in phi1:
test_phi(p)
phi2 = spot.formula("(G((F a) U b)) W a")
a2 = spot.automaton("""
HOA: v1
States: 7
Start: 1
AP: 2 "a" "b"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels trans-acc complete univ-branch
--BODY--
State: 0
[t] 0 {0 1}
State: 1
[0] 0 {0 1}
[1] 1&2 {0 1}
[0&!1] 1&3 {0 1}
[!0&!1] 1&4 {0 1}
State: 2
[1] 2 {0 1}
[0&!1] 3 {0 1}
[!0&!1] 4 {0 1}
State: 3
[1] 2 {0 1}
[0&!1] 3 {1}
[!0&!1] 4 {1}
State: 4
[0&1] 2 {0 1}
[0&!1] 3 {1}
[!0&!1] 4 {1}
[!0&1] 5 {0 1}
State: 5
[0&1] 2 {0 1}
[0&!1] 3 {0 1}
[!0&1] 5 {0}
[!0&!1] 6 {0}
State: 6
[0&1] 2 {0 1}
[0&!1] 3 {1}
[!0&1] 5 {0}
[!0&!1] 6
--END--
""")
a2 = spot.to_weak_alternating(a2)
assert equivalent(a2, phi2)