1. 06 Dec, 2013 1 commit
  2. 22 Nov, 2013 6 commits
    • Alexandre Duret-Lutz's avatar
      ltlcross: report statistics about Rabin and Streett automata · d719c706
      Alexandre Duret-Lutz authored
      * src/bin/ltlcross.cc: Implement it.
      * src/bin/man/ltlcross.x, doc/org/ltlcross.org, NEWS: Document it.
      * src/tgbatest/ltl2dstar.test, src/tgbatest/ltlcross3.test: Test it.
      d719c706
    • Alexandre Duret-Lutz's avatar
      ltlcross: support --products=+N · 2b10745d
      Alexandre Duret-Lutz authored
      * src/bin/ltlcross.cc: Implement it.
      * NEWS, doc/org/ltlcross.org: Document it.
      * src/tgbatest/ltlcross3.test: Test it.
      2b10745d
    • Alexandre Duret-Lutz's avatar
      ltlcross: report exit_status and exit_code columns in CSV and JSON · f65c621a
      Alexandre Duret-Lutz authored
      * src/bin/ltlcross.cc: Report exit_status and exit_code columns in CSV
      and JSON files.  Also output lines for failed translations, and add
      a --omit-missing option to disable that.  Move the time column right
      after exit_status and exit_code.
      * src/bin/man/ltlcross.x: Document each column of the output.
      * bench/ltl2tgba/tools: Use the "{name}cmd" notation.
      * bench/ltl2tgba/sum.py: Adjust to the new columns.
      * bench/ltl2tgba/README: Update to point to the man page for a
      description of the columns.
      * bench/ltl2tgba/Makefile.am: Build results.pdf as said announced in
      README.
      * bench/spin13/html.bottom: Update code to ignore these two new
      columns and lines with null values.
      * src/tgbatest/ltlcross3.test: Add tests.
      * doc/org/ltlcross.org: Adjust examples.
      * NEWS: Mention this.
      f65c621a
    • Alexandre Duret-Lutz's avatar
      ltlcross: report missing input/output sequence · 686a4548
      Alexandre Duret-Lutz authored
      * src/bin/ltlcross.cc: Fix it.
      * src/tgbatest/ltlcross3.test: New file.
      * src/tgbatest/Makefile.am: Add it.
      * NEWS: Mention it.
      686a4548
    • Alexandre Duret-Lutz's avatar
      ltlcross: support short names · 7de25a32
      Alexandre Duret-Lutz authored
      * NEWS: Mention it.
      * doc/org/ltlcross.org: Document it.
      * src/bin/ltlcross.cc: Implement it.
      * src/tgbatest/Makefile.am, src/tgbatest/defs.in,
      src/tgbatest/ltlcross4.test: Test it.
      7de25a32
    • Alexandre Duret-Lutz's avatar
      ltlcross: follow RFC 4180 for CSV output. · 1c5536ea
      Alexandre Duret-Lutz authored
      * src/misc/escape.cc, src/misc/escape.hh (escape_rfc4180): New
      function.
      * src/bin/ltlcross.cc: Do not output space after ',', use
      "\r\n" for end of line, and use escape_rfc4180().
      * NEWS: Mention it.
      1c5536ea
  3. 08 Sep, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      rename dba_complement() to dtgba_complement() · 7a7ed8a6
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/dbacomp.cc, src/tgbaalgos/dbacomp.hh
      (dba_complement): Rename to...
      * src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/dtgbacomp.hh
      (dtgba_complement): ... this.
      * src/tgbaalgos/minimize.cc, src/tgbaalgos/powerset.cc,
      src/tgbatest/ltl2tgba.cc, src/bin/ltlcross.cc,
      src/tgbaalgos/Makefile.am: Adjust to name change.
      7a7ed8a6
  4. 26 Aug, 2013 3 commits
  5. 23 Aug, 2013 1 commit
  6. 29 Jul, 2013 3 commits
  7. 25 Jul, 2013 1 commit
  8. 20 Jul, 2013 1 commit
  9. 09 Jul, 2013 1 commit
  10. 17 May, 2013 1 commit
  11. 12 May, 2013 2 commits
  12. 27 Apr, 2013 1 commit
  13. 15 Apr, 2013 1 commit
  14. 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
  15. 20 Jan, 2013 1 commit
  16. 16 Jan, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix several warnings reported by clang++ 3.2. · aa7b43ea
      Alexandre Duret-Lutz authored
      * src/tgba/tgbakvcomplement.cc
      (tgba_kv_complement_succ_iterator::current_state_),
      src/ta/taexplicit.hh (state_ta_explicit::source_):
      Remove useless private member.
      * src/ta/taexplicit.cc: Adjust constructors.
      * src/ta/tgta.cc, src/ta/taexplicit.hh: Also fix
      copyright banner.
      * src/bin/ltlcross.cc (exec_with_timeout): Work
      around warning about status not being set in the
      error path.
      aa7b43ea
  17. 24 Dec, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Address several issues reported by cppcheck all over the place. · a577850e
      Alexandre Duret-Lutz authored
      * src/bin/common_finput.cc, src/tgbaalgos/lbtt.cc: Use !empty() instead
      of size() > 0.
      * src/bin/ltl2tgta.cc, src/kripke/kripkeexplicit.cc,
      src/tgbatest/complementation.cc: Avoid useless assignments.
      * src/bin/ltlcross.cc: Correct mistaken assignment inside assert().
      * src/evtgba/symbol.hh, src/tgba/tgbabddcoredata.cc,
      src/tgba/tgbabddcoredata.hh,
      src/tgba/tgbasafracomplement.cc (operator=): Do not return a const
      reference.
      * src/evtgbatest/ltl2evtgba.cc, src/evtgbatest/product.cc,
      src/evtgbatest/product.cc: Check indices before using them, not after.
      * src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
      src/tgbatest/randtgba.cc: Pass constant strings by reference.
      * src/kripke/kripkeprint.cc, src/tgbaalgos/simulation.cc:
      Remove a useless operation.
      * src/ltlvisit/simplify.cc: Remove a duplicate condition.
      * src/misc/formater.hh: Remove unused attribute.
      * src/misc/modgray.cc: Initialize done_ in the constructor.
      * src/saba/explicitstateconjunction.cc,
      src/saba/explicitstateconjunction.hh (operator=): Fix prototype.
      * src/saba/sabacomplementtgba.cc: Remove unused default constructor.
      * src/ta/taexplicit.cc, src/ta/taproduct.cc, src/ta/tgtaproduct.cc,
      src/ta/tgtaproduct.hh, src/taalgos/emptinessta.cc,
      src/taalgos/minimize.cc, src/taalgos/reachiter.cc,
      src/taalgos/tgba2ta.cc, src/tgbaalgos/cutscc.cc: Use C++ casts, and
      ++it instead of it++.
      * src/taalgos/dotty.cc, src/tgbatest/ltl2tgba.cc: Refine the scope of
      variables.
      * src/tgba/tgbakvcomplement.hh (bdd_order): Always initialize bdd_.
      * src/tgba/tgbasgba.cc, src/tgba/wdbacomp.cc: Use the initialization
      line to initialize all members.
      a577850e
  18. 14 Nov, 2012 1 commit
  19. 23 Oct, 2012 1 commit
  20. 21 Oct, 2012 1 commit
    • 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
  21. 20 Oct, 2012 1 commit
  22. 19 Oct, 2012 2 commits
    • Alexandre Duret-Lutz's avatar
      bin: Adjust version display and help options. · b8ed85a3
      Alexandre Duret-Lutz authored
      In particular, this get rid of the ugly -? option that argp adds by
      default, and we also remove -V so that we can use it for something
      else later.
      
      * src/bin/common_setup.cc, src/bin/common_setup.hh (misc_argp):
      Provide support for --help/--version/--usage output, replacing argp's
      default builting version.
      * src/bin/genltl.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc,
      src/bin/ltlcheck.cc, src/bin/ltlfilt.cc, src/bin/randltl.cc:
      Call argp_parse() with ARGP_NO_HELP, and use misc_argp instead.
      b8ed85a3
    • Alexandre Duret-Lutz's avatar
  23. 15 Oct, 2012 4 commits
  24. 14 Oct, 2012 3 commits