1. 08 Aug, 2016 5 commits
  2. 07 Aug, 2016 1 commit
  3. 06 Aug, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      org: more typos and small fixups · 2b4cf8e7
      Alexandre Duret-Lutz authored
      * doc/org/autfilt.org, doc/org/compile.org, doc/org/concepts.org,
      doc/org/csv.org, doc/org/ltl2tgba.org, doc/org/oaut.org: Here.
      * tools/help2man: Adjust regex for optional arguments.
      2b4cf8e7
  4. 05 Aug, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      org: fix some automata rendering · ce7b9c51
      Alexandre Duret-Lutz authored
      The new ob-dot.el installed by 15ea2e66
      makes all the sed escaping useless (and actually harmful).
      
      * doc/org/ltl2tgta.org, doc/org/oaut.org: Fix those.
      ce7b9c51
    • Alexandre Duret-Lutz's avatar
      org: several typos · 06d5aa5e
      Alexandre Duret-Lutz authored
      * doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org,
      doc/org/tut04.org, doc/org/tut10.org, doc/org/tut20.org,
      doc/org/tut21.org, doc/org/tut50.org: Fix some typos and reword some
      sentences.
      06d5aa5e
  5. 04 Aug, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      implement conversion to GRA and GSA · 14bee1ae
      Alexandre Duret-Lutz authored
      Fixes #174.
      
      * spot/twaalgos/totgba.hh, spot/twaalgos/totgba.cc
      (to_generalized_streett, to_generalized_rabin): New functions.
      * spot/twa/acc.hh: Declare more methods as static.
      * bin/autfilt.cc: Implement --generalized-rabin and
      --generalized-streett options.
      * NEWS: Mention these.
      * tests/core/gragsa.test: New file.
      * tests/Makefile.am: Add it.
      14bee1ae
  6. 03 Aug, 2016 1 commit
  7. 02 Aug, 2016 2 commits
  8. 31 Jul, 2016 1 commit
  9. 29 Jul, 2016 4 commits
    • Alexandre Duret-Lutz's avatar
      python: make it possible to modify edges during iteration · d271dfd5
      Alexandre Duret-Lutz authored
      Reported by Laurent Xu.
      
      * python/spot/impl.i: Fix the iterator to return pointers instead of
      references.  Because references are ultimately copied.
      * tests/python/automata.ipynb: Add test cases.
      * NEWS: Mention it.
      d271dfd5
    • Alexandre Duret-Lutz's avatar
      * NEWS: Typo. · 09c63939
      Alexandre Duret-Lutz authored
      09c63939
    • Alexandre Duret-Lutz's avatar
      ltlcross: show cross-comparison checks counterexamples · 59efe470
      Alexandre Duret-Lutz authored
      Part of #38.
      
      * bin/ltlcross.cc: Implement it.
      * NEWS: Mention it.
      * doc/org/ltlcross.org: Adjust example.
      * tests/core/ltlcrossce2.test: New test case.
      59efe470
    • Alexandre Duret-Lutz's avatar
      update gnulib · f6c7ed54
      Alexandre Duret-Lutz authored
      This comes from gnulib 348402f2aac342bc925b7aaea9ee3cc353f427a9 plus
      a custom patch to support compilation of arpg in C++11.
      
      * lib/hard-locale.c, lib/hard-locale.h, m4/hard-locale.m4, m4/ltargz.m4:
      New files.
      * lib/Makefile.am, lib/alloca.in.h, lib/argmatch.c, lib/argmatch.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/c-ctype.h, lib/c-strcase.h, lib/c-strcasecmp.c,
      lib/c-strcaseeq.h, lib/c-strncasecmp.c, lib/config.charset,
      lib/dirname-lgpl.c, lib/dirname.h, lib/dosname.h, lib/errno.in.h,
      lib/error.c, lib/error.h, lib/exitfail.c, lib/exitfail.h,
      lib/fcntl.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/gettimeofday.c, lib/hard-locale.h, lib/intprops.h, lib/isatty.c,
      lib/itold.c, lib/localcharset.c, lib/localcharset.h, lib/lstat.c,
      lib/malloc.c, lib/mbrtowc.c, lib/mbsinit.c, lib/memchr.c, lib/mempcpy.c,
      lib/mkstemp.c, lib/mkstemps.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/quote.h,
      lib/quotearg.c, lib/quotearg.h, lib/rawmemchr.c, lib/ref-add.sin,
      lib/ref-del.sin, lib/secure_getenv.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/stpcpy.c,
      lib/strcasecmp.c, lib/strchrnul.c, lib/streq.h, 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/strverscmp.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/unistd.in.h,
      lib/vasnprintf.c, lib/vasnprintf.h, lib/verify.h, lib/vsnprintf.c,
      lib/wchar.in.h, lib/wctype.in.h, lib/xalloc-die.c,
      lib/xalloc-oversized.h, lib/xalloc.h, lib/xmalloc.c, lib/xsize.h,
      m4/00gnulib.m4, m4/absolute-header.m4, m4/alloca.m4, m4/argp.m4,
      m4/codeset.m4, m4/configmake.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/getopt.m4, m4/gettimeofday.m4, m4/glibc21.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/isatty.m4,
      m4/largefile.m4, m4/localcharset.m4, m4/locale-fr.m4, m4/locale-ja.m4,
      m4/locale-zh.m4, m4/longlong.m4, m4/lstat.m4, m4/malloc.m4,
      m4/math_h.m4, m4/mbrtowc.m4, m4/mbsinit.m4, m4/mbstate_t.m4,
      m4/memchr.m4, m4/mempcpy.m4, m4/mkstemp.m4, m4/mkstemps.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/quote.m4,
      m4/quotearg.m4, m4/rawmemchr.m4, m4/secure_getenv.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/stpcpy.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/strverscmp.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/unistd_h.m4, m4/vasnprintf.m4,
      m4/vsnprintf.m4, m4/warn-on-use.m4, m4/wchar_h.m4, m4/wchar_t.m4,
      m4/wctype_h.m4, m4/wint_t.m4, m4/xalloc.m4, m4/xsize.m4,
      tests/core/randtgba.cc, tools/snippet/arg-nonnull.h,
      tools/snippet/c++defs.h, tools/snippet/warn-on-use.h: Update.
      f6c7ed54
  10. 27 Jul, 2016 9 commits
  11. 26 Jul, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      org: document explicit vs. on-the-fly · da464d81
      Alexandre Duret-Lutz authored
      * doc/org/tut50.org: New file.
      * doc/org/tut.org: Add it.
      * NEWS: Mention it.
      * doc/Makefile.am: Add tut50.org, and download plantuml.jar when needed.
      * doc/org/.dir-locals.el.in, doc/org/init.el.in: Activate plantum.
      * HACKING: Mention the Java dependency.
      da464d81
  12. 25 Jul, 2016 1 commit
  13. 24 Jul, 2016 3 commits
    • Alexandre Duret-Lutz's avatar
      use SPOT_ASSERT instead of assert · 20cf43b3
      Alexandre Duret-Lutz authored
      For #184.
      
      * spot/graph/graph.hh, spot/kripke/kripkegraph.hh,
      spot/misc/bitvect.hh, spot/misc/common.hh, spot/misc/fixpool.hh,
      spot/misc/mspool.hh, spot/misc/timer.hh, spot/tl/formula.hh,
      spot/twa/acc.hh, spot/twa/taatgba.hh, spot/twa/twa.hh,
      spot/twa/twagraph.hh, spot/twaalgos/emptiness_stats.hh,
      spot/twaalgos/mask.hh, spot/twaalgos/ndfs_result.hxx,
      spot/twaalgos/sccinfo.hh, spot/twaalgos/translate.hh: Replace
      assert() by SPOT_ASSERT(), or an exception, or nothing, depending
      on the case.
      * tests/sanity/style.test: Flag all asserts in headers.
      * HACKING: Discuss assertions.
      20cf43b3
    • Alexandre Duret-Lutz's avatar
      configure: support --enable-glibgxx-debug · 9f7bf5ab
      Alexandre Duret-Lutz authored
      Part of #184.
      
      * m4/devel.m4 (adl_ENABLE_GLIBCXX_DEBUG): New macro.
      * configure.ac: Use it.
      * README: Mention it.
      * spot/twa/acc.cc: Fix a small issue found with this
      option.
      9f7bf5ab
    • Alexandre Duret-Lutz's avatar
      1a5de86c
  14. 22 Jul, 2016 1 commit
  15. 20 Jul, 2016 1 commit
  16. 19 Jul, 2016 6 commits
    • Alexandre Duret-Lutz's avatar
      bin: overhaul default input selection · dd6875d5
      Alexandre Duret-Lutz authored
      If no input have been specified, and the standard input is not a tty all
      tools now default to reading it.  If standard input is a tty, all tools
      display an error message.  Additionally, - is now a shorthand for -F- in
      all tools.
      
      * NEWS: Summarize this.
      * bin/common_finput.cc, bin/common_finput.hh (check_no_formulas,
      check_no_automaton): New functions that implement the above istty()
      logic.
      * bin/autfilt.cc, bin/dstar2tgba.cc, bin/ltl2tgba.cc, bin/ltl2tgta.cc,
      bin/ltlcross.cc, bin/ltldo.cc, bin/ltlgrind.cc: Use these function,
      and recognize '-' if it was not the case.
      * tests/core/acc_word.test, tests/core/ltldo.test,
      tests/core/minusx.test, tests/core/readsave.test,
      tests/core/unambig.test: Adjust some tests to exercise this.
      * doc/org/autfilt.org, doc/org/csv.org, doc/org/dstar2tgba.org,
      doc/org/ltl2tgba.org, doc/org/ltlcross.org, doc/org/ltlfilt.org,
      doc/org/oaut.org: Adjust the documentation and simplify some
      examples.
      dd6875d5
    • Alexandre Duret-Lutz's avatar
      simplifier: new PSL simplifications · abff7eba
      Alexandre Duret-Lutz authored
      {e[*0..j]}<>->f = {e[*1..j]}<>->f
      {e[*0..j]}[]->f = {e[*1..j]}[]->f
      
      Fixes #81.
      
      This required a small change to the bounded-star-normal-form to prevent
      infinite recursion.
      
      * spot/tl/simplify.cc: Implement these rules.
      * doc/tl/tl.tex, NEWS: Document them.
      * tests/core/reduccmp.test: Add tests, and adjust others.
      * tests/core/unambig.test: Replace formula that used to generated an
      ambiguous automaton, but now generates a deterministic one.
      abff7eba
    • Alexandre Duret-Lutz's avatar
      simplifier: new LTL simplifications · d5b2de7f
      Alexandre Duret-Lutz authored
      if e is pure eventuality and g => e, then e U g = Fg
      if u is purely universal and u => g, then u R g = Gg
      
      Fixes #93.
      
      * doc/tl/tl.tex, NEWS: Document the rules.
      * spot/tl/simplify.cc: Implement them.
      * tests/core/reduccmp.test: Test them.
      * tests/core/det.test: Adjust.
      d5b2de7f
    • Alexandre Duret-Lutz's avatar
      python: have %%dve and %%pml honor SPOT_TMPDIR and TMPDIR · e37f62dc
      Alexandre Duret-Lutz authored
      * python/spot/aux.py (tmpdir): New context manager.
      * python/spot/ltsmin.i: Use it for the two magics.
      * NEWS: Mention this.
      e37f62dc
    • Alexandre Duret-Lutz's avatar
      new test case to improve coverage stats · b136b81c
      Alexandre Duret-Lutz authored
      The streett_to_generalized_buchi() function was not tested unless
      ltl2dstar is installed.
      
      * tests/core/streett.test: New file.
      * tests/Makefile.am: Add it.
      b136b81c
    • Alexandre Duret-Lutz's avatar
      autfilt: add --stutter-invariant · 4c0500a8
      Alexandre Duret-Lutz authored
      * bin/autfilt.cc: Implement the option.
      * NEWS: Mention it.
      * tests/core/readsave.test, tests/core/stutter-tgba.test: Add some
      tests.
      4c0500a8