alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
4360 commits 6 branches 0 tags 36 MiB
Commit graph

86 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
93f6e21759 Install gnulib to make sure we can use argp in ltlfilt. 
* lib/Makefile.am, lib/alloca.c, 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/float+.h, lib/float.c, lib/float.in.h, lib/getopt.c,
lib/getopt.in.h, lib/getopt1.c, lib/getopt_int.h, lib/gettext.h,
lib/intprops.h, lib/itold.c, lib/malloc.c, lib/memchr.c,
lib/memchr.valgrind, lib/mempcpy.c, lib/printf-args.c,
lib/printf-args.h, lib/printf-parse.c, lib/printf-parse.h,
lib/rawmemchr.c, lib/rawmemchr.valgrind, lib/size_max.h,
lib/sleep.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/strchrnul.valgrind, 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_types.in.h, lib/sysexits.in.h,
lib/unistd.in.h, lib/vasnprintf.c, lib/vasnprintf.h, lib/verify.h,
lib/vsnprintf.c, lib/wchar.in.h, lib/xsize.h, m4/00gnulib.m4,
m4/alloca.m4, m4/argp.m4, m4/dirname.m4, m4/double-slash-root.m4,
m4/errno_h.m4, m4/exponentd.m4, m4/extensions.m4, m4/float_h.m4,
m4/getopt.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/longlong.m4, m4/malloc.m4,
m4/math_h.m4, m4/memchr.m4, m4/mempcpy.m4, m4/mmap-anon.m4,
m4/multiarch.m4, m4/nocrash.m4, m4/off_t.m4, m4/printf.m4,
m4/rawmemchr.m4, m4/size_max.m4, m4/sleep.m4, m4/ssize_t.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_types_h.m4,
m4/sysexits.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/_Noreturn.h, tools/snippet/arg-nonnull.h,
tools/snippet/c++defs.h, tools/snippet/warn-on-use.h: New files from
gnulib 1af55d85d9762a679b4302d5995f05ccd883e956.
* configure.ac, Makefile.am: Adjust to compile gnulib.
* src/bin/Makefile.am: Adjust to use gnulib.
* README: Mention lib/.
 2012-09-07 14:32:10 +02:00
Alexandre Duret-Lutz
a0e1a144ad ltlfilt: initial implementation. 
* src/bin/ltlfilt.cc, src/bin/Makefile.am: New files.
* src/Makefile.am (SUBDIRS): Add bin.
* configure.ac: Add src/bin/Makefile.am.
* README: Document src/bin/.
 2012-09-04 14:47:48 +02:00
Ala-Eddine Ben-Salem
9319b0ca25 Changes in order to pass sanity tests 
* src/tgbatest/ltl2tgba.cc, src/ta/Makefile.am, README: code style
 2012-08-21 14:21:30 +02:00
Alexandre Duret-Lutz
c483053a85 Add documentation for temporal logic operators. 
* doc/tl/Makefile.am, doc/tl/tl.tex, doc/tl/tl.bib: New files.
* doc/Makefile.am (SUBDIRS): Recurse into tl/.
* configure.ac: Output doc/tl/Makefile
* README: Describe doc/tl/.
 2012-04-28 09:34:43 +02:00
Alexandre Duret-Lutz
cdd576458c Document --without-included-lbtt. 
* README: Here.
 2012-04-27 15:40:54 +02:00
Alexandre Duret-Lutz
4b0a3a7a37 Make it possible not to build Python bindings. 
* configure.ac: Add a --disable-python option tied to
a USE_PYTHON conditional.
* README: Document the option.
* wrap/Makefile.am: Use the conditional.
 2012-01-17 14:42:34 +01:00
Alexandre Duret-Lutz
6acf30b2ab Remove the old CGI interface. 
* wrap/python/cgi-bin: Remove this directory.
* wrap/python/Makefile.am (SUBDIRS): Remove it.
* configure.ac, README, wrap/python/ajax/README: Likewise.
 2011-11-28 18:17:50 +01:00
