1. 18 Jun, 2019 1 commit
  2. 27 Jul, 2018 2 commits
    • Maximilien Colange's avatar
      ltlsynt: new algorithm, based on LAR · 8d5d453e
      Maximilien Colange authored
      * bin/ltlsynt.cc: here
      * tests/core/ltlsynt.test: test it
      * NEWS: document it
    • Maximilien Colange's avatar
      ltlsynt: rework synthesis algorithms · bd75ab5b
      Maximilien Colange authored
      ltlsynt now offers two algorithms: one where splitting occurs before
      determinization (the historical one) and one where determinization
      occurs before splitting.
      * bin/ltlsynt.cc: here
      * tests/core/ltlsynt.test: test it and refactor test file
      * NEWS: document it
      * spot/misc/game.hh, spot/misc/game.cc: remove Calude's algorithm
  3. 16 May, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      bin: factor exception-handling code · 645bb556
      Alexandre Duret-Lutz authored
      * bin/common_setup.cc, bin/common_setup.hh: Define a protected_main()
      function that deal with exceptions.
      * bin/autcross.cc, bin/autfilt.cc, bin/dstar2tgba.cc, bin/genaut.cc,
      bin/genltl.cc, bin/ltl2tgba.cc, bin/ltl2tgta.cc, bin/ltlcross.cc,
      bin/ltldo.cc, bin/ltlfilt.cc, bin/ltlgrind.cc, bin/ltlsynt.cc,
      bin/randaut.cc, bin/randltl.cc: Use it for all tools.
  4. 30 Apr, 2018 1 commit
    • Maximilien Colange's avatar
      ltlsynt: improve construction of turn-based games · 1fdc32f9
      Maximilien Colange authored
      Improve the way transitions are duplicated when preparing the turn-based
      game for synthesis. The resulting arena should now be deterministic on
      nodes owned by the environment. Also move the code to another file, so
      that it is easier to test (e.g. in Python).
      * bin/ltlsynt.cc: move the code
      * spot/twaalgos/split.cc, spot/twaalgos/split.hh: move the code and
        implement the improvements
      * tests/Makefile.am, tests/python/split.py: test it
      * tests/core/ltlsynt.test: update existing tests to reflect the changes
  5. 23 Apr, 2018 3 commits
  6. 15 Mar, 2018 1 commit
    • Maximilien Colange's avatar
      Clean the usage of spot::acc_cond::mark_t · b09c293f
      Maximilien Colange authored
      spot::acc_cond::mark_t is implemented as a bit vector using a single
      unsigned, and implicit conversions between mark_t and unsigned may be
      confusing. We try to use the proper interface.
      * bin/autfilt.cc, bin/ltlsynt.cc, spot/kripke/kripke.cc,
        spot/misc/game.hh, spot/parseaut/parseaut.yy, spot/priv/accmap.hh,
        spot/ta/ta.cc, spot/ta/taexplicit.cc, spot/ta/taproduct.cc,
        spot/taalgos/emptinessta.cc, spot/taalgos/tgba2ta.cc, spot/twa/acc.cc,
        spot/twa/acc.hh, spot/twa/taatgba.cc, spot/twa/taatgba.hh,
        spot/twa/twagraph.hh, spot/twaalgos/alternation.cc,
        spot/twaalgos/cleanacc.cc, spot/twaalgos/cobuchi.cc,
        spot/twaalgos/complete.cc, spot/twaalgos/couvreurnew.cc,
        spot/twaalgos/degen.cc, spot/twaalgos/dot.cc,
        spot/twaalgos/dtwasat.cc, spot/twaalgos/dualize.cc,
        spot/twaalgos/emptiness.cc, spot/twaalgos/gtec/ce.cc,
        spot/twaalgos/gtec/gtec.cc, spot/twaalgos/gtec/sccstack.cc,
        spot/twaalgos/gv04.cc, spot/twaalgos/hoa.cc, spot/twaalgos/lbtt.cc,
        spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/magic.cc,
        spot/twaalgos/ndfs_result.hxx, spot/twaalgos/rabin2parity.cc,
        spot/twaalgos/randomgraph.cc, spot/twaalgos/remfin.cc,
        spot/twaalgos/sbacc.cc, spot/twaalgos/sccfilter.cc,
        spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh,
        spot/twaalgos/se05.cc, spot/twaalgos/sepsets.cc,
        spot/twaalgos/simulation.cc, spot/twaalgos/strength.cc,
        spot/twaalgos/stripacc.cc, spot/twaalgos/stutter.cc,
        spot/twaalgos/sum.cc, spot/twaalgos/tau03.cc,
        spot/twaalgos/tau03opt.cc, spot/twaalgos/totgba.cc,
        spot/twaalgos/toweak.cc, python/spot/impl.i, tests/core/acc.cc,
        tests/core/twagraph.cc: do not confuse mark_t and unsigned
      * tests/python/acc_cond.ipynb: warn about possible change of the API
  7. 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
  8. 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.
    • Alexandre Duret-Lutz's avatar
      ltlsynt: handle --algo with XARGMATCH · c473e4ca
      Alexandre Duret-Lutz authored
      * bin/ltlsynt.cc: Use XARGMATCH for better error handling.
    • 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.
  9. 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.
    • 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.