* src/graph/graph.hh: Add some framework to erase transitions, and
defrag the resulting transitions_ vector on demand. Also remove
the nb_states() and nb_transitions() because num_states() and
num_transitions() already exist.
* src/graphtest/graph.cc, src/graphtest/ngraph.cc: Adjust to
use num_states().
* src/tgba/tgbagraph.hh (merge_transitions): New method.
* src/misc/hash.hh: Add a pair_hash class, needed by
merge_transitions().
* src/graphtest/tgbagraph.cc, src/graphtest/tgbagraph.test: Add states
for transitions removal and merge_transitions().
This of course concerns push_back and push_front as well.
* src/bin/common_finput.cc, src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc,
src/bin/ltl2tgta.cc, src/bin/ltlcross.cc, src/bin/ltlfilt.cc,
src/dstarparse/dstarparse.yy, src/kripkeparse/kripkeparse.yy,
src/ltlast/formula.cc, src/ltlparse/ltlparse.yy, src/misc/minato.cc,
src/neverparse/neverclaimparse.yy, src/priv/bddalloc.cc, src/ta/ta.cc,
src/taalgos/emptinessta.cc, src/tgba/taatgba.cc,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/sccstack.cc,
src/tgbaalgos/magic.cc, src/tgbaalgos/ndfs_result.hxx,
src/tgbaalgos/rundotdec.cc, src/tgbaalgos/scc.cc, src/tgbaalgos/se05.cc,
src/tgbaalgos/simulation.cc, src/tgbaalgos/tau03.cc,
src/tgbaalgos/tau03opt.cc, src/tgbaparse/tgbaparse.yy: Use emplace
to make the code less verbose and avoid creating temporaries.
* src/misc/random.cc, src/misc/random.hh (srand, drand, mrand, rrand,
barand): Simplify using <random> from C++11.
(nrand, bmrand, prand): Remove these unused functions.
* src/tgbaalgos/randomgraph.cc: Adjust the use of barand.
* configure.ac: Do not check for srand48 and drand48.
But do not replace it by std::unique_ptr, because this was not
really equivalent.
* src/misc/unique_ptr.hh: Delete.
* src/misc/Makefile.am: Adjust.
* src/tgbaalgos/simulation.cc, src/tgbatest/ltl2tgba.cc: Call
delete explicitly.
Apparently their hash tables store the hash functions in a const
member, and this requires a user-supplied default constructor.
Reported by Étienne Renault.
* src/misc/hash.hh: Add an empty constructor to all hash functions.
* src/misc/satsolver.hh, src/misc/satsolver.cc: Present
the SAT solver as an object with a stream interface, to
prepare for a better implementation.
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc:
Adjust to the new interface, removing all the handling
of temporary files.
* src/tgbatest/readsat.cc: Adjust.
* src/misc/bitvect.cc, src/misc/bitvect.hh: Do
not assume the two bitvect with the same size have
the same number of allocated blocks. Fix an
assertion in extra_range().
* src/misc/bitvect.cc: Conditionally declare fnv<8>, so that the C++
parser does not choke on 14695981039346656037UL when compiling on a
32bit host. Problem observed with g++ 4.0.1 and 4.2.1 on Darwin.
* src/misc/escape.cc, src/misc/escape.hh (escape_rfc4180): New
function.
* src/bin/ltlcross.cc: Do not output space after ',', use
"\r\n" for end of line, and use escape_rfc4180().
* NEWS: Mention it.
* src/misc/satsolver.cc, src/misc/satsolver.hh (satsolver_get_solution):
New function, that accepts a solution split on multiple 'v ' lines.
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc (get_solution):
Remove, and adjust existing code to use satsolver_get_solution().
* src/tgbatest/readsat.cc, src/tgbatest/readsat.test: New files.
* src/tgbatest/Makefile.am: Add them.
* src/bin/man/spot-x.x: Mention the SAT competition rules for
the expected input/output format.
Uses the value of the SPOT_SATSOLVER environment variable
to decide how to call the SAT solver.
* src/misc/satsolver.cc, src/misc/satsolver.hh: New files.
* src/misc/Makefile.am: Add them.
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Use satsolver().
This is needed now that lib/ is in the include path.
* src/misc/bareword.cc, src/misc/bddop.cc, src/misc/escape.cc,
src/misc/formater.cc, src/misc/intvcmp2.cc, src/misc/intvcomp.cc,
src/misc/memusage.cc, src/misc/minato.cc, src/misc/optionmap.cc,
src/misc/random.cc, src/misc/timer.cc, src/misc/version.cc: Include
config.h.
* configure.ac: Check for flags and fill CXXFLAGS and CFLAGS.
* iface/dve2/dve2.hh: Mark load_dve2 for export.
* src/eltlparse/Makefile.am, src/kripke/Makefile.am,
src/kripkeparse/Makefile.am, src/ltlast/Makefile.am,
src/ltlenv/Makefile.am, src/ltlparse/Makefile.am,
src/ltlvisit/Makefile.am, src/misc/Makefile.am,
src/neverparse/Makefile.am, src/priv/Makefile.am, src/saba/Makefile.am,
src/sabaalgos/Makefile.am, src/ta/Makefile.am, src/taalgos/Makefile.am,
src/tgba/Makefile.am, src/tgbaalgos/Makefile.am,
src/tgbaalgos/gtec/Makefile.am, src/tgbaparse/Makefile.am:
Remove $(VISIBILITY_CXXFLAGS) now that it is set globally.
* configure.ac: Check for -fvisibility support.
* m4/ax_check_compile_flag.m4: New file.
* src/misc/common.hh: New file.
* src/misc/Makefile.am: Add common.hh, and adjust to use -fvisibility.
* src/misc/bareword.hh, src/misc/escape.hh, src/misc/formater.hh,
src/misc/intvcmp2.hh, src/misc/intvcomp.hh, src/misc/memusage.hh,
src/misc/minato.hh, src/misc/optionmap.hh, src/misc/random.hh,
src/misc/timer.hh, src/misc/version.hh, src/misc/bddop.hh: Include
common.hh and add SPOT_API tags.
* src/misc/acccompl.hh, src/misc/accconv.hh: Prepare for upcoming
move.
* src/sanity/style.test: Ignore SPOT_API tags.
* wrap/python/Makefile.am: Ignore SPOT_API.
* wrap/python/spot.i: Do not emit binding for bddalloc.hh.
* wrap/python/tests/minato.py: Do not use bdd_allocator.
* src/misc/formater.cc, src/misc/formater.hh (scan): New method.
(prime): Use it.
* src/bin/ltlcross.cc (translator_runner::translator_runner): Scan each
specification string, and report those missing an input or output
%-sequence.
* NEWS: Mention it.
Spin 6 supports formulas such as []<>(a < b) so that atomic properties
need not be specified using #define. Of course we don't want to
implement all the syntax of Spin in our LTL parser because other tools
may have different syntaxes for their atomic propositions. The
lenient mode tells the scanner to return any (...), {...}, or {...}!
block as a single token. The parser will try to recursively parse
this block as a LTL/SERE formula, and if this fails, it will consider
the block to be an atomic proposition. The drawback is that most
syntax errors will no be considered to be atomic propositions. For
instance (a U b U) is a single atomic proposition in lenient mode, and
a syntax error in default mode.
* src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll,
src/ltlparse/parsedecl.hh, src/ltlparse/public.hh: Add a
lenient parsing mode. Simplify the lexer using yy_scan_string.
* src/bin/common_finput.cc: Add a --lenient option.
* src/ltltest/lenient.test: New file.
* src/ltltest/Makefile.am: Add it.
* src/neverparse/neverclaimparse.yy: Parse the guards in lenient mode.
* src/tgbatest/neverclaimread.test: Adjust.
* src/ltlvisit/tostring.cc: When outputing a formula in Spin's syntax,
output (a < b) instead of "a < b".
* src/misc/escape.cc, src/misc/escape.hh (trim): New helper function.
* src/misc/formater.hh (formater::format, formater::prime): Move ...
* src/misc/formater.cc: ... in this new file.
* src/misc/Makefile.am: Add it.
* src/sanity/style.test: Allow <iostream> in headers where << or >> are
used.
* src/misc/formater.hh (printable_value): Add more accessors.
* src/bin/ltlcheck.cc: Use the formater class to factor the %-expansion
loop, and reuse filenames (such as %F, %S, and %L) between executions
on the same formula.
* src/misc/unique_ptr.hh: Create unique_ptr for Spot.
* src/misc/Makefile.am: Register this new file.
* src/tgbatest/ltl2tgba.cc: Replace two calls to delete by the
utilisation of unique_ptr.
* src/tgbaalgos/simulation.cc: Replace two calls to delete by the
utilisation of unique_ptr.