Alexandre Duret-Lutz
6b503d43a9 Remove spotref.pdf. 
* doc/Doxyfile.in: Do not generate LaTeX output.
* doc/Makefile.am: Do not build spotref.pdf.
* NEWS, README: Adjust.
 2011-11-28 15:22:48 +01:00
Thomas Badie
bb5949f6de Add text I/O for Kripke structures. 
* src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh: New files.
* src/kripke/Makefile.am: Add them.
* src/kripkeparse/fmterror.cc, src/kripkeparse/kripkeparse.yy,
src/kripkeparse/kripkescan.ll, src/kripkeparse/parsedecl.hh,
src/kripkeparse/public.hh, src/kripkeparse/scankripke.ll: New
files.
* src/kripkeparse/Makefile.am: Add them.
* src/kripketest/bad_parsing.test, src/kripketest/defs.in,
src/kripketest/kripke.test, src/kripketest/origin,
src/kripketest/parse_print_test.cc: New files.
* src/kripketest/Makefile.am: Add them.
* src/Makefile.am (SUBDIRS): Add kripkeparse and kripketest.
* README: Document src/kripketest/ and src/kripkeparse/.
* configure.ac: Generate src/kripkeparse/Makefile,
src/kripketest/Makefile, src/kripketest/defs.
* iface/dve2/defs.in (run2): New function.
* iface/dve2/dve2check.cc (syntax, main): Add option -gK.
* iface/dve2/kripke.test: New file.
* iface/dve2/Makefile.am (TESTS): Add kripke.test.
 2011-11-24 22:47:41 +01:00
Alexandre Duret-Lutz
6d213e5e4c Remove the Nips interface. 
* NEWS: Mention it.
* configure.ac, README: Remove it.
* iface/Makefile.am (SUBDIRS): Remove nips.
* iface/nips/: Delete this directory.
 2011-03-07 14:04:25 +01:00
Alexandre Duret-Lutz
155d76f4fb Setup libltdl in ltdl/, so we can use it in the dve2 interface. 
Don't keep it under version control since it is installed by
autoreconf.

* configure.ac: Call LT_CONFIG_LTDL_DIR and LTDL_INIT.
* README: Mention ltdl/.
* Makefile.am: Recurse into ldtl.
* iface/dve2/Makefile.am: Link with it.
 2011-03-05 12:29:04 +01:00
Alexandre Duret-Lutz
3427f3bf0e Setup build system for a new dve2 interface. 
* iface/dve2/dve2.cc, iface/dve2/dve2.hh: New dummy files.
* iface/dve2/Makefile.am: New file.
* iface/Makefile.am (SUBDIRS): Add dve2.
* configure.ac: Build iface/dve2/Makefile.
* README: Mention the new directory.
 2011-03-05 11:13:37 +01:00
Alexandre Duret-Lutz
dd13bfa07b Add some tricks into HACKING. 
* README: Typo.
* HACKING: s/CVS/GIT/ and add some tricks about libtool and doxygen.
 2011-02-08 12:23:34 +01:00
Alexandre Duret-Lutz
34f49a8692 Preliminary implementation of an ajax-based ltl2tgba translator. 
* configure.ac: Output wrap/python/ajax/Makefile.
* wrap/python/Makefile.am (SUBDIRS): Add ajax.
* wrap/python/ajax/Makefile.am, wrap/python/ajax/README,
wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/spot.in: New files.
* wrap/python/ajax/css/, wrap/python/ajax/js,
wrap/python/ajax/logos: New directories.
* README: Document wrap/python/ajax/.
 2011-01-18 16:31:33 +01:00
