* src/ltlvisit/simplify.hh, src/ta/taexplicit.hh, src/ta/taproduct.hh,
src/tgba/bdddict.hh, src/tgba/taatgba.hh, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.hh, src/tgba/tgbasgba.hh,
src/tgba/tgbatba.hh, src/tgba/tgbaunion.hh, src/tgba/wdbacomp.cc: Here.

* src/bin/common_finput.cc, src/bin/genltl.cc, src/bin/ltlcross.cc,
src/bin/randltl.cc: Simplify.

* bench/scc-stats/stats.cc, bench/split-product/cutscc.cc,
iface/gspn/ssp.cc, src/bin/ltlcross.cc, src/bin/ltlfilt.cc,
src/bin/randltl.cc, src/dstarparse/nsa2tgba.cc, src/ltlast/formula.hh,
src/ltlast/nfa.hh, src/ltlvisit/contain.hh, src/ltlvisit/dotty.cc,
src/ltlvisit/mark.hh, src/ltlvisit/relabel.cc, src/ltlvisit/relabel.hh,
src/ltlvisit/simplify.cc, src/ltlvisit/snf.hh, src/misc/hash.hh,
src/misc/mspool.hh, src/priv/acccompl.hh, src/priv/accconv.hh,
src/saba/explicitstateconjunction.hh, src/saba/sabastate.hh,
src/sabaalgos/sabareachiter.hh, src/sanity/style.test,
src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/taalgos/emptinessta.cc,
src/taalgos/minimize.cc, src/taalgos/reachiter.hh, src/tgba/state.hh,
src/tgba/taatgba.hh, src/tgba/tgbabddconcretefactory.hh,
src/tgba/tgbaexplicit.hh, src/tgba/tgbakvcomplement.cc,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbatba.cc,
src/tgba/tgbatba.hh, src/tgbaalgos/cutscc.cc, src/tgbaalgos/cycles.hh,
src/tgbaalgos/degen.cc, src/tgbaalgos/dtbasat.cc,
src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/emptiness.cc, src/tgbaalgos/gtec/explscc.hh,
src/tgbaalgos/gtec/nsheap.hh, src/tgbaalgos/gv04.cc,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/magic.cc,
src/tgbaalgos/minimize.cc, src/tgbaalgos/ndfs_result.hxx,
src/tgbaalgos/powerset.hh, src/tgbaalgos/randomgraph.cc,
src/tgbaalgos/reachiter.hh, src/tgbaalgos/replayrun.cc,
src/tgbaalgos/safety.cc, src/tgbaalgos/scc.hh, src/tgbaalgos/se05.cc,
src/tgbaalgos/simulation.cc, src/tgbaalgos/tau03.cc,
src/tgbaalgos/tau03opt.cc: Adjust code.
* src/sanity/style.test: Remove check.

* m4/stl.m4: Delete.
* configure.ac: Do not check for unordered_map and friends.
* src/misc/hash.hh: Remove all conditional code.

* src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
src/ltlast/automatop.cc, src/ltlast/automatop.hh, src/ltlast/binop.cc,
src/ltlast/binop.hh, src/ltlast/bunop.cc, src/ltlast/bunop.hh,
src/ltlast/constant.cc, src/ltlast/constant.hh, src/ltlast/multop.cc,
src/ltlast/multop.hh, src/ltlast/unop.cc, src/ltlast/unop.hh: Move all
one-line accessors methods like nth(), child(), op()... from *.cc files
to their respective *.hh files.

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/kripke/kripkeexplicit.cc: Add missing const, reported by Etienne
Renault using Apple's clang version that is installed with OS X 10.9.

* doc/Makefile.am, src/ltltest/defs.in, src/ltltest/latex.test: Here.

* src/misc/satsolver.cc: Add the "-model" option.
* NEWS, doc/org/satmin.org, src/bin/man/spot-x.x: Mention it.

* doc/org/satmin.org, src/bin/man/spot-x.x: Document it.
* NEWS: Mention it.

* src/misc/timer.hh: Fix.
* NEWS: Mention the bug.

* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Record
statistics about intermediate automata if SPOT_SATLOG is set to some
filename, and display intermediate automata if SPOT_SATSHOW is set.
* bench/dtgbasat/stat.sh, bench/dtgbasat/stats.sh,
bench/dtgbasat/tabl.pl, bench/dtgbasat/tabl1.pl,
bench/dtgbasat/tabl2.pl, bench/dtgbasat/tabl3.pl,
bench/dtgbasat/tabl4.pl: Gather these extra statistics.

* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Compute the
actual number of reachable states in the produced automaton to prepare
the next iteration.

This was simply wrong.

* src/tgbaalgos/dtbasat.cc: reverts commit
fc5a00d24d5964d6f6a48d362ecbdec357eaf154.

* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: More debuging
code.

* 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/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Rewrite the
loops that number the states of the reference automaton so that
they declare CNF variable numbers in the same order as the states
of the automaton.

* src/misc/satsolver.cc: Call glucose with -verb=0.
* src/bin/man/spot-x.x: Document it.

* src/tgbatest/ltlcross4.test: Work around Pandas 0.13.
* NEWS: Mention it.

* src/ltlvisit/randomltl.cc: Fix generation of formulas when unary or
binary operators are missing.
* src/ltlvisit/apcollect.cc, src/ltlvisit/apcollect.hh
(destroy_atomic_prop_set): New function.
* src/bin/randltl.cc: Use it, and also honnor --boolean-priorities
when generating SEREs.
* src/ltltest/rand.test: New file.
* src/ltltest/Makefile.am: Add it.

* src/dstarparse/public.hh: Avoid LaTeX in comments to please clang-3.5.
* src/tgbaalgos/isdet.hh: Typo in Doxygen comment.

* src/ltlvisit/length.cc (length_boolone_visitor): Simplify.
* NEWS: Mention Alexandre's fix.

Alexandre Lewkowicz authored Jan 15, 2014 and Alexandre Duret-Lutz committed Feb 03, 2014

* src/ltlvisit/length.cc: Consider length of all Boolean
expressions combined in a multop as one.
* src/ltltest/length.test: Test it.

The bug was introduced by 52237398.

* src/misc/bitvect.hh (block_count): Here.
* src/tgbatest/dstar.test: Add a test case.

* src/ltlast/formula_tree.hh: Mark nodes with SPOT_API.

* 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/bitvect.hh: Remove SPOT_API from class forward declarations.
* src/ltlast/nfa.hh: Likewise.

* src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh (flex_set_buffer):
Take a std::string as argument and call yy_scan_bytes() with
the string size() instead of calling yy_scan_string() which does
strlen() on the supplied string.
* src/ltlparse/ltlparse.yy: Adjust calls.
* src/eltlparse/eltlscan.ll, src/eltlparse/parsedecl.hh,
src/eltlparse/eltlparse.yy: Use a similar interface.  This
also fixes a memory leak as the scanned buffer was not
released.

* src/tgbaalgos/cutscc.cc, src/tgbaalgos/ltl2taa.cc:  Include
<algorithm> for set_difference and binary_search.

* src/bin/common_finput.cc (job_processor::process_stream): Read
multi-line CSV fields.
* src/ltltest/lbt.test, src/tgbatest/nondet.test: Add tests.

* src/bin/ltlcross.cc (print_stats_csv): Revert the recent
addition of \r, it is caussing too many issues.
* NEWS: Mention it.

* src/bin/common_output.cc, src/bin/common_output.hh:
(output_formula_checked, aut_stat_printer): New.
* src/bin/genltl.cc, src/bin/randltl.cc, src/bin/ltlfilt.cc: Call
output_formula_checked() instead of output_formula().
* src/bin/ltl2tgba.cc: Use aut_stat_printer and add option --csv-escape.
* doc/org/csv.org: New file to document CSV I/O.
* doc/Makefile.am: Add it.
* doc/org/ioltl.org, doc/org/ltlfilt.org, doc/org/ltl2tgba.org,
doc/org/tools.org: Link to csv.org