1. 12 Mar, 2020 1 commit
  2. 11 Mar, 2020 2 commits
  3. 15 Feb, 2020 1 commit
    • Alexandre Duret-Lutz's avatar
      autfilt add support for --partial-degeneralize · b5e464e0
      Alexandre Duret-Lutz authored
      * bin/autfilt.cc: Add a --partial-degeneralize option.
      * NEWS: Mention it.
      * spot/twaalgos/degen.cc: Do not restrict partial_degeneralize() to
      deterministic automata.
      * spot/twaalgos/degen.hh: Adjust documentation.
      * tests/core/pdegen.test: New test case.
      * tests/Makefile.am: Add it.
      * tests/python/pdegen.py: Adjust.
      b5e464e0
  4. 26 Sep, 2019 2 commits
    • Alexandre Duret-Lutz's avatar
      bin: handle any exception before returning from parse_opt() · d523ce8b
      Alexandre Duret-Lutz authored
      On some architectures (e.g., ARM, or even some -flto setups on Intel)
      C++ exceptions to not traverse the C functions.  So even if the C++
      main() has a try/catch, it will not catch the exception thrown by C++
      code called from the argp module (which is compiled in C).
      
      * bin/common_setup.cc, bin/common_setup.hh: Define some macros
      and function to factorize exception handling.
      * bin/autcross.cc, bin/autfilt.cc, bin/common_aoutput.cc,
      bin/common_color.cc, bin/common_finput.cc, bin/common_hoaread.cc,
      bin/common_output.cc, bin/common_post.cc, bin/common_trans.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:
      Protect all parse_opt() functions, even those where there is currently
      no exception risk.
      d523ce8b
    • Alexandre Duret-Lutz's avatar
      bin: handle any exception before returning from parse_opt() · 6bdb1357
      Alexandre Duret-Lutz authored
      On some architectures (e.g., ARM, or even some -flto setups on Intel)
      C++ exceptions to not traverse the C functions.  So even if the C++
      main() has a try/catch, it will not catch the exception thrown by C++
      code called from the argp module (which is compiled in C).
      
      * bin/common_setup.cc, bin/common_setup.hh: Define some macros
      and function to factorize exception handling.
      * bin/autcross.cc, bin/autfilt.cc, bin/common_aoutput.cc,
      bin/common_color.cc, bin/common_finput.cc, bin/common_hoaread.cc,
      bin/common_output.cc, bin/common_post.cc, bin/common_trans.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:
      Protect all parse_opt() functions, even those where there is currently
      no exception risk.
      6bdb1357
  5. 17 Jul, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      forbid the use of std::endl on std::cerr · 09c93a3a
      Alexandre Duret-Lutz authored
      std::cerr will flush after each operator<< by default, so it's simpler
      to use \n instead of std::endl, especially if we can merge \n into the
      previous string.  Ideally we should prefer \n for std::cout as well,
      but there are reasonable cases where we want to call std::endl there,
      so it's hard to enforce.
      
      * tests/sanity/style.test: Diagnose occurrences of cerr.*<<.*endl.
      * bin/autcross.cc, bin/autfilt.cc, bin/ltlcross.cc, bin/ltlsynt.cc,
      spot/tl/formula.cc, spot/twa/bdddict.cc, tests/core/checkpsl.cc,
      tests/core/checkta.cc, tests/core/consterm.cc, tests/core/emptchk.cc,
      tests/core/equalsf.cc, tests/core/ikwiad.cc, tests/core/kind.cc,
      tests/core/length.cc, tests/core/ltlrel.cc, tests/core/parity.cc,
      tests/core/randtgba.cc, tests/core/reduc.cc, tests/core/syntimpl.cc,
      tests/ltsmin/modelcheck.cc: Fix them.
      09c93a3a
  6. 07 Apr, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      complement: add a complement() function · 948f99bc
      Alexandre Duret-Lutz authored
      * spot/twaalgos/complement.cc,
      spot/twaalgos/complement.hh (complement): New function.
      * bin/autfilt.cc, spot/twa/twa.cc, spot/twaalgos/contains.cc,
      spot/twaalgos/powerset.cc, spot/twaalgos/stutter.cc: Use it.
      * tests/core/complement.test: Adjust.
      * NEWS: Mention it.
      948f99bc
  7. 20 Mar, 2019 1 commit
  8. 02 Aug, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      contains: fix the semantics · 701a3b1c
      Alexandre Duret-Lutz authored
      spot::contains(a, b) should test a⊇b.  It was testing a⊆b instead.
      
      * NEWS: Mention the bug.
      * spot/twaalgos/contains.cc, spot/twaalgos/contains.hh: Fix the
      code and documentation.
      * tests/python/contains.ipynb: Adjust description and expected
      results.
      * python/spot/__init__.py: Also swap the argument of
      language_containment_checker.contains()
      * bin/autfilt.cc: Adjust usage.
      701a3b1c
  9. 01 Aug, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      contains: fix the semantics · 23722c03
      Alexandre Duret-Lutz authored
      spot::contains(a, b) should test a⊇b.  It was testing a⊆b instead.
      
      * NEWS: Mention the bug.
      * spot/twaalgos/contains.cc, spot/twaalgos/contains.hh: Fix the
      code and documentation.
      * tests/python/contains.ipynb: Adjust description and expected
      results.
      * python/spot/__init__.py: Also swap the argument of
      language_containment_checker.contains()
      * bin/autfilt.cc: Adjust usage.
      23722c03
  10. 05 Jun, 2018 1 commit
  11. 25 May, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      fix and check shifting issue · b12eb050
      Alexandre Duret-Lutz authored
      The exception raised by << and >> when shifting mark_t by too many
      bits are only enabled in SPOT_DEBUG, as those operations are quite
      low-level.  However we were always testing them, and although we
      wanted them to be active in Python, it was not always the case.
      
      * spot/twa/acc.hh: introduce max_accsets() as
      a static constexpr method, so we can see it in Python.
      * spot/misc/bitset.hh: Fix preprocessing directive
      so the check is actually enabled when compiling the Python
      bindings.
      * bin/autcross.cc, bin/autfilt.cc, bin/ltlcross.cc: Use max_accsets().
      * tests/core/acc.cc: Comment out the shifting exception when
      SPOT_DEBUG is unset.
      * tests/python/except.py: Make sure the exception is always raised in
      Python.
      b12eb050
  12. 24 May, 2018 2 commits
    • Alexandre Duret-Lutz's avatar
      rename SPOT_NB_ACC to SPOT_MAX_ACCSETS · 2e165f18
      Alexandre Duret-Lutz authored
      * NEWS, bin/autcross.cc, bin/autfilt.cc, bin/ltlcross.cc,
      configure.ac, spot/parseaut/parseaut.yy, spot/twa/acc.cc,
      spot/twa/acc.hh, tests/core/acc.cc, .gitlab-ci.yml: Here.
      2e165f18
    • 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
  13. 23 May, 2018 1 commit
  14. 21 May, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      bin: teach conversion options to report about the options · c369f899
      Alexandre Duret-Lutz authored
      * bin/common_conv.cc, bin/common_conv.hh: Here.
      * bin/autfilt.cc, bin/common_trans.cc, bin/ltlcross.cc, bin/ltldo.cc,
      bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randaut.cc, bin/randltl.cc: Pass
      the name of the argumennt to the conversion function.
      * tests/core/ltlcross3.test, tests/core/ltldo.test,
      tests/core/randaut.test: Add test cases.
      c369f899
  15. 18 May, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      autfilt: support --is-colored · 47974cd0
      Alexandre Duret-Lutz authored
      This also improve the coverage of the is_colored() function, because
      it was not used in negative cases so far.
      
      * bin/autfilt.cc: Implement it.
      * tests/core/satmin2.test: Test it.
      * NEWS: Mention it.
      47974cd0
  16. 16 May, 2018 2 commits
    • 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.
      645bb556
    • Alexandre Duret-Lutz's avatar
      autfilt: --complement accepts non-deterministic input · 4d827587
      Alexandre Duret-Lutz authored
      * bin/autfilt.cc: Fix the --help string for --complement, and also
      merge edges in the resulting automaton, as suggested by František
      Blahoudek.
      * tests/core/complement.test: Adjust output and add František's
      example.
      4d827587
  17. 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
  18. 18 Mar, 2018 2 commits
  19. 16 Mar, 2018 2 commits
  20. 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
      b09c293f
  21. 14 Mar, 2018 1 commit
    • Maximilien Colange's avatar
      Fix various typos · 6a3e8e95
      Maximilien Colange authored
      * 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
  22. 01 Mar, 2018 1 commit
    • Maximilien Colange's avatar
      Fix various typos · 5b2ce273
      Maximilien Colange authored
      * 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
      5b2ce273
  23. 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
  24. 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
  25. 04 Nov, 2017 1 commit
    • 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
  26. 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
  27. 19 Sep, 2017 3 commits
    • Alexandre GBAGUIDI AISSE's avatar
      misc/timer: Gather handling of %r and %R options · ad9bc644
      Alexandre GBAGUIDI AISSE authored
      * bin/autcross.cc: Update.
      * bin/autfilt.cc: Update.
      * bin/common_aoutput.cc: Gather them. Move process_timer struct.
      * bin/common_aoutput.hh: Gather them.
      * bin/common_output.hh: Update.
      * bin/dstar2tgba.cc: Update.
      * bin/ltl2tgba.cc: Update.
      * bin/ltlcross.cc: Update.
      * bin/ltldo.cc: Update.
      * bin/ltlfilt.cc: Update.
      * bin/randaut.cc: Update.
      * spot/misc/formater.hh: Remove an useless function.
      * spot/misc/timer.hh: Add process_timer struct definition.
      * spot/misc/timer.cc: Remove old dead code.
      * spot/twaalgos/stats.cc: Update.
      * spot/twaalgos/stats.hh: Update.
      ad9bc644
    • 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. 05 Sep, 2017 1 commit
    • Clément Gillard's avatar
      fix typos and indentation · ad358842
      Clément Gillard authored
      * bin/autfilt.cc, python/spot/__init__.py, spot/twa/twa.hh,
      spot/twa/twaproduct.cc, spot/twaalgos/couvreurnew.cc,
      tests/python/bugdet.py: Here.
      ad358842
  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. 26 Jul, 2017 2 commits
  31. 30 Jun, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      decompose: merge decompose_strength() and decompose_scc() · 09e47d64
      Alexandre Duret-Lutz authored
      These two functions were doing almost identical work, the only
      difference was the way to select the SCC to keep.  Now we have a more
      uniform way to do that.  Closes #172.
      
      * bin/autfilt.cc: Offer a unique --decompose-scc option, but keep
      --decompose-strength as an alias for backward compatibility.
      * spot/twaalgos/strength.cc, spot/twaalgos/strength.hh: Rename
      decompose_strength as decompose_scc, and handle a way to list
      all SCC numers in the string specifier.  This gets rid
      of the nearly identical
      * tests/core/scc.test, tests/core/strength.test,
      tests/python/decompose.ipynb, tests/python/decompose_scc.py: Adjust
      test cases.
      * NEWS: Adjust.
      09e47d64