Skip to content
  • Alexandre Duret-Lutz's avatar
    ltl2tgba_fm: mark persistence formulas as weak automata · 729921c0
    Alexandre Duret-Lutz authored
    ... instead of inherently-weak.  The reason they were tagged
    as inherently-weak is historical: this property was introduced
    1.5 years before the weak propery.
    
    Fixes #351.
    
    * spot/twaalgos/ltl2tgba_fm.cc: Use prop_weak() instead of
    prop_inherently_weak().  Also be more conservative about the use of
    single_acc when unambiguous automata are generated.
    729921c0