-
Alexandre Duret-Lutz authored
Because scc_info does not perform a full emptiness check, it is not always able to tell whether an SCC is accepting if the acceptance condition use Fin primitives. This introduce is_rejecting_scc() in addition to to is_accepting_scc(). Only one of them may be true, but they can both be false if scc_info has no idea whether the SCC is accepting. * src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh: Implement is_rejecting_scc(). * src/bin/ltlcross.cc, src/tgba/acc.cc, src/tgba/acc.hh, src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/isweakscc.cc, src/tgbaalgos/remfin.cc, src/tgbaalgos/safety.cc, src/tgbaalgos/sccfilter.cc: Use it. * src/tgbaalgos/dotty.cc: Use is_rejecting_scc() and is_accepting_scc() to color SCCs. * doc/org/oaut.org: Document the colors used. * src/tgbatest/neverclaimread.test, src/tgbatest/readsave.test: Adjust tests. * src/tgbatest/sccdot.test: New test case. * src/tgbatest/Makefile.am: Add it.
ebe4ffc5