Commit 95fd7594 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

sbacc: fix sbacc producing complete automata marked as incomplete

Fixes #312, reported by František Blahoudek.

* spot/twaalgos/ Detect the case were this can happen,
and fix it.
* tests/core/sbacc.test: New test case.
* NEWS: Mention the bug.
parent 9ec7df67
......@@ -248,6 +248,10 @@ New in spot (not yet released)
Fin-less & CNF version of the acceptance condition had several
unit clauses.
- If the automaton passed to sbacc() was incomplete because of some
unreachable states, then it was possible that the output would
marked incomplete while it was in fact complete.
New in spot 2.4.3 (2017-12-19)
Bugs fixed:
......@@ -168,6 +168,17 @@ namespace spot
// If the automaton was marked as not complete, and we have
// ignored some unreachable state, then it is possible that the
// result becomes complete.
if (res->prop_complete().is_false())
for (unsigned i = 0; i < ns; ++i)
if (!si.reachable_state(i))
return res;
......@@ -262,3 +262,17 @@ EOF
autfilt --sbacc alt.hoa > out.hoa
diff out.hoa expect.hoa
# Issue #312
autfilt -S <<EOF | autfilt --is-complete
HOA: v1
States: 2
Start: 0
AP: 0
Acceptance: 1 Inf(0)
properties: !complete
State: 0 [t] 0 {0}
State: 1
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment