Skip to content
  • Alexandre Duret-Lutz's avatar
    add a stutter-invariant property to automata · 1f0bb428
    Alexandre Duret-Lutz authored
    ... and show it in the HOA output.  Fixes #60.
    
    * src/tgba/tgba.hh: Add is_stutter_invariant().
    * src/tgbaalgos/hoa.cc: Print stutter-invariant
    and inherently-weak.
    * src/tgbaalgos/ltl2tgba_fm.cc: Set both.
    * src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/complete.cc,
    src/tgbaalgos/degen.cc, src/tgbaalgos/dtgbacomp.cc,
    src/tgbaalgos/mask.cc, src/tgbaalgos/minimize.cc,
    src/tgbaalgos/remfin.cc, src/tgbaalgos/sccfilter.cc,
    src/tgbaalgos/simulation.cc, src/tgbaalgos/stutter.cc,
    src/tgbatest/hoaparse.test, src/tgbatest/ltldo.test,
    src/tgbatest/monitor.test, src/tgbatest/randomize.test,
    src/tgbatest/remfin.test, src/tgbatest/sbacc.test: Adjust.
    1f0bb428