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

simulation: fix determinism check

Browse source 
Commit bda40a5f introduced a subtle bug where nm_minato was being
increased in more cases causing some non-deterministic automata to be
incorrectly tagged as deterministic automata.

Fixes issue #575, reported by Dávid Smolka.

* spot/twaalgos/simulation.cc (create_edges): Do not increment
nm_minato when dest is bddfalse.
* tests/core/568.test: Add Dávid's first test-case.
* tests/python/forq_contains.py: Add Dávid's second test-case.
This commit is contained in:
Alexandre Duret-Lutz 2024-04-24 23:45:47 +02:00
parent ffddbd84d0
commit ab7f4f51c4
3 changed files with 51 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
spot/twaalgos/simulation.cc
View file

@ -582,6 +582,8 @@ namespace spot
unsigned srcst = 0;
auto create_edges = [&](int srcid, bdd one, bdd dest) {
if (dest == bddfalse)
return;
// Iterate over all possible destination classes. We
// use minato_isop here, because if the same valuation
// of atomic properties can go to two different