1. 12 Jan, 2012 1 commit
  2. 06 Jan, 2012 1 commit
  3. 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.
      0ca40d72
    • 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.
      984c715c
  4. 18 Dec, 2011 4 commits
  5. 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
      requested.
      * 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.
      e531da8d
    • 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,
      AC_HEADER_TR1_UNORDERED_MAP, and AC_HEADER_EXT_HASH_MAP.
      * src/misc/hash.hh: Include _config.h, and used the
      SPOT_HAVE_UNORDERED_MAP, SPOT_HAVE_TR1_UNORDERED_MAP,
      or SPOT_HAVE_EXT_HASH_MAP defines to decide which
      file to include.
      96790325
  6. 01 Dec, 2011 1 commit
  7. 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.
      1e7cda5e
  8. 28 Nov, 2011 11 commits
  9. 27 Nov, 2011 1 commit
  10. 24 Nov, 2011 3 commits
    • Thomas Badie's avatar
      Add text I/O for Kripke structures. · bb5949f6
      Thomas Badie authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
      src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh: New files.
      * src/kripke/Makefile.am: Add them.
      * src/kripkeparse/fmterror.cc, src/kripkeparse/kripkeparse.yy,
      src/kripkeparse/kripkescan.ll, src/kripkeparse/parsedecl.hh,
      src/kripkeparse/public.hh, src/kripkeparse/scankripke.ll: New
      files.
      * src/kripkeparse/Makefile.am: Add them.
      * src/kripketest/bad_parsing.test, src/kripketest/defs.in,
      src/kripketest/kripke.test, src/kripketest/origin,
      src/kripketest/parse_print_test.cc: New files.
      * src/kripketest/Makefile.am: Add them.
      * src/Makefile.am (SUBDIRS): Add kripkeparse and kripketest.
      * README: Document src/kripketest/ and src/kripkeparse/.
      * configure.ac: Generate src/kripkeparse/Makefile,
      src/kripketest/Makefile, src/kripketest/defs.
      * iface/dve2/defs.in (run2): New function.
      * iface/dve2/dve2check.cc (syntax, main): Add option -gK.
      * iface/dve2/kripke.test: New file.
      * iface/dve2/Makefile.am (TESTS): Add kripke.test.
      bb5949f6
    • Alexandre Duret-Lutz's avatar
      Fix bench/emptchk/pml2tgba.pl for more recent Spin version. · 71d1a4fe
      Alexandre Duret-Lutz authored
      * bench/emptchk/pml2tgba.pl: Stop checking for version start lines
      depending on the Spin version.  This check was never always
      correct.  Reported by Étienne Renault.
      71d1a4fe
    • Alexandre Duret-Lutz's avatar
      Update formulae.ltl not to use uncommon operators. · fdf8878d
      Alexandre Duret-Lutz authored
      * bench/emptchk/formulae.ltl: Do not use + and * in the list of
      formulas.  Use | and & instead.  The * operator was removed on
      2010-01-30.  Reported by Étienne Renault.
      fdf8878d
  11. 23 Nov, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      More documentation. · fd98345c
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/randomgraph.hh: Document the fact that adding
      acceptance conditions to the graph may generate graphs that do not
      have any accepting cycle.
      fd98345c
  12. 17 Nov, 2011 2 commits
  13. 16 Nov, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Fully quote guards used by neverclaims. · ea6a1ffc
      Alexandre Duret-Lutz authored
      Especially with should write !(p0) and not !p0, because p0 is
      usually #define'd by the user and he may have forgotten to quote
      the value of the macro.  This issue was discovered by Kristin
      Yvonne Rozier and diagnosed by Gerard Holzmann.
      
      * src/tgbaalgos/neverclaim.cc (process_link): Call
      to_spin_string(..., true) to fully parentheses the string.
      * src/tgbatest/neverclaimread.test: Add a test.
      ea6a1ffc
  14. 11 Nov, 2011 1 commit
  15. 08 Nov, 2011 1 commit
  16. 26 Oct, 2011 1 commit
  17. 24 Oct, 2011 2 commits
  18. 23 Oct, 2011 3 commits
    • Alexandre Duret-Lutz's avatar
      Safra: Fix usage of multiple acceptance conditions and fix text output. · a4d1e18b
      Alexandre Duret-Lutz authored
      * src/tgba/tgbasafracomplement.cc
      (tgba_safra_complement::tgba_safra_complement)
      (tgba_safra_complement::succ_iter): Correct the declaration and
      use of multiple acceptance conditions.
      (state_complement::to_string): Output the L set, not U.  The previous
      code caused different states to share the same names, causing issues
      with the text-based output (state with identical names get merged).
      * src/tgba/tgbasafracomplement.hh
      (tgba_safra_complement::acceptance_cond_vec_): Adjust type to
      store BDDs.
      * src/tgbatest/complementation.cc: Implement a new "-b" option
      to output automata in Spot's syntax.
      * src/tgbatest/complementation.test: Add a test-case supplied
      by Martin Dieguez Lodeiro.
      * THANKS: Add Martin.
      a4d1e18b
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      Improve the print_safra_automaton output. · 73d9f65d
      Alexandre Duret-Lutz authored
      * src/tgba/tgbasafracomplement.cc (print_safra_tree): Fix output in
      case of hash collision.  Use the actual states to get a number, not
      their hash value.
      (print_safra_automaton): Output a mapping of values to states names.
      (safra_tree_automaton::get_sba): New method, used by
      print_safra_automaton.
      73d9f65d
  19. 28 Aug, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix errors reported by clang++-2.9. · 101b18b2
      Alexandre Duret-Lutz authored
      * src/evtgbaalgos/tgba2evtgba.cc (process_link): Fix prototype
      to match tgba_reachable_iterator::process_link.
      * src/ltlvisit/tunabbrev.hh: Add using super::visit, so that the
      other visit() method are in scope when we overload one.
      * src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc (start, end,
      process_link): Remove these empty methods.  The default
      implementations are empty too, and process_link had the
      wrong prototype.
      * src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc
      (start, end, process_link): Likewise.
      101b18b2