1. 03 Oct, 2017 1 commit
  2. 02 Oct, 2017 1 commit
  3. 29 Sep, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      tests: speed up two slow tests · f0dc9d44
      Alexandre Duret-Lutz authored
      These were the most expansive tests, each taking more than 5min.
      This should bring them back below 1min.
      * tests/core/parity.test: Do not run through valgrind.
      * tests/python/toweak.py: Remove one very long case.
    • Alexandre Duret-Lutz's avatar
      degen: detect superfluous SCCs and remove them · 900b344c
      Alexandre Duret-Lutz authored
      Suggested by Maximilien Colange.
      * spot/twaalgos/degen.cc: If the output has more SCC than the input,
      detect useless SCCs and remove them.
      * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
      spot/twaalgos/degen.hh: Add support for a degen-remscc option.
      * bin/spot-x.cc, NEWS: Document it.
      * tests/core/degenscc.test: New file.
      * tests/Makefile.am: Add it.
      * tests/core/det.test: Lower some expected size (yay!).
  4. 28 Sep, 2017 1 commit
  5. 27 Sep, 2017 2 commits
  6. 26 Sep, 2017 7 commits
  7. 25 Sep, 2017 13 commits
    • Maximilien Colange's avatar
      Fix a bug in scc_info, and clarify documentation · 2697fcdd
      Maximilien Colange authored
      * spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: Implement it
      * tests/python/sccinfo.py: Test it
      * NEWS: Document the fix
    • Thibaud Michaud's avatar
      ltlsynt: translate winning strategy to AIGER · d6ae7af5
      Thibaud Michaud authored
      * bin/ltlsynt.cc: Here.
      * doc/org/ltlsynt.org: Document it.
      * tests/core/ltlsynt.test: Test it.
    • Thibaud Michaud's avatar
      parity game: compute winning strategy · 601e1405
      Thibaud Michaud authored
      * spot/misc/game.cc, spot/misc/game.hh: Here.
      * bin/ltlsynt.cc: Realizability is now done by checking if the winning
      strategy contains the initial state.
    • Thibaud Michaud's avatar
      parity game: add Zielonka's recursive algorithm · f414e9f5
      Thibaud Michaud authored
      * spot/misc/game.cc, spot/misc/game.hh: Implement it.
      * bin/ltlsynt.cc: Use it.
      * doc/org/ltlsynt.org: Document it.
    • Thibaud Michaud's avatar
      add ltlsynt executable · 0821c97e
      Thibaud Michaud authored
      For now, ltlsynt only handles LTL realizability. It uses a reduction to
      parity game followed by Calude et al.'s reduction from parity game to
      reachability game.
      * bin/ltlsynt.cc, bin/Makefile.am, bin/man/ltlsynt.x,
      bin/man/Makefile.am, bin/.gitignore: New binary.
      * doc/org/arch.tex, doc/Makefile.am, doc/org/tools.org,
      doc/org/ltlsynt.org: Document it.
      * spot/misc/game.cc, spot/misc/game.hh, spot/misc/Makefile.am: Parity
      game wrapper for parity automata + reachability game interface from
      Calude et al.'s paper.
    • Laurent XU's avatar
      parity: add spot::parity_product_or() · 7a118426
      Laurent XU authored
      parity_product_or constructs the sum of two parity automata and it keeps
      the parity.
      * spot/twaalgos/parity.cc, spot/twaalgos/parity.hh: Here.
      * tests/core/parity.cc: Add tests here.
    • Laurent XU's avatar
      parity: merge states having same cleaned matrices in parity_product · 192fb6c1
      Laurent XU authored
      Some states can become identical once their history matrix are
      cleaned. These states are merged and only store the cleaned matrix.
      * spot/twaalgos/parity.cc: Here.
    • Laurent XU's avatar
      parity: remove history matrices in parity_product() · cb7e43cb
      Laurent XU authored
      The history matrix of size n*m is replaced by couples of vectors with a
      total size of n + m. These couples of vectors are simplified
      representations of the history matrices, they ecnode the exact same
      data. They are cached as well as the method to get the next history
      matrix using the acc_sets and the current history matrix.
      * spot/twaalgos/parity.cc: Here.
    • Laurent XU's avatar
      parity: add spot::parity_product() · b92320cc
      Laurent XU authored
      Compute the synchronized product of two parity automata, this product
      keeps the parity acceptance.
      * spot/twaalgos/parity.cc, spot/twaalgos/parity.hh: Here
      * tests/core/parity.cc: Add tests for spot::parity_product()
    • Laurent XU's avatar
      parity: add spot::cleanup_parity_acceptance() · 3e650f18
      Laurent XU authored
      Merge the acceptance sets of a parity acceptance with the same priority
      level to simplify this acceptance.
      * spot/twaalgos/parity.cc, spot/twaalgos/parity.hh: Here
      * tests/core/parity.cc: Add tests for spot::cleanup_parity_acceptance()
    • Laurent XU's avatar
      parity: add spot::colorize_parity() · 0bf0a99d
      Laurent XU authored
      These functions colorize automata with parity acceptance. They output
      parity automata.
      * spot/twaalgos/parity.cc, spot/twaalgos/parity.hh: Here
      * tests/core/parity.cc: Add tests for spot::colorize_parity()
      * tests/python/parity.ipynb: Add documentation about
    • Laurent XU's avatar
      parity: add spot::change_parity() · 27982fb8
      Laurent XU authored
      This function changes the parity acceptance of an automaton.
      * spot/twaalgos/parity.cc, spot/twaalgos/parity.hh: Here
      * python/spot/impl.i: Add spot/twaalgos/parity.hh
      * spot/twaalgos/Makefile.am: Add spot/twaalgos/parity.{cc,hh}
      * tests/core/parity.cc, tests/core/parity.test: Add
      spot::change_parity() tests
      * tests/python/parity.ipynb: Add documentation about
      * tests/Makefile.am: Add tests/core/parity.{cc,hh} and
      * doc/org/tut.org: Add the html page of tests/python/parity.ipynb
    • Laurent XU's avatar
      misc: add spot::is_colored() · b7ef7c55
      Laurent XU authored
      This function checks whether an automaton is colored, an automaton
      is said to be colored iff all the transitions belong to exactly one
      acceptance set.
      * spot/twaalgos/iscolored.cc, spot/twaalgos/iscolored.hh: Here.
      * spot/twaalgos/Makefile.am: add spot/twaalgos/iscolored.{cc,hh}
      * python/spot/impl.i: add spot/twaalgos/iscolored.hh
  8. 24 Sep, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      twa_graph: do not order BDDs by IDs in merge_edges() · 5e5a6948
      Alexandre Duret-Lutz authored
      Fixes #282.
      * spot/misc/bddlt.hh (bdd_less_than_stable): New function.
      * spot/twa/twagraph.cc (merge_edges): Use it.
      * tests/core/genltl.test: Adjust, and add an extra test
      for the behavior of #282.
      * tests/core/complement.test, tests/core/degenid.test,
      tests/core/ltldo.test, tests/core/prodor.test,
      tests/core/readsave.test, tests/core/sbacc.test,
      tests/python/atva16-fig2a.ipynb, tests/python/automata.ipynb,
      tests/python/decompose.ipynb, tests/python/dualize.py,
      tests/python/highlighting.ipynb, tests/python/piperead.ipynb,
      tests/python/product.ipynb, tests/python/simstate.py,
      tests/python/tra2tba.py: Adjust all expected outputs.
      * NEWS: Mention the bug.
    • Alexandre Duret-Lutz's avatar
      postproc: fix a comment · 2bca21f7
      Alexandre Duret-Lutz authored
      * spot/twaalgos/postproc.cc: Here.
  9. 22 Sep, 2017 1 commit
  10. 20 Sep, 2017 2 commits
  11. 19 Sep, 2017 8 commits