• 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/closure.cc, src/tgbaalgos/closure.hh:
    Add closure function.
    * src/tgbaalgos/stutterize.cc, src/tgbaalgos/stutterize.hh:
    Add two implementations of "self-loopize" function.
    * src/tgbaalgos/Makefile.am: Add them.
    * src/tgba/tgbasl.cc, src/tgba/tgbasl.hh: On-the-fly implementation of
    * src/tgba/Makefile.am: Add it.
    * src/tgbatest/ltl2tgba.cc, src/tgbatest/stutter_invariant.test: Test
    closure and sl.
    * src/tgbatest/Makefile.am: Adjust.
    * src/bin/ltlfilt.cc: Modify stutter-invariant option to use
    automaton-based checking rather than syntactic-based checking.
    * src/ltlvisit/remove_x.cc, src/ltlvisit/remove_x.hh:
    Remove is_stutter_insensitive function.
    * src/tgbaalgos/stutter_invariance.cc,
    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/stutter_invariance_formulas.cc: Generate benchmarks from
    given formulas.
    * bench/stutter/stutter_invariance_randomgraph.cc: Generate benchmarks
    from random automata.
    * bench/stutter/Makefile.am: Add them.
    * configure.ac: Add bench/stutter/Makefile.
    * bench/Makefile.am: Add stutter subdirectory.
    * README: Document bench/stutter directory.
To learn more about this project, read the wiki.