Commit graph

2457 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
c568b4d337 hash.hh: Remove conditional code.
* m4/stl.m4: Delete.
* configure.ac: Do not check for unordered_map and friends.
* src/misc/hash.hh: Remove all conditional code.
2014-02-12 14:04:57 +01:00
Alexandre Duret-Lutz
f3874e05cc * configure.ac: Turn on C++11 flags. 2014-02-12 14:04:10 +01:00
Alexandre Duret-Lutz
2c05a9fdb6 ltlast: move all accessor methods to headers to help the optimizer
* 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.
2014-02-12 10:43:42 +01:00
Alexandre Duret-Lutz
9020ac8bef * doc/org/satmin.org: Reword last paragraph. 2014-02-12 10:06:53 +01:00
Alexandre Duret-Lutz
be43c1e957 * NEWS, configure.ac: Bump version to 1.2.3a. 2014-02-11 17:30:10 +01:00
Alexandre Duret-Lutz
2a7d5f5f7f Release Spot 1.2.3
* NEWS, configure.ac, doc/org/tools.org: Update version.
2014-02-11 17:20:58 +01:00
Alexandre Duret-Lutz
327b7e18b2 * bench/dtgbasat/README: Update glucose URL. 2014-02-11 17:17:15 +01:00
Alexandre Duret-Lutz
f567d88ff8 * NEWS: mention recent fixes. 2014-02-11 10:45:15 +01:00
Alexandre Duret-Lutz
58878cd405 Work around the clang version installed with MacOS X 10.9.
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.
2014-02-11 10:40:19 +01:00
Alexandre Duret-Lutz
0b5f63c296 Add missing const.
* src/kripke/kripkeexplicit.cc: Add missing const, reported by Etienne
Renault using Apple's clang version that is installed with OS X 10.9.
2014-02-11 10:05:57 +01:00
Alexandre Lewkowicz
cb0b3d3c67 testsuite: find files when building in remote directory
* doc/Makefile.am, src/ltltest/defs.in, src/ltltest/latex.test: Here.
2014-02-10 16:56:20 +01:00
Alexandre Duret-Lutz
eb778c569a sat: adjust SPOT_SATSOLVER default for glucose 3.0
* src/misc/satsolver.cc: Add the "-model" option.
* NEWS, doc/org/satmin.org, src/bin/man/spot-x.x: Mention it.
2014-02-08 21:34:35 +01:00
Alexandre Duret-Lutz
fd4a963a26 * src/bin/common_setup.cc: Bump copyright year. 2014-02-08 20:31:49 +01:00
Alexandre Duret-Lutz
3c985a3235 sat: document the SPOT_SATLOG envvar
* doc/org/satmin.org, src/bin/man/spot-x.x: Document it.
* NEWS: Mention it.
2014-02-08 20:31:49 +01:00
Alexandre Duret-Lutz
20824b96b9 timer: also consider the time spent in child processes
* src/misc/timer.hh: Fix.
* NEWS: Mention the bug.
2014-02-08 20:31:49 +01:00
Alexandre Duret-Lutz
55ee18b96a sat-minimize: more statistics.
* 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.
2014-02-08 20:31:49 +01:00
Alexandre Duret-Lutz
1319ec0bad sat-minimize: limit number of iterations
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Compute the
actual number of reachable states in the produced automaton to prepare
the next iteration.
2014-02-08 20:31:49 +01:00
Alexandre Duret-Lutz
e1be8e6e42 * bench/dtgbasat/README: Typo. 2014-02-08 20:31:49 +01:00
Alexandre Duret-Lutz
9c0021fac8 * src/tgbatest/satmin2.test, src/tgbatest/Makefile.am: New test. 2014-02-08 20:31:49 +01:00
Alexandre Duret-Lutz
7a26a4f1ec Revert "* src/tgbaalgos/dtbasat.cc: Better encoding for weak SCCs."
This was simply wrong.

