• Alexandre Duret-Lutz's avatar
    This should help getting accurate statistics (on both the · 7069d540
    Alexandre Duret-Lutz authored
    formula automaton and the synchronized product) from LBTT.
    Idea from Jean-Michel Couvreur.
    
    * src/tgbaalgos/lbtt.cc (nonacceptant_lbtt_bfs): New class.
    (nonacceptant_lbtt_reachable): New function.
    * src/tgbaalgos/lbtt.hh (nonacceptant_lbtt_reachable): New
    function.
    * src/tgbatest/ltl2tgba.cc (main): Call nonacceptant_lbtt_reachable
    if the -T option is used.
    * src/tgbatest/spotlbtt.test: Setup the -T variants, disabled by
    default.
    7069d540
lbtt.cc 9.28 KB