• Alexandre Duret-Lutz's avatar
    psl: add support for the [:*i..j] operator · a79db4ee
    Alexandre Duret-Lutz authored
    This operator is to ':' what [*i..j] is to ';'.
    Part of issue #51.
    * doc/tl/tl.tex: Document syntax, semantic, and trivial
    * doc/tl/spotltl.sty: Add macros for new operators.
    * src/ltlast/bunop.cc, src/ltlast/bunop.hh: Implement it.
    * src/ltlast/multop.cc: Add some trivial simplifications.
    * src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse it.
    * src/ltltest/equals.test, src/ltltest/latex.test,
    src/tgbatest/ltl2tgba.test: Add more tests.
    * src/ltlvisit/randomltl.cc: Output this operator in
    random PSL formulas.
    * src/ltltest/rand.test: Adjust.
    * src/tgbaalgos/ltl2tgba_fm.cc: Add translation rules.
    * src/ltlvisit/tostring.cc: Add pretty printing code.
    * src/ltlvisit/simplify.cc, src/ltlvisit/snf.cc: Adjust
    * NEWS: Mention the new operator.