* 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/ltlparse/ltlparse.yy (parse_ratexp): New function.
(START_LTL, START_RATEXP): Add these new tokens.
(result): Parse and LTL formula or a rational expression depending
on the start symbol.
* src/ltlparse/public.hh (parse_ratexp): New function.
* src/ltlparse/parsedecl.hh (flex_set_buffer): Add a new argument
to set the starting rule.
* src/ltlparse/ltlscan.ll (flex_set_buffer): Adjust.
(start_token): New global variable. Return this as first token if
it is set.
* 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.
* configure.ac: Check for times() and sys/times.h.
* src/misc/timer.hh: Include sys/times.h conditionally
and use clock() if times() is not available.
Reported by Yann Thierry-Mieg.
* src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh: New files.
* src/tgbaalgos/Makefile.am: Add the new files to the compilation.
* src/tgbatest/spotlbtt.test: Add the simulation.
* src/tgbatest/ltl2tgba.cc: Add direct simulation (-RSD).
* src/misc/acccompl.cc, src/misc/acccompl.hh: Add a way to
an acceptance condition in an automaton, into its
complement.
Create a method to make the reverse operation.
* src/misc/Makefile.am: Add the new files to the compilation.
* src/tgba/sba.hh: New file, extrated from...
* src/tgba/tgbaexplicit.hh: ... here. Also rename
sba_explicit::is_accepting as sba_explicit::state_is_accepting for
consistency with tgba_sba_proxy.
* src/tgbatest/explicit2.cc: Adjust to the renaming.
* src/tgba/Makefile.am: Add sba.hh.
* src/tgba/tgbaexplicit.hh (explicit_graph, tgba_explicit): Make the
transition type explicit.
(state_explicit_string::get_iterator): New method.
(explicit_graph::get_transition): Use it.
(tba): Rename as ...
(sba): ... this.
* wrap/python/spot.i: Instanciate explicit_graph and tgba_explicit
for all three types.
* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc: Factor most of
the code in an explicit_graph<State, Type> that inherits from type.
The tgba_explicit type<State> now inherits from
explicit_graph<State,tgba>.
* src/ltlvisit/contain.cc, src/neverparse/neverclaimparse.yy
src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh, src/tgbaalgos/cutscc.cc,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh,
src/tgbaalgos/emptiness.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/minimize.cc,
src/tgbaalgos/powerset.cc, src/tgbaalgos/randomgraph.cc,
src/tgbaalgos/sccfilter.cc, src/tgbaparse/tgbaparse.yy,
src/tgbatest/complementation.cc, src/tgbatest/explicit.cc,
src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc,
src/tgbatest/mixprod.cc, src/tgbatest/powerset.cc,
src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc:
Replace tgba_explicit* by the actual type used.
* src/tgbatest/explicit2.cc: New file.
* src/tgbatest/Makefile.am: Add it.
* src/tgbaalgos/emptiness.cc
(emptiness_check_instantiator::construct): Set *err = 0
on success. This avoids problem with the python bindings
always converting *err to a string and sometimes failing
to do so when err was not initialized.
* src/misc/intvcmp2.cc (stream_compression_base::run): Fix a case
where the "id" of the compression to use would be miscalculated,
causing wrong values to be encoded.
* src/tgbatest/intvcmp2.cc: Add this particular test case.
Suggested by Nikos Gorogiannis.
* src/tgba/tgbatba.hh (tgba_tba_proxy::create_state): New method.
(tgba_tba_proxy::uniq_map_): New attribute.
* src/tgba/tgbatba.cc (state_tba_proxy): Use the default
copy constructor. Empty the destructor. Implement an empty
destroy() method. Use addresses for comparison. Make clone()
a no-op.
(tgba_tba_proxy): Allocate and deallocate the unicity table.
Implement create_sates().
(tgba_tba_proxy, tgba_sba_proxy, tgba_tba_proxy_succ_iterator):
Adjust state construction to call create_state().
* src/tgba/tgbasafracomplement.cc (safra_tree:succ_create): Do not
lookup *i twice, and do not copy it->second.
(safra_tree::normalize_siblings): Do not lookup *node_it before
insertion.
* src/tgbaalgos/minimize.cc (minimize_wdba): Fix the Löding
algorithm to use colors. The previous implementation was an
incorrect approximation.
* src/tgbatest/wdba2.test: New file showing two equivalent
formulas that were minimized in automata with different sizes.
* src/tgbatest/Makefile.am: Add it.
* src/kripketest/defs.in (run2): Remove this function. It was
incorrectly trying to run valgrind even when valgrind is not
installed.
* src/kripketest/kripke.test: Simplify and use run().
* src/tgbaalgos/minimize.cc (minimize_dfa): Fix detection of the
last iteration. An extra iteration case could be missed in case
where a split generates only singletons, and yet predecessor
classes need to be refined.
* src/ltlvisit/length.cc: Fix computation for ltl::multop
operator. "a&b&c" was reported with length 3, ignoring the
"&" operators, because of a typo.
* src/ltlvisit/length.hh: Fix description to correctly
reflect this change intended since 2010-01-22.
* src/ltltest/length.test, src/ltltest/length.cc: New files.
* src/ltltest/Makefile.am: Add them.
There is no point in degeneralizing an automaton if it can be WDBA
minimized. Doing so will only augment the number of states and
slow down the powerset construction used by the WDBA minimization.
* src/tgbatest/babiak.test: New file. It includes 5 formulae
which Tomáš Babiak reported Spot 0.7.1 would take over one hour to
translate if degeneralization and WDBA minimization were both
requested.
* src/tgbatest/Makefile.am (TESTS): Add it.
* src/tgbatest/ltl2tgba.cc: Do WDBA minimization before
degeneralization. The above formulae are now all translated in a
few seconds.
The previous setup failed with clang++ 3.0.
* m4/stl.m4: New file.
* configure.ac: Call AC_HEADER_UNORDERED_MAP,
AC_HEADER_TR1_UNORDERED_MAP, and AC_HEADER_EXT_HASH_MAP.
* src/misc/hash.hh: Include _config.h, and used the
SPOT_HAVE_UNORDERED_MAP, SPOT_HAVE_TR1_UNORDERED_MAP,
or SPOT_HAVE_EXT_HASH_MAP defines to decide which
file to include.
* src/kripketest/Makefile.am (LDADD): Remove a broken dependency.
Reported by Yann Thierry-Mieg.
* src/sanity/style.test: Make sure it does not appear again.
* src/misc/bddalloc.cc (bdd_allocator::initialize): Call
bdd_setmaxincrease(500000), because the default is 50000,
which cause garbage collection to occur too often.
* src/tgbaalgos/neverclaim.cc, src/tgbaalgos/dotty.cc,
src/tgbaalgos/save.cc: Prefer '\n' over std::endl to speedup I/O.
* src/ltltest/genltl.cc (syntax): Use '\n' too, although it won't
make a big difference.
* src/tgbaalgos/randomgraph.hh: Document the fact that adding
acceptance conditions to the graph may generate graphs that do not
have any accepting cycle.
Especially with should write !(p0) and not !p0, because p0 is
usually #define'd by the user and he may have forgotten to quote
the value of the macro. This issue was discovered by Kristin
Yvonne Rozier and diagnosed by Gerard Holzmann.
* src/tgbaalgos/neverclaim.cc (process_link): Call
to_spin_string(..., true) to fully parentheses the string.
* src/tgbatest/neverclaimread.test: Add a test.
