It cause issues when <ctime> latter undefine the gmtime/localtime macros
to access the real function.
* lib/Makefile.am, lib/time.in.h, m4/gettimeofday.m4, m4/time_h.m4:
These changes are mostly based on the patch posted in
http://permalink.gmane.org/gmane.comp.lib.gnulib.bugs/29229 but
with the prototype of gmtime() and localtime() fixed.
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.
* src/tgbaalgos/postproc.cc: Move the count_state() function...
* src/priv/countstates.cc, src/priv/countstates.hh: ... in these
new files.
* src/priv/Makefile.am: Add them.
* src/saba/sabacomplementtgba.cc, src/tgba/tgbakvcomplement.cc,
src/tgbaalgos/minimize.cc: Use count_states() instead of
stats_reachable().
* 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 gcc and g++ for -fvisibility and
-fvisibility-inlines-hidden. Add these options to
CFLAGS and CXXFLAGS.
* m4/ax_check_compile_flag.m4: New file.
* src/Makefile.am: Build BuDDy as a single library, reverting part of
the changes introduced in my previous patch to this file. Since
the options are set in CFLAGS/CXXFLAGS, there is no possibility
for -fvisibility-inlines-hidden to be passed to the C compiler.
If an installed header has an associated *.cc file (in the source
tree), but does not declare any SPOT_API symbol, something is fishy.
Either that header should not be installed, or it is missing the
SPOT_API markers.
* src/sanity/private.test: New test.
* src/sanity/Makefile.am: Call it.
* src/ltlast/Makefile.am: Do not install formula_tree.hh.
* src/ltlvisit/Makefile.am: Do not install mark.hh.
* src/tgbaalgos/Makefile.am: Do not intall weight.hh.
* src/ta/Makefile.am, src/taalgos/Makefile.am: Use
$(VISIBILITY_CXXFLAGS).
* src/ta/ta.hh, src/ta/taexplicit.hh, src/ta/taproduct.hh,
src/ta/tgta.hh, src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.hh,
src/taalgos/dotty.hh, src/taalgos/emptinessta.hh,
src/taalgos/minimize.hh, src/taalgos/reachiter.hh,
src/taalgos/statessetbuilder.hh, src/taalgos/stats.hh,
src/taalgos/tgba2ta.hh: Add SPOT_API in front
of all public symbols.
* src/eltlparse/Makefile.am, src/kripkeparse/Makefile.am,
src/ltlparse/Makefile.am, src/neverparse/Makefile.am,
src/tgbaparse/Makefile.am: Use $(VISIBILITY_CXXFLAGS)
* src/eltlparse/public.hh, src/kripkeparse/public.hh,
src/ltlparse/ltlfile.hh, src/ltlparse/public.hh,
src/neverparse/public.hh, src/tgbaparse/public.hh:
Mark public symbols with SPOT_API.
* 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/bdd.h, src/bvec.h, src/fdd.h: Declare all exported
symbols using BUDDY_API, a new macro that sets visibility=default.
* src/Makefile.am: Compile with -fvisibility=hidden by default,
and compile the C++ part with -fvisibility-inlines-hidden as well.
This follows from a discussion with Ernesto Posse.
The semantics for the {...} operator we use in Spot comes from the
cl(...) operator defined by Dax et al. (ATVA'09). This is slightly
different from the the way the PSL spec interprets a SERE used in the
context of a temporal formula (appendix B.3.1.1.2, item 7).
cl({a;b}[*]) would match any infinite word that starts with a;b, while
in PSL {a;b}[*] would match any infinite word that alternates a and b.
Spot documents that {SERE} in a temporal formula is interpreted like
cl(SERE) however it failed to ignore the empty prefix of SERE. So
{{a;b}[*]} would match anything, because the empty word is a prefix of
any word, and is also accepted by {a;b}[*]. Some trivial identities
and basic rewritings were also wrongly considering these empty
prefixes as well.
This patch therefore fixes the translation and syntactic
simplification rules, to really ignore these empty prefixes.
In some future version it should probably be wise to rename this {...}
operator as cl(...), and use {...} for the semantics given in appendix
B.3.1.1.2 (item 7) of the PSL specs.
* src/ltlast/unop.cc: Fix trivial identities. We have
{[*0]} = 0 and !{[*0]} = 1.
* src/ltlvisit/simplify.cc: Fix basic rewriting rules.
{e[*]} = {e} and !{e[*]} = !{e}.
* doc/tl/tl.tex: Adjust documentation.
* doc/tl/tl.bib (dax.09.atva): New entry.
* src/tgbaalgos/ltl2tgba_fm.cc: Do not accept any
infinite word for {e[*]} just because the empty
prefix is matched by e[*].
* src/tgbatest/ltl2tgba.test: Add a test case.
* NEWS: Mention it.
* THANKS: Add Ernesto.
Also accept guards of the form (a) || !(b) or (a) && !(b).
* src/neverparse/neverclaimscan.ll: Adjust.
* src/tgbatest/neverclaimread.test: Add a test case.
These translator may output guards such as (a) || (b), but with the
changes in Spot 1.1.3 it would only work with ((a) || (b)).
Furthermore when ltlcross would fail to parse a neverclaim containing
such a guard, it would fail to parse all later neverclaims, because
the lexer was not properly reset.
* src/neverparse/neverclaimscan.ll: Scan (a) || (b) as a single
token.
(neverclaimyyopen): Reset the lexer.
* src/tgbatest/neverclaimread.test: Add a test for (a) || (b).
* NEWS: Update.
