Skip to content
  • Alexandre Duret-Lutz's avatar
    simplify: some new simplification rules · 646c5170
    Alexandre Duret-Lutz authored
    For #263, reported by Mikuláš Klokočka.
    
    G(a & Xe1 & F(b & e2)) = G(a & e1 & Fb & e2)
    F(a | Xu1 | G(b | u2)) = F(a | u1 | Gb | u2)
    
    * spot/tl/simplify.cc: Implement the rules.
    * doc/tl/tl.tex, NEWS: Document them.
    * tests/core/reduccmp.test, tests/core/eventuniv.test: Add test cases.
    * tests/core/det.test, tests/core/ltl2tgba2.test: Adjust to expect
    smaller automata.
    * THANKS: Add Mikuláš.
    646c5170
To find the state of this project's repository at the time of any of these versions, check out the tags.