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

is_unambiguous: fix detection of empty languages

* src/tests/unambig.test: New test case.  Reported by Ming-Hsien Tsai.
* src/twaalgos/sccfilter.cc: Always create an initial state.
* src/twaalgos/isunamb.cc: Speed up on empty languages.
* NEWS, THANKS: Update.
parent 61bf5daa
......@@ -65,6 +65,8 @@ New in spot 1.99.4a (not yet released)
* "ltlgrind -F FILENAME/COL" did not preserve other CSV columns.
* "ltlgrind --help" did not document FORMAT.
* unabbreviate could easily use forbidden operators.
* "autfilt --is-unambiguous" could fail to detect the nonambiguity
of some automata with empty languages.
New in spot 1.99.4 (2015-10-01)
......
......@@ -21,6 +21,7 @@ Kristin Y. Rozier
Martin Dieguez Lodeiro
Michael Tautschnig
Michael Weber
Ming-Hsien Tsai
Nikos Gorogiannis
Rüdiger Ehlers
Silien Hong
......
......@@ -153,4 +153,22 @@ test `grep -c unambiguous output` = 0
../../bin/randltl --psl -n 1000 3 | $ltl2tgba -U -F- -H |
$autfilt -v --is-unamb --stats=%M && exit 1
:
cat >input <<EOF
HOA: v1
properties: explicit-labels state-acc trans-labels
States: 3
Start: 0
AP: 0
Acceptance: 1 Inf(0)
acc-name: Buchi
name: ""
tool: "GOAL" ""
--BODY--
State: 0
[t] 2
[t] 1
State: 1
State: 2
--END--
EOF
run 0 $autfilt -q --is-unambiguous input
......@@ -30,6 +30,8 @@ namespace spot
if (aut->is_deterministic() || aut->is_unambiguous())
return true;
auto clean_a = scc_filter_states(aut);
if (clean_a->num_edges() == 0)
return true;
auto prod = product(clean_a, clean_a);
auto clean_p = scc_filter_states(prod);
return clean_a->num_states() == clean_p->num_states()
......
......@@ -324,11 +324,12 @@ namespace spot
}
if (!given_si)
delete si;
// If the initial state has been filtered out, we don't attempt
// to fix it.
// If the initial state has been filtered out, we have to create
// a new one (not doing so may cause empty automata, which in turn
// cause all sort of issue with algorithms assuming an automaton
// has one initial state).
auto init = inout[aut->get_init_state_number()];
if (init < out_n)
filtered->set_init_state(init);
filtered->set_init_state(init < out_n ? init : filtered->new_state());
return filtered;
}
......
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