Skip to content

simulation: fix determinism check

Alexandre Duret-Lutz requested to merge adl/575 into next

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 (closed), 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.

Merge request reports