1. 07 Sep, 2012 3 commits
    • Alexandre Duret-Lutz's avatar
      ltlfilt: use error() to report errors. · 90279bd4
      Alexandre Duret-Lutz authored
      * lib/error.c, lib/error.h, lib/msvc-inval.c, lib/msvc-inval.h,
      lib/msvc-nothrow.c, lib/msvc-nothrow.h, m4/error.m4, m4/msvc-inval.m4,
      m4/msvc-nothrow.m4: New files from gnulib
      1af55d85d9762a679b4302d5995f05ccd883e956.
      * lib/Makefile.am, m4/gnulib-cache.m4, m4/gnulib-comp.m4: Adjust.
      * src/bin/ltlfilt.cc: Use error() and error_at_line().
      90279bd4
    • Alexandre Duret-Lutz's avatar
      ltlfilt: Call set_program_name(). · 8132f918
      Alexandre Duret-Lutz authored
      * src/bin/ltlfilt.cc (main): Call set_program_name().
      * lib/progname.c, lib/progname.h: New files, from gnulib
      1af55d85d9762a679b4302d5995f05ccd883e956.
      * lib/Makefile.am, m4/gnulib-cache.m4, m4/gnulib-comp.m4: Adjust.
      8132f918
    • Alexandre Duret-Lutz's avatar
      Install gnulib to make sure we can use argp in ltlfilt. · 93f6e217
      Alexandre Duret-Lutz authored
      * 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/.
      93f6e217
  2. 04 Sep, 2012 3 commits
  3. 29 Aug, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Add back the '*' syntax for And. · 5939d6f4
      Alexandre Duret-Lutz authored
      This somehow revert changes from 2010-01-30 which killed this use of
      star to make room for the Kleen star.  Here we only allow '*' in the
      temporal formula, so that it can still be the Kleen star in SERE.  The
      motivation for '*' available as And is better compatibility with Wring
      and VIS.
      
      * src/ltlparse/ltlscan.ll: Distinguish * from [*].
      * src/ltlparse/ltlparse.yy: Allows * to be used as AND between
      temporal formulae.
      * src/ltltest/equals.test, src/ltltest/parse.test: Add a few
      tests.
      * doc/tl/tl.tex: Document it.
      5939d6f4
  4. 28 Aug, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Add an option to use WDBA only if it reduces the size of the automaton. · 60ec3ace
      Alexandre Duret-Lutz authored
      * src/tgba/tgbaexplicit.hh (num_states): New method.
      * src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc
      (minimize_obligation): Add a reject_bigger option.
      * src/tgbatest/ltl2tgba.cc (-RM): New option.
      * src/tgbatest/spotlbtt.test: Test -RM.
      * bench/ltl2tgba/algorithms: Include -RM in addition to -Rm, and
      replace -RDS by -RIS.
      * NEWS: Mention this.
      60ec3ace
  5. 24 Aug, 2012 2 commits
  6. 22 Aug, 2012 2 commits
  7. 21 Aug, 2012 28 commits