• Alexandre Duret-Lutz's avatar
    simplify: GF(f)=GF(dnf(f)) FG(f)=FG(cnf(f)) · da5d23f0
    Alexandre Duret-Lutz authored
    These rules come from Delag's paper, and help some cases
    in issue #385.
    
    * spot/tl/simplify.cc: Implement the simplification.
    * doc/tl/tl.tex, NEWS: Document it.
    * tests/core/385.test: New file.
    * tests/Makefile.am: Add it.
    * tests/core/reduccmp.test: More tests.
    * tests/core/ltl2tgba2.test: Adjust one improved case.
    * tests/python/automata.ipynb, tests/python/twagraph-internals.ipynb:
    Adjust expected output, as the cnf/dnf reorder some subformulas.
    da5d23f0
Makefile.am 12.4 KB