1. 12 May, 2013 3 commits
  2. 11 May, 2013 1 commit
  3. 09 May, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      lbtt: improve the LBTT output · eed7e2df
      Alexandre Duret-Lutz authored
      Provide a way to output automata with state-based acceptance.  Also
      print the guards using to_lbt_string() for consistency: as a
      consequence, atomic proposition that do not match p[0-9]+ are now
      double-quoted.
      
      * src/tgbaalgos/lbtt.hh (lbtt_reachable): Add a sba option.
      * src/tgbaalgos/lbtt.cc: Implement it, and use to_lbt_string().
      * src/ltlvisit/lbt.cc (is_pnum): Reject 'p' without number.
      * src/bin/ltl2tgba.cc: Activate the sba option of --ba was given.
      Add an option --lbtt=t to get the old behavior.
      * src/bin/man/ltl2tgba.x: Document the LBTT format we use with
      some links and examples.
      * src/tgbatest/lbttparse.test: More tests.
      * src/tgbatest/ltlcross2.test: Add a check with --lbtt --ba.
      * NEWS: Update.
      eed7e2df
  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.
      e2378b49
  5. 28 Apr, 2013 2 commits
  6. 27 Apr, 2013 3 commits
    • Alexandre Duret-Lutz's avatar
      ltlcross: count SCCs of various strenghts · fec939c1
      Alexandre Duret-Lutz authored
      * src/bin/ltlcross.cc: Implement the counters.
      * doc/org/ltlcross.org: Update the documentation.
      * bench/ltl2tgba/sum.py: Do not assume a fixed column for the time.
      * NEWS: Update.
      fec939c1
    • Alexandre Duret-Lutz's avatar
      isweakscc: cleanup interfaces and code · cb7cd868
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/isweakscc.cc, src/tgbaalgos/isweakscc.hh: Do not pass
      automata since they are known from the scc.  Avoid several dynamic
      casts.  Try to match the established vocabulary wrt "weak" and
      "inherently weak".  The old is_weak_scc() that used to enumerate cycles
      is therefore renamed to is_inherently_weak_scc(), while the new
      is_weak_scc() will should ensure all transitions are fully accepting.
      * NEWS: Mention the new interface.
      cb7cd868
    • Alexandre Duret-Lutz's avatar
      * NEWS: Mention recent changes. · 9cd7500f
      Alexandre Duret-Lutz authored
      9cd7500f
  7. 15 Apr, 2013 1 commit
  8. 09 Apr, 2013 4 commits
  9. 06 Mar, 2013 2 commits
  10. 05 Mar, 2013 2 commits
  11. 23 Jan, 2013 2 commits
  12. 21 Jan, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      ltlcross: diagnose missing i/o specifications earlier. · 6a547371
      Alexandre Duret-Lutz authored
      * src/misc/formater.cc, src/misc/formater.hh (scan): New method.
      (prime): Use it.
      * src/bin/ltlcross.cc (translator_runner::translator_runner): Scan each
      specification string, and report those missing an input or output
      %-sequence.
      * NEWS: Mention it.
      6a547371
  13. 20 Jan, 2013 4 commits
  14. 18 Jan, 2013 1 commit
  15. 14 Jan, 2013 1 commit
  16. 11 Jan, 2013 1 commit
  17. 06 Jan, 2013 1 commit
  18. 28 Nov, 2012 1 commit
  19. 27 Oct, 2012 2 commits
  20. 26 Oct, 2012 1 commit
  21. 21 Oct, 2012 2 commits
    • Alexandre Duret-Lutz's avatar
      rename ltlcheck as ltlcross · f3ef9de0
      Alexandre Duret-Lutz authored
      * src/bin/ltlcheck.cc, src/bin/man/ltlcheck.x,
      src/tgbatest/ltlcheck.test, src/tgbatest/ltlcheck2.test: Rename as ...
      * src/bin/ltlcross.cc, src/bin/man/ltlcross.x,
      src/tgbatest/ltlcross.test, src/tgbatest/ltlcross2.test: ... these.
      * NEWS, src/bin/Makefile.am, src/bin/man/Makefile.am,
      src/tgbatest/Makefile.am: Adjust.
      f3ef9de0
    • Alexandre Duret-Lutz's avatar
      postproc: add the possibility to output a monitor · 76787b23
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/stripacc.cc, src/tgbaalgos/stripacc.hh: New files.
      * src/tgbaalgos/Makefile.am: Add them.
      * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Add a Monitor
      output option.
      * src/bin/ltl2tgba.cc: Add a --monitor/-M option.
      * NEWS: Mention monitors.
      * src/tgba/tgbaexplicit.hh (is_accepting_state): Fix for the
      case where the automaton has no acceptance set.
      76787b23
  22. 20 Oct, 2012 1 commit
  23. 17 Oct, 2012 1 commit
  24. 15 Oct, 2012 1 commit