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

twagraph: merge_edge() can determinize automata

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2019-12-31 22:34:39 +01:00
parent 2764e81588
commit d1ef380d32
3 changed files with 40 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

10
spot/twa/twagraph.cc
View file

@ -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()