-
Alexandre Duret-Lutz authored
We need a marked version of !{r} to perform breakpoint unroling. * src/ltlast/unop.cc, src/ltlast/unop.hh: Declare a NegClosureMarked operator. * src/ltlvisit/mark.hh, src/ltlvisit/mark.cc, src/tgbaalgos/ltl2tgba_fm.cc: Adjust to deal with NegClosureMarked and NegClosure as apropriate. * src/ltlvisit/simplify.cc, src/ltlvisit/tostring.cc, src/ltlvisit/tunabbrev.cc, src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_lacim.cc, src/tgba/formula2bdd.cc: Deal with NegClosureMarked in the same way as we deal with NegClosure. * src/tgbatest/ltl2tgba.test: More tests. * src/ltltest/kind.test: Adjust. * doc/tl/tl.tex: Mention the marked negated closure.
e2f70e72