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

twagraph: merge_edge() can determinize automata

Reported by František Blahoudek.

* spot/twa/twagraph.cc: Reset prop_universal() if edges are merged in
a non-deterministic automaton.
* tests/core/det.test: Add test case.
* NEWS: Mention the issue.
parent 383d1c00
......@@ -5,6 +5,15 @@ New in spot 2.8.4.dev (not yet released)
- ltl2tgba -B could return automata with "t" acceptance, instead
of the expected Inf(0).
- twa_graph::merge_edges() (a.k.a. autfilt --merge-transitions) was
unaware that merging edges can sometimes transform a
non-deterministic automaton into a deterministic one, causing the
following unexpected diagnostic:
"print_hoa(): automaton is universal despite prop_universal()==false"
The kind of non-deterministic automata where this occurs is not
naturally produced by any Spot algorithm, but can be found for
instance in automata produced by Goal 2015-10-18.
New in spot 2.8.4 (2019-12-08)
Bugs fixed:
......
......@@ -148,7 +148,8 @@ namespace spot
});
auto& trans = this->edge_vector();
unsigned tend = trans.size();
unsigned orig_size = trans.size();
unsigned tend = orig_size;
unsigned out = 0;
unsigned in = 1;
// Skip any leading false edge.
......@@ -233,6 +234,13 @@ namespace spot
}
g_.chain_edges_();
// Did we actually reduce the number of edges?
if (trans.size() != orig_size)
// Merging some edges may turn a non-deterministic automaton
// into a deterministic one.
if (prop_universal().is_false())
prop_universal(trival::maybe());
}
void twa_graph::merge_states()
......
......@@ -275,3 +275,25 @@ State: 1
--END--
EOF
diff output expected
# This is a syntactically non-deterministic automaton, which is
# semantically equivalent to a deterministic automaton (once
# transitions with compatible src/dst are merged). Running
# --merge-transition on this used to fail because merge_edges() would
# preserve the determism bit (or rather, the non-determinism bit).
cat >in.hoa <<EOF
HOA: v1
States: 2
Start: 1
AP: 2 "a" "b"
Acceptance: 1 Inf(0)
--BODY--
State: 0 {0}
[t] 0
State: 1
[0] 0
[1] 0
--END--
EOF
autfilt -q --is-deterministic in.hoa && exit 1
autfilt --merge-transitions in.hoa | autfilt --is-deterministic
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