Skip to content
  • Thibaud Michaud's avatar
    Adding tgba-based stutter-invariance checking · 37bcb5d9
    Thibaud Michaud authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
    * src/tgbaalgos/, src/tgbaalgos/closure.hh:
    Add closure function.
    * src/tgbaalgos/, src/tgbaalgos/stutterize.hh:
    Add two implementations of "self-loopize" function.
    * src/tgbaalgos/ Add them.
    * src/tgba/, src/tgba/tgbasl.hh: On-the-fly implementation of
    * src/tgba/ Add it.
    * src/tgbatest/, src/tgbatest/stutter_invariant.test: Test
    closure and sl.
    * src/tgbatest/ Adjust.
    * src/bin/ Modify stutter-invariant option to use
    automaton-based checking rather than syntactic-based checking.
    * src/ltlvisit/, src/ltlvisit/remove_x.hh:
    Remove is_stutter_insensitive function.
    * src/tgbaalgos/,
    src/tgbaalgos/stutter_invariance.hh: Check if a formula is
    stutter-invariant using closure and sl.
    * wrap/python/spot.i: Add closure and sl bindings.
    * bench/stutter/ Generate benchmarks from
    given formulas.
    * bench/stutter/ Generate benchmarks
    from random automata.
    * bench/stutter/ Add them.
    * Add bench/stutter/Makefile.
    * bench/ Add stutter subdirectory.
    * README: Document bench/stutter directory.
To learn more about this project, read the wiki.