1. 06 Jul, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      tl: add support for X[n], F[n:m] and G[n:m] · e7aa334a
      Alexandre Duret-Lutz authored
      * NEWS, doc/tl/tl.tex, doc/tl/tl.bib: Document these new operators.
      * spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Parse those.
      * spot/tl/formula.cc, spot/tl/formula.hh: Add constructors.
      * spot/gen/formulas.cc: Use it.
      * tests/core/sugar.test: New file.
      * tests/Makefile.am: Add it.
      e7aa334a
  2. 02 Jul, 2018 1 commit
    • Antoine Martin's avatar
      implement NCSB complementation · c717b588
      Antoine Martin authored
      * spot/twaalgos/isdet.cc,spot/twaalgos/isdet.hh: Two new functions to
      highlight deterministic SCCs
      * spot/twaalgos/complement.cc,spot/twaalgos/complement.hh:
      Implementation of the NCSB complementation algorithm
      * tests/Makefile.am, tests/python/complement_semidet.py: Test the
      implementation
      * NEWS: document function
      c717b588
  3. 20 Jun, 2018 2 commits
    • Maximilien Colange's avatar
      make valgrind understand our memory pools · 3fe74f1c
      Maximilien Colange authored
      Annotate pools with valgrind macros so that it detects errors in pool
      usage. Typically, we wish valgrind to detect a leak when the user fails
      to call proper deallocation function.
      
      * spot/misc/fixpool.hh, spot/misc/mspool.hh: here
      * configure.ac: ensure that valgrind header exists
      * tests/Makefile.am, tests/core/mempool.cc, tests/core/mempool.test,
        tests/core/.gitignore: add tests to ensure valgrind accurately detects
        leaks
      3fe74f1c
    • Alexandre Duret-Lutz's avatar
      product_susp: new function · 4f2e9512
      Alexandre Duret-Lutz authored
      * spot/twaalgos/product.cc, spot/twaalgos/product.hh: Implement it.
      * tests/python/_product_susp.ipynb: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention it.
      4f2e9512
  4. 24 May, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      autfilt: better handling of chain of products with -B · c87c13db
      Alexandre Duret-Lutz authored
      Fixes #348, reported by Jeroen Meijer.
      
      * bin/autfilt.cc: If -B is used with many --product,
      degeneralize intermediate products as needed.
      * NEWS: Mention the change.
      * tests/core/prodchain.test: New file.
      * tests/Makefile.am: Add it.
      * spot/twa/acc.cc, spot/twa/acc.hh: Fix reporting of
      overflow.
      * tests/core/acc.cc: Adjust.
      c87c13db
  5. 23 May, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      product: optimize product with weak automata · a738801e
      Alexandre Duret-Lutz authored
      Fixes #350.
      
      * spot/twaalgos/product.cc: Implement this change.
      * NEWS, spot/twaalgos/product.hh: Mention it.
      * spot/twa/acc.cc, spot/twa/acc.hh (acc_cond::sat_mark): New method.
      * tests/python/_product_weak.ipynb: New file.
      * tests/Makefile.am: Add it.
      * tests/python/automata.ipynb, tests/python/highlighting.ipynb,
      tests/python/product.ipynb, tests/core/prodor.test: Adjust test cases.
      a738801e
  6. 04 May, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      introduce containement checks functions · d6f96181
      Alexandre Duret-Lutz authored
      * spot/twaalgos/contains.hh, spot/twaalgos/contains.cc: New files.
      * spot/twaalgos/Makefile.am, python/spot/impl.i: Add them.
      * python/spot/__init__.py: Also attach these functions as methods,
      and support string arguments.
      * tests/python/contains.ipynb: New file.
      * tests/Makefile.am, doc/org/tut.org: Add it.
      * bin/autfilt.cc, tests/python/streett_totgba.py, tests/python/sum.py,
      tests/python/toweak.py: Use the new function.
      d6f96181
  7. 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
      1fdc32f9
  8. 03 Apr, 2018 2 commits
  9. 30 Mar, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      sat_minimize: improve logs and document Python bindings · c766f58d
      Alexandre Duret-Lutz authored
      * spot/priv/satcommon.cc, spot/priv/satcommon.hh: Make it possible to
      set the log file without setting the environment variable.  Adjust
      print_log to take the input state and print it as a new column.
      * spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc: Adjust all
      calls to print_log.  Fix log output for incremental approaches.
      Prefer purge_unreachable_states() over stats_reachable().  Do
      not call scc_filter() on colored automata.
      * spot/twaalgos/dtwasat.hh: Document the new "log" option.
      * NEWS: Mention the changes.
      * tests/python/satmin.ipynb: New file.
      * tests/Makefile.am: Add it.
      * doc/org/satmin.org, doc/org/tut.org: Link to it.
      * doc/org/satmin.org, bin/man/spot-x.x: Adjust description
      of CSV files.
      * bench/dtgbasat/gen.py, bench/dtgbasat/tabl.pl,
      bench/dtgbasat/tabl1.pl, bench/dtgbasat/tabl2.pl,
      bench/dtgbasat/tabl3.pl, bench/dtgbasat/tabl4.pl: Adjust for
      the new column.
      * spot/misc/satsolver.cc, spot/misc/satsolver.hh (stats): Make it
      const.
      * python/spot/__init__.py (sat_minimize): Add display_log and
      return_log options.
      * tests/python/ipnbdoctest.py: Adjust to not compare SAT-minimization
      logs as they contain timings.
      c766f58d
  10. 19 Mar, 2018 1 commit
  11. 21 Feb, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      include config.h in all *.cc files · ac6b0c94
      Alexandre Duret-Lutz authored
      This helps working around missing C functions like strcasecmp that do
      not exist everywhere (e.g. on Cygwin), and for which lib/ supplies a
      replacement.  Unfortunately we do not have such build in our current
      continuous integration suite, so we cannot easily detect files where
      such config.h inclusion would be useful.  Therefore this patch simply
      makes it mandatory to include config.h in *.cc files.  Including this
      in public *.hh file is currently forbidden.
      
      * spot/gen/automata.cc, spot/gen/formulas.cc,
      spot/kripke/fairkripke.cc, spot/kripke/kripke.cc,
      spot/ltsmin/ltsmin.cc, spot/misc/game.cc, spot/parseaut/fmterror.cc,
      spot/parsetl/fmterror.cc, spot/parsetl/parsetl.yy,
      spot/priv/bddalloc.cc, spot/priv/freelist.cc, spot/priv/satcommon.cc,
      spot/priv/trim.cc, spot/priv/weight.cc, spot/ta/ta.cc,
      spot/ta/taexplicit.cc, spot/ta/taproduct.cc, spot/ta/tgtaexplicit.cc,
      spot/ta/tgtaproduct.cc, spot/taalgos/dot.cc,
      spot/taalgos/emptinessta.cc, spot/taalgos/minimize.cc,
      spot/taalgos/reachiter.cc, spot/taalgos/statessetbuilder.cc,
      spot/taalgos/stats.cc, spot/taalgos/tgba2ta.cc, spot/tl/apcollect.cc,
      spot/tl/contain.cc, spot/tl/declenv.cc, spot/tl/defaultenv.cc,
      spot/tl/dot.cc, spot/tl/exclusive.cc, spot/tl/hierarchy.cc,
      spot/tl/length.cc, spot/tl/ltlf.cc, spot/tl/mark.cc,
      spot/tl/mutation.cc, spot/tl/nenoform.cc, spot/tl/print.cc,
      spot/tl/randomltl.cc, spot/tl/relabel.cc, spot/tl/remove_x.cc,
      spot/tl/simplify.cc, spot/tl/snf.cc, spot/tl/unabbrev.cc,
      spot/twa/acc.cc, spot/twa/bdddict.cc, spot/twa/bddprint.cc,
      spot/twa/formula2bdd.cc, spot/twa/taatgba.cc, spot/twa/twa.cc,
      spot/twa/twagraph.cc, spot/twa/twaproduct.cc, spot/twaalgos/aiger.cc,
      spot/twaalgos/alternation.cc, spot/twaalgos/are_isomorphic.cc,
      spot/twaalgos/bfssteps.cc, spot/twaalgos/canonicalize.cc,
      spot/twaalgos/cleanacc.cc, spot/twaalgos/cobuchi.cc,
      spot/twaalgos/complement.cc, spot/twaalgos/complete.cc,
      spot/twaalgos/compsusp.cc, spot/twaalgos/couvreurnew.cc,
      spot/twaalgos/cycles.cc, spot/twaalgos/degen.cc,
      spot/twaalgos/determinize.cc, spot/twaalgos/dot.cc,
      spot/twaalgos/dtbasat.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/gtec/status.cc,
      spot/twaalgos/gv04.cc, spot/twaalgos/hoa.cc,
      spot/twaalgos/iscolored.cc, spot/twaalgos/isdet.cc,
      spot/twaalgos/isunamb.cc, spot/twaalgos/isweakscc.cc,
      spot/twaalgos/langmap.cc, spot/twaalgos/lbtt.cc,
      spot/twaalgos/ltl2taa.cc, spot/twaalgos/ltl2tgba_fm.cc,
      spot/twaalgos/magic.cc, spot/twaalgos/mask.cc,
      spot/twaalgos/minimize.cc, spot/twaalgos/neverclaim.cc,
      spot/twaalgos/parity.cc, spot/twaalgos/postproc.cc,
      spot/twaalgos/powerset.cc, spot/twaalgos/product.cc,
      spot/twaalgos/rabin2parity.cc, spot/twaalgos/randomgraph.cc,
      spot/twaalgos/randomize.cc, spot/twaalgos/reachiter.cc,
      spot/twaalgos/relabel.cc, spot/twaalgos/remfin.cc,
      spot/twaalgos/remprop.cc, spot/twaalgos/sbacc.cc,
      spot/twaalgos/sccfilter.cc, spot/twaalgos/sccinfo.cc,
      spot/twaalgos/se05.cc, spot/twaalgos/sepsets.cc,
      spot/twaalgos/simulation.cc, spot/twaalgos/split.cc,
      spot/twaalgos/stats.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, spot/twaalgos/translate.cc,
      spot/twaalgos/word.cc, tests/core/acc.cc, tests/core/bitvect.cc,
      tests/core/checkpsl.cc, tests/core/checkta.cc, tests/core/consterm.cc,
      tests/core/emptchk.cc, tests/core/equalsf.cc, tests/core/graph.cc,
      tests/core/ikwiad.cc, tests/core/intvcmp2.cc, tests/core/intvcomp.cc,
      tests/core/kind.cc, tests/core/kripkecat.cc, tests/core/length.cc,
      tests/core/ltlrel.cc, tests/core/ngraph.cc, tests/core/parity.cc,
      tests/core/randtgba.cc, tests/core/readltl.cc, tests/core/reduc.cc,
      tests/core/safra.cc, tests/core/sccif.cc, tests/core/syntimpl.cc,
      tests/core/taatgba.cc, tests/core/tostring.cc, tests/core/trival.cc,
      tests/core/twagraph.cc, tests/ltsmin/modelcheck.cc,
      spot/parseaut/scanaut.ll, spot/parsetl/scantl.ll: Include config.h.
      * spot/gen/Makefile.am, spot/graph/Makefile.am,
      spot/kripke/Makefile.am, spot/ltsmin/Makefile.am,
      spot/parseaut/Makefile.am, spot/parsetl/Makefile.am,
      spot/priv/Makefile.am, spot/ta/Makefile.am, spot/taalgos/Makefile.am,
      spot/tl/Makefile.am, spot/twa/Makefile.am, spot/twaalgos/Makefile.am,
      spot/twaalgos/gtec/Makefile.am, tests/Makefile.am: Add the -I lib/
      flags.
      * tests/sanity/includes.test: Catch missing config.h in *.cc, and
      diagnose config.h in *.hh.
      * tests/sanity/style.test: Better diagnostics.
      ac6b0c94
  12. 19 Jan, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      more coverage · 527c8025
      Alexandre Duret-Lutz authored
      * python/spot/impl.i: Add missing bindings from remprop.hh
      * tests/python/except.py: New file to test several error cases.
      * tests/Makefile.am: Add it.
      * spot/twaalgos/rabin2parity.cc (iar): Fix error message.
      527c8025
  13. 16 Jan, 2018 1 commit
    • Maximilien Colange's avatar
      Rabin to parity translation · 7e02aae3
      Maximilien Colange authored
      * spot/twaalgos/rabin2parity.cc, spot/twaalgos/rabin2parity.hh:
        implement it
      * spot/twaalgos/postproc.cc: use it
      * spot/twaalgos/Makefile.am: build the new files
      * NEWS: document the new function
      * python/spot/impl.i: Python bindings for the new function
      * tests/Makefile.am, tests/core/rabin2parity.test: test the new function
      7e02aae3
  14. 14 Jan, 2018 3 commits
    • Alexandre Duret-Lutz's avatar
      work around issue #317 · c920825f
      Alexandre Duret-Lutz authored
      * spot/twaalgos/cobuchi.cc: Call sbacc() on transition-based input.
      * tests/Makefile.am: Remove XFAIL_TESTS.
      * NEWS: Adjust.
      c920825f
    • 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
    • Alexandre Duret-Lutz's avatar
      fix streett_to_generalized_buchi · 9464043d
      Alexandre Duret-Lutz authored
      Fixes #316.
      
      * spot/twaalgos/totgba.cc: Fix confusing definition of scc_inf_wo_fin.
      * tests/python/streett_totgba2.py: New test case.
      * tests/Makefile.am: Add it.
      * NEWS: Mention the bug.
      9464043d
  15. 07 Jan, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      python: remove error recovery checks from the public notebooks · 6bad8aeb
      Alexandre Duret-Lutz authored
      * tests/python/_autparserr.ipynb: New files, containing error
      checking code from automata-io.ipynb and piperead.ipynb.
      * tests/python/automata-io.ipynb: Remove error checks, and pipe
      examples from piperead.ipynb.
      * tests/python/piperead.ipynb: Delete.
      * tests/python/word.ipynb: Move error checking code...
      * tests/python/_word.ipynb: ... in this new file.
      * doc/org/tut.org, tests/Makefile.am: Adjust.
      6bad8aeb
  16. 06 Jan, 2018 1 commit
  17. 02 Jan, 2018 2 commits
  18. 18 Dec, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      introduce check_determinism() · ac80b07d
      Alexandre Duret-Lutz authored
      * spot/twaalgos/isdet.hh, spot/twaalgos/isdet.cc (check_determinism):
      New function.
      * NEWS: Mention it.
      * tests/python/semidet.py: New file.
      * tests/Makefile.am: Add it.
      ac80b07d
  19. 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
  20. 05 Nov, 2017 1 commit
  21. 02 Nov, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      test the SPOT_SATSOLVER envvar · f84ca999
      Alexandre Duret-Lutz authored
      * tests/core/satmin3.test: New file.
      * tests/Makefile.am: Add it.
      * spot/misc/satsolver.cc: Cleanup error messages.
      * spot/misc/satsolver.hh (satsolver_get_solution): Remove this unused
      function.
      * tests/core/readsat.cc, tests/core/readsat.test: Delete (unused).
      * tests/Makefile.am: Adjust.
      f84ca999
    • Alexandre Duret-Lutz's avatar
      test the SPOT_BDD_TRACE envvar · 161bb067
      Alexandre Duret-Lutz authored
      * tests/core/bdd.test: New file.
      * tests/Makefile.am: Add it.
      161bb067
  22. 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
  23. 15 Oct, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      ltlcross, autcross, ltldo: support --fail-on-timeout · 183ec1fb
      Alexandre Duret-Lutz authored
      Suggested by Tobias Meggendorfer.  Fixes #294.
      
      * bin/autcross.cc, bin/ltlcross.cc, bin/ltldo.cc: Add the option.
      * tests/core/autcross3.test, tests/core/ltlcross3.test,
      tests/core/ltldo.test: Test it.
      * tests/Makefile.am: Add autcross3.test.
      * NEWS, doc/org/autcross.org, doc/org/ltlcross.org, doc/org/ltldo.org:
      Mention the option.
      * THANKS: Add Tobias.
      183ec1fb
  24. 11 Oct, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      stutter: detect stutter-invariance at the state level · 9b187297
      Alexandre Duret-Lutz authored
      * spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh: Implement
      stutter-invariance detection at the state level.
      * python/spot/impl.i: Instantiate std::vector<bool>
      * tests/python/stutter-inv-states.ipynb: New file.
      * tests/Makefile.am, doc/org/tut.org: Add it.
      9b187297
  25. 29 Sep, 2017 1 commit
    • 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
  26. 25 Sep, 2017 1 commit
    • 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
      spot::change_parity()
      * tests/Makefile.am: Add tests/core/parity.{cc,hh} and
      tests/python/parity.ipynb
      * doc/org/tut.org: Add the html page of tests/python/parity.ipynb
      27982fb8
  27. 19 Sep, 2017 2 commits
    • Alexandre GBAGUIDI AISSE's avatar
      twaalgos/totgba: Add dnf_to_streett() method · 50e99cdc
      Alexandre GBAGUIDI AISSE authored
      * NEWS: Update.
      * spot/twaalgos/totgba.hh: Declare dnf_to_streett().
      * spot/twaalgos/totgba.cc: Implement dnf_to_streett().
      * bin/autfilt.cc: Add --dnf-to-streett cmd line option.
      * tests/core/dnfstreett.test: Add test.
      * tests/Makefile.am: Add test file.
      50e99cdc
    • Alexandre GBAGUIDI AISSE's avatar
      twaalgos/cobuchi: Add nsa_to_nca() · cf18c069
      Alexandre GBAGUIDI AISSE authored
      * NEWS: Update.
      * spot/twaalgos/cobuchi.hh: Declare to_dca() and nsa_to_nca().
      * spot/twaalgos/cobuchi.cc: Implement them.
      * python/spot/impl.i: Include new file for python bindings.
      * spot/twaalgos/Makefile.am: Add new file.
      * bin/autfilt.cc: Add --dca command line option. This option does not
      return a deterministic automaton yet, but it will.
      * tests/core/dca.test: Add tests for Büchi automata.
      * tests/python/dca.py: Add a python script that builds a nondet. Streett
      automaton.
      * tests/python/dca.test: Add tests for Streett automata.
      * tests/Makefile.am: Add all tests.
      cf18c069
  28. 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
  29. 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
  30. 19 Jul, 2017 1 commit
    • Thomas Medioni's avatar
      Implement to_weak_alternating() which weakifies tgbas · c8889e65
      Thomas Medioni authored
      * NEWS: mention the modification.
      * python/spot/impl.i: makes to_weak_alternating visible from python
      * spot/twaalgos/Makefile.am, spot/twaalgos/toweak.cc,
        spot/twaalgos/toweak.hh: Implements to_weak_alternating.
      * tests/Makefile.am, tests/python/toweak.py: Test the results of
        to_weak_alternating.
      c8889e65
  31. 17 Jul, 2017 3 commits
    • Henrich Lauko's avatar
      tra2tba: Add support for Rabin like automata · 69cf3c55
      Henrich Lauko authored
      * spot/twaalgos/tra2tba.cc: Support Rabin like input
      * tests/core/tra2tba.cc: Remove C tests
      * tests/core/tra2tba.test: Remove C tests
      * tests/python/tra2tba.py: Convert C tests to python
      * tests/Makefile.am: Remove C tests and add python tests
      69cf3c55
    • Henrich Lauko's avatar
      tra2tba: Implement transformation of TRA to TBA acceptance condition · e1271bf8
      Henrich Lauko authored
      * python/spot/impl.i: Add bindings for tra2tba
      * spot/twaalgos/Makefile.am: Record tra2tba.cc, tra2tba.hh
      * spot/twaalgos/tra2tba.cc: Implement transformation of TRA to TBA
      * spot/twaalgos/tra2tba.hh: Introduce declaration of tra_to_tba
      * tests/Makefile.am: Record tra2tba tests
      * tests/core/tra2tba.cc: Add driver for tests
      * tests/core/tra2tba.test: Add tests of tra2tba transformation
      e1271bf8
    • Alexandre Duret-Lutz's avatar
      python: export the sbacc() algorithm · 2ecd93ac
      Alexandre Duret-Lutz authored
      Fixes #274.
      
      * python/spot/impl.i: Bind sbacc().
      * tests/python/sbacc.py: New tesat.
      * tests/Makefile.am: Add sbacc.py.
      2ecd93ac