* src/tgbaalgos/dtbasat.cc: reverts commit
fc5a00d24d5964d6f6a48d362ecbdec357eaf154.
2014-02-08 20:31:26 +01:00
Alexandre Duret-Lutz
b4d0b9ee42 sat: more debug.
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: More debuging
code.
2014-02-07 12:07:16 +01:00
Alexandre Duret-Lutz
9c98975c19 sat: factor the creation of temporary files
* 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.
2014-02-07 12:07:16 +01:00
Alexandre Duret-Lutz
1853bdd53b sat: fix some non-determinism of the encoding
* 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.
2014-02-07 12:07:16 +01:00
Alexandre Duret-Lutz
e5874ee4c7 Call glucose with -verb=0.
* src/misc/satsolver.cc: Call glucose with -verb=0.
* src/bin/man/spot-x.x: Document it.
2014-02-07 12:07:16 +01:00
Alexandre Duret-Lutz
977a6dfaee * src/tgbaalgos/dtbasat.cc: Better encoding for weak SCCs. 2014-02-07 12:07:16 +01:00
Alexandre Duret-Lutz
4334abdeed org: Fix UP links and center them on the page.
* doc/org/init.el.in: Center links.
* doc/org/csv.org, doc/org/dstar2tgba.org, doc/org/genltl.org,
doc/org/ioltl.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org,
doc/org/ltlcross.org, doc/org/ltlfilt.org, doc/org/randltl.org,
doc/org/satmin.org: Fix links.  Reported by Akim Demaille.
2014-02-06 22:28:37 +01:00
Alexandre Duret-Lutz
c2195600b8 Fix spurious failre with Pandas 0.13.
* src/tgbatest/ltlcross4.test: Work around Pandas 0.13.
* NEWS: Mention it.
2014-02-06 01:33:17 +01:00
Alexandre Duret-Lutz
38388748b0 * NEWS: Mention recent fixes. 2014-02-06 00:45:18 +01:00
Alexandre Duret-Lutz
50bdc24514 randltl: gracefully handle the absence of unary or binary operators.
* 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.
2014-02-06 00:15:27 +01:00
Alexandre Duret-Lutz
4911e7dc1f Fix warning of Clang-3.5 against Doxygen comments.
* src/dstarparse/public.hh: Avoid LaTeX in comments to please clang-3.5.
* src/tgbaalgos/isdet.hh: Typo in Doxygen comment.
2014-02-05 15:07:34 +01:00
Alexandre Duret-Lutz
17dd281b33 * doc/org/ltlfilt.org: Typo, reported by Fabrice Kordon. 2014-02-04 07:58:52 +01:00
Alexandre Duret-Lutz
494dbe2041 length: slight simplification
* src/ltlvisit/length.cc (length_boolone_visitor): Simplify.
* NEWS: Mention Alexandre's fix.
2014-02-03 09:49:30 +01:00
Alexandre Lewkowicz
02334867da length_boolone: fix inconsistency
* src/ltlvisit/length.cc: Consider length of all Boolean
expressions combined in a multop as one.
* src/ltltest/length.test: Test it.
2014-02-03 09:40:25 +01:00
Alexandre Duret-Lutz
b6e5ce7e15 python: better support for Python 3
* wrap/python/spot.i (spot::ltl::parse_error_list,
spot::tgba_parse_error_list): Add a __bool__ method, that is used
instead of __nonzero__ in Python 3.
* wrap/python/tests/interdep.py, wrap/python/tests/parsetgba.py:
Force destruction order.
* NEWS: Update.
2014-02-02 15:45:19 +01:00
Alexandre Duret-Lutz
a6714119f9 * NEWS, configure.ac: Bump version to 1.2.2a. 2014-01-24 12:19:58 +01:00
Alexandre Duret-Lutz
35612f3626 Release Spot 1.2.2
* NEWS, configure.ac, doc/org/tools.org: Set version to 1.2.2.
2014-01-24 11:16:07 +01:00
Alexandre Duret-Lutz
4f31a9bbed bitvect: fix block_count() on 0-sized bit-vectors
The bug was introduced by 522373984c.

* src/misc/bitvect.hh (block_count): Here.
* src/tgbatest/dstar.test: Add a test case.
2014-01-24 09:25:48 +01:00
Alexandre Duret-Lutz
91789b9b12 * src/tgbaalgos/degen.cc: Do not copy the unicity table. 2014-01-23 15:05:25 +01:00
Alexandre Duret-Lutz
bbf6a68228 Workaround another g++-4.0.1 bug on Darwin.
* src/ltlast/formula_tree.hh: Mark nodes with SPOT_API.
2014-01-15 23:04:38 +01:00
Alexandre Duret-Lutz
ff816fbebb * NEWS: Update with recent fixes. 2014-01-15 16:42:53 +01:00
Alexandre Duret-Lutz
522373984c bitvect: fix some issues observed on 32bit architectures.
* 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().
2014-01-15 16:27:49 +01:00
Alexandre Duret-Lutz
534edd4d1c bitvect: Fix compilation on 32-bits hosts.
* 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.
2014-01-15 15:57:58 +01:00
Alexandre Duret-Lutz
9ccdef9cbd Workaround GCC 4.0.1 on the Darwin builds.
* src/misc/bitvect.hh: Remove SPOT_API from class forward declarations.
* src/ltlast/nfa.hh: Likewise.
2014-01-15 14:39:45 +01:00
Alexandre Duret-Lutz
e19e56fba3 * AUTHORS: Add Alexandre Lewkowicz 2014-01-13 17:27:58 +01:00
Alexandre Lewkowicz
d2e43c3b61 python: use new print syntax.
* wrap/python/tests/alarm.py: Here.
2014-01-13 17:26:39 +01:00
Alexandre Duret-Lutz
72b616c8cc * src/eltlparse/eltlscan.ll (_atoi): Fix range checking. 2014-01-13 17:25:35 +01:00
Alexandre Duret-Lutz
e2143c0313 ltlparse, eltlparse: avoid unnecessary calls to strlen().
* 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.
2014-01-13 17:25:35 +01:00
Alexandre Duret-Lutz
0c06844655 * src/taalgos/emptinessta.cc: Include <cstdlib> for abs(). 2014-01-13 17:25:35 +01:00
Alexandre Duret-Lutz
7a6af3aa0d Add missing #include.
* src/tgbaalgos/cutscc.cc, src/tgbaalgos/ltl2taa.cc:  Include
<algorithm> for set_difference and binary_search.
2013-12-18 17:03:37 +01:00
Alexandre Duret-Lutz
51d6fa7347 Upgrade to gnulib 23eecb48e39afd0d267d64d40ba6bf97aa865e13.
* lib/Makefile.am, lib/time.in.h, m4/gettimeofday.m4, m4/time_h.m4:
Update.
2013-12-18 08:07:45 +01:00