9caa9ad134
The set of rules enabled by favor_even_univ try to "lift" the subformulae that are both eventual and universal, so they appear higher in the AST. This is contrary to what we used to do (and still do when the option is unset), were we try to postpone such subformulae (by moving them down the AST). It is still a bit experimental. * src/ltlvisit/simplify.hh: Add option favor_event_univ. * src/ltlvisit/simplify.cc: Implement new rewriting rules. * doc/tl/tl.tex: Document them. * src/tgbatest/ltl2tgba.cc: Add option -ra to enable them. * src/tgbatest/spotlbtt.test: Test the translation with this option. * src/ltltest/reduc.cc, src/ltltest/equals.cc: Add option to enable the new rules. * src/ltltest/eventuniv.test: New file to test them. * src/ltltest/Makefile.am: Add it. |
||
|---|---|---|
| .. | ||
| org | ||
| tl | ||
| .cvsignore | ||
| .gitignore | ||
| dot.in | ||
| Doxyfile.in | ||
| footer.html | ||
| mainpage.dox | ||
| Makefile.am | ||