1. 07 Jan, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      org: typo · 365fde83
      Alexandre Duret-Lutz authored
      * doc/org/concepts.org: Typo reported by Paul Guénézan.
      * THANKS: Add him.
      365fde83
  2. 10 Nov, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix Alpine Linux builds · 6cfdf02c
      Alexandre Duret-Lutz authored
      Reported by Maxime Bouton.
      
      * spot/misc/tmpfile.cc: Include stdlib.h, not cstdlib, so
      that our replacement secure_getenv() is found.
      * THANKS: Add Maxime.
      6cfdf02c
  3. 26 Sep, 2018 2 commits
  4. 25 Sep, 2018 1 commit
  5. 11 Aug, 2018 1 commit
  6. 09 Apr, 2018 2 commits
  7. 23 Mar, 2018 2 commits
  8. 15 Oct, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      ltlcross, autcross, ltldo: support --fail-on-timeout · 183ec1fb
      Alexandre Duret-Lutz authored
      Suggested by Tobias Meggendorfer.  Fixes #294.
      
      * bin/autcross.cc, bin/ltlcross.cc, bin/ltldo.cc: Add the option.
      * tests/core/autcross3.test, tests/core/ltlcross3.test,
      tests/core/ltldo.test: Test it.
      * tests/Makefile.am: Add autcross3.test.
      * NEWS, doc/org/autcross.org, doc/org/ltlcross.org, doc/org/ltldo.org:
      Mention the option.
      * THANKS: Add Tobias.
      183ec1fb
  9. 29 Sep, 2017 1 commit
  10. 26 Sep, 2017 1 commit
  11. 02 Sep, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      simplify: some new simplification rules · 646c5170
      Alexandre Duret-Lutz authored
      For #263, reported by Mikuláš Klokočka.
      
      G(a & Xe1 & F(b & e2)) = G(a & e1 & Fb & e2)
      F(a | Xu1 | G(b | u2)) = F(a | u1 | Gb | u2)
      
      * spot/tl/simplify.cc: Implement the rules.
      * doc/tl/tl.tex, NEWS: Document them.
      * tests/core/reduccmp.test, tests/core/eventuniv.test: Add test cases.
      * tests/core/det.test, tests/core/ltl2tgba2.test: Adjust to expect
      smaller automata.
      * THANKS: Add Mikuláš.
      646c5170
  12. 28 Feb, 2017 2 commits
  13. 14 Jan, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      debian: distribute static libraries · 7574d6d1
      Alexandre Duret-Lutz authored
      Suggested by Jeroen Meijer.
      
      * debian/rules: Enable static libraries.
      * debian/libbddx-dev.install, debian/libspot-dev.install: Distribute
      them.
      * THANKS: Add Jeroen.
      * NEWS: Mention the change.
      7574d6d1
  14. 10 Dec, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      ltlf: ensure alive holds initially · 15709084
      Alexandre Duret-Lutz authored
      Reported by Shufang Zhu.
      
      * spot/tl/ltlf.cc, spot/tl/ltlf.hh: Fix the transltion
      and update the comments.
      * tests/core/ltlfilt.test: Adjust test cases.
      * NEWS: Mention the fix.
      * THANKS: Add Shufang Zhu.
      15709084
  15. 09 Dec, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      ltlf: ensure alive holds initially · 413eab1d
      Alexandre Duret-Lutz authored
      Reported by Shufang Zhu.
      
      * spot/tl/ltlf.cc, spot/tl/ltlf.hh: Fix the transltion
      and update the comments.
      * tests/core/ltlfilt.test: Adjust test cases.
      * NEWS: Mention the fix.
      * THANKS: Add Shufang Zhu.
      413eab1d
  16. 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
  17. 01 Nov, 2016 1 commit
  18. 11 Jul, 2016 1 commit
  19. 07 Jul, 2016 1 commit
  20. 07 Mar, 2016 1 commit
    • Amaury Fauchille's avatar
      autfilt: add new option --accept-word · 1c824443
      Amaury Fauchille authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      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
  21. 03 Feb, 2016 1 commit
  22. 20 Oct, 2015 1 commit
  23. 26 Aug, 2015 1 commit
  24. 23 Aug, 2015 1 commit
  25. 30 Jun, 2015 1 commit
  26. 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
  27. 19 Aug, 2014 1 commit
  28. 04 Feb, 2014 1 commit
  29. 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
  30. 09 Jul, 2013 1 commit
  31. 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
  32. 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
  33. 10 May, 2012 1 commit
  34. 07 May, 2012 1 commit
  35. 24 Nov, 2011 1 commit