1. 04 Feb, 2014 1 commit
  2. 29 Jul, 2013 2 commits
    • Alexandre Duret-Lutz's avatar
    • 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., 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. (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.
  3. 09 Jul, 2013 1 commit
  4. 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.
  5. 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
      * src/tgba/formula2bdd.hh (formula_to_bdd): Mention
      (bdd_to_formula): Complete the documentation.
      * THANKS: Add Sonali Dutta.
  6. 10 May, 2012 1 commit
  7. 07 May, 2012 1 commit
  8. 24 Nov, 2011 1 commit
  9. 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.
  10. 26 Oct, 2011 1 commit
  11. 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::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.
  12. 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.
  13. 21 Mar, 2011 1 commit
  14. 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
      * src/tgba/tgbasafracomplement.cc: static_cast void* to
      safra_tree_automaton* anywhere needed.
  15. 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.
  16. 09 Nov, 2009 1 commit
  17. 09 Jul, 2004 1 commit
  18. 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.