Skip to content
  • Alexandre Duret-Lutz's avatar
    ltl: rename is_X_free() into is_syntactic_stutter_invariant() · 34f1601b
    Alexandre Duret-Lutz authored
    and adjust it to detect siPSL formulas, as in the paper of Dax et
    al. (ATVA'09).  For issue #51.
    
    * src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
    src/ltlast/bunop.cc, src/ltlast/constant.cc, src/ltlast/formula.cc,
    src/ltlast/formula.hh, src/ltlast/multop.cc, src/ltlast/unop.cc: Rename
    the property, and adjust its computation on siSERE.
    * src/ltlvisit/remove_x.cc, src/ltlvisit/simplify.cc,
    src/tgbaalgos/stutter.cc: Adjust to new names.
    * src/bin/ltlfilt.cc: Add option --syntactic-sutter-invariant.
    * src/ltltest/kind.test: Update tests and add some new.
    34f1601b