Skip to content
  • Alexandre Duret-Lutz's avatar
    Track finite formulae. · fb386209
    Alexandre Duret-Lutz authored
    I.e., SERE without star, or LTL formula using only X and Boolean
    operators.
    
    * src/ltlast/formula.hh, src/ltlast/formula.cc: Add a bit for
    tracking finite formulas.
    * src/ltlast/atomic_prop.cc, src/ltlast/automatop.cc,
    src/ltlast/bunop.cc, src/ltlast/constant.cc, src/ltlast/formula.cc:
    Adjust.
    * src/ltlast/unop.cc, src/ltlast/binop.cc: Adjust and use that
    bit to refine the computation of some LTL classes.
    * src/ltltest/kind.test: New tests.
    fb386209