1. 11 Dec, 2019 1 commit
  2. 12 Sep, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      fix failing tests on Debian unstable · b1007a3d
      Alexandre Duret-Lutz authored
      * tests/Makefile.am (ltsmin_modelcheck_LDADD): Add -lpthread as it
      seems Debian's libtool does not carries this dependency over from
      libspotltsmin.la.  Also using $(LTLIBMULTITHREAD) does not work,
      because that would add -pthread which is currently ignored when
      linking shared libraries (because libtool adds -nostdlib for some
      reason).
      b1007a3d
  3. 18 Jun, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      simplify: GF(f)=GF(dnf(f)) FG(f)=FG(cnf(f)) · da5d23f0
      Alexandre Duret-Lutz authored
      These rules come from Delag's paper, and help some cases
      in issue #385.
      
      * spot/tl/simplify.cc: Implement the simplification.
      * doc/tl/tl.tex, NEWS: Document it.
      * tests/core/385.test: New file.
      * tests/Makefile.am: Add it.
      * tests/core/reduccmp.test: More tests.
      * tests/core/ltl2tgba2.test: Adjust one improved case.
      * tests/python/automata.ipynb, tests/python/twagraph-internals.ipynb:
      Adjust expected output, as the cnf/dnf reorder some subformulas.
      da5d23f0
  4. 04 Jun, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      remprop: reset no-terminal property · 7d6bfe54
      Alexandre Duret-Lutz authored
      Reported by Yong Li.
      
      * spot/twaalgos/remprop.cc: Here.
      * tests/python/removeap.py: New test case.
      * tests/Makefile.am: Add it.
      * NEWS: Document the issue.
      * THANKS: Add Yong Li.
      7d6bfe54
  5. 02 Jun, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      remprop: reset no-terminal property · 74786324
      Alexandre Duret-Lutz authored
      Reported by Yong Li.
      
      * spot/twaalgos/remprop.cc: Here.
      * tests/python/removeap.py: New test case.
      * tests/Makefile.am: Add it.
      * NEWS: Document the issue.
      * THANKS: Add Yong Li.
      74786324
  6. 24 May, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      word: introduce use_all_aps() · 36d20696
      Alexandre Duret-Lutz authored
      This allows fixing issue #388 reported by Victor Khomenko.
      
      * spot/twaalgos/word.cc, spot/twaalgos/word.hh (use_all_aps): New
      method.
      * tests/python/stutter-inv.ipynb: Use it.
      * tests/python/stutter.py: New file, with Victor's test case.
      * tests/Makefile.am: Add python/stutter.py.
      36d20696
  7. 16 Mar, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      python: improve kripke_graph bindings · 8f7a0c2f
      Alexandre Duret-Lutz authored
      Related to issue #376.
      
      * spot/kripke/kripkegraph.hh: Avoid indirect type definitions for the
      benefit of Swig.
      * python/spot/impl.i: Add bindings for iterators over kripke_graph
      states and edges.
      * tests/python/kripke.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Update.
      8f7a0c2f
  8. 21 Feb, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      python: improve kripke_graph bindings · eb02db85
      Alexandre Duret-Lutz authored
      Related to issue #376.
      
      * spot/kripke/kripkegraph.hh: Avoid indirect type definitions for the
      benefit of Swig.
      * python/spot/impl.i: Add bindings for iterators over kripke_graph
      states and edges.
      * tests/python/kripke.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Update.
      eb02db85
  9. 02 Feb, 2019 1 commit
  10. 14 Jan, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      python: improve bdd_dict bindings · 3908cc1b
      Alexandre Duret-Lutz authored
      Fixes #372.
      
      * python/spot/impl.i: Refactor the handling of exceptions using a
      Lippincott function.  Map out_of_range to IndexError.  Add
      PyObject* version for bdd_dict's register and unregister functions
      so we can use Python objects as well.
      * tests/python/bdddict.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention the changes.
      3908cc1b
  11. 02 Aug, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      scc_info: fix split_on_sets · b2e51545
      Alexandre Duret-Lutz authored
      * spot/twaalgos/sccinfo.cc (split_on_sets): Correctly register APs.
      * tests/python/sccsplit.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention the bug.
      b2e51545
  12. 26 Jul, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      scc_info: fix split_on_sets · 9f81df2c
      Alexandre Duret-Lutz authored
      * spot/twaalgos/sccinfo.cc (split_on_sets): Correctly register APs.
      * tests/python/sccsplit.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention the bug.
      9f81df2c
  13. 24 Jul, 2018 2 commits
    • Maximilien Colange's avatar
      translate any automaton to a parity automaton · 465536d1
      Maximilien Colange authored
      * spot/twaalgos/toparity.cc, spot/twaalgos/toparity.hh: implement it,
        based on last-appearance record (LAR)
      * spot/twaalgos/Makefile.am: build it
      * NEWS: document it
      * python/spot/impl.i: add to python bindings
      * tests/Makefile.am, tests/python/toparity.py: test it
      465536d1
    • Alexandre Duret-Lutz's avatar
      genem: implement a generic emptiness check for twa_graph_ptr · d708174c
      Alexandre Duret-Lutz authored
      * spot/twa/acc.cc, spot/twa/acc.hh (fin_unit, one_fin): New function.
      * spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: New files.
      * spot/twaalgos/Makefile.am: Add it.
      * tests/python/genem.py: New file.
      * tests/Makefile.am: Add it.
      * python/spot/impl.i: Add bindings for genem.hh.
      * NEWS: Mention the new function.
      d708174c
  14. 12 Jul, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      more documentation for twa_graph internals · 46590af6
      Alexandre Duret-Lutz authored
      * spot/graph/graph.hh, spot/twa/twagraph.hh, spot/twa/twagraph.cc:
      Implement a dump_storage_as_dot() method.
      * python/spot/__init__.py (twa_graph.show_storage): New method, above
      dump_storage_as_dot().
      * tests/python/twagraph-internals.ipynb: New file, with documentation
      about the twa_graph internals, using show_storage() to illustrate
      everything.
      * tests/Makefile.am, doc/org/tut.org: Add it.
      * python/spot/impl.i: Add bindings for out_iterasor, demonstrated in
      the Python notebook.
      * spot/twa/twa.hh: Add prop_reset().  Used in the notebook.
      * NEWS: Mention the new notebook and function.
      * doc/org/tut50.org: Link to the notebook.
      * tests/python/ipnbdoctest.py: Adjust for twa_graph_ptr being
      redefined in the spot namespace.
      46590af6
  15. 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
  16. 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
  17. 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
  18. 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
  19. 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
  20. 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
  21. 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
  22. 03 Apr, 2018 2 commits
  23. 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
  24. 19 Mar, 2018 1 commit
  25. 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
  26. 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
  27. 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
  28. 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
  29. 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
  30. 06 Jan, 2018 1 commit
  31. 02 Jan, 2018 2 commits
  32. 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
  33. 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
  34. 05 Nov, 2017 1 commit