1. 01 Oct, 2013 3 commits
  2. 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.
  3. 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.
  4. 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.
  5. 27 Sep, 2013 2 commits
  6. 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.
    • 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.
    • 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.
  7. 23 Sep, 2013 1 commit
  8. 22 Sep, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      tools: Add a --format option · ce5ea829
      Alexandre Duret-Lutz authored
      * src/bin/common_output.cc: Add option --format and implement
      * src/bin/ltlfilt.cc, src/bin/randltl.cc: Document the
      supported %-sequences.
      * src/bin/genltl.cc: Document the %-sequences, and supply
      the name of the pattern to output_formula().
      * doc/org/genltl.org, doc/org/ioltl.org, doc/org/ltlfilt.org,
      NEWS: Document it.
      * src/ltltest/latex.test: Use it.
  9. 18 Sep, 2013 1 commit
  10. 16 Sep, 2013 14 commits
  11. 08 Sep, 2013 7 commits
    • Alexandre Duret-Lutz's avatar
      sat: implement partial symmetry breaking · e9f60df8
      Alexandre Duret-Lutz authored
      Thanks to Rüdiger Ehlers for his helpful email.
      * src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Here.
    • Alexandre Duret-Lutz's avatar
      tostring: add LaTeX output · 9cfe1a34
      Alexandre Duret-Lutz authored
      * src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh
      (to_latex_string): New function.
      * src/bin/common_output.cc, src/bin/common_output.hh:
      Add a --latex option.
      * doc/tl/spotltl.sty: New file.
      * doc/tl/Makefile.am: Distribute it.
      * src/ltltest/latex.test: New test.
      * src/ltltest/Makefile.am: Add it.
      * NEWS: Mention it.
    • Alexandre Duret-Lutz's avatar
      sat: generalize the code for reading the solution · 90c106f8
      Alexandre Duret-Lutz authored
      * src/misc/satsolver.cc, src/misc/satsolver.hh (satsolver_get_solution):
      New function, that accepts a solution split on multiple 'v ' lines.
      * src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc (get_solution):
      Remove, and adjust existing code to use satsolver_get_solution().
      * src/tgbatest/readsat.cc, src/tgbatest/readsat.test: New files.
      * src/tgbatest/Makefile.am: Add them.
      * src/bin/man/spot-x.x: Mention the SAT competition rules for
      the expected input/output format.
    • Alexandre Duret-Lutz's avatar
      postproc: Add option to output Complete automata. · 1ab46b08
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Tweak set_pref()
      to also accept Any|Complete, Small|Complete, or Deterministic|Complete.
      * src/bin/common_post.hh, src/bin/common_post.cc: Add option --complete
      and set comp.
      * src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc: Pass
      comp to set_pref().
      * src/tgbaalgos/complete.cc: Preserve state-based acceptance.
      * src/tgbatest/dstar.test, src/tgbatest/ltlcross2.test,
      src/tgbatest/nondet.test: Augment tests.
      * doc/org/dstar2tgba.org, doc/org/ltl2tgba.org, NEWS: Document.
    • Alexandre Duret-Lutz's avatar
      * NEWS: Summarize recent changes · b31facff
      Alexandre Duret-Lutz authored
    • 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.
    • Alexandre Duret-Lutz's avatar
      satmin: cleanup interfaces and minimization loops · fdb157bf
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtbasat.hh:
      (dtba_sat_minimize): Split into...
      (dtba_sat_synthetize, dtba_sat_minimize): These.
      (dtba_sat_minimize_dichotomy): New function.
      * src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dtgbasat.hh
      (dtgba_sat_minimize, dtgba_sat_synthetize): Likewise.
      * src/tgbatest/ltl2tgba.cc: Adjust to new interface.
      * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh:
      Cleanup option processing for SAT options.
      * src/tgbatest/satmin.test: Adjust.
      * src/bin/spot-x.cc, src/bin/man/spot-x.x, NEWS: Document.