Skip to content
  • Alexandre Duret-Lutz's avatar
    minimize_obligation: can complement the input TGBA if deterministic · 2dda2c91
    Alexandre Duret-Lutz authored
    This makes dstar2tgba able to produce a minimal WDBA when the input DRA
    represent an obligation property.
    
    * src/tgbaalgos/minimize.cc (minimize_obligation): When the
    formula is not supplied but the input automaton is deterministic,
    complement it to check the result of WDBA minimization.
    * src/tgbatest/ltl2dstar.test, src/tgbatest/ltl2dstar2.test: Improve
    tests.
    2dda2c91