1. 05 Mar, 2011 1 commit
  2. 04 Mar, 2011 2 commits
  3. 01 Mar, 2011 1 commit
  4. 27 Feb, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      [buddy] · 8f5ecc14
      Alexandre Duret-Lutz authored
      * examples/cmilner/Makefile.am (cmilner_LDADD): Link with -lm, to
      find the pow() function.
      8f5ecc14
  5. 21 Feb, 2011 2 commits
  6. 14 Feb, 2011 1 commit
  7. 13 Feb, 2011 1 commit
  8. 10 Feb, 2011 3 commits
  9. 09 Feb, 2011 2 commits
  10. 08 Feb, 2011 3 commits
  11. 07 Feb, 2011 5 commits
  12. 06 Feb, 2011 3 commits
  13. 05 Feb, 2011 1 commit
  14. 04 Feb, 2011 3 commits
  15. 03 Feb, 2011 3 commits
    • Alexandre Duret-Lutz's avatar
      Read guard of the form !(x) in neverclaims. · 91e51c4c
      Alexandre Duret-Lutz authored
      So far all neverclaims encountered would use (!(x)), but the
      files from the Büchi store do not.
      
      * src/neverparse/neverclaimscan.ll: Accept ! in front of guard,
      so that we can read Promela files from Goal's Büchi store.
      * src/tgbatest/neverclaimread.test: Test it.
      91e51c4c
    • Alexandre Duret-Lutz's avatar
      Recognize Goal's syntax for Boolean operators. · 3278844c
      Alexandre Duret-Lutz authored
      * src/ltlparse/ltlscan.ll: Recognize ~, -->, and <--> operators
      from Goal, to ease the use of formulas provided by the Goal team.
      * src/ltltest/equals.test: Use these once, just to be on the
      safe side.
      3278844c
    • Alexandre Duret-Lutz's avatar
      Minor fixes to ltl2tgba.html. · 2fe5b3fb
      Alexandre Duret-Lutz authored
      * wrap/python/ajax/css/ltl2tgba.css,
      wrap/python/ajax/ltl2tgba.html: Tweak a few things for Firefox
      3.0, and fix a </li> tag.
      2fe5b3fb
  16. 01 Feb, 2011 3 commits
  17. 28 Jan, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Fixup minimize_monitor(). · ad93f875
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/minimize.cc (minimize_monitor): Fix typo yielding
      incorrect monitor if the input tgba is not deterministic.
      * src/tgbatest/ltl2tgba.test: Add test case.
      ad93f875
  18. 27 Jan, 2011 4 commits
    • Alexandre Duret-Lutz's avatar
      more files to ignore · dd0f01fe
      Alexandre Duret-Lutz authored
      dd0f01fe
    • Alexandre Duret-Lutz's avatar
      Report formulas that are both safety and guarantee. · c8140de9
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (-O): Report formulas that are both
      safety and guarantee.
      * src/tgbatest/obligation.test: Add cases.
      c8140de9
    • Alexandre Duret-Lutz's avatar
      Rename is_safety_automaton() as is_guarantee_automaton() and · db124d02
      Alexandre Duret-Lutz authored
      implement is_safety_mwdba().
      
      Note: I swapped the name of safety and guarantee when I
      implemented is_safety_automaton() on 2010-03-20.  Fortunately,
      is_safety_automaton() was only used where is_guarantee_automaton()
      would have been correct.
      
      * src/tgbaalgos/safety.cc (is_guarantee_automaton): Rename as ...
      (is_guarantee_automaton): ... this.
      (is_safety_mwdba): New function.
      * src/tgbaalgos/safety.hh: Adjust and add documentation.
      * src/tgbaalgos/minimize.cc: Use is_guarantee_automaton() instead
      of is_safety_automaton().
      * src/tgbatests/safety.test: Rename as ...
      * src/tgbatests/obligation.test: ... this, and augment the
      test.
      * src/tgbatest/Makefile.am: Adjust.
      * src/tgbatest/ltl2tgba.cc (-O): Display whether a formula
      represent a safety, guarantee, or obligation property.
      * NEWS: Adjust.
      db124d02
    • Alexandre Duret-Lutz's avatar
      * NEWS: Minor rewritings. · 14b701b5
      Alexandre Duret-Lutz authored
      14b701b5