Skip to content
  • Alexandre Duret-Lutz's avatar
    Trim DFAs used when translating PSL's closure operators. · b3cc033e
    Alexandre Duret-Lutz authored
    This fixes a bug where {(a&!a)[=2]} was translated either into an
    universal automaton (with simplification turned off) or in an
    empty automaton (with simplification turned on).
    
    * src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate): Trim
    the automaton.
    (ratexp_to_dfa::succ, ratexp_to_dfa::get_label): Deal with trimed
    states.
    (ltl_trad_visitor::visit(unop::Closure)): Likewise.
    * src/tgbatest/ltl2tgba.test, src/ltltest/reduccmp.test: New test
    cases.
    b3cc033e