1. 17 Sep, 2012 4 commits
  2. 16 Sep, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Add a visitor to relabel the atomic proposition in formulas. · d9dc1f48
      Alexandre Duret-Lutz authored
      * src/ltlvisit/relabel.cc, src/ltlvisit/relabel.hh: New files.
      * src/ltlvisit/Makefile.am: Add them.
      * src/ltlvisit/clone.cc (recurse): Don't call clone(), nobody
      needs that.  Instead, really recurse.
      * src/bin/ltlfilt.cc: Add a --relabel option.
      * src/bin/genltl.cc: Relabel formulas if --lbt is used.
      * src/sanity/style.test: Tweak detection of i++.
  3. 14 Sep, 2012 4 commits
    • Alexandre Duret-Lutz's avatar
      Add an LTL printer in LBT's syntax. · 1a84c17e
      Alexandre Duret-Lutz authored
      * src/ltlvisit/lbt.cc, src/ltlvisit/lbt.hh: New files.
      * src/ltlvisit/Makefile.am: Add them.
      * src/bin/common_output.cc, src/bin/common_output.hh: Add
      support for LBT output, and reporting formulae that cannot
      be output in this syntax.
      * src/bin/ltlfilt.cc: Pass filename and linenum to
      output_formula() for better error reporting.
    • Alexandre Duret-Lutz's avatar
      Implement a parser for LBT's prefix syntax for LTL. · 106a14f8
      Alexandre Duret-Lutz authored
      * src/ltlparse/public.hh (parse_lbt): New function.
      * src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Implement it.
      * src/bin/ltlfilt.cc: Use it.
    • Alexandre Duret-Lutz's avatar
      Use more sba_explicit more often. · a010ebc8
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh
      (minimize_dfa, minimize_wdba): Return a sba_explicit_number automaton
      instead of tgba_explicit_number.
      * src/tgba/tgbaexplicit.hh (declare_acceptance_condition): Fix code
      so it works on sba as well.
      * src/tgbaalgos/dotty.cc, src/tgbaalgos/neverclaim.cc: Specialize
      for sba instead of tgba_sba_proxy.
      * src/tgbaalgos/neverclaim.hh: Point to degeneralize().
    • Alexandre Duret-Lutz's avatar
      Detect fail conditions on std::cout in user's tools. · 807834ec
      Alexandre Duret-Lutz authored
      * src/bin/common_cout.cc, src/bin/common_cout.hh: New files.
      * src/bin/Makefile.am: Add them.
      * src/bin/ltl2tgba.cc, src/bin/ltlfilt.cc, src/bin/common_output.cc:
      Report error when writing to std::cout failed.  This is mainly
      motivated by ltlfilt not being killed by SIGPIPE on lip6's OSX
      buildfarm (SIGPIPE is probably ignored when the build is started), but
      it could detect other errors such as a disk full.
  4. 12 Sep, 2012 4 commits
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      bin/ltl2tgba: New user binary. · 6a3cf753
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: New class to
      capture the postprocessing logic.
      * src/tgbaalgos/Makefile.am: Add them.
      * src/bin/ltl2tgba.cc, src/bin/man/ltl2tgba.x: New files.
      * src/bin/Makefile.am, src/bin/man/Makefile.am: Add them.
      * src/tgbatest/spotlbtt.test: Prune the list of configurations slightly.
      * src/tgbatest/spotlbtt2.test: New file.
      * src/tgbatest/Makefile.am: Add it.
      * bench/ltl2tgba/algorithms, bench/ltl2tgba/defs.in: Adjust to
      use the new binary.
      * NEWS: Update.
    • Alexandre Duret-Lutz's avatar
      Fix multiple inclusions of config.h. · 26deb56a
      Alexandre Duret-Lutz authored
      * src/bin/common_sys.hh: New file.
      * src/bin/Makefile.am: Add it.
      * src/bin/common_output.hh, src/bin/common_r.cc,
      src/bin/common_range.cc, src/bin/genltl.cc, src/bin/ltlfilt.cc,
      src/bin/randltl.cc: Include common_sys.hh instead of config.h.
    • Alexandre Duret-Lutz's avatar
      Add count_nondet_states(aut) and is_deterministic(aut). · 04b5e370
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/isdet.cc, src/tgbaalgos/isdet.hh: New files.
      * src/tgbaalgos/Makefile.am: Add them.
      * wrap/python/spot.i: Wrap them.
      * wrap/python/ajax/spot.in: Display count of nondeterministic
      * src/tgbatest/ltl2tgba.cc (-kt): Likewise.
      * NEWS: Upadte.
  5. 07 Sep, 2012 21 commits
    • Alexandre Duret-Lutz's avatar
      * NEWS: Summarize recent changes. · 45e93ea1
      Alexandre Duret-Lutz authored
    • Alexandre Duret-Lutz's avatar
      Kill the gspn-ssp benchmark (it was not working anymore). · 2d1460a2
      Alexandre Duret-Lutz authored
      * bench/gspn-ssp/: Delete recursively.
      * bench/Makefile.am, README, configure.ac: Adjust.
    • Alexandre Duret-Lutz's avatar
      Kill src/ltltest/randltl and replace it by src/bin/randltl. · 649e8e2d
      Alexandre Duret-Lutz authored
      * src/ltltest/randltl.cc: Delete.
      * src/ltltest/Makefile.am (noinst_PROGRAMS, randltl_SOURCES): Remove.
      * src/ltltest/reduc.test, src/ltltest/reducpsl.test,
      src/ltltest/utf8.test, src/tgbatest/randpsl.test,
      bench/emptchk/README: Adjust to use bin/randltl.
    • Alexandre Duret-Lutz's avatar
      Kill src/ltltest/genltl now that src/bin/genltl does everything it did. · 1257893f
      Alexandre Duret-Lutz authored
      * src/ltltest/genltl.cc: Delete.
      * src/ltltest/Makefile.am (noinst_PROGRAMS): Remove genltl.
      * src/tgbatest/ltlcounter.test, bench/ltlclasses/run,
      bench/ltlcounter/run: Adjust to call bin/genltl.
    • Alexandre Duret-Lutz's avatar
      Fix missing spaces after comma. · 0990de50
      Alexandre Duret-Lutz authored
      * src/sanity/style.test: Fix the space-after-comma test.
      * src/bin/randltl.cc, src/tgba/tgbaexplicit.hh: Add missing spaces.
    • Alexandre Duret-Lutz's avatar
      randltl: Output unique formulae by default. · f19526a9
      Alexandre Duret-Lutz authored
      * src/bin/randltl.cc: Replace the --unique by an --allow-dups option.
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      randltl: add option to simplify formulas · e43bc893
      Alexandre Duret-Lutz authored
      * src/bin/common_r.cc, src/bin/common_r.hh: New files, extracted from...
      * src/bin/ltlfilt.cc: Here.
      * src/bin/randltl.cc: Use them.
      * src/bin/Makefile.am: Adjust.
    • Alexandre Duret-Lutz's avatar
      Fix prototype of ltl_simplifier::ltl_simplifier. · 7274ca2b
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc: Here.
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      randltl: first stage of the reimplementation · 760d75cc
      Alexandre Duret-Lutz authored
      * src/bin/common_range.cc, src/bin/common_range.hh: New files,
      extracted from...
      * src/bin/genltl.cc: ... here.
      * src/bin/randltl.cc, src/bin/man/randltl.x: New files.
      * src/bin/Makefile.am, src/bin/man/Makefile.am: Adjust.
      * src/bin/man/genltl.x: Point to randltl(1).
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      help2man: generate man pages for genltl and ltlfilt · c96513b6
      Alexandre Duret-Lutz authored
      * tools/help2man, tools/x-to-1.in: New files, copied from gnulib
      * configure.ac: Create x-to-1 and export CROSS_COMPILING.
      * Makefile.am: Distribute help2man.
      * src/bin/Makefile.am (SUBDIRS): New.
      * src/bin/man/Makefile.am: New file.
      * src/bin/man/genltl.x, src/bin/man/ltlfilt.x: New files.
      * src/bin/genltl.cc: Document the RANGE in the options,
      and move the bibliography to genltl.x.
      * README: Document src/bin/man
    • Alexandre Duret-Lutz's avatar
      ltlfilt, genltl: factor the common output options. · e0873cc7
      Alexandre Duret-Lutz authored
      * src/bin/common_output.cc, src/bin/common_output.hh: New file
      with the common output code.
      * src/bin/Makefile.am: Add them.
      * src/bin/genltl.cc, src/bin/ltlfilt.cc: Simplify, using
      argp's children parser, and calling output_formula().
    • Alexandre Duret-Lutz's avatar
      ltlfilt: update the exit status in the same way as grep · 267183bd
      Alexandre Duret-Lutz authored
      * src/bin/ltlfilt.cc: Do it.
    • Alexandre Duret-Lutz's avatar
      ltlfilt: add option to filter by implication or equivalence · 24a8c031
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh: Add a
      implication() option.
      * src/bin/ltlfilt.cc: Add options --implied-by, --imply, and
    • Alexandre Duret-Lutz's avatar
      genltl: reimplement using argp, and allowing ranges. · d1b8537f
      Alexandre Duret-Lutz authored
      * src/bin/genltl.cc: New file.
      * src/bin/Makefile.am: Add it.
    • 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
      * lib/Makefile.am, m4/gnulib-cache.m4, m4/gnulib-comp.m4: Adjust.
      * src/bin/ltlfilt.cc: Use error() and error_at_line().
    • 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
      * lib/Makefile.am, m4/gnulib-cache.m4, m4/gnulib-comp.m4: Adjust.
    • 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/.
  6. 04 Sep, 2012 3 commits
  7. 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
      * doc/tl/tl.tex: Document it.
  8. 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.
  9. 24 Aug, 2012 1 commit