1. 05 Mar, 2011 3 commits
    • Alexandre Duret-Lutz's avatar
      Setup build system for a new dve2 interface. · 3427f3bf
      Alexandre Duret-Lutz authored
      * iface/dve2/dve2.cc, iface/dve2/dve2.hh: New dummy files.
      * iface/dve2/Makefile.am: New file.
      * iface/Makefile.am (SUBDIRS): Add dve2.
      * configure.ac: Build iface/dve2/Makefile.
      * README: Mention the new directory.
      3427f3bf
    • Alexandre Duret-Lutz's avatar
      Using double borders for acceptance states in SBAs. · e1ef47d9
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/dotty.hh (dotty_reachable): Take a new
      assume_sba argument.
      * src/tgbaalgos/dotty.cc (dotty_bfs): Take a new
      mark_accepting_states arguments.
      (dotty_bfs::process_state): Check if a state is accepting using
      the state_is_accepting() method for tgba_sba_proxies, or by
      looking at the first outgoing transition of the state.  Pass
      the result to the dectorator.
      (dotty_reachable): Adjust function.
      * src/tgbaalgos/dottydec.hh, src/tgbaalgos/dottydec.cc,
      src/tgbaalgos/rundotdec.hh, src/tgbaalgos/rundotdec.cc
      (state_decl): Add an "accepting" argument, and use it to
      decorate accepting states with a double border.
      * src/tgbatest/ltl2tgba.cc: Keep track of whether the output
      is an SBA or not, so that we can tell it to dotty().
      * wrap/python/ajax/spot.in: Likewise.
      * wrap/python/cgi-bin/ltl2tgba.in: Likewise.
      e1ef47d9
    • Alexandre Duret-Lutz's avatar
      2c5bae3d
  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 2 commits