1. 18 Mar, 2015 7 commits
  2. 17 Mar, 2015 3 commits
    • Alexandre Duret-Lutz's avatar
      sat: add missing prop_state_based_acc() call · 72eed9b2
      Alexandre Duret-Lutz authored
      Fixes #62.
      
      * src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Add call to
      prop_state_based_acc() when building an automaton with state-based
      acceptance.
      * src/tgbatest/satmin2.test: New test.
      * doc/org/satmin.org: Update.
      72eed9b2
    • Alexandre Duret-Lutz's avatar
      man: fix section number of spot-x.7 · 6712fa3c
      Alexandre Duret-Lutz authored
      * src/bin/man/Makefile.am: Make sure the header of spot-x.7 refers to
      section 7, not 1.  This error was caught by lintian on the Debian
      packages.
      6712fa3c
    • Alexandre Duret-Lutz's avatar
      dotty: colored acceptance sets · 838bfb2a
      Alexandre Duret-Lutz authored
      This implement several new options for --dot in order to
      allow emptiness sets to be output as colored ⓿ or ❶...
      Also add a SPOT_DOTDEFAULT environment variable.
      
      * NEWS, src/bin/man/spot-x.x, src/bin/common_aoutput.cc,
      src/bin/dstar2tgba.cc: Document the new options.
      * doc/org/.dir-locals.el, doc/org/init.el.in: Setup
      SPOT_DOTEXTRA and SPOT_DOTDEFAULT for all documents.
      * doc/org/autfilt.org, doc/org/dstar2tgba.org, doc/org/ltl2tgba.org,
      doc/org/ltldo.org, doc/org/oaut.org, doc/org/randaut.org,
      doc/org/satmin.org: Adjust to this new setup.
      * src/misc/escape.cc, src/misc/escape.hh (escape_html): New function.
      * src/tgba/acc.cc, src/tgba/acc.hh (to_text, to_html): New method.
      * src/tgbaalgos/dotty.cc: Implement the new options.
      * src/tgbatest/readsave.test, wrap/python/tests/automata.ipynb: More
      tests.
      * wrap/python/spot.py: Make sure the default argument for
      dotty_reachable is None, so that SPOT_DOTDEFAULT is honored.
      838bfb2a
  3. 16 Mar, 2015 3 commits
  4. 15 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      python: some bindings for translating formulas and diplaying automata · 3c38780d
      Alexandre Duret-Lutz authored
      * wrap/python/spot.py: Introduce spot.translate (and
      spot.formula.translate) as well, as a wrapper around the
      spot.translator class.  Also implement spot.tgba.show()
      to allow passing argument to dotty_reachable() before
      the result is converted to SVG.
      * wrap/python/tests/automata.ipynb: New test file.
      * wrap/python/tests/Makefile.am: Add it.
      3c38780d
  5. 13 Mar, 2015 1 commit
  6. 11 Mar, 2015 5 commits
  7. 10 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      [buddy] fix undefined behavior · 787e3f93
      Alexandre Duret-Lutz authored
      The bug was found while running Spot's src/tgbatest/randpsl.test
      on Debian i386 with gcc-4.9.2.  The following call would crash:
      
      ./ltl2tgba -R3 -t '(!(F(({{{(p0) |
      {[*0]}}:{{{(p1)}[*2]}[:*]}[*]:[*2]}[:*0..3]}[]-> (G(F(p1)))) &
      (G((!(p1)) | ((!(p2)) W (G(!(p0)))))))))'
      
      On amd64 the call does not crash, but valgrind nonetheless
      report that uninitialized memory is being read by bdd_gbc()
      during the second garbage collect.
      
      * src/kernel.h (PUSHREF): Define as a function rather than a macro
      to avoid undefined behavior.  See comments for details.
      787e3f93
  8. 09 Mar, 2015 1 commit
  9. 08 Mar, 2015 4 commits
    • Alexandre Duret-Lutz's avatar
      debian: build a python3 package · 5adec919
      Alexandre Duret-Lutz authored
      * debian/python3-spot.install: New file.
      * Makefile.am: Ship it.
      * debian/control, debian/rules, debian/spot.install: Adjust.
      5adec919
    • Alexandre Duret-Lutz's avatar
      randltl: some code cleanup · 4ffb0cb9
      Alexandre Duret-Lutz authored
      * src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh: Throw
      invalid_argument exceptions consistently (not std::string), and use
      forwarding constructors to avoid the construct() method.
      * src/bin/randltl.cc: Catch the above exceptions.  Destroy
      the opts variable right after its use, so that we don't need
      explicit destructor calls.
      * src/ltltest/rand.test: Add a test.
      4ffb0cb9
    • Alexandre Duret-Lutz's avatar
    • Thibaud Michaud's avatar
      Adding python functions to mirror the functionalities found in src/bin · 3bf3d2c8
      Thibaud Michaud authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * wrap/python/spot.i: Rename to...
      * wrap/python/spot_impl.i: ...this, and import spot_impl from spot.py so
      that it is not needed to recompile everything when modifying python
      code.
      * wrap/python/spot.py: Adding python functions to mirror the
      functionalities found in src/bin.
      * src/bin/common_r.cc: Move simplification level...
      * src/ltlvisit/simplify.hh: ... here as a constructor of
      ltl_simplifier_options, to make it available in wrap/python.
      * src/bin/ltlfilt.cc: Set simplification level using the new
      ltl_simplifier_options constructor.
      * src/bin/randltl.cc: Move most of the code...
      * src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh: ... here, as a
      class named randltlgenerator.
      * wrap/python/tests/bddnqueen.py, wrap/python/tests/minato.py: Avoid
      calling bdd_init twice by moving 'import spot' after bdd initialization.
      * wrap/python/Makefile.am: Rename spot to spot_impl
      * wrap/python/tests/Makefile.am: Add ipnbdoctest.py.
      * wrap/python/.gitignore: Rename spot.py to spot_impl.py
      * src/ltlvisit/tostring.cc: \ttrue and \ffalse should be \top and \bot.
      * wrap/python/tests/ipnbdoctest.py: Run code cells of a python notebook
      and compare the output to the actual content of the notebook.
      * wrap/python/tests/randltl.ipynb: Document and test randltl.
      * wrap/python/tests/run.in: Call ipnbdoctest.py to run ipython
      notebooks.
      3bf3d2c8
  10. 05 Mar, 2015 3 commits
    • Alexandre Duret-Lutz's avatar
      org: fix -o example · cb9867b7
      Alexandre Duret-Lutz authored
      * doc/org/oaut.org: Adjust the parameters of randaut so that we get a
      mix of deterministic and nondeterministic automata.
      cb9867b7
    • Alexandre Duret-Lutz's avatar
      acc: add a to_cnf() function · a0ac8dc5
      Alexandre Duret-Lutz authored
      * src/tgba/acc.cc, src/tgba/acc.hh (to_cnf, is_cnf): New functions.
      * src/bin/autfilt.cc: Add a --cnf-acceptance option.
      * src/tgbatest/acc2.test: Test it.
      a0ac8dc5
    • Alexandre Duret-Lutz's avatar
      acc: fix is_dnf() · b71e6add
      Alexandre Duret-Lutz authored
      A Fin() terms with multiple sets should not appear under an And.
      
      * src/tgba/acc.cc (is_dnf): Fix it.
      * src/tgbatest/acc.cc, src/tgbatest/acc.test: Augment test case.
      b71e6add
  11. 04 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      acc: implement to_dnf() using BDDs · 518de8d5
      Alexandre Duret-Lutz authored
      This way we have for instance
        (Inf(1) | Fin(2)) & (Fin(1) | Inf(3)) & Inf(0)
      converted into just
        (Fin(1) & Fin(2) & Inf(0)) | (Inf(0)&Inf(1)&Inf(3))
      while previously we would produce 4 terms:
        (Fin(2) & Fin(1) & Inf(0)) | (Fin(2) & (Inf(0)&Inf(3)))
        | (Fin(1) & (Inf(0)&Inf(1))) | (Inf(0)&Inf(1)&Inf(3))
      
      * src/tgba/acc.cc (to_dnf): Recode it.
      * src/tgbatest/acc2.test: Adjust.
      518de8d5
  12. 03 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      sccinfo: introduce is_rejecting() · ebe4ffc5
      Alexandre Duret-Lutz authored
      Because scc_info does not perform a full emptiness check, it is not
      always able to tell whether an SCC is accepting if the acceptance
      condition use Fin primitives.  This introduce is_rejecting_scc() in
      addition to to is_accepting_scc().  Only one of them may be true, but
      they can both be false if scc_info has no idea whether the SCC is
      accepting.
      
      * src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh: Implement
      is_rejecting_scc().
      * src/bin/ltlcross.cc, src/tgba/acc.cc, src/tgba/acc.hh,
      src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/isweakscc.cc,
      src/tgbaalgos/remfin.cc, src/tgbaalgos/safety.cc,
      src/tgbaalgos/sccfilter.cc: Use it.
      * src/tgbaalgos/dotty.cc: Use is_rejecting_scc() and is_accepting_scc()
      to color SCCs.
      * doc/org/oaut.org: Document the colors used.
      * src/tgbatest/neverclaimread.test, src/tgbatest/readsave.test: Adjust
      tests.
      * src/tgbatest/sccdot.test: New test case.
      * src/tgbatest/Makefile.am: Add it.
      ebe4ffc5
  13. 02 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      bin: use enums instead of #define for option codes · 86584418
      Alexandre Duret-Lutz authored
      * src/bin/autfilt.cc, src/bin/common_aoutput.cc,
      src/bin/common_finput.cc, src/bin/common_output.cc,
      src/bin/common_post.cc, src/bin/common_setup.cc,
      src/bin/common_trans.cc, src/bin/dstar2tgba.cc, src/bin/genltl.cc,
      src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc, src/bin/ltlcross.cc,
      src/bin/ltlfilt.cc, src/bin/ltlgrind.cc, src/bin/randaut.cc,
      src/bin/randltl.cc: Here.
      86584418
  14. 01 Mar, 2015 3 commits
  15. 28 Feb, 2015 5 commits