* src/tgbaalgos/ltl2tgba_fm.cc (implied_subforfmulae): New function.
(ltl_trad_visitor::visit(const binop*)): Use it. This is an attempt
to correct the unoptimal translation of 'Fa & GFa' left by previous
patch. It still fails to optimize 'Fa & GF(a&b)', but this is not a
regression compared to previous version.
* src/tgbaalgos/ltl2tgba_fm.cc: Add a "recurring" mode for the
translation of the child of G. This generalizes Couvreur's original
trick to translate GFa as (a|Prom(a))&X(GFa) without generating an
intermediate GF(a)&F(a) state that would have to be merged with GF(a)
latter. This implementation will also speedup formulas such a G((a U
b) & (c M d)). With this patch, translating GF(p1) & GF(p2) &
... GF(p20) into a TGBA takes 57s instead of 128s on my computer.
However it alsos causes some formulas to be translated into larger
automata that are not immediately reduced (the simulation-reduction is
needed). For instance Fa & GFa now has a different signature than
GFa, so translating 'Fa & GFa' generates two states where is used to
generate only one.
We need a marked version of !{r} to perform breakpoint unroling.
* src/ltlast/unop.cc, src/ltlast/unop.hh: Declare a NegClosureMarked
operator.
* src/ltlvisit/mark.hh, src/ltlvisit/mark.cc,
src/tgbaalgos/ltl2tgba_fm.cc: Adjust to deal with NegClosureMarked
and NegClosure as apropriate.
* src/ltlvisit/simplify.cc, src/ltlvisit/tostring.cc,
src/ltlvisit/tunabbrev.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_lacim.cc,
src/tgba/formula2bdd.cc: Deal with NegClosureMarked in the same way as
we deal with NegClosure.
* src/tgbatest/ltl2tgba.test: More tests.
* src/ltltest/kind.test: Adjust.
* doc/tl/tl.tex: Mention the marked negated closure.
* src/misc/acccompl.hh, src/misc/acccompl.cc (AccCompl): Rename to
acc_compl.
* src/tgbaalgos/simulation.cc (AccComplAutomaton, Simulation): Rename
to acc_compl_automaton and direct_simulation. At the same time,
reindent the whole file.
* src/sanity/style.test: Detect capitalized class names.
* src/kripke/kripkeexplicit.hh (KripkePrint): Remove useless
predeclaration.
* src/tgbaalgos/simulation.hh: Typo in comment.
* src/tgba/tgbaexplicit.hh: Rerganize a bit to
allow different functions to be used to format
states. Add an enabled_utf8() method to
tgba_explicit_formula.
* src/tgbaalgos/dotty.hh, src/tgbaalgos/dotty.cc:
Simplify the interface by not depending on
dotty_decorator explicitely.
* src/tgba/bddprint.hh (enable_utf8): New function.
* src/tgba/bddprint.cc (enable_utf8): Implement it
and use the global utf8 flag in other functions.
* src/tgbatest/ltl2tgba.cc: Add an -8 option for
UTF-8 outpout.
* wrap/python/spot.i: Adjust for tgbexplicit.hh
changes.
It was a mistake to try to overload And/Or LTL operator for these when
trivial simplification are performed. The reason is so simple it is
embarassing: And(f,1)=f is a trivial identity that should not be
applied with AndRat. E.g. AndRat(a;b, 1) is equal to 0, not a;b.
* src/ltlast/multop.hh, src/ltlast/multop.cc: Add the AndRat and OrRat
operators.
* src/ltlparse/ltlparse.yy: Build them.
* src/ltlvisit/mark.cc, src/ltlvisit/simplify.cc,
src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc,
src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc:
Adjust all switches.
* src/ltlast/bunop.hh, src/ltlast/bunop.cc, src/ltlvisit/randomltl.cc,
src/ltlvisit/simplify.cc, src/ltlvisit/tostring.cc,
src/tgbaalgos/ltl2tgba_fm.cc: Remove all traces of these two
operators since they are not handled like sugar.
* doc/tl/tl.tex: Adjust documentation to reflect the fact that these
two operators are sugar.
* src/ltlvisit/mark.hh, src/ltlvisit/mark.cc (mark_concat_ops,
simplify_mark): Rewrite these two functions as methods of
(mark_tools): this new class.
* src/ltlast/binop.cc, src/ltlast/unop.cc: Adjust computation
of not_marked to ignore marked operators that are not at
the top-level. I.e., something like X(!{a}) is not marked.
* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::mt): New
instance of mark_tools.
(formula_canonizer::translate) Adjust calls to
mark_concat_ops() and simplify_mark().
* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate): Do not
translate a subformula if we have already proved it useless in
a previous rational expression.
* src/tgbatest/ltl2tgba.test: Add an example, although that
test does not ensure the subformula is ignored early in the
translation. I.e., it would still work without the patch.
* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate,
ltl_to_tgba_fm): Do not convert labels as Boolean formulas before
creating transitions. Use the bdd directly, and register the used
transitions later.
We used to cache it only for formulas used as states.
* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::ltl_to_bdd): New method.
(ltl_trad_visitor::recurse): Use ltl_to_bdd().
(formula_canonizer): Likewise.
(ltl_to_tgba_fm): Adjust.
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.
This is especially important when translating the Closure
operators, because normally we should only keep the satisfiable
formulae (i.e. co-accessible states), which seems hard to check on
the fly. After this patch we need to teach
ratexp_to_dfa::translate() how to trim (and then minimize) the DFA
to prune those useless (non co-accessible) states.
* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa): New class.
(translate_dict::transdfa): New member.
(ltl_trad_visitor::visit(unop::Closure)): Use transdfa.
* src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc
(ltl_simplifier::ltl_simplifier, ltl_simplifier::get_dict): Make
it possible to supply and retrieve the dictionary used.
(ltl_simplifier::as_bdd): New function, exported from the cache.
* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict): Store the
ltl_simplifier object.
(translate_dict::boolean_to_bdd): Call ltl_simplifier::as_bdd.
(translate_ratexp): New wrapper around the ratexp_trad_visitor,
calling boolean_to_bdd whenever possible.
(ratexp_trad_visitor): Do not deal with negated formulae, there
are necessarily Boolean and handled by translate_ratexp().
(ltl_visitor): Adjust to call translate_ratexp.
(ltl_to_tgba_fm): Adjust passing of the ltl_simplifier to the
translate_dict, and make sure everybody is using the same
dictionary.
* src/tgbatest/ltl2tgba.cc: Pass the dictionary to the
ltl_simplifier.
* 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.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/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor::visit):
Use a different translating rule for E* if E accepts [*0].
* src/tgbatest/ltl2tgba.test: Add test case.
* src/ltlparse/ltlparse.yy (rationalexp): Allow ->, <->, and xor,
in rational expressions as long as they apply only to Boolean
formulae.
* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor): Adjust
assert in handling of unop::Not.
* 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.
* src/ltlast/bunop.hh, src/ltlast/bunop.cc: New files for
bounded unary operators.
* src/ltlast/Makefile.am, src/ltlast/allnodes.hh: Add them.
* src/ltlast/predecl.hh (bunop): Declare.
* src/ltlast/unop.hh, src/ltlast/unop.cc (Star): Remove
declaration of Star and associated code.
* src/ltlast/visitor.hh: Add visit(bunop* node) methods.
* src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Add parse
rules for LTL. This required passing the parse_error list
to the lexer, so it can report scanning errors when it reads
a number that does not fit in an unsigned int.
* src/ltlparse/parsedecl.hh (YY_DECL): Take error_list
as third argument.
* src/ltltest/consterm.test, src/ltltest/tostring.test,
src/ltltest/equals.test, src/tgbatest/ltl2tgba.test: More tests.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/clone.cc,
src/ltlvisit/clone.hh, src/ltlvisit/consterm.cc,
src/ltlvisit/dotty.cc, src/ltlvisit/mark.cc,
src/ltlvisit/nenoform.cc, src/ltlvisit/postfix.cc,
src/ltlvisit/postfix.hh, src/ltlvisit/reduce.cc,
src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
src/ltlvisit/tunabbrev.cc, src/tgba/formula2bdd.cc,
src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc,
src/tgbaalgos/ltl2tgba_lacim.cc: Adjust syntax to use
"bunop::Star" instead of "unop::Star".
* src/tgbaalgos/ltl2tgba_fm.cc: Likewise, but also adjust
the code to handle the bounds of the operator.
* src/ltlast/multop.cc, src/ltlast/multop.hh: Declare AndNML
operator.
* src/ltlparse/ltlscan.ll: Distinguish "&" and "&&".
* src/ltlparse/ltlparse.yy: Handle them both as "And" for LTL
formula, use AndNML or And for rational expressions.
* src/ltlvisit/tostring.cc: Adjust to distinguish "&" and "&&" in
rational expressions. Also use {braces} to group rational
expressions.
* src/tgbaalgos/ltl2tgba_fm.cc
(ratexp_trad_visitor::ratexp_trad_visitor): Remove the possibility
to select the empty_word should act like true, and fix the rules
for Closure and NegClosure to rely on constant_term instead.
(ratexp_trad_visitor::visit) Adjust the And translation to also
support AndNML.
(ratexp_trad_visitor::recurse_and_concat): Introduce this new
method to simplify some calls to recurse(f, to_concat_).
* src/tgbatest/ltl2tgba.test: Add more test cases.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/consterm.cc,
src/ltlvisit/contain.cc, src/ltlvisit/mark.cc,
src/ltlvisit/nenoform.cc, src/ltlvisit/syntimpl.cc,
src/tgba/formula2bdd.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_lacim.cc: Add
missing cases in switches.
* src/ltlast/unop.hh, src/ltlast/unop.cc: Introduce Closure and
NegClosure operators.
* src/ltlparse/ltlparse.yy: Recognize {foo} as a Closure.
* src/ltlvisit/mark.cc: Consider NegClosure as a marked operator.
* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor): Add option to
select whether the empty_word should act like true (for {SERE}
and {!SERE}) or false (for {SERE}<>->Exp or {SERE}[]->Exp).
(ltl_trad_visitor): Translate Closure and NegClosure.
* src/tgbatest/ltl2tgba.test: Add more tests.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/consterm.cc,
src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.cc,
src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
src/ltlvisit/tunabbrev.cc, src/tgba/formula2bdd.cc,
src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2tgba_lacim.cc,
src/tgbaalgos/ltl2taa.cc: Straightforward update to support or
assert on these new operators.
* src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor): Take
an exprop argument, and use it while translation <>-> operators.
* src/tgbatest/ltl2tgba.test (check_psl): Use -x too.
* src/ltlast/binop.cc, src/ltlast/binop.hh: Introduce
EConcatMarked ("<>+>").
* src/ltlvisit/basicreduce.cc, src/ltlvisit/consterm.cc,
src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc,
src/ltlvisit/reduce.cc, src/ltlvisit/simpfg.cc,
src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/ltl2tgba_lacim.cc, src/tgba/formula2bdd.cc,
src/tgba/formula2bdd.cc: Deal with it if possible or ignore
it.
* src/ltlast/binop.hh, src/ltlast/binop.cc (EConcat, UConcat):
Add these new operators.
* src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse
these new operators.
* src/ltlvisit/simpfg.cc, src/ltlvisit/syntimpl.cc,
src/ltlvisit/tostring.cc, src/ltlvisit/basicreduce.cc,
src/ltlvisit/consterm.cc, src/ltlvisit/lunabbrev.cc,
src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.cc
src/tgba/formula2bdd.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_lacim.cc: Add these new operators into the
switches.
Trivial simplifications rules (such as "FFa=Fa" or "x&1=x")
are performed any time a formule is instanciated.
* src/ltlast/constant.hh, src/ltlast/constant.cc
(true_instance, true_instance_): Declare the true_instance_ as a
static member, and move true_instance() into the .hh so it gets
inlined. Have true_instance_ as a class variable will ensure that
it is the first formula instantiated. Binop simplifications rely
on this to order arguments.
(false_instance, false_instance_): Likewise.
(empty_word_instance, empty_word_instance_): New method and static
member.
* src/ltlast/formula.hh (formula::formula): If max_count_ ever
loops, skip the first three values so that constants always have
smaller hash codes.
* src/ltlast/binop.hh, src/ltlast/binop.cc (instance): Add
simplifications and document them.
* src/ltlast/multop.hh (multop::Concat): New operator.
* src/ltlast/multop.cc (op_name): Handle Concat.
(instance): Inline Concat arguments without reordering. Handle
absorbent and neutral elements for all operators.
* src/ltlast/unop.hh (unop::Star): New operator.
* src/ltlast/unop.cc (op_name): Handle Star.
(instance): Handle Star, and add trivial simplifications for
other unary operators.
* src/ltlparse/ltlparse.yy (OP_CONCAT, OP_STAR, CONST_EMPTYWORD):
Declare these new operators and add rules for them.
* src/ltlparse/ltlscan.ll (OP_CONCAT, OP_STAR, CONST_EMPTYWORD):
Output these new operators.
* src/ltltest/equals.test: New tests.
* src/ltltest/parse.test: Remove redundant test.
* src/ltltest/tunabbrev.test, src/tgbatest/emptchk.test: Adjust tests.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/contain.cc,
src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.cc,
src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
src/ltlvisit/tunabbrev.cc: Complete visitors to handle new
operators.
* src/ltltest/nenoform.test: More tests.
* src/ltlvisit/lunabbrev.cc (unabbreviate_logic_visitor::visit):
Clone formulae before instance() function actually have a chance
to destroy them.
* src/tgba/formula2bdd.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_lacim.cc: Adjust switches to assert on new
operators.
This implementation of direct simulation was only working on
degeneralized automata, and produce automata that are inferiors to
those output by the new direct simulation implementation (in
tgba/simulation.hh) which can also work on TGBA. The delayed
simulation has never been reliable. It's time for some spring
cleaning.
* src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc: Delete.
* src/tgba/Makefile.am: Adjust.
* src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh:
Remove all code, and keep only a deprecated replacement
from reduc_tgba_sim().
* src/tgbaalgos/reductgba_sim_del.cc: Delete.
* src/tgbaalgos/Makefile.am: Adjust.
* src/tgbatest/reduccmp.test, src/tgbatest/reductgba.cc,
src/tgbatest/reductgba.test: Delete.
* src/tgbatest/Makefile.am: Adjust.
* src/tgbatest/ltl2tgba.cc: Undocument options -R1s, -R1t,
-R2s, -R2t, and implement them using the new direct simulation.
Remove options -Rd and -RD.
* src/tgbatest/spotlbtt.test: Remove entry using these old options.
* wrap/python/spot.i: Do not process tgbaalgos/reductgba_sim.cc.
* src/tgbaalgos/simulation.hh: Mention the fact that this is
a "direct" simulation.
* wrap/python/ajax/ltl2tgba.html: Likewise, and change the key
to "ds".
* wrap/python/ajax/protocol.txt, wrap/python/ajax/spot.in: Adjust.
