1. 16 Dec, 2013 1 commit
  2. 11 Dec, 2013 2 commits
  3. 06 Dec, 2013 5 commits
    • Alexandre Duret-Lutz's avatar
      bin: support multi-line CSV fields. · f0bcab4a
      Alexandre Duret-Lutz authored
      * src/bin/common_finput.cc (job_processor::process_stream): Read
      multi-line CSV fields.
      * src/ltltest/lbt.test, src/tgbatest/nondet.test: Add tests.
    • Alexandre Duret-Lutz's avatar
      ltlcross: end CSV lines with \n, not \r\n · 6c210895
      Alexandre Duret-Lutz authored
      * src/bin/ltlcross.cc (print_stats_csv): Revert the recent
      addition of \r, it is caussing too many issues.
      * NEWS: Mention it.
    • Alexandre Duret-Lutz's avatar
      ltl2tgba: Add a --csv-escape option and document CSV I/O. · 846e33b9
      Alexandre Duret-Lutz authored
      * src/bin/common_output.cc, src/bin/common_output.hh:
      (output_formula_checked, aut_stat_printer): New.
      * src/bin/genltl.cc, src/bin/randltl.cc, src/bin/ltlfilt.cc: Call
      output_formula_checked() instead of output_formula().
      * src/bin/ltl2tgba.cc: Use aut_stat_printer and add option --csv-escape.
      * doc/org/csv.org: New file to document CSV I/O.
      * doc/Makefile.am: Add it.
      * doc/org/ioltl.org, doc/org/ltlfilt.org, doc/org/ltl2tgba.org,
      doc/org/tools.org: Link to csv.org
    • Alexandre Duret-Lutz's avatar
      bin: add support for reading formulas from CSV files. · 0faea814
      Alexandre Duret-Lutz authored
      * NEWS: Mention it.
      * src/bin/common_finput.cc, src/bin/common_finput.hh: Implement it.
      * src/bin/common_output.cc, src/bin/common_output.hh: Add the %< and
      %> escapes.
      * src/bin/ltlfilt.cc: Connect %< and %> to the
      prefix andsuffix of the input, and document them.
      * src/tgbatest/det.test, src/tgbatest/nondet.test: Simplify these
      tests that read CSV files.
    • Alexandre Duret-Lutz's avatar
      * doc/org/satmin.org: Typo · 8c587531
      Alexandre Duret-Lutz authored
  4. 28 Nov, 2013 1 commit
  5. 22 Nov, 2013 10 commits
  6. 11 Nov, 2013 1 commit
  7. 22 Oct, 2013 2 commits
  8. 17 Oct, 2013 1 commit
  9. 11 Oct, 2013 1 commit
  10. 01 Oct, 2013 4 commits
  11. 30 Sep, 2013 4 commits
    • Alexandre Duret-Lutz's avatar
      Fix uninitialized variables in spot::postprocessor. · f3b87c85
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/postproc.cc: Initialize option
      variables when opt is not given.
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      Add support for Bison 3.0. · 3c943d83
      Alexandre Duret-Lutz authored
      We still want to remain compatible with Bison 2.7 so instead of fixing
      all the new errors reported by 3.0 we silence some warning.  We should
      fix these for good once Bison 3.0 is more widespread.
      * m4/bison.m4: New file. Test if bison support -Wno-empty-rule and
      -Wno-deprecated.  Define BISON and BISON_EXTRA_FLAGS.
      * configure.ac: Do not test for yacc, use the above test instead.
      * src/dstarparse/Makefile.am, src/eltlparse/Makefile.am,
      src/kripkeparse/Makefile.am, src/ltlparse/Makefile.am,
      src/neverparse/Makefile.am, src/tgbaparse/Makefile.am: Use BISON
      * src/ltlparse/ltlparse.yy: Fix or and remove useless %right/%nonassoc
      * src/eltlparse/eltlparse.yy: Likewise, and remove "%pure-parser".
    • Alexandre Duret-Lutz's avatar
      Work around some configurations of latexmk. · 56638720
      Alexandre Duret-Lutz authored
      * src/ltltest/latex.test: Use latexmk -pvc- like in doc/tl/Makefile.am.
      Reported by Étienne Renault.
  12. 29 Sep, 2013 2 commits
    • Alexandre Duret-Lutz's avatar
      Generalize implication-based simplifications for multops. · df109869
      Alexandre Duret-Lutz authored
      And also speedup implication checks for Boolean expressions.
      * src/ltlvisit/simplify.cc: Improve implication-based rules
      rules for multops by checking one operand against all the
      other at once (instead of one by one).  Do not break
      Boolean expressions while performing implication checks.
      * src/ltlvisit/simplify.hh: Typo.
      * src/ltltest/reduccmp.test: More tests.
    • Alexandre Duret-Lutz's avatar
      Sort comutative binops like we sort multops. · c01909e3
      Alexandre Duret-Lutz authored
      * src/ltlast/formula.hh (is_literal): Rename as...
      (get_literal): ... this.
      (is_literal): New method.
      (formula_ptr_less_than_multop): Rename as...
      (formula_ptr_less_than_bool_first): ... this.
      * src/ltlast/binop.cc: Use formula_ptr_less_than_bool_first.
      * src/ltlast/multop.cc, src/ltlast/formula.cc: Adjust
      to renamings.
  13. 28 Sep, 2013 2 commits
    • Alexandre Duret-Lutz's avatar
      Include lib/ and config.h in ltlast/. · 228121c9
      Alexandre Duret-Lutz authored
      * src/ltlast/Makefile.am: Include lib/ in search path.
      * src/ltlast/atomic_prop.cc, src/ltlast/automatop.cc,
      src/ltlast/binop.cc, src/ltlast/bunop.cc,
      src/ltlast/constant.cc, src/ltlast/formula_tree.cc,
      src/ltlast/multop.cc, src/ltlast/nfa.cc,
      src/ltlast/refformula.cc, src/ltlast/unop.cc: Include
    • Alexandre Duret-Lutz's avatar
      relabel: implement relabeling of Boolean subexpressions. · 87b65b9b
      Alexandre Duret-Lutz authored
      * src/ltlast/multop.cc, src/ltlast/multop.hh (multop::boolean_operands,
      multop::boolean_count): New methods.
      * src/ltlvisit/relabel.cc, src/ltlvisit/relabel.hh
      (relabel): Take an optional relabeling_map as parameter.
      (relabel_bse): New.
      * src/ltltest/ltlrel.test, src/ltltest/ltlrel.cc: New files.
      * src/ltltest/Makefile.am: Add them.
      * src/bin/ltlfilt.cc: Add option --relabel-bool.
      * src/ltltest/ltlfilt.test: Test it.
      * NEWS: Mention it.
      * doc/org/ltlfilt.org: Illustrate it.
  14. 27 Sep, 2013 2 commits
  15. 26 Sep, 2013 2 commits
    • Alexandre Duret-Lutz's avatar
      Arrange multops so that Boolean arguments come first. · 536e45b3
      Alexandre Duret-Lutz authored
      This helps recursive implication checks.  Also order
      atomic propositions with strverscmp().
      * src/ltlast/formula.hh (formula_ptr_less_than_multop,
      is_literal, atomic_prop_cmp): New.
      * src/ltlast/formula.cc (is_literal, atomic_prop_cmp): Implement them.
      * src/ltlast/multop.cc: Use formula_ptr_less_than_multop.
      * src/ltltest/isop.test, src/ltltest/ltlfilt.test,
      src/tgbatest/det.test, src/tgbatest/dstar.test,
      src/tgbatest/explicit.test, src/tgbatest/explpro2.test,
      src/tgbatest/explpro3.test, src/tgbatest/explprod.test,
      src/tgbatest/nondet.test, src/tgbatest/tripprod.test: Adjust tests.
      * NEWS: Mention the new order.
    • Alexandre Duret-Lutz's avatar
      gnulib: Add module strverscmp. · 1f384c2c
      Alexandre Duret-Lutz authored
      * lib/strverscmp.c, m4/strverscmp.m4: New files.
      * lib/Makefile.am, m4/gnulib-cache.m4, m4/gnulib-comp.m4: Update.