1. 07 Nov, 2017 2 commits
  2. 18 Oct, 2017 3 commits
  3. 05 Oct, 2017 1 commit
  4. 03 Oct, 2017 1 commit
  5. 29 Sep, 2017 5 commits
  6. 06 Sep, 2017 1 commit
  7. 05 Sep, 2017 3 commits
  8. 04 Sep, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      bin: make --stats and --format synonyms · e452e09f
      Alexandre Duret-Lutz authored
      * bin/common_output.cc: Make --stats an alias of --format.
      * bin/common_aoutput.cc: Make --format an alias of --stats.
      * tests/core/acc2.test, tests/core/format.test: Test these aliases.
      * NEWS: Mention this.
      e452e09f
  9. 02 Sep, 2017 3 commits
    • Alexandre Duret-Lutz's avatar
      Improve simplification of expr[*0..1] · e8527d5a
      Alexandre Duret-Lutz authored
      Fixes #108.
      
      * spot/tl/simplify.cc: Implement the reduction.
      * doc/tl/tl.tex, NEWS: Document it.
      * tests/core/reduccmp.test: Test it.
      e8527d5a
    • Alexandre Duret-Lutz's avatar
      genltl: add --gxf-and and --fxg-or · 42abcf85
      Alexandre Duret-Lutz authored
      As suggested in #263.
      
      * spot/gen/formulas.cc, spot/gen/formulas.hh, bin/genltl.cc: Implement
      these options.
      * tests/core/genltl.test: Use them.
      * NEWS: Mention them.
      42abcf85
    • Alexandre Duret-Lutz's avatar
      simplify: some new simplification rules · 646c5170
      Alexandre Duret-Lutz authored
      For #263, reported by Mikuláš Klokočka.
      
      G(a & Xe1 & F(b & e2)) = G(a & e1 & Fb & e2)
      F(a | Xu1 | G(b | u2)) = F(a | u1 | Gb | u2)
      
      * spot/tl/simplify.cc: Implement the rules.
      * doc/tl/tl.tex, NEWS: Document them.
      * tests/core/reduccmp.test, tests/core/eventuniv.test: Add test cases.
      * tests/core/det.test, tests/core/ltl2tgba2.test: Adjust to expect
      smaller automata.
      * THANKS: Add Mikuláš.
      646c5170
  10. 31 Aug, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      dot: add x option for dot2tex · fbb9e437
      Alexandre Duret-Lutz authored
      * spot/twa/acc.cc, spot/twa/acc.hh: Add a LaTeX output for acceptance
      conditions.
      * spot/twaalgos/dot.cc: Implement the 'x' option and refactor the code
      a bit to limit duplication.
      * tests/core/dot2tex.test: New test case (requires dot2tex).
      * tests/Makefile.am: Add dot2tex.test.
      * tests/core/alternating.test, tests/core/readsave.test,
      tests/python/automata-io.ipynb: Adjust expected output.
      * NEWS, doc/org/oaut.org: Mention the new option.
      fbb9e437
  11. 30 Aug, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      dot: add option 'A' to disable 'a' · b242122c
      Alexandre Duret-Lutz authored
      This way in 2.5 we can make 'a' the default, and tell people to use
      SPOT_DOTDEFAULT=A if they want the old behavior in both 2.4 and 2.5.
      
      * spot/twaalgos/dot.cc: Implement the option.
      * NEWS, bin/common_aoutput.cc: Mention it.
      * tests/core/readsave.test: Test it.
      b242122c
  12. 28 Aug, 2017 2 commits
    • Maximilien Colange's avatar
      Fix a bug in spot.complete() · 1b2f2a79
      Maximilien Colange authored
      spot.complete() could complete an empty co-Büchi automaton into an
      automaton accepting everything.
      
      * NEWS: Document it
      * spot/twaalgos/complete.cc: Fix it
      * tests/core/complete.test, tests/core/prodor.test: Test it
      1b2f2a79
    • Maximilien Colange's avatar
      Typos · eb91ecf6
      Maximilien Colange authored
      * NEWS, doc/org/concepts.org, doc/org/hierarchy.org,
        spot/misc/optionmap.hh, spot/twa/acc.hh, spot/twaalgos/ltl2tgba_fm.hh,
        spot/twaalgos/sccinfo.hh, spot/twaalgos/translate.cc: fix typos
      eb91ecf6
  13. 22 Aug, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      switch to C++14 compilation · f5dce597
      Alexandre Duret-Lutz authored
      * configure.ac: Compile in C++14 by default and rename
      --enable-c++14 as c++17.
      * doc/org/compile.org, doc/org/concepts.org, doc/org/index.org,
      doc/org/install.org, doc/org/tut.org, doc/org/upgrade2.org, HACKING,
      NEWS, README: Adjust all mentions of C++11.
      * spot/twaalgos/stats.hh: Use std::make_unique.
      f5dce597
  14. 17 Aug, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      dot: display acceptance names · 1cc45b24
      Alexandre Duret-Lutz authored
      * spot/twaalgos/dot.cc: Display common acceptance names.
      * NEWS: Mention the change.
      * doc/org/oaut.org: Adjust text.
      * tests/core/alternating.test, tests/core/readsave.test,
      tests/python/_altscc.ipynb, tests/python/alternation.ipynb,
      tests/python/atva16-fig2a.ipynb, tests/python/atva16-fig2b.ipynb,
      tests/python/automata.ipynb, tests/python/decompose.ipynb,
      tests/python/gen.ipynb, tests/python/highlighting.ipynb,
      tests/python/product.ipynb, tests/python/randaut.ipynb: Adjust test
      cases.
      1cc45b24
  15. 09 Aug, 2017 2 commits
  16. 04 Aug, 2017 2 commits
  17. 03 Aug, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      dot: extend the palette from 9 to 16 colors · e041db61
      Alexandre Duret-Lutz authored
      Let's close #212 even if this does not cover the 32 sets.
      
      * spot/twaalgos/dot.cc: Change the palette.
      * doc/org/autfilt.org, NEWS: Adjust documentation.
      * tests/core/alternating.test, tests/core/readsave.test,
      tests/core/tgbagraph.test, tests/python/_altscc.ipynb,
      tests/python/alternation.ipynb, tests/python/atva16-fig2a.ipynb,
      tests/python/automata-io.ipynb, tests/python/automata.ipynb,
      tests/python/decompose.ipynb, tests/python/gen.ipynb,
      tests/python/highlighting.ipynb, tests/python/ltsmin-dve.ipynb,
      tests/python/piperead.ipynb, tests/python/product.ipynb,
      tests/python/randaut.ipynb, tests/python/word.ipynb: Adjust
      test cases.
      e041db61
  18. 01 Aug, 2017 1 commit
  19. 31 Jul, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      hoa: fix I/O of determinism · d3607a7c
      Alexandre Duret-Lutz authored
      Fixes #212.
      
      * spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Recognize
      exist-branch, and adjust printer to the 1.1 semantics.
      * tests/core/alternating.test, tests/core/complete.test,
      tests/core/det.test, tests/core/explsum.test,
      tests/core/parseaut.test, tests/core/readsave.test,
      tests/core/sbacc.test, tests/core/tgbagraph.test,
      tests/python/alternating.py, tests/python/dualize.py: Adjust test
      cases.
      * NEWS: Mention the change.
      d3607a7c
  20. 28 Jul, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      bin: introduce autcross · 0cf250d8
      Alexandre Duret-Lutz authored
      Fixes #252.
      
      * NEWS: Mention it.
      * bin/autcross.cc, bin/man/autcross.x, doc/org/autcross.org: New
      files.
      * bin/Makefile.am, bin/man/Makefile.am, doc/org/tools.org,
      doc/Makefile.am: Add them.
      * bin/autfilt.cc: Use is_universal() instead of is_deterministic().
      * bin/common_hoaread.hh, bin/common_trans.cc, bin/common_trans.hh,
      bin/ltlcross.cc, bin/ltldo.cc: Factor some bits common between
      ltlcross, ltldo and autcross.
      * tests/core/autcross.test, tests/core/autcross2.test: New files.
      * tests/Makefile.am: Add them.
      * tests/core/dra2dba.test, tests/core/sbacc.test,
      tests/core/streett.test: Use autcross.
      0cf250d8
  21. 27 Jul, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      parseaut: make the scanner reentrant · b9fff6a4
      Alexandre Duret-Lutz authored
      * spot/parseaut/parseaut.yy, spot/parseaut/parsedecl.hh,
      spot/parseaut/public.hh, spot/parseaut/scanaut.ll: Use a reentrant
      scanner, so that we can now parse multiple automaton streams at the
      same time.  This is needed for the future autcross, which is going to
      read several individual automata produced by different tools, while
      reading the stream of automata to process.
      b9fff6a4
  22. 25 Jul, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      acc: make &= and |= symmetrical · abe2c08b
      Alexandre Duret-Lutz authored
      Operator &= used to always move Fin to the front, it does not anymore.
      The only thing it does now is to merge Inf(x)&Inf(y) as Inf({x,y}).
      Operator |= is now symmetrical and merges Fin()s.
      
      Fixes #253.
      
      * spot/twa/acc.cc, spot/twa/acc.hh: Simplify &= and make |= symmetrical.
      * spot/twaalgos/cleanacc.cc: Fix conjunction order.
      * tests/core/acc.test, tests/core/acc2.test, tests/core/parseaut.test,
      tests/core/readsave.test, tests/core/satmin2.test,
      tests/core/sccdot.test, tests/python/acc_cond.ipynb,
      tests/python/accparse.ipynb, tests/python/automata.ipynb,
      tests/python/product.ipynb, tests/python/randaut.ipynb: Adjust test
      cases.
      abe2c08b
    • Alexandre Duret-Lutz's avatar
      deprecate copy() in favor of make_twa_graph() · 8e685e00
      Alexandre Duret-Lutz authored
      Fixes #258.
      
      * spot/twaalgos/copy.cc: Delete, and move the code...
      * spot/twa/twagraph.cc: ... in some anonymous namespace here.
      * spot/twa/twagraph.hh: Adjust the make_twa_graph() overload.
      * spot/twaalgos/copy.hh, NEWS: Mark copy() as deprecated and redirect
      to make_twa_graph().
      * doc/org/upgrade2.org, doc/org/tut51.org, python/spot/impl.i,
      spot/twaalgos/dot.cc, spot/twaalgos/langmap.cc, tests/core/ikwiad.cc:
      Adjust callers.
      * spot/twaalgos/Makefile.am: Remove copy.cc.
      8e685e00
  23. 24 Jul, 2017 2 commits
  24. 20 Jul, 2017 1 commit