1. 18 Mar, 2018 1 commit
  2. 14 Mar, 2018 1 commit
    • Maximilien Colange's avatar
      Fix various typos · 6a3e8e95
      Maximilien Colange authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * bin/autfilt.cc, bin/common_post.cc, spot/graph/graph.hh,
        spot/twa/twa.hh, spot/twa/twagraph.hh, spot/twaalgos/remfin.cc: typos
      * spot/twaalgos/toweak.cc: incorrect types when invoking std::hash
      6a3e8e95
  3. 14 Jan, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      postproc: add support for co-Büchi output · 61b0a542
      Alexandre Duret-Lutz authored
      * spot/twaalgos/cobuchi.cc, spot/twaalgos/cobuchi.hh (to_nca): New
      function.
      (weak_to_cobuchi): New internal function, used in to_nca and to_dca
      when appropriate.
      * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Implement
      the CoBuchi option.
      * python/spot/__init__.py: Support it in Python.
      * bin/common_post.cc: Add support for --buchi.
      * bin/autfilt.cc: Remove the --dca option.
      * tests/core/dca.test, tests/python/automata.ipynb: Adjust and add
      more tests.  In particular, add more complex persistence and
      recurrence formulas to the list of dca.test.
      * tests/python/dca.test: Adjust and rename to...
      * tests/core/dca2.test: ... this.  Add more tests, to the point
      that this is now failing, as described in issue #317.
      * tests/python/dca.py: Remove.
      * tests/Makefile.am: Adjust.
      61b0a542
  4. 09 Jan, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      genltl: add --gf-implies · 0b71df3f
      Alexandre Duret-Lutz authored
      * spot/gen/formulas.cc, spot/gen/formulas.hh: Implement
      LTL_GF_IMPLIES.
      * bin/genltl.cc: Add --gf-implies.
      * NEWS: Mention it.
      * tests/core/genltl.test: Use it.
      0b71df3f
  5. 08 Jan, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      postproc: add support for colored-parity · bd6dc7a8
      Alexandre Duret-Lutz authored
      * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Add support
      for a colored option.
      * bin/common_post.cc, bin/common_post.hh bin/autfilt.cc,
      bin/ltl2tgba.cc, bin/dstar2tgba.cc: Add support for --colored-parity.
      * bin/ltldo.cc: Adjust as well for consistency, even if --parity and
      --colored-parity is not used here.
      * tests/core/parity2.test: Add tests.
      * doc/org/autfilt.org, doc/org/ltl2tgba.org: Add examples.
      * NEWS: Mention --colored-parity.
      bd6dc7a8
  6. 06 Jan, 2018 1 commit
  7. 02 Jan, 2018 2 commits
  8. 28 Dec, 2017 1 commit
  9. 10 Dec, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      Add support for computing operator nesting depth · 62d1e021
      Alexandre Duret-Lutz authored
      * spot/tl/hierarchy.hh, spot/tl/hierarchy.cc (nesting_depth): New
      function.
      * python/spot/__init__.py: Also make it a method of formula in Python
      * bin/common_output.cc, bin/common_output.hh: Implement
      --stats=%[OP]n.
      * NEWS: Mention it.
      * tests/core/format.test, tests/python/formulas.ipynb: Test it.
      62d1e021
  10. 28 Nov, 2017 2 commits
  11. 24 Nov, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      rename one printable_formula · a31ba7ff
      Alexandre Duret-Lutz authored
      We currently have 3 printable_formula classes in Spot; let's reduce
      this to 2.
      
      * bin/common_output.cc (anonymous::printable_formula): Rename to...
      (anonymous::printable_formula_with_location): ... this.
      a31ba7ff
  12. 23 Nov, 2017 1 commit
    • Maximilien Colange's avatar
      Improve ltlsynt interface · 1da0afba
      Maximilien Colange authored
      To ease debugging and testing, ltlsynt can output the synthesized
      strategy as an automaton, not just an aiger circuit.
      Also, its exit code has been changed to something meaningful.
      
      * bin/ltlsynt.cc: Various improvements: options, exit code, code style
      * spot/twaalgos/aiger.hh, spot/twaalgos/aiger.cc,
        spot/twaalgos/Makefile.am: Move the aiger printer to separate files
      * tests/core/ltlsynt.test: Clean up and update test file
      * tests/Makefile.am: Add the test file to the test suite
      * NEWS: document the new aiger printer
      * doc/org/concepts.org: document the named property "synthesis-outputs",
        used by print_aiger
      1da0afba
  13. 16 Nov, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      introduce is_obligation(f) · 50fe34a5
      Alexandre Duret-Lutz authored
      This is not optimal yet because it still construct a minimal WDBA
      internally, but it's better than the previous way to call
      minimize_obligation() since it can avoid constructing the minimized
      automaton in a few more cases.
      
      * spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: Introduce
      is_obligation().
      * bin/ltlfilt.cc: Wire it to --obligation.
      * spot/twaalgos/minimize.cc: Implement is_wdba_realizable(),
      needed by the above.
      * tests/core/obligation.test: Test it.
      * bin/man/spot-x.x, NEWS: Document it.
      50fe34a5
  14. 15 Nov, 2017 2 commits
  15. 07 Nov, 2017 1 commit
  16. 04 Nov, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      autfilt: introduce --acceptance-is · 62302b60
      Alexandre Duret-Lutz authored
      Fixes #288.
      
      * bin/autfilt.cc: Implement it.
      * spot/twa/acc.cc, spot/twa/acc.hh: Add
      acc_cond::is_generalized_streett, acc_cond::operator==, and
      acc_cond::operator!=.
      * tests/core/randaut.test: Add some tests.
      * NEWS: Mention it.
      62302b60
    • Alexandre Duret-Lutz's avatar
      bin: add %g options to print acceptance name · 75a1d6ac
      Alexandre Duret-Lutz authored
      Fixes #289.
      
      * spot/twaalgos/stats.cc, spot/twaalgos/stats.hh,
      bin/common_aoutput.cc, bin/common_aoutput.hh: plug %g and %G into
      acc_cond::name() when arguments are given as %[arg]g.  or %[arg]G.
      * tests/core/acc2.test: Add test case.
      * doc/org/randaut.org, NEWS: Document it.
      75a1d6ac
  17. 01 Nov, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      overhaul the stutter-invariance checks · 6459877a
      Alexandre Duret-Lutz authored
      * spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh: Cleanup and
      document the api.
      * spot/twa/twa.hh, doc/mainpage.dox: Add a stutter-invariant section.
      * tests/python/stutter-inv-states.ipynb: Rename as ...
      * tests/python/stutter-inv.ipynb: ... this, and add more comments.
      * tests/Makefile.am, doc/org/tut.org: Adjust renaming.
      * bench/stutter/stutter_invariance_randomgraph.cc,
      bench/stutter/stutter_invariance_formulas.cc,
      bench/stutter/Makefile.am: Make it compile again.
      * bin/autfilt.cc: Call inplace variants.
      * NEWS: Mention the overhaul.
      6459877a
  18. 19 Oct, 2017 1 commit
  19. 18 Oct, 2017 1 commit
  20. 15 Oct, 2017 4 commits
  21. 13 Oct, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      translate: add support for -x tls-impl=N · 689aa7fd
      Alexandre Duret-Lutz authored
      This is long overdue, and we probably want to use tls-impl=1 in
      ltlsynt.
      
      * spot/twaalgos/translate.cc, spot/twaalgos/translate.hh:
      Add support for tls-impl=N.
      * tests/core/ltl2tgba.test: Test it.
      * bin/spot-x.cc, NEWS: Document it.
      689aa7fd
  22. 07 Oct, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      scc_info: add ways to speedup scc_info · 9ca5b8c2
      Alexandre Duret-Lutz authored
      * spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: Add an optional
      argument to abort on accepting SCC, to not keep track of SCC states,
      and some one_accepting_scc() method.
      * NEWS: Mention it.
      * bin/ltlcross.cc, spot/twaalgos/alternation.cc,
      spot/twaalgos/cobuchi.cc, spot/twaalgos/degen.cc,
      spot/twaalgos/determinize.cc, spot/twaalgos/dtbasat.cc,
      spot/twaalgos/dtwasat.cc, spot/twaalgos/isunamb.cc,
      spot/twaalgos/powerset.cc, spot/twaalgos/remfin.cc,
      spot/twaalgos/sbacc.cc, spot/twaalgos/sccfilter.cc,
      spot/twaalgos/totgba.cc: Adjust arguments passed to scc_info.
      9ca5b8c2
  23. 05 Oct, 2017 1 commit
  24. 29 Sep, 2017 2 commits
    • Alexandre GBAGUIDI AISSE's avatar
      Fix: Remove SBAcc option in bin/ltlfilt · 697c9460
      Alexandre GBAGUIDI AISSE authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * bin/ltlfilt.cc: Remove SBAcc option as rabin_to_buchi_maybe() works
      with transition-based acceptance as well.
      697c9460
    • 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!).
      900b344c
  25. 26 Sep, 2017 3 commits
    • Alexandre Duret-Lutz's avatar
      sanity: also check the 80-column limit in bin · a2cbf0af
      Alexandre Duret-Lutz authored
      * tests/sanity/80columns.test: Check bin sources.
      * bin/ltlsynt.cc: Fix it.
      a2cbf0af
    • Alexandre Duret-Lutz's avatar
      ltlsynt: handle --algo with XARGMATCH · c473e4ca
      Alexandre Duret-Lutz authored
      * bin/ltlsynt.cc: Use XARGMATCH for better error handling.
      c473e4ca
    • Alexandre Duret-Lutz's avatar
      bin: make sure that all options are in a named section · 69daf9c2
      Alexandre Duret-Lutz authored
      This also fixes some empty lines and unsorted options
      that appeared in some tools.
      
      * tests/sanity/bin.test: Ensure this is done.
      * bin/README: Add a new paragraph about this.
      * bin/autcross.cc, bin/ltlcross.cc: Move the
      output options in their own section.
      * bin/common_color.cc: Assume color options are
      in group -15.
      * bin/common_finput.cc, bin/common_finput.hh:
      Add a headless variant.
      * bin/genltl.cc, bin/ltlfilt.cc, bin/ltlgrind.cc,
      bin/randaut.cc, bin/randltl.cc:  Do not force the
      children groups, so that the options are correctly sorted.
      * bin/ltlsynt.cc: Add missing groups.
      69daf9c2
  26. 25 Sep, 2017 4 commits
    • 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.
      d6ae7af5
    • 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.
      601e1405
    • 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.
      f414e9f5
    • 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.
      0821c97e
  27. 22 Sep, 2017 1 commit