1. 11 Dec, 2013 2 commits
  2. 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.
      f0bcab4a
    • 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.
      6c210895
    • 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
      846e33b9
    • 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.
      0faea814
    • Alexandre Duret-Lutz's avatar
      * doc/org/satmin.org: Typo · 8c587531
      Alexandre Duret-Lutz authored
      8c587531
  3. 28 Nov, 2013 1 commit
  4. 22 Nov, 2013 10 commits
  5. 11 Nov, 2013 1 commit
  6. 22 Oct, 2013 2 commits
  7. 17 Oct, 2013 1 commit
  8. 11 Oct, 2013 1 commit
  9. 01 Oct, 2013 4 commits
  10. 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.
      f3b87c85
    • 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
      and BISON_EXTRA_FLAGS.
      * src/ltlparse/ltlparse.yy: Fix or and remove useless %right/%nonassoc
      settings.
      * src/eltlparse/eltlparse.yy: Likewise, and remove "%pure-parser".
      3c943d83
    • 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.
      56638720
  11. 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.
      df109869
    • 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.
      c01909e3
  12. 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
      config.h.
      228121c9
    • 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.
      87b65b9b
  13. 27 Sep, 2013 2 commits
  14. 26 Sep, 2013 3 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.
      536e45b3
    • 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.
      1f384c2c
    • Alexandre Duret-Lutz's avatar
      Fix compilation with g++-4.4.7. · b486d4f1
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/reducerun.cc: Remove
      superfluous definition of state_set.  Reported by František Blahoudek.
      b486d4f1