The actual rules are a bit more complex:
a & X(G(a&b...)&c...) = Ga & X(G(b...)&c...)
a | X(Fa | c) = F(a) | c
with the second rule being applied only if all XF can
be removed. See the documentation for an example.
* src/ltlvisit/simplify.cc: Implement these new rules.
* doc/tl/tl.tex: Document them.
* src/ltltest/reduccmp.test: Add test cases.
* src/ltlvisit/simplify.cc: Implement them here, and augment them
to support M, and W operators.
* src/ltltest/reduccmp.test: Add some tests.
* doc/tl/tl.tex (Simplifications Based on Implications): Document
these rules.
* doc/tl/tl.bib (babiak.12.tacas): New entry.
* src/ltlvisit/length.hh (length_boolone): New function.
* src/ltlvisit/length.cc (length_boolone): Implement it using...
(length_boolone_visitor): ... this new visitor.
* src/ltltest/randltl.cc: Use length_boolone() to check the result
of the random generator, and ignore any formula larger (in
length()) than opt_f. This fix a bug where the random formula
generator would sometime produce formula larger than requested,
because of the trivial rewriting of {f}[]->e as e|!f.
* src/ltltest/length.cc: Add option -b to call length_boolone().
* src/ltltest/length.test: Test length_boolone().
* src/ltlparse/ltlparse.yy: Cleanup the names used in the grammar.
* src/ltlparse/public.hh (parse_ratexp): Rename as...
(parse_sere): ... this.
* src/ltltest/consterm.cc: Adjust call to parse_ratexp().
* src/ltlvisit/simplify.cc (simplify_visitor): Do it.
* src/ltltest/reduccmp.test: Add a test.
* doc/tl/tl.tex: Document it.
* src/ltlast/multop.cc: Fix the computation of is.accepting_eword
for Fusion. The Fusion operator never accepts [*0].
This fixes a bug where {(a&!a)[=2]} was translated either into an
universal automaton (with simplification turned off) or in an
empty automaton (with simplification turned on).
* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate): Trim
the automaton.
(ratexp_to_dfa::succ, ratexp_to_dfa::get_label): Deal with trimed
states.
(ltl_trad_visitor::visit(unop::Closure)): Likewise.
* src/tgbatest/ltl2tgba.test, src/ltltest/reduccmp.test: New test
cases.
* src/ltlvisit/simplify.cc (syntactic_implication_aux): Refine
rules to deal with pure eventualities and purely universal
properties.
* src/ltltest/reduccmp.test: Add tests.
* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor::visit): Fix
the translation of the Goto operator.
(ratexp_trad_visitor::next_to_concat): More comments.
* src/ltltest/reduccmp.test: Add a test case.
* src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh
(are_equivalent): Export this function from the cache.
* src/ltltest/reduc.cc, src/ltltest/equals.cc: Use
are_equivalent() to check that the reductions are legitimate.
* src/ltlast/binop.cc: a M b is eventual if both a and b are
eventual, or if b == 1. a W b is universal if both a and b
are universal or if b == 0.
* src/ltltest/kind.test: New test case.
So that we can latter use some combined optimizations.
* src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc: Integrate
the code from syntimpl.cc
* src/ltlvisit/syntimpl.hh, src/ltlvisit/syntimpl.cc: Delete. All
code has been moved above.
* src/ltlvisit/Makefile.am: Adjust.
* src/ltltest/syntimpl.cc: Adjust code.
* src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc
(ltl_simplify::negative_normal_form): Remove the third
parameter and always rewrite XOR, =>, and <=>. This avoid
problems with the cache, that could have been populated with
a different value for this third parameter.
* src/ltltest/reduc.cc, src/tgbaalgos/ltl2tgba_fm.cc: Adjust
calls to negative_normal_form().
* src/ltltest/nenoform.test: Adjust tests.
* src/ltlvisit/contain.hh (reduce_tau03): Mark as deprecated.
* src/tgbaalgos/ltl2tgba_fm.cc, src/tgbatest/ltl2tgba.cc,
src/ltltest/equals.cc: Do not include ltlvisit/contain.hh, since
it's not used.
* src/ltlvisit/reduce.hh: Mark the file as obsolete.
(reduce): Declare this function as obsolete.
* src/ltlvisit/reduce.cc: Define SKIP_DEPRECATED_WARNING
so we can include reduce.hh.
* src/sanity/includes.test: Also use SKIP_DEPRECATED_WARNING
when compiling headers.
* iface/dve2/dve2check.cc,
src/ltltest/equals.cc, src/ltltest/randltl.cc,
src/ltltest/reduc.cc, src/tgbaalgos/ltl2tgba_fm.hh,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbatest/randtgba.cc,
wrap/python/ajax/spot.in, wrap/python/spot.i: Adjust
to use ltl_simplifier.
* src/tgbatest/ltl2tgba.cc: Adjust to use ltl_simplifier,
and replace -fr1...-fr7 options by a single -fr option.
* src/tgbatest/spotlbtt.test: Adjust -fr flags accordingly.
* src/tgbatest/reductgba.cc: Do not include reduce.hh.
* src/ltlvisit/simplify.hh
(ltl_simplifier::negative_normal_form): Allow logical
unabbreviations during the NNF pass.
* src/ltlvisit/simplify.cc
(ltl_simplifier::negative_normal_form)
(negative_normal_form_visitor): Adjust.
(ltl_simplifier::simplify): Request unabbreviations.
* src/ltlvisit/reduce.cc (reduce): Remove most
of the code, leaving only a call ltl_simplifier
and some wrapper code to convert options.
* src/ltltest/reduccmp.test: Add more test cases.
* src/ltlvisit/simplify.cc (ltl_simplifier): Add more rewritings
for formulae that are both universal and eventual.
* src/ltltest/reduccmp.test: Add six more cases.
* src/ltlvisit/simplify.cc (ltl_simplifier): Since we are processing
the formula bottom-up, don't assume all trivial simplification have
been done.
* src/ltltest/reduccmp.test: More tests.
So far I have only checked these rewritings with reduccmp.test.
There are probably a few kinks to iron out.
* src/ltlvisit/simplify.cc: Reimplement most of the basic
rewriting rules, leaving some FIXME comments for dubious ones.
* src/ltlast/multop.cc, src/ltlast/multop.hh: Ignore NULL
pointers in the vector.
* src/ltlvisit/reduce.cc (reduce): Do not call basic_reduce().
* src/ltltest/reduccmp.test: Adjust tests.
* src/ltlast/binop.cc (binop::binop): Generalize detection
of pure eventualities and purely universal formulae. E.g.
`f U g' is a pure eventuality if g is a pure eventuality
(regardless of f) or if g is 1.
* src/ltlast/unop.cc (unop::unop): Compute is.eventual
and is.universal for Not.
* src/ltltest/kind.test: Adjust.
I.e., SERE without star, or LTL formula using only X and Boolean
operators.
* src/ltlast/formula.hh, src/ltlast/formula.cc: Add a bit for
tracking finite formulas.
* src/ltlast/atomic_prop.cc, src/ltlast/automatop.cc,
src/ltlast/bunop.cc, src/ltlast/constant.cc, src/ltlast/formula.cc:
Adjust.
* src/ltlast/unop.cc, src/ltlast/binop.cc: Adjust and use that
bit to refine the computation of some LTL classes.
* src/ltltest/kind.test: New tests.
These are safety, guarantee, obligation, persistence, and recurrence.
* src/ltlast/formula.hh, src/ltlast/formula.cc: Declare a bit for
each of these classes.
* src/ltlast/atomic_prop.cc, src/ltlast/constant.cc,
src/ltlast/automatop.cc, src/ltlast/binop.cc, src/ltlast/bunop.cc,
src/ltlast/unop.cc: Update these bits.
* src/ltltest/kind.test: Update tests and add more.
* src/ltlast/binop.cc (EConcat, UConcat): Rewrite "{b}<>-> f"
as "b && f", and rewrite "{b}[]->f" as "b->f".
* src/ltlast/binop.hh (binop::instance): Document trivial
identities for <>-> and []->.
* src/ltlast/multop.cc (multop::instance): Rewrite "b1 & b2"
as "b1 && b2" when b1 and b2 are Boolean.
(multop::multop): Always disable is.boolean for AndNLM.
* src/ltlast/multop.hh: Document the rewriting.
* src/ltltest/equals.cc: Show the two formulas if the exit_code
is 1, to help debugging.
* src/ltltest/equals.test: Add more tests.
* src/ltltest/kind.test: Adjust tests.
We still don't have any PSL-specific reductions, but at least
the LTL reduction now appear to work on PSL formulas.
* src/ltlvisit/basicreduce.cc (basic_reduce_visitor): Fix the
call to std::copy to handle Concat, Fusion, and AndNLM.
* src/ltlvisit/reduce.cc (reduce_visitor): Fix handling
of UConcat, EConcat, and EConcatMarked.
* src/tgbatest/randpsl.test: Activate reductions.
* src/ltltest/reducpsl.test: New file.
* src/ltltest/Makefile.am (TESTS): Add it.
* src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh:
(random_boolean, random_sere, random_psl): Add new classes.
* src/ltltest/randltl.cc: Add options to support the above.
Nore: the -p option was renamed to -pL for consistency, but
it is still understood.
* src/ltlvisit/syntimpl.hh (syntactic_implication,
syntactic_implication_neg): Move as member of ...
(syntactic_implication_cache): ... this new class, that holds
a cache of results to speedup these functions.
* src/ltlvisit/syntimpl.cc: Adjust to use (lookup, populate,
and cleanup) the cache.
* src/ltltest/syntimpl.cc: Likewise.
* src/ltlvisit/reduce.hh (reduce): Take an optional
syntactic_implication_cache parameter.
* src/ltlvisit/reduce.cc: Adjust to use a
syntactic_implication_cache.
* src/ltltest/equals.cc: Call dump_instances() to help debugging.
This bitfield is easily updated as the formulae are constructed.
Doing so avoids many AST recursions to compute these properties
individually. This patch removes the eventual_universal_visitor,
as well as the kind_of() function.
* src/ltlast/formula.hh (is_boolean, is_sugar_free_boolean,
is_in_nenoform, is_X_free, is_sugar_free_ltl,
is_ltl_formula, is_eltl_formula, is_psl_formula, is_eventual,
is_universal, is_marked): New methods to query formula
properties in constant time.
(get_props, ltl_prop): A method and structure for
implementation as a field bit in an unsigned, for fast
computation.
(print_formula_props): New function.
* src/ltlast/formula.cc (print_formula_props): Implement it.
* src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
src/ltlast/bunop.cc, src/ltlast/constant.cc, src/ltlast/multop.cc,
src/ltlast/unop.cc, src/ltlast/automatop.cc: Compute the
properties as instances are constructed.
* src/ltlparse/ltlparse.yy: Update to use is_boolean() instead
of kind_of().
* src/ltltest/kind.cc: Update to use print_formula_props().
* src/ltltest/kind.test: Adjust to test eventual and universal
properties.
* src/ltlvisit/kind.cc, src/ltlvisit/kind.hh: Delete these files.
* src/ltlvisit/Makefile.am: Remove kind.hh and kind.cc.
* src/ltlvisit/reduce.cc (recurse_eu, eventual_universal_visitor):
Remove, no longer needed.
(reduce_visitor, is_eventual, is_universal): Adjust to
use formula::is_eventual(), and formula::is_universal().
* src/ltlvisit/reduce.hh (is_eventual, is_universal): Declare as
deprecated.
* src/ltlast/binop.cc (binop::instance): Simplify fUf, fRf, fWf,
and fRF.
* src/ltlast/binop.hh: Document it.
* src/ltltest/equals.test: Add new tests for 'Exp U Exp'
and 'Exp R Exp', and all missing tests for W and M.
* src/ltlparse/ltlscan.ll (OP_SQBKT_SEP): Accept ":" and "to"
in addition to ".." and ",".
(OP_UNBOUNDED): Recognize "$" for the rule below.
* src/ltlparse/ltlparse.yy: Accept [OP1:$] as a synonym
for [OP1:], for people used to SVA's syntax.
* src/ltltest/equals.test: Test these syntaxes.
* src/ltlast/bunop.hh: Declare bunop::Goto
* src/ltlast/bunop.cc: Handle it.
* src/ltlparse/ltlparse.yy,
src/ltlparse/ltlscan.ll: Add rules for [->min..max].
* src/tgbaalgos/ltl2tgba_fm.cc: Handle bunop::Goto in
the translation.
* src/ltltest/equals.test: Test trivial identities.
* src/tgbatest/ltl2tgba.test: Test two more formulae using [->].
* src/ltlast/bunop.hh: Declare bunop::Equal
* src/ltlast/bunop.cc: Handle it.
* src/ltlparse/ltlparse.yy,
src/ltlparse/ltlscan.ll: Add rules for [=min..max].
* src/tgbaalgos/ltl2tgba_fm.cc: Handle bunop::Equal in
the translation.
* src/ltltest/equals.test: Test trivial identities
for [=min..max].
* src/tgbatest/ltl2tgba.test: Add new formulae to test.
