Skip to content
  • Alexandre Duret-Lutz's avatar
    minimize_wdba: fix handling of input with useless SCCs · c9918f64
    Alexandre Duret-Lutz authored
    * spot/twaalgos/minimize.cc (minimize_wdba): Diminish the color of
    terminal SCCs that are incomplete, as if they had a non-accepting
    sink as successor.
    * spot/twaalgos/strength.hh, spot/twaalgos/strength.cc
    (is_terminal_automaton): Add an option to ignore trivial SCC as we did
    before, since it matters for deciding membership to the guarantee
    class.
    (is_safety_mwdba): Rewrite as ...
    (is_safety_automaton): ... generalizating to any acceptance, and
    ignoring trivial SCCs.
    * bin/ltlfilt.cc, python/ajax/spotcgi.in, spot/tl/hierarchy.cc,
    tests/core/ikwiad.cc: Adjust usage of is_terminal_automaton and
    is_safety_automaton().
    * tests/core/hierarchy.test: Add a problematic formula as test-case.
    * NEWS: Mention the bug.
    c9918f64