• Alexandre Duret-Lutz's avatar
    * src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(unop::G)): Do · f661b0ad
    Alexandre Duret-Lutz authored
    not create Now/Next variable when G is the root of the formula.
    (ltl_trad_visitor::ltl_trad_visitor): Take a root argument.
    (ltl_trad_visitor::recurse): Create a new visitor, do not copy
    the current one.
    (ltl_to_tgba): Build ltl_trad_visitor with root = true.
    
    * src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(unop::X)):
    Remove FIXME about handling X(a U b) and X(a R b) better, it's
    done naturally.
    f661b0ad
To find the state of this project's repository at the time of any of these versions, check out the tags..
ChangeLog 45.8 KB