new keyword in the ELTL format: finish, which applies to an
automaton operator and tells whether it just completed.
* src/eltlparse/eltlparse.yy: Clean it. Add finish.
* src/eltlparse/eltlscan.ll: Add finish.
* src/formula_tree.cc, src/formula_tree.hh: New files. Define a
small AST representing formulae where atomic props are unknown
which is used in the ELTL parser.
* src/ltlast/automatop.cc, ltlast/automatop.hh, ltlast/nfa.cc,
ltlast/nfa.hh: Adjust.
* src/ltlast/unop.cc, src/ltlast/unop.hh: Finish is an unop.
* src/ltlvisit/basicreduce.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/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_lacim.cc: Handle finish in switches.
* src/tgbaalgos/eltl2tgba_lacim.cc: Translate finish.
* src/tgbatest/eltl2tgba.test: More tests.
for ELTL. This is a new version of the work started in 2008 with
LTL and ELTL formulae now sharing the same class hierarchy.
* configure.ac: Adjust for src/eltlparse/ and src/eltltest/
directories, and call AX_BOOST_BASE.
* m4/boost.m4: New file defining AX_BOOST_BASE([MINIMUM-VERSION]).
* src/Makefile.am: Add eltlparse and eltltest.
* src/eltlparse/: New directory. Contains the ELTL parser.
* src/eltltest/: New directory. Contains tests related to
ELTL (parser and AST).
* src/ltlast/Makefile.am: Adjust for ELTL AST files.
* src/ltlast/automatop.cc, src/ltlast/automatop.hh: New files.
Represent automaton operators nodes used in ELTL ASTs.
* src/ltlast/nfa.cc, src/ltlast/nfa.hh: New files. Represent
simple NFAs used internally by automatop nodes.
* src/ltlast/allnode.hh, src/ltlast/predecl.hh,
src/ltlast/visitor.hh: Adjust for automatop.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/clone.cc,
src/ltlvisit/clone.hh, src/ltlvisit/contain.cc,
src/ltlvisit/dotty.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: Because LTL and ELTL formulae share the
same class hierarchy, LTL visitors need to handle automatop nodes
to compile. When it's meaningful the visitor applies on automatop
nodes or simply assert(0) otherwise.
* src/tgba/tgbabddconcretefactory.cc (create_anonymous_state),
src/tgba/tgbabddconcretefactory.hh (create_anonymous_state): New
function used by the LaCIM translation algorithm for ELTL.
* src/tgbaalgos/Makefile.am: Adjust for eltl2tgba_lacim* files.
* src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/eltl2tgba_lacim.hh: New files. Implementation of
the LaCIM translation algorithm for ELTL.
* src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc:
Handle automatop nodes in the translation by an assert(0).
* src/tgbatest/Makefile.am: Adjust for eltl2tgba.* files.
* src/src/tgbatest/eltl2tgba.cc, src/tgbatest/eltl2tgba.test: New
files
* src/ltlenv/environment.hh, src/ltlvisit/basicreduce.cc: Remove
useless FIXMEs.
* src/ltlvisit/reduce.cc (reduce_visitor::visit(binop)): Compute
syntactic implications only when needed.
* src/tgbaalgos/reductgba_sim_del.cc
(build_recurse_successor_spoiler): Remplace the FIXME by an assert.
* src/tgba/tgbareduc.cc: Reword some comments, discard old
commented code.
* src/ltlvisit/reduce.hh, src/ltlvisit/reduce.hh:
Add Reduce_Containment_Checks and Reduce_Containment_Checks_Stronger
flags, and call reduce_tau03.
* src/ltlvisit/contain.hh (reduce_tau03): Make "stronger" the
default.
* src/ltlvisit/contain.cc: Style.
* src/ltltest/reduc.cc: Simplify using the reduce() interface
instead of reduce_tau03.
* src/tgbatest/ltl2tgba.cc: Likewise. Add -fr5, -fr6, and -fr7
options.
* src/tgbatest/spotlbtt.test: Remove cases using "-c", since its
current implementation is not always correct (and apparently
reduces less than -fr7).
instead of empty().
* src/misc/bddalloc.cc (bdd_allocator::extend): Use empty() rather
than size() when checking emptiness of lists.
* src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/minimalce.cc,
src/ltlvisit/basicreduce.cc, src/ltlvisit/reduce.cc,
src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/misc/minato.cc: Likewise.
* src/ltlast/multop.cc (multop::instance): Call ->size() only once.
extracted from ...
* src/ltlvisit/lunabbrev.cc: ... this one, which now work as documented
again.
* src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc: Adjust to call
simplify_f_g() in addition to unabbreviate_logic().
* src/ltlvisit/Makefile.am (ltlvisit_HEADERS, libltlvisit_la_SOURCES):
Add simpfg.cc and simpfg.hh.
* src/ltlvisit/reduce.hh, src/ltlvisit/reduce.cc: ... this, to match
the function name.
* ltltest/equals.cc, ltltest/reduc.cc, ltlvisit/Makefile.am,
tgbatest/ltl2tgba.cc, tgbatest/reductgba.cc: Adjust filenames.
