Skip to content
  • Alexandre Duret-Lutz's avatar
    Fix translation of !{r}. · e2f70e72
    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