Skip to content
  • Alexandre Duret-Lutz's avatar
    Safra: Fix usage of multiple acceptance conditions and fix text output. · a4d1e18b
    Alexandre Duret-Lutz authored
    * src/tgba/tgbasafracomplement.cc
    (tgba_safra_complement::tgba_safra_complement)
    (tgba_safra_complement::succ_iter): Correct the declaration and
    use of multiple acceptance conditions.
    (state_complement::to_string): Output the L set, not U.  The previous
    code caused different states to share the same names, causing issues
    with the text-based output (state with identical names get merged).
    * src/tgba/tgbasafracomplement.hh
    (tgba_safra_complement::acceptance_cond_vec_): Adjust type to
    store BDDs.
    * src/tgbatest/complementation.cc: Implement a new "-b" option
    to output automata in Spot's syntax.
    * src/tgbatest/complementation.test: Add a test-case supplied
    by Martin Dieguez Lodeiro.
    * THANKS: Add Martin.
    a4d1e18b