Alexandre Duret-Lutz
3a8e1cdce0 * README: Mention bench/wdba/. 2011-01-05 08:02:39 +01:00
Alexandre Duret-Lutz
48e4c13da9 * README: Mention bench/ltlclases/. 2010-12-07 15:52:22 +01:00
Alexandre Duret-Lutz
ac08c5abce Cleanup neverclaim support. 
* src/neverclaimparse/: Shorthen as ...
* src/neverparse/:... this.
* src/Makefile.am: Adjust, and add back the directories mistakenly
removed by previous patch.
* README: Adjust, and keep the file's width under 80 columns.
* configure.ac: Adjust.
* src/neverparse/Makefile.am, src/neverparse/fmterror.cc,
src/neverparse/neverclaimparse.yy,
src/neverparse/neverclaimscan.ll, src/neverparse/public.hh:
Fix copyright.
* src/tgbatest/Makefile.am (check_PROGRAMS): Remove neverclaimread.
* src/tgbatest/ltl2tgba.cc: Add option -XN to read a neverclaim.
* src/tgbatest/readneverclaim.cc: Delete.
* src/tgbatest/neverclaimread.test: Use ltl2tgba instead of
neverclaimread.
 2010-11-06 14:35:31 +01:00
Felix Abecassis
ab6ec5cb63 Add never claim parser. 
* src/neverclaimparse/: New directory.
* src/neverclaimparse/fmterror.cc: New file.  Print a formatted parse
error on a output stream.
* src/neverclaimparse/neverclaimparse.yy: New file.  Parser declaration
for Bison.
* src/neverclaimparse/neverclaimscan.ll: New file.  Scanner declaration
for Flex.
* src/neverclaimparse/public.hh: New file.  Public header for external
use.
* src/neverclaimparse/parsedecl.hh: New file.  Header file for
Flex-Bison interaction.
* src/neverclaimparse/Makefile.am: New Makefile.
* src/tgbatest/neverclaimread.cc: New file.  Test program for the
never claim parser.
* src/tgbatest/neverclaimread.test: New file.  Test script for the
never claim parser.
* src/tgbatest/Makefile.am: Adjust.
* configure.ac : Adjust.
* README: Adjust.
 2010-11-06 14:35:23 +01:00
Alexandre Duret-Lutz
498b44f742 Revert "Add never claim parser." 
Such changes should not be pushed to master before they are finished
(this doesn't pass distcheck).

This reverts commit 9aaa638b27.
 2010-06-21 17:42:29 +02:00
Felix Abecassis
9aaa638b27 Add never claim parser. 
* src/neverclaimparse/: New directory.
* src/neverclaimparse/fmterror.cc: New file.  Print a formatted parse
error on a output stream.
* src/neverclaimparse/neverclaimparse.yy: New file.  Parser declaration
for Bison.
* src/neverclaimparse/neverclaimscan.ll: New file.  Scanner declaration
for Flex.
* src/neverclaimparse/public.hh: New file.  Public header for external
use.
* src/neverclaimparse/parsedecl.hh: New file.  Header file for
Flex-Bison interaction.
* src/neverclaimparse/Makefile.am: New Makefile.
* src/tgbatest/neverclaimread.cc: New file.  Test program for the
never claim parser.
* src/tgbatest/neverclaimread.test: New file.  Test script for the
never claim parser.
* src/tgbatest/Makefile.am: Adjust.
* configure.ac : Adjust.
* README: Adjust.
 2010-05-25 16:45:08 +02:00
Alexandre Duret-Lutz
c00a80a2fc Update some text files for upcoming 0.5. 
* NEWS: Update for upcoming 0.5.
* HACKING: Update Automake requirement.
* README: Mention the mailing list.
* bench/ltlcounter/README: More text.
* configure.ac: Report bugs to spot@lrde.epita.fr.
 2010-01-29 18:18:45 +01:00
Alexandre Duret-Lutz
7d5f493fb2 Rename wrap/python/cgi/ as wrap/python/cgi-bin/. 
* wrap/python/cgi/: Rename as ...
* wrap/python/cgi-bin/: ... this.
* configure.ac, spot/wrap/python/Makefile.am, README: Adjust.
 2010-01-29 15:48:56 +01:00
Alexandre Duret-Lutz
06f0fe1d40 Check that all directories are documented. 
* src/sanity/readme.test: For each AC_OUTPUT Makefile, check that
the directory is documented in README.  Also skip non distributed
directories in readme.test.
* README: Fit on 80 columns.
 2010-01-24 15:20:54 +01:00
Alexandre Duret-Lutz
9f41e397d5 * README: Typo. 2010-01-24 11:53:35 +01:00
Alexandre Duret-Lutz
2919b64532 * README: Add descriptions for subdirectories of bench/, src/sanity, 
and src/kripke.
 2010-01-24 10:37:07 +01:00
Guillaume Sadegh
3633fced1d Update the README. 
* README: Reference src/saba/, src/sabaalgos/, src/sabatest/,
iface/nips/, iface/nips/nipstest/ and iface/nips/nips_vm/.
 2010-01-24 02:48:31 +01:00
Damien Lefortier
355461ae99 Extend the ELTL parser to support basic aliases of automaton 
operators such as F=U(true,$0) or R=!U(!$0,!$1), and infix
notation for binary automaton operators.

* README: Document the ELTL directories.
* src/eltlparse/eltlparse.yy, src/eltlparse/eltlscan.ll: Add
support for aliases and infix notation.
* src/eltlparse/public.hh, src/ltlast/nfa.cc, src/ltlast/nfa.hh:
Clean them.
* src/eltltest/acc.test, src/tgbatest/eltl2tgba.test: Add tests
for the ELTL parser's extensions.
* src/tgbatest/eltl2tgba.cc: Adjust.
 2009-04-04 22:35:23 +02:00
Alexandre Duret-Lutz
98fd480506 * README: Update lbtt references. 2008-02-25 14:36:55 +01:00
Alexandre Duret-Lutz
7ef117e3dc * bench/ltl2tgba/README: More instructions. 
* bench/Makefile.am (SUBDIRS): Add ltl2tgba.
* README: Mention bench/ltl2tgba.
 2005-04-19 09:04:22 +00:00
Alexandre Duret-Lutz
acf61d1a46 * README: Typos. 2005-04-12 09:18:54 +00:00
Alexandre Duret-Lutz
7bba6dc63d * src/tgbaalgos/emptiness_stats.hh: Make sure depth() >= 0. 
* src/tgbaalgos/gtec/gtec.hh (couvreur99_check, couvreur99_check_shy):
Add the poprem option.
* src/tgbaalgos/gtec/gtec.cc: Implement it.
* src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh
(scc_stack::rem, scc_stack::clear_rem,
scc_stack::connected_component::rem): New.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Add rem variants.
 2005-01-28 23:55:33 +00:00
Alexandre Duret-Lutz
01566183d8 * README: Update. 2004-08-09 09:41:00 +00:00
Alexandre Duret-Lutz
579c343e13 * src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/emptinesscheck.cc: 
Delete and split into ...
* src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh,
src/tgbaalgos/gtec/explscc.cc, src/tgbaalgos/gtec/explscc.hh,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh,
src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh,
src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh: ...
these new files.
* src/tgbaalgos/gtec/Makefile.am: New file.
* src/tgbaalgos/Makefile.am (SUBDIRS, libtgbaalgos_la_LIBADD):
Recurse into gtec and link gtec/libgtec.la.
(tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Remove emptinesscheck.hh
and emptinesscheck.cc.
* configure.ac: Output src/tgbalagos/gtec/Makefile.
* iface/gspn/ltlgspn.cc, src/tgbatest/ltl2tgba.cc: Update includes.
* README: Update tree description.
 2004-04-14 10:56:36 +00:00
Alexandre Duret-Lutz
4bffe7bfc7 * README: More build instructions. 
* HACKING: Update.
 2003-10-31 08:33:53 +00:00
Alexandre Duret-Lutz
b90e0d611f * README: Update layout. 2003-08-05 14:23:35 +00:00
Alexandre Duret-Lutz
53bf08014e * configure.ac: Bump version to 0.0d. 
* NEWS, README: New files.
 2003-07-13 14:52:38 +00:00