Commit ec393708 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

sbacc: more fixes related to #312

The issue also exists with determinism.

* tests/core/sbacc.test: New test case.
* spot/twaalgos/sbacc.cc: Fix it.
* NEWS: Update.
parent 5467fa16
...@@ -248,9 +248,10 @@ New in spot 2.4.3.dev (not yet released) ...@@ -248,9 +248,10 @@ New in spot 2.4.3.dev (not yet released)
Fin-less & CNF version of the acceptance condition had several Fin-less & CNF version of the acceptance condition had several
unit clauses. unit clauses.
- If the automaton passed to sbacc() was incomplete because of some - If the automaton passed to sbacc() was incomplete or
unreachable states, then it was possible that the output would non-deterministic because of some unreachable states, then it was
marked incomplete while it was in fact complete. possible that the output would marked similarly while it was in
fact complete or deterministic.
New in spot 2.4.3 (2017-12-19) New in spot 2.4.3 (2017-12-19)
......
...@@ -169,14 +169,17 @@ namespace spot ...@@ -169,14 +169,17 @@ namespace spot
} }
res->merge_edges(); res->merge_edges();
// If the automaton was marked as not complete, and we have // If the automaton was marked as not complete or not universal,
// ignored some unreachable state, then it is possible that the // and we have ignored some unreachable state, then it is possible
// result becomes complete. // that the result becomes complete or universal.
if (res->prop_complete().is_false()) if (res->prop_complete().is_false() || res->prop_universal().is_false())
for (unsigned i = 0; i < ns; ++i) for (unsigned i = 0; i < ns; ++i)
if (!si.reachable_state(i)) if (!si.reachable_state(i))
{ {
res->prop_complete(trival::maybe()); if (res->prop_complete().is_false())
res->prop_complete(trival::maybe());
if (res->prop_universal().is_false())
res->prop_universal(trival::maybe());
break; break;
} }
return res; return res;
......
...@@ -276,3 +276,16 @@ State: 0 [t] 0 {0} ...@@ -276,3 +276,16 @@ State: 0 [t] 0 {0}
State: 1 State: 1
--END-- --END--
EOF EOF
autfilt -S <<EOF | autfilt --is-deterministic
HOA: v1
States: 2
Start: 0
AP: 1 "a"
Acceptance: 1 Inf(0)
properties: !complete !deterministic
--BODY--
State: 0 [0] 0 {0}
State: 1 [0] 1 [0] 0
--END--
EOF
Markdown is supported
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