1. 27 Sep, 2013 2 commits
  2. 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
  3. 23 Sep, 2013 1 commit
  4. 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
      it.
      * 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.
      ce5ea829
  5. 18 Sep, 2013 1 commit
  6. 16 Sep, 2013 14 commits
  7. 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.
      e9f60df8
    • 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.
      9cfe1a34
    • 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.
      90c106f8
    • 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.
      1ab46b08
    • Alexandre Duret-Lutz's avatar
      * NEWS: Summarize recent changes · b31facff
      Alexandre Duret-Lutz authored
      b31facff
    • 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
    • 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.
      fdb157bf
  8. 26 Aug, 2013 11 commits
    • Alexandre Duret-Lutz's avatar
      postproc: disable WDBA-minimization on request · b09ef5be
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh:
      Implement the wdba-minimize option.
      * src/bin/spot-x.cc (wdba-minimize): Document.
      * src/bin/man/spot-x.x: Update references.
      b09ef5be
    • Alexandre Duret-Lutz's avatar
      stats: add %r to display run-time · bfbe5b44
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh: Add
      support for printing run-time.
      * src/bin/ltl2tgba.cc, src/bin/dstar2tgba.cc: Compute
      the run-time and show the option.
      * NEWS: Mention it.
      bfbe5b44
    • Alexandre Duret-Lutz's avatar
      isdet: simplify is_deterministic(), add is_complete(). · 4dd8d802
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/isdet.cc: Simplify determinism check.
      * src/tgbaalgos/isdet.hh, src/tgbaalgos/isdet.cc (is_complete): New
      function.
      * src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh, src/bin/dstar2tgba.cc
      src/bin/ltl2tgba.cc: Add escape sequence %p to the possible statistics
      to show whether an automaton is complete.
      * src/tgbatest/nondet.test: Add a couple more tests.
      4dd8d802
    • Alexandre Duret-Lutz's avatar
      sat: improve our algorithms · bcd794c6
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtbasat.hh:
      Rename dba_sat_minimize to dtba_sat_minimize.
      Make it possible to produce state-based automata, and do
      not output useless clauses.
      * src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dtgbasat.hh:
      likewise, but also add the possibility to set the
      target number of states, as in dtba_sat_minimize.
      * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh:
      Add new options for state-based computations and
      setting acceptance and states number when using
      dtgba_sat_minimize().
      * src/tgbatest/ltl2tgba.cc: Adjust calls to
      dtba_sat_minimize().
      * src/tgbatest/satmin.test: Adjust calls.
      bcd794c6
    • Alexandre Duret-Lutz's avatar
      ltlcross: Complement deterministic automata. · 1029d08a
      Alexandre Duret-Lutz authored
      * src/bin/ltlcross.cc: Complement deterministic automata,
      and use them for additional intersection checks.
      * NEWS, doc/org/ltlcross.org, src/bin/man/ltlcross.x: Document it.
      1029d08a
    • Alexandre Duret-Lutz's avatar
      minimize_obligation: can complement the input TGBA if deterministic · 2dda2c91
      Alexandre Duret-Lutz authored
      This makes dstar2tgba able to produce a minimal WDBA when the input DRA
      represent an obligation property.
      
      * src/tgbaalgos/minimize.cc (minimize_obligation): When the
      formula is not supplied but the input automaton is deterministic,
      complement it to check the result of WDBA minimization.
      * src/tgbatest/ltl2dstar.test, src/tgbatest/ltl2dstar2.test: Improve
      tests.
      2dda2c91
    • Alexandre Duret-Lutz's avatar
      satsolver: new function · 3b10bb3b
      Alexandre Duret-Lutz authored
      Uses the value of the SPOT_SATSOLVER environment variable
      to decide how to call the SAT solver.
      
      * src/misc/satsolver.cc, src/misc/satsolver.hh: New files.
      * src/misc/Makefile.am: Add them.
      * src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Use satsolver().
      3b10bb3b
    • Alexandre Duret-Lutz's avatar
      * .gitignore: More files to ignore. · 6ce005b2
      Alexandre Duret-Lutz authored
      6ce005b2
    • Alexandre Duret-Lutz's avatar
      Implement dtgba_sat_minimize(). · 679df4ee
      Alexandre Duret-Lutz authored
      Joint work with Soheib Baarir.
      
      * src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dtgbasat.hh: New files.
      * src/tgbaalgos/Makefile.am: Add them.
      * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Add
      a dtgba-sat-minimize option.
      * src/tgbatest/ltl2tgba.cc: Add option -RG.
      * src/tgbatest/satmin.test: Add more tests.
      679df4ee
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      Add some test of the SAT-based minimization. · 84dabae3
      Alexandre Duret-Lutz authored
      * src/tgbatest/satmin.test: New file.
      * src/tgbatest/Makefile.am: Add it.
      84dabae3