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.
The first issue was reported by Victor Khomenko.
* spot/tl/formula.cc: Introduce a single-argument
version of sugar_delay().
* spot/parsetl/parsetl.yy: Use it.
* doc/tl/tl.tex, spot/tl/formula.hh: Adjust doc.
* tests/core/ltlfilt.test, tests/core/sugar.test: More tests.
Following a discussion with Victor Khomenko.
* doc/tl/tl.tex: Document those rules.
* spot/tl/simplify.cc: Implement them.
* tests/core/reduccmp.test: Test them.
* spot/tl/formula.cc, spot/tl/formula.hh (formula::sugar_delay): New
function to implement this operator as syntactic sugar.
* spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Parse it.
* doc/tl/tl.tex: Document the syntactic sugar rules and precedence.
* tests/core/sugar.test: Add tests.
* NEWS: Mention this new feature.
Based on a report by Simon Jantsch. Fixes#362.
* NEWS, doc/tl/tl.tex: Mention the new rules.
* spot/tl/unabbrev.cc: Implement them.
* tests/core/unabbrevwm.test: Test them.
* tests/python/randltl.ipynb: Adjust.
This prevents an exception from being raised if NNF is not performed
on Boolean properties and implication-based checks are used.
* NEWS: Mention the issue.
* spot/tl/simplify.cc, doc/tl/tl.tex: Add some rules.
* tests/python/ltlsimple.py: Test them.
* NEWS, doc/tl/tl.tex, doc/tl/tl.bib: Document these new operators.
* spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Parse those.
* spot/tl/formula.cc, spot/tl/formula.hh: Add constructors.
* spot/gen/formulas.cc: Use it.
* tests/core/sugar.test: New file.
* tests/Makefile.am: Add it.
{e[*0..j]}<>->f = {e[*1..j]}<>->f
{e[*0..j]}[]->f = {e[*1..j]}[]->f
Fixes#81.
This required a small change to the bounded-star-normal-form to prevent
infinite recursion.
* spot/tl/simplify.cc: Implement these rules.
* doc/tl/tl.tex, NEWS: Document them.
* tests/core/reduccmp.test: Add tests, and adjust others.
* tests/core/unambig.test: Replace formula that used to generated an
ambiguous automaton, but now generates a deterministic one.
if e is pure eventuality and g => e, then e U g = Fg
if u is purely universal and u => g, then u R g = Gg
Fixes#93.
* doc/tl/tl.tex, NEWS: Document the rules.
* spot/tl/simplify.cc: Implement them.
* tests/core/reduccmp.test: Test them.
* tests/core/det.test: Adjust.
This implies learning alternative rules for G, and W as well, since
those would use R.
Fixes#103. Suggested by Joachim Klein.
* src/ltlvisit/unabbrev.cc, src/ltlvisit/unabbrev.hh: Implement the
new rules.
* doc/tl/tl.tex: Document the rules.
* src/tests/unabbrevwm.test: Test them.
* src/bin/ltlfilt.cc, NEWS: Mention that --unabbreviate accepts R.
This operator is to ':' what [*i..j] is to ';'.
Part of issue #51.
* doc/tl/tl.tex: Document syntax, semantic, and trivial
simplifications.
* 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
switches.
* NEWS: Mention the new operator.
* src/ltlvisit/simplify.cc, doc/tl/tl.tex: Remove the rule.
* src/ltltest/reduc0.test: Add a regression test.
* src/ltltest/reduccmp.test: Adjust test cases for its removal.
* NEWS: Mention it.
star_normal_form() used to be called under bounded
repetitions like [*0..4], but some of these rewritings
are only correct for [*0..]. For instance
(a*|1)[*] can be rewritten to 1[*]
but (a*|1)[*0..1] cannot be rewritten to 1[*0..1]
it would be correct to rewrite the latter as (a[+]|1)[*0..1],
canceling the empty word in a*.
Also (a*;b*)[*] can be rewritten to (a|b)[*]
but (a*;b*)[*0..1] cannot be rewritten to (a|b)[*0..1]
and it cannot either be rewritten to (a[+]|b[+])[*0..1].
This patch introduces a new function to implement
rewritings under bounded repetition.
* src/ltlvisit/snf.hh, src/ltlvisit/snf.cc (star_normal_form_unbounded):
New function.
* src/ltlvisit/simplify.cc: Use it.
* src/ltltest/reduccmp.test: Add tests.
* doc/tl/tl.tex: Document the rewritings implemented.
Fortunately was only enabled with the
ltl_simplifier_options::favor_event_univ option, which cannot yet be
turned on from the command-line tools.
* src/ltlvisit/simplify.cc, doc/tl/tl.tex: Remove the rule.
* src/ltltest/eventuniv.test: Adjust.
* NEWS: Mention the bug.
* src/ltlvisit/simplify.cc: Remove two incorrect rules, and
partially disable another one.
* doc/tl/tl.tex: Reflect the change.
* src/ltltest/reduccmp.test: Likewise.
* src/ltltest/equals.cc: Add safety checks to catch such errors in the
future.
* NEWS: Mention the bug.
