Skip to content
  • Alexandre Duret-Lutz's avatar
    fix handling of Rabin-like input for dnf_to_dca() · 81e5357e
    Alexandre Duret-Lutz authored
    The bug is mentioned by Maximilien Colange in a comment to issue #317,
    but turned out to be unrelated to that original issue.
    
    * spot/twaalgos/totgba.cc (dnf_to_streett): Save the correspondence
    between the created states an the DNF clause in a named property.
    * doc/org/concepts.org, spot/twaalgos/totgba.hh: Mention the new
    property.
    * spot/twaalgos/cobuchi.cc (save_inf_nca_st): Rewrite using the named
    property.  Relying on seen marks and trying to deduce the matching
    original clause could only work from plain Rabin.
    * tests/core/dca.test: Add the test from Maximilien.
    * NEWS: Mention the issue.
    81e5357e