1. 02 Nov, 2017 1 commit
  2. 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
  3. 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
  4. 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
  5. 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
  6. 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
  7. 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
  8. 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
  9. 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
  10. 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
  11. 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
  12. 11 Jun, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      libtool: surrender to Debian's castrated libtool · 97e903b1
      Alexandre Duret-Lutz authored
      The libtool version distributed by Debian is patched to *not* propagate
      dependencies (i.e., if libA depends on libB, then linking against libA
      will not automatically link against libB, it has to be explicit),
      contrary to what the Libtool manual document.  So now we explicitly
      link against both libA and libB in such case.
      
      * configure.ac: Remove the workaround that does not work for
      MinGW.
      * doc/org/compile.org: Mention the issue.
      * bin/Makefile.am, tests/Makefile.am, spot/ltsmin/Makefile.am,
      doc/org/g++wrap.in: Make the dependencies explicit.
      97e903b1
  13. 08 Jun, 2017 2 commits
    • Thomas Medioni's avatar
      streett_to_generalized_buchi() now works on Streett-like · 7b5b8f34
      Thomas Medioni authored
      * NEWS: Mention the modification.
      * spot/twaalgos/remfin.cc: Adapt to avoid infinite recursion.
      * spot/twaalgos/totgba.cc: Work on Streett-like.
      * tests/Makefile.am, tests/python/streett_totgba.py: Tests the
        modification.
      * tests/core/remfin.test: Fix one test case that is now handled by
        the modification.
      7b5b8f34
    • Thomas Medioni's avatar
      introduce spot::simplify_acceptance() · a12d676b
      Thomas Medioni authored
      Simplify some automata where some marks are identical,
      or complementary to another. Fixes #216.
      
      * NEWS: mention the new function.
      * spot/twaalgos/cleanacc.cc, spot/twaalgos/cleanacc.hh: Implement
        the function.
      * tests/Makefile.am, tests/python/merge.py: Test this implementation.
      a12d676b
  14. 07 Jun, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      libtool: surrender to Debian's castrated libtool · 1042a8da
      Alexandre Duret-Lutz authored
      The libtool version distributed by Debian is patched to *not* propagate
      dependencies (i.e., if libA depends on libB, then linking against libA
      will not automatically link against libB, it has to be explicit),
      contrary to what the Libtool manual document.  So now we explicitly
      link against both libA and libB in such case.
      
      * configure.ac: Remove the workaround that does not work for
      MinGW.
      * doc/org/compile.org: Mention the issue.
      * bin/Makefile.am, tests/Makefile.am, spot/ltsmin/Makefile.am,
      spot/gen/Makefile.am, doc/org/g++wrap.in: Make the dependencies
      explicit.
      1042a8da
  15. 31 May, 2017 3 commits
  16. 30 May, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      scc_info: make it possible to ignore or cut edges · 42562015
      Alexandre Duret-Lutz authored
      * spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: Take
      a filter function as optional argument.
      * tests/core/sccif.cc, tests/core/sccif.test: New files.
      * tests/Makefile.am, tests/core/.gitignore: Adjust.
      * NEWS: Mention the new feature.
      42562015
  17. 05 May, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      introduce spot::split_edges() · 19aae6f9
      Alexandre Duret-Lutz authored
      Fixes #255.
      
      * spot/twaalgos/split.cc, spot/twaalgos/split.hh,
      tests/core/split.test: New files.
      * spot/twaalgos/Makefile.am, tests/Makefile.am: Add them.
      * bin/autfilt.cc (--split-edges): New option.
      * python/spot/impl.i: Process split.hh.
      * tests/python/alternating.py: Test split_edges() on
      an alternating automaton.
      19aae6f9
    • Alexandre Duret-Lutz's avatar
      twa_graph: introduce copy_state_names_from() · 46d8aaaa
      Alexandre Duret-Lutz authored
      * spot/twa/twagraph.cc, spot/twa/twagraph.hh: Here.  Also
      make sure "original-states" survives defrag_states().
      * NEWS: Mention it.
      * tests/python/origstate.py: New file.
      * tests/Makefile.am: Add it.
      46d8aaaa
  18. 26 Apr, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      gen: rename genltl() to ltl_pattern() and introduce ltl_patterns() · 540b9713
      Alexandre Duret-Lutz authored
      * spot/gen/formulas.hh, spot/gen/formulas.cc (genltl): Rename as...
      (ltl_pattern): This.
      (ltl_pattern_max): New function.
      * bin/genltl.cc: Adjust names, and simplify using ltl_pattern_max().
      * python/spot/gen.i (ltl_patterns): New function.
      * tests/python/gen.py: Test it.
      * tests/python/gen.ipynb: New file to document the spot.gen package.
      * tests/Makefile.am, doc/org/tut.org: Add gen.ipynb.
      540b9713
  19. 23 Apr, 2017 1 commit
  20. 22 Apr, 2017 2 commits
  21. 21 Apr, 2017 1 commit
    • Thomas Medioni's avatar
      Implements is_streett_like() and streett_like_pairs(), is_rabin_like... · b428ed31
      Thomas Medioni authored
      Adds the method spot::acc_cond::is_streett_like() that behaves like
      spot::acc_cond::is_streett() except that it works on a wider range
      of acceptance conditions, called Streett-like. Also adds
      spot::acc_cond::streett_like_pairs() that returns a boolean assessing
      whether the acceptance condition is Streett-like and also returns all
      the Streett_like pairs.
      Defines the new struct type spot::acc_cond::rs_pair.
      Similarily, Adds the methods spot::acc_cond::is_rabin_like() and
      spot::acc_cond::rabin_like_pairs().
      
      * NEWS: Mention this modification
      * python/spot/impl.i: Declares the new struct to SWIG, and defines
      the streett_like_pairs() vector as an output parameter, which makes
      the python code return a tuple (boolean, vector) rather than a
      pass-by-reference vector.
      * spot/twa/acc.cc, spot/twa/acc.hh: Declares an implements the new
      methods and the new nested struct.
      * tests/Makefile.am: Add new tests to the suite
      * tests/python/rs_like.py: Tests the new methods and
      the SWIG bindings.
      b428ed31
  22. 07 Apr, 2017 2 commits
    • Thomas Medioni's avatar
      autfilt: Add --dualize option · 0d884d4a
      Thomas Medioni authored
      * NEWS: Mention this addition.
      * bin/autfilt.cc: Add dualize option
      * tests/Makefile.am: Add dualize option test file to the suite.
      * tests/core/dualize.test: Test the dualize option.
      0d884d4a
    • Thomas Medioni's avatar
      implement dualize to complement automatons · c9d8d41f
      Thomas Medioni authored
      * NEWS: Mention the implementation
      * python/spot/impl.i: Add dualize() to python interface.
      * spot/twaalgos/Makefile.am: Add dualize.cc,hh to the build
      * spot/twaalgos/dualize.cc: Implement dualize() that takes an automaton
        and returns its dual
      * spot/twaalgos/dualize.hh: Implement dualize()
      * tests/Makefile.am: Add dualize tests to the test suite
      * tests/python/dualize.py: Test cases for dualize
      c9d8d41f
  23. 10 Mar, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      emptiness checks: replace assert-preconditions by exceptions · d6d987bd
      Alexandre Duret-Lutz authored
      * spot/twaalgos/couvreurnew.cc, spot/twaalgos/gv04.cc,
      spot/twaalgos/magic.cc, spot/twaalgos/se05.cc, spot/twaalgos/tau03.cc,
      spot/twaalgos/tau03opt.cc: Throw if precondition on acceptance
      condition is not satisfied.
      * tests/python/misc-ec.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention the change.
      d6d987bd
    • Alexandre Duret-Lutz's avatar
      emptiness checks: replace assert-preconditions by exceptions · 2e3fc0d4
      Alexandre Duret-Lutz authored
      * spot/twaalgos/couvreurnew.cc, spot/twaalgos/gv04.cc,
      spot/twaalgos/magic.cc, spot/twaalgos/se05.cc, spot/twaalgos/tau03.cc,
      spot/twaalgos/tau03opt.cc: Throw if precondition on acceptance
      condition is not satisfied.
      * tests/python/misc-ec.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention the change.
      2e3fc0d4
  24. 09 Mar, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      python: add python bindings for declarative_environment · b81d7e58
      Alexandre Duret-Lutz authored
      * python/spot/impl.i: Here.
      * tests/python/declenv.py: New file.
      * tests/Makefile.am: Add it.
      b81d7e58
    • Thomas Medioni's avatar
      Implement sum(..) and sum_and(..). · 194c1992
      Thomas Medioni authored
      Fixes #231.
      
      * NEWS: Mention of implementation of sum, sum_and.
      * bin/autfilt.cc: Add --sum, --sum-or and --sum-and options.
      * python/spot/impl.i: Add bindings for sum, sum_and.
      * spot/twaalgos/Makefile.am: Add sum.cc, sum.hh.
      * spot/twaalgos/sum.cc: Implement sum, sum_and.
      * spot/twaalgos/sum.hh: Declaration of sum, sum_and.
      * tests/Makefile.am: Add sum tests.
      * tests/core/explsum.test: Test the sum of two automatons,
        false or false, unsatisfied mark propagation, handling of univ.
        transitions.
      * tests/python/sum.py: Check that two automatons that does not
        share their bdd dict are not accepted, then run tests over the
        sum of randomly generated LTL formulas.
      194c1992
  25. 08 Mar, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      python: add bindings for bdd_to_formula() · d1d3ee38
      Alexandre Duret-Lutz authored
      Follow-up to an email from Ayrat Khalimov.
      
      * python/spot/impl.i: Include twa/formula2bdd.hh.
      * python/spot/__init__.py: Make the dictionnary
      optional.
      * spot/twa/formula2bdd.cc: Throw an exception instead of asserting.
      * tests/python/bdditer.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Update.
      d1d3ee38
    • Alexandre Duret-Lutz's avatar
      python: add bindings for bdd_to_formula() · 4e9303e3
      Alexandre Duret-Lutz authored
      Follow-up to an email from Ayrat Khalimov.
      
      * python/spot/impl.i: Include twa/formula2bdd.hh.
      * python/spot/__init__.py: Make the dictionnary
      optional.
      * spot/twa/formula2bdd.cc: Throw an exception instead of asserting.
      * tests/python/bdditer.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Update.
      4e9303e3
  26. 07 Mar, 2017 3 commits
    • Alexandre Duret-Lutz's avatar
      twa_graph: more test coverage · cd4c326f
      Alexandre Duret-Lutz authored
      The goal is to improve coverage stats, but I discovered two issues
      while doing so.
      
      * tests/python/twagraph.py: New test case.
      * tests/Makefile.am: Add it.
      * spot/twa/twagraph.hh: Add fix typos in error messages.
      * python/spot/impl.i: Fix broken wrappers for state_from_number and
      state_acc_sets.
      cd4c326f
    • Alexandre Duret-Lutz's avatar
      twa_graph: more test coverage · 2e763a08
      Alexandre Duret-Lutz authored
      The goal is to improve coverage stats, but I discovered two issues
      while doing so.
      
      * tests/python/twagraph.py: New test case.
      * tests/Makefile.am: Add it.
      * spot/twa/twagraph.hh: Add fix typos in error messages.
      * python/spot/impl.i: Fix broken wrappers for state_from_number and
      state_acc_sets.
      2e763a08
    • Alexandre Duret-Lutz's avatar
      tests: remove ltlprod · be4f1397
      Alexandre Duret-Lutz authored
      This very old test did not do anything useful today.
      
      * tests/core/ltlprod.cc, tests/core/ltlprod.test: Delete.
      * tests/Makefile.am: Adjust.
      be4f1397