- 29 Jul, 2013 25 commits
-
-
Alexandre Duret-Lutz authored
* 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.
-
Alexandre Duret-Lutz authored
* lib/Makefile.am lib/alloca.in.h lib/argp-ba.c lib/argp-eexst.c lib/argp-fmtstream.c lib/argp-fmtstream.h lib/argp-fs-xinl.c lib/argp-help.c lib/argp-namefrob.h lib/argp-parse.c lib/argp-pin.c lib/argp-pv.c lib/argp-pvh.c lib/argp-xinl.c lib/argp.h lib/asnprintf.c lib/basename-lgpl.c lib/dirname-lgpl.c lib/dirname.h lib/dosname.h lib/errno.in.h lib/error.c lib/error.h lib/fcntl.in.h lib/float+.h lib/float.c lib/float.in.h lib/gethrxtime.c lib/gethrxtime.h lib/getopt.c lib/getopt.in.h lib/getopt1.c lib/getopt_int.h lib/gettext.h lib/gettime.c lib/gettimeofday.c lib/intprops.h lib/itold.c lib/lstat.c lib/malloc.c lib/memchr.c lib/mempcpy.c lib/mkstemp.c lib/msvc-inval.c lib/msvc-inval.h lib/msvc-nothrow.c lib/msvc-nothrow.h lib/pathmax.h lib/printf-args.c lib/printf-args.h lib/printf-parse.c lib/printf-parse.h lib/progname.c lib/progname.h lib/rawmemchr.c lib/size_max.h lib/sleep.c lib/stat.c lib/stdalign.in.h lib/stdbool.in.h lib/stddef.in.h lib/stdint.in.h lib/stdio.in.h lib/stdlib.in.h lib/strcasecmp.c lib/strchrnul.c lib/strerror-override.c lib/strerror-override.h lib/strerror.c lib/string.in.h lib/strings.in.h lib/stripslash.c lib/strncasecmp.c lib/strndup.c lib/strnlen.c lib/sys_stat.in.h lib/sys_time.in.h lib/sys_types.in.h lib/sys_wait.in.h lib/sysexits.in.h lib/tempname.c lib/tempname.h lib/time.in.h lib/timespec.h lib/unistd.in.h lib/vasnprintf.c lib/vasnprintf.h lib/verify.h lib/vsnprintf.c lib/wchar.in.h lib/xsize.h lib/xtime.h m4/00gnulib.m4 m4/alloca.m4 m4/argp.m4 m4/clock_time.m4 m4/dirname.m4 m4/double-slash-root.m4 m4/errno_h.m4 m4/error.m4 m4/exponentd.m4 m4/extensions.m4 m4/extern-inline.m4 m4/fcntl-o.m4 m4/fcntl_h.m4 m4/float_h.m4 m4/gethrxtime.m4 m4/getopt.m4 m4/gettime.m4 m4/gettimeofday.m4 m4/gnulib-cache.m4 m4/gnulib-common.m4 m4/gnulib-comp.m4 m4/gnulib-tool.m4 m4/include_next.m4 m4/intmax_t.m4 m4/inttypes_h.m4 m4/largefile.m4 m4/longlong.m4 m4/lstat.m4 m4/malloc.m4 m4/math_h.m4 m4/memchr.m4 m4/mempcpy.m4 m4/mkstemp.m4 m4/mmap-anon.m4 m4/msvc-inval.m4 m4/msvc-nothrow.m4 m4/multiarch.m4 m4/nocrash.m4 m4/off_t.m4 m4/pathmax.m4 m4/printf.m4 m4/rawmemchr.m4 m4/size_max.m4 m4/sleep.m4 m4/ssize_t.m4 m4/stat.m4 m4/stdalign.m4 m4/stdbool.m4 m4/stddef_h.m4 m4/stdint.m4 m4/stdint_h.m4 m4/stdio_h.m4 m4/stdlib_h.m4 m4/strcase.m4 m4/strchrnul.m4 m4/strerror.m4 m4/string_h.m4 m4/strings_h.m4 m4/strndup.m4 m4/strnlen.m4 m4/sys_socket_h.m4 m4/sys_stat_h.m4 m4/sys_time_h.m4 m4/sys_types_h.m4 m4/sys_wait_h.m4 m4/sysexits.m4 m4/tempname.m4 m4/time_h.m4 m4/timespec.m4 m4/unistd_h.m4 m4/vasnprintf.m4 m4/vsnprintf.m4 m4/warn-on-use.m4 m4/wchar_h.m4 m4/wchar_t.m4 m4/wint_t.m4 m4/xsize.m4 tools/snippet/arg-nonnull.h tools/snippet/c++defs.h tools/snippet/warn-on-use.h: Upgrade to gnulib 9ceceed274f83094127f9ff0bf061293c9fe1e7f. * m4/secure_getenv.m4, lib/secure_getenv.c, lib/unistd.c, lib/xtime.c: New files. * src/bin/Makefile.am: Link with the libtool library.
-
Alexandre Duret-Lutz authored
* 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.
-
Alexandre Duret-Lutz authored
* src/sanity/80columns.test, src/sanity/includes.test, src/sanity/private.test, src/sanity/style.test: Here.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
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.
-
Alexandre Duret-Lutz authored
* 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.
-
Alexandre Duret-Lutz authored
* 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.
-
Alexandre Duret-Lutz authored
* src/misc/location.hh, src/misc/position.hh: New files, from Bison 2.7. * src/misc/Makefile.am: Distribute them. * src/eltlparse/Makefile.am, src/eltlparse/eltlparse.yy, src/eltlparse/parsedecl.hh, src/eltlparse/public.hh, src/kripkeparse/Makefile.am, src/kripkeparse/kripkeparse.yy, src/kripkeparse/parsedecl.hh, src/kripkeparse/public.hh, src/ltlparse/Makefile.am, src/ltlparse/fmterror.cc, src/ltlparse/ltlparse.yy, src/ltlparse/parsedecl.hh, src/ltlparse/public.hh, src/neverparse/Makefile.am, src/neverparse/neverclaimparse.yy, src/neverparse/parsedecl.hh, src/neverparse/public.hh, src/tgbaparse/Makefile.am, src/tgbaparse/parsedecl.hh, src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy: Adjust to use and include misc/location.hh. * NEWS: Mention this change.
-
Alexandre Duret-Lutz authored
* src/tgbaalgos/Makefile.am, src/tgbaalgos/gtec/Makefile.am: Add $(VISIBILITY_CXXFLAGS). * src/tgbaalgos/bfssteps.hh, src/tgbaalgos/compsusp.hh, src/tgbaalgos/cutscc.hh, src/tgbaalgos/cycles.hh, src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.hh, src/tgbaalgos/dottydec.hh, src/tgbaalgos/dupexp.hh, src/tgbaalgos/eltl2tgba_lacim.hh, src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/explscc.hh, src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/nsheap.hh, src/tgbaalgos/gtec/sccstack.hh, src/tgbaalgos/gtec/status.hh, src/tgbaalgos/gv04.hh, src/tgbaalgos/isdet.hh, src/tgbaalgos/isweakscc.cc, src/tgbaalgos/isweakscc.hh, src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/magic.hh, src/tgbaalgos/minimize.hh, src/tgbaalgos/neverclaim.hh, src/tgbaalgos/postproc.hh, src/tgbaalgos/powerset.hh, src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.hh, src/tgbaalgos/reachiter.hh, src/tgbaalgos/reducerun.hh, src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/replayrun.hh, src/tgbaalgos/rundotdec.hh, src/tgbaalgos/safety.hh, src/tgbaalgos/save.hh, src/tgbaalgos/scc.hh, src/tgbaalgos/sccfilter.hh, src/tgbaalgos/se05.hh, src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.hh, src/tgbaalgos/stripacc.hh, src/tgbaalgos/tau03.hh, src/tgbaalgos/tau03opt.hh, src/tgbaalgos/translate.hh: Mark public symbol with SPOT_API.
-
Alexandre Duret-Lutz authored
* src/kripke/Makefile.am, src/saba/Makefile.am, src/sabaalgos/Makefile.am: Use $(VISIBILITY_CXXFLAGS). * src/kripke/fairkripke.hh, src/kripke/kripke.hh, src/kripke/kripkeexplicit.hh, src/kripke/kripkeprint.hh, src/saba/explicitstateconjunction.hh, src/saba/saba.hh, src/saba/sabacomplementtgba.hh, src/saba/sabastate.hh, src/saba/sabasucciter.hh, src/sabaalgos/sabadotty.hh, src/sabaalgos/sabareachiter.hh: Mark exported symbols with SPOT_API.
-
Alexandre Duret-Lutz authored
* src/tgba/Makefile.am: Use $(VISIBILITY_CXXFLAGS). * src/tgba/bdddict.hh, src/tgba/bddprint.hh, src/tgba/formula2bdd.hh, src/tgba/futurecondcol.hh, src/tgba/state.hh, src/tgba/statebdd.hh, src/tgba/succiter.hh, src/tgba/succiterconcrete.hh, src/tgba/taatgba.hh, src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddcoredata.hh, src/tgba/tgbabddfactory.hh, src/tgba/tgbaexplicit.hh, src/tgba/tgbakvcomplement.hh, src/tgba/tgbaproduct.hh, src/tgba/tgbasafracomplement.hh, src/tgba/tgbascc.hh, src/tgba/tgbasgba.hh, src/tgba/tgbatba.hh, src/tgba/tgbaunion.hh, src/tgba/wdbacomp.hh: Mark exported symbols with SPOT_API. * src/tgba/public.hh: Mark the file as deprecated. * src/tgbaalgos/cutscc.hh: Adjust.
-
Alexandre Duret-Lutz authored
* src/ltlast/Makefile.am, src/ltlenv/Makefile.am, src/ltlvisit/Makefile.am: Use $(VISIBILITY_CXXFLAGS). * src/misc/common.hh (SPOT_DEPRECATED): New macro. * src/ltlast/atomic_prop.hh, src/ltlast/automatop.hh, src/ltlast/binop.hh, src/ltlast/bunop.hh, src/ltlast/constant.hh, src/ltlast/formula.hh, src/ltlast/formula_tree.hh, src/ltlast/multop.hh, src/ltlast/nfa.hh, src/ltlast/refformula.hh, src/ltlast/unop.hh, src/ltlast/visitor.hh, src/ltlenv/declenv.hh, src/ltlenv/defaultenv.hh, src/ltlvisit/apcollect.hh, src/ltlvisit/clone.hh, src/ltlvisit/contain.hh, src/ltlvisit/destroy.hh, src/ltlvisit/dotty.hh, src/ltlvisit/dump.hh, src/ltlvisit/lbt.hh, src/ltlvisit/length.hh, src/ltlvisit/lunabbrev.hh, src/ltlvisit/nenoform.hh, src/ltlvisit/postfix.hh, src/ltlvisit/randomltl.hh, src/ltlvisit/reduce.hh, src/ltlvisit/relabel.hh, src/ltlvisit/remove_x.hh, src/ltlvisit/simpfg.hh, src/ltlvisit/simplify.hh, src/ltlvisit/snf.hh, src/ltlvisit/tostring.hh, src/ltlvisit/tunabbrev.hh, src/ltlvisit/wmunabbrev.hh: Add SPOT_API in fron of exported symbols. * src/ltlvisit/nenoform.cc, src/ltlvisit/remove_x.cc: Add missing include of the corresponding header file.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* src/misc/bddalloc.cc, src/misc/bddalloc.hh, src/misc/freelist.cc, src/misc/freelist.hh: Move ... * src/priv/bddalloc.cc, src/priv/bddalloc.hh, src/priv/freelist.cc, src/priv/freelist.hh: ... here. * src/misc/Makefile.am, src/priv/Makefile.am: Adjust. * src/tgba/bdddict.cc: Adjust include. * src/tgbaalgos/ltl2tgba_fm.cc: Remove useless include.
-
Alexandre Duret-Lutz authored
* src/tgba/bdddict.cc, src/tgba/bdddict.hh: Hide the bdd_allocator dependency in a bdd_dict_priv class that is not defined publicly.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* src/misc/modgray.cc, src/misc/modgray.hh: Delete. * src/misc/Makefile.am: Adjust. * wrap/python/tests/modgray.py: Delete. * wrap/python/tests/Makefile.am: Adjust. * wrap/python/spot.i: Remove binding.
-
Alexandre Duret-Lutz authored
* README: Document it. * configure.ac: Generate src/priv/Makefile. * src/Makefile.am: Recurse into priv/. * src/priv/Makefile.am: New file. * src/misc/acccompl.cc, src/misc/acccompl.hh, src/misc/accconv.cc, src/misc/accconv.hh: Move to... * src/priv/acccompl.cc, src/priv/acccompl.hh, src/priv/accconv.cc, src/priv/accconv.hh: ... here. * src/misc/Makefile.am: Adjust. * src/tgbaalgos/scc.cc, src/tgbaalgos/simulation.cc: Adjust includes. * src/sanity/style.test: Make sure no public header file include a private one.
-
Alexandre Duret-Lutz authored
* 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.
-
Alexandre Duret-Lutz authored
* 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.
-
Alexandre Duret-Lutz authored
* NEWS: Bump version. * configure.ac: Bump version, and add a banner about this being a development version at the end.
-
Alexandre Duret-Lutz authored
* NEWS, configure.ac, doc/org/tools.org: Update version.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
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.
-
- 27 Jul, 2013 1 commit
-
-
Alexandre Duret-Lutz authored
-
- 26 Jul, 2013 2 commits
-
-
Alexandre Duret-Lutz authored
Also accept guards of the form (a) || !(b) or (a) && !(b). * src/neverparse/neverclaimscan.ll: Adjust. * src/tgbatest/neverclaimread.test: Add a test case.
-
Alexandre Duret-Lutz authored
* src/neverparse/neverclaimparse.yy: Remove %expect-rr, that's only for GLR parsers.
-
- 25 Jul, 2013 1 commit
-
-
Alexandre Duret-Lutz authored
* src/bin/ltlcross.cc: Add that missing new line. * NEWS: Mention it.
-
- 23 Jul, 2013 1 commit
-
-
Alexandre Duret-Lutz authored
-
- 20 Jul, 2013 3 commits
-
-
Alexandre Duret-Lutz authored
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.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
- 09 Jul, 2013 6 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* configure.ac, doc/org/tools.org, NEWS: Set version to 1.1.3.
-
Alexandre Duret-Lutz authored
Reported by Joachim Klein. * src/bin/ltlcross.cc: Here. * NEWS, THANKS: Update.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* src/neverparse/neverclaimparse.yy, src/neverparse/neverclaimscan.ll: Allow transitions between do..od, recognize atomic and assert. * src/neverparse/parsedecl.hh: Pass the error_list to the lexer. * src/tgbatest/neverclaimread.test: Add a test case.
-
- 25 Jun, 2013 1 commit
-
-
Alexandre Duret-Lutz authored
Reported by Étienne Renault. * bench/spin13/run.sh: Here.
-