1. 11 Nov, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      twa: do not set prop_state_acc in set_acceptance · dd706d78
      Alexandre Duret-Lutz authored
      Reported by Juraj Major.
      
      * spot/twa/twa.hh: check num_sets() in prop_state_acc() so we do not
      have to set it in set_acceptance(), causing trouble if set_acceptance()
      is called multiple times.
      * tests/python/setacc.py: New test case.
      * tests/Makefile.am: Add it.
      * THANKS: Add Juraj.
      * NEWS: Mention the bug.
      dd706d78
  2. 01 Nov, 2016 1 commit
  3. 11 Jul, 2016 1 commit
  4. 07 Jul, 2016 1 commit
  5. 07 Mar, 2016 1 commit
    • Amaury Fauchille's avatar
      autfilt: add new option --accept-word · 1c824443
      Amaury Fauchille authored
      Suggested by Matthias Heizmann. Fixes #109.
      
      * NEWS: notify the new option
      * THANKS: add Matthias Heizmann
      * bin/autfilt.cc: add new option --accept-word=WORD which filters
      automata that accept WORD
      * doc/org/autfilt.org: add an example of the new option
      * tests/Makefile.am: add core/acc_word.test to the list of test files
      * tests/core/acc_word.test: test some uses of the new option
      1c824443
  6. 03 Feb, 2016 1 commit
  7. 20 Oct, 2015 1 commit
  8. 26 Aug, 2015 1 commit
  9. 23 Aug, 2015 1 commit
  10. 30 Jun, 2015 1 commit
  11. 05 Feb, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      nra2nba: Fix initial state construction. · 78e63d03
      Alexandre Duret-Lutz authored
      This bug caused tgbatest/ltl2dstar.test to fail but because I had
      no ltl2dstar on my computer for a while, I only discovered it after
      David Müller and Joachim Klein reported a bug against ltlcross.
      It might be the case that their bug is different (I can't reproduce it
      using their format), but I hope it was caused by this as well.
      
      * src/dstarparse/nra2nba.cc: Revert 57cda2d9, with a comment.
      * THANKS: Add David.
      78e63d03
  12. 19 Aug, 2014 1 commit
  13. 04 Feb, 2014 1 commit
  14. 29 Jul, 2013 2 commits
    • Alexandre Duret-Lutz's avatar
      ce6114f4
    • Alexandre Duret-Lutz's avatar
      Fix interpretation of {e[*]} and !{e[*]}. · cb7bdf8c
      Alexandre Duret-Lutz authored
      This follows from a discussion with Ernesto Posse.
      
      The semantics for the {...} operator we use in Spot comes from the
      cl(...) operator defined by Dax et al. (ATVA'09).  This is slightly
      different from the the way the PSL spec interprets a SERE used in the
      context of a temporal formula (appendix B.3.1.1.2, item 7).
      
      cl({a;b}[*]) would match any infinite word that starts with a;b, while
      in PSL {a;b}[*] would match any infinite word that alternates a and b.
      
      Spot documents that {SERE} in a temporal formula is interpreted like
      cl(SERE) however it failed to ignore the empty prefix of SERE.  So
      {{a;b}[*]} would match anything, because the empty word is a prefix of
      any word, and is also accepted by {a;b}[*].  Some trivial identities
      and basic rewritings were also wrongly considering these empty
      prefixes as well.
      
      This patch therefore fixes the translation and syntactic
      simplification rules, to really ignore these empty prefixes.
      
      In some future version it should probably be wise to rename this {...}
      operator as cl(...), and use {...} for the semantics given in appendix
      B.3.1.1.2 (item 7) of the PSL specs.
      
      * src/ltlast/unop.cc: Fix trivial identities.  We have
      {[*0]} = 0 and !{[*0]} = 1.
      * src/ltlvisit/simplify.cc: Fix basic rewriting rules.
      {e[*]} = {e} and !{e[*]} = !{e}.
      * doc/tl/tl.tex: Adjust documentation.
      * doc/tl/tl.bib (dax.09.atva): New entry.
      * src/tgbaalgos/ltl2tgba_fm.cc: Do not accept any
      infinite word for {e[*]} just because the empty
      prefix is matched by e[*].
      * src/tgbatest/ltl2tgba.test: Add a test case.
      * NEWS: Mention it.
      * THANKS: Add Ernesto.
      cb7bdf8c
  15. 09 Jul, 2013 1 commit
  16. 30 Apr, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix genltl --gh-r · e2378b49
      Alexandre Duret-Lutz authored
      Reported by František Blahoudek.
      
      * src/bin/genltl.cc (R_n): Really generate (GFp1 || FGp2), not
      (GFp1 || GFp2).
      * NEWS: Mention the bug.
      * THANKS: Update.
      e2378b49
  17. 20 Feb, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      Improve some Doxygen comments. · 543de077
      Alexandre Duret-Lutz authored
      This follows up on a mail from Sonali Dutta.
      
      * src/tgba/bdddict.hh (assert_emptiness, ~bdd_dict): Better
      documentation.
      * src/tgba/formula2bdd.hh (formula_to_bdd): Mention
      unregister_all_my_variables().
      (bdd_to_formula): Complete the documentation.
      * THANKS: Add Sonali Dutta.
      543de077
  18. 10 May, 2012 1 commit
  19. 07 May, 2012 1 commit
  20. 24 Nov, 2011 1 commit
  21. 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
  22. 26 Oct, 2011 1 commit
  23. 23 Oct, 2011 1 commit
    • 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
  24. 17 Aug, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix a nondeterministic behavior of the degeneralization algorithm. · 03aabf9a
      Alexandre Duret-Lutz authored
      Reported by Tomáš Babiak <xbabiak@fi.muni.cz>.
      
      * src/tgba/tgbatba.cc (tgba_tba_proxy): Replace the std::map used
      to record outgoing transitions by an Sgi::hash_map, and keep the
      order of these transitions in a separate list.
      * src/tgbatest/degendet.test: New file.
      * src/tgbatest/Makefile.am (TESTS): Add it.
      * THANKS: Add Tomáš and convert to utf8.
      03aabf9a
  25. 21 Mar, 2011 1 commit
  26. 07 Oct, 2010 1 commit
    • Alexandre Duret-Lutz's avatar
      Hide the safra_tree_automaton type from the public interface. · 1fa1621a
      Alexandre Duret-Lutz authored
      We do that because the declaration of this type, which is local to
      src/tgba/tgbasafracomplement.cc has a member in an anonymous
      namespace, and some versions of g++-4.2 issue a very annoying
      warning about this legitimate code.  See Bug 29365 on GCC's
      Bugzilla.  Report by Silien Hong <silien.hong@lip6.fr>.
      
      * src/tgba/tgbasafracomplement.hh (safra_tree_automaton): Do not
      forward declare.
      (tgba_safra_complement): Use void* instead of
      safra_tree_automaton*.
      * src/tgba/tgbasafracomplement.cc: static_cast void* to
      safra_tree_automaton* anywhere needed.
      1fa1621a
  27. 03 Mar, 2010 1 commit
    • Alexandre Duret-Lutz's avatar
      ltl2tgba: apply -R3 before -D or -DS. · efb15a91
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (main): Call scc_filter() before the
      degeneralization, because it might remove useless acceptance
      conditions.  I realized this while looking at experiments from
      Rüdiger Ehlers.
      efb15a91
  28. 09 Nov, 2009 1 commit
  29. 09 Jul, 2004 1 commit
  30. 29 Dec, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/ltltest/defs.in (run): New function, run valgrind. · 6f88e518
      Alexandre Duret-Lutz authored
      * src/ltltest/equals.test, src/ltltest/lunabbrev.test,
      src/ltltest/nenoform.test, src/ltltest/parse.test,
      src/ltltest/parseerr.test, src/ltltest/tostring.test,
      src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test: Use run().
      * Makefile.am (EXTRA_DIST): Don't list the m4/*.m4 files,
      Automake 1.8 find them automatically.
      * configure.ac: Require Automake 1.8, in gnits mode, and check
      for valgrind.
      * THANKS: New empty file.
      6f88e518