1. 04 Mar, 2012 1 commit
  2. 25 Feb, 2012 4 commits
    • Alexandre Duret-Lutz's avatar
      * NEWS: Summarize recent changes. · 503a57ca
      Alexandre Duret-Lutz authored
    • Alexandre Duret-Lutz's avatar
      Make all python code compatible with Python 2.x and Python 3.x. · 61127a3f
      Alexandre Duret-Lutz authored
      * wrap/python/buddy.i (__le__, __lt__, __eq__, __ne__, __ge__
      __gt__): New operators for bdd.
      * wrap/python/spot.i (__le__, __lt__, __eq__, __ne__, __ge__
      __gt__, __hash__): New operators for formula.
      (nl_cout, nl_cerr): New functions.
      * wrap/python/tests/bddnqueen.py,
      wrap/python/tests/interdep.py, wrap/python/tests/ltl2tgba.py,
      wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py,
      wrap/python/tests/minato.py, wrap/python/tests/modgray.py: Adjust
      to the new print syntax by using sys.output.write() or nl_cout()
      * wrap/python/tests/optionmap.py: Remove all print calls.
      * wrap/python/ajax/spot.in: Massive adjustments in order to work
      with both Python 2 and 3.  In python 3, reopening stdout as
      unbuffered requires it to be open as binary, which in turns
      requires any string output to be encoded manually.  BaseHTTPServer
      and CGIHTTPServer have been merged into http.server, so we have
      to try two different import syntaxes.  execfile no longer exists,
      so it has to be emulated.
      This also fixes two bugs where the script would segfault on
      empty input, or when calling Tau03 on automata with less then
      one acceptance conditions.
    • Alexandre Duret-Lutz's avatar
      Fix computation of PYTHONINC for Python 3. · 5e77b249
      Alexandre Duret-Lutz authored
      * m4/pypath.m4: The print syntax changed in Python 3, so use
      sys.stdout.write for compatibility with all versions.
    • Alexandre Duret-Lutz's avatar
  3. 15 Feb, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix a race condition on the CGI script. · 62914059
      Alexandre Duret-Lutz authored
      * wrap/python/ajax/spot.in: Create all cache files in a temporary
      directory, and only rename this directory at the end.  This way if
      two processes are processing the same request, they won't attempt
      to populate the same directory (and only one of the first of two
      renames will succeed, but that is OK).
  4. 24 Jan, 2012 1 commit
  5. 20 Jan, 2012 1 commit
  6. 19 Jan, 2012 2 commits
  7. 18 Jan, 2012 6 commits
  8. 17 Jan, 2012 4 commits
  9. 13 Jan, 2012 2 commits
  10. 12 Jan, 2012 1 commit
  11. 06 Jan, 2012 1 commit
  12. 05 Jan, 2012 2 commits
    • Ala-Eddine Ben-Salem's avatar
      Fix detection of the last iteration of minimize_dfa(). · 0ca40d72
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/tgbaalgos/minimize.cc (minimize_dfa): Fix detection of the
      last iteration.  An extra iteration case could be missed in case
      where a split generates only singletons, and yet predecessor
      classes need to be refined.
    • Alexandre Duret-Lutz's avatar
      Fix computation of length of LTL formulas. · 984c715c
      Alexandre Duret-Lutz authored
      * src/ltlvisit/length.cc: Fix computation for ltl::multop
      operator. "a&b&c" was reported with length 3, ignoring the
      "&" operators, because of a typo.
      * src/ltlvisit/length.hh: Fix description to correctly
      reflect this change intended since 2010-01-22.
      * src/ltltest/length.test, src/ltltest/length.cc: New files.
      * src/ltltest/Makefile.am: Add them.
  13. 18 Dec, 2011 4 commits
  14. 16 Dec, 2011 2 commits
    • Alexandre Duret-Lutz's avatar
      Perform WDBA minimization before degeneralization. · e531da8d
      Alexandre Duret-Lutz authored
      There is no point in degeneralizing an automaton if it can be WDBA
      minimized.  Doing so will only augment the number of states and
      slow down the powerset construction used by the WDBA minimization.
      * src/tgbatest/babiak.test: New file.  It includes 5 formulae
      which Tomáš Babiak reported Spot 0.7.1 would take over one hour to
      translate if degeneralization and WDBA minimization were both
      * src/tgbatest/Makefile.am (TESTS): Add it.
      * src/tgbatest/ltl2tgba.cc: Do WDBA minimization before
      degeneralization.  The above formulae are now all translated in a
      few seconds.
    • Alexandre Duret-Lutz's avatar
      Don't rely on the g++ version to include tr1/unordered_map and co. · 96790325
      Alexandre Duret-Lutz authored
      The previous setup failed with clang++ 3.0.
      * m4/stl.m4: New file.
      * configure.ac: Call AC_HEADER_UNORDERED_MAP,
      * src/misc/hash.hh: Include _config.h, and used the
      or SPOT_HAVE_EXT_HASH_MAP defines to decide which
      file to include.
  15. 01 Dec, 2011 1 commit
  16. 29 Nov, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix build on MacOS X. · 1e7cda5e
      Alexandre Duret-Lutz authored
      * src/kripketest/Makefile.am (LDADD): Remove a broken dependency.
      Reported by Yann Thierry-Mieg.
      * src/sanity/style.test: Make sure it does not appear again.
  17. 28 Nov, 2011 6 commits