1. 27 Mar, 2014 1 commit
  2. 20 Mar, 2014 1 commit
  3. 12 Feb, 2014 4 commits
    • Alexandre Duret-Lutz's avatar
      Replace << "c" by << 'c', and check for it in style.sh · ba5aff24
      Alexandre Duret-Lutz authored
      * src/sanity/style.test: Add a test.
      * iface/dve2/dve2.cc, iface/dve2/dve2check.cc, src/bin/common_output.cc,
      src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc, src/bin/ltlcross.cc,
      src/dstarparse/dra2ba.cc, src/dstarparse/fmterror.cc,
      src/dstarparse/nsa2tgba.cc, src/kripke/kripkeprint.cc,
      src/kripkeparse/fmterror.cc, src/ltlast/atomic_prop.cc,
      src/ltlast/bunop.cc, src/ltltest/ltlrel.cc, src/ltltest/reduc.cc,
      src/ltltest/syntimpl.cc, src/ltlvisit/dotty.cc, src/ltlvisit/lbt.cc,
      src/ltlvisit/randomltl.cc, src/ltlvisit/relabel.cc,
      src/ltlvisit/simplify.cc, src/ltlvisit/tostring.cc, src/misc/bitvect.cc,
      src/misc/optionmap.cc, src/misc/timer.cc, src/neverparse/fmterror.cc,
      src/priv/freelist.cc, src/saba/sabacomplementtgba.cc,
      src/sabaalgos/sabadotty.cc, src/taalgos/dotty.cc,
      src/taalgos/minimize.cc, src/tgba/bdddict.cc, src/tgba/bddprint.cc,
      src/tgba/futurecondcol.cc, src/tgba/taatgba.hh,
      src/tgba/tgbakvcomplement.cc, src/tgba/tgbasafracomplement.cc,
      src/tgbaalgo...
      ba5aff24
    • Alexandre Duret-Lutz's avatar
      c++11: introduce tgba::succ(s) to replace tgba::succ_iter(s). · 487cd01d
      Alexandre Duret-Lutz authored
      | tgba_succ_iterator* i = aut->succ_iter(s);
      | for (i->begin(); !i->done(); i->next())
      |   {
      |      // ...
      |   }
      | delete i;
      
      becomes
      
      | for (auto i: aut->succ(s))
      |   {
      |      // ...
      |   }
      
      hiding the begin()/done()/next() interface, taking care of the delete,
      and allowing more optimization to come.
      
      * src/tgba/succiter.hh, src/tgba/tgba.hh: Implement the above
      new interface.
      * iface/gspn/ssp.cc, src/dstarparse/nsa2tgba.cc,
      src/saba/sabacomplementtgba.cc, src/tgba/tgbakvcomplement.cc,
      src/tgba/tgbamask.cc, src/tgba/tgbasafracomplement.cc,
      src/tgba/tgbatba.cc, src/tgbaalgos/compsusp.cc, src/tgbaalgos/cutscc.cc,
      src/tgbaalgos/degen.cc, src/tgbaalgos/emptiness.cc,
      src/tgbaalgos/isdet.cc, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/powerset.cc,
      src/tgbaalgos/safety.cc, src/tgbaalgos/simulation.cc,
      src/tgbaalgos/tau03.cc, src/tgbatest/explicit2.cc: Update for
      loops.
      487cd01d
    • Alexandre Duret-Lutz's avatar
      bitvect: add a is_subset_of method. · 9a097bb0
      Alexandre Duret-Lutz authored
      * src/misc/bitvect.hh: New method.
      * src/tgbatest/bitvect.cc, src/tgbatest/bitvect.test: Test it.
      9a097bb0
    • Alexandre Duret-Lutz's avatar
      c++11: get rid of spot::unique_ptr · 67b9e8d8
      Alexandre Duret-Lutz authored
      But do not replace it by std::unique_ptr, because this was not
      really equivalent.
      
      * src/misc/unique_ptr.hh: Delete.
      * src/misc/Makefile.am: Adjust.
      * src/tgbaalgos/simulation.cc, src/tgbatest/ltl2tgba.cc: Call
      delete explicitly.
      67b9e8d8
  4. 08 Feb, 2014 1 commit
  5. 07 Feb, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      sat: factor the creation of temporary files · 9c98975c
      Alexandre Duret-Lutz authored
      * src/misc/satsolver.hh, src/misc/satsolver.cc: Present
      the SAT solver as an object with a stream interface, to
      prepare for a better implementation.
      * src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc:
      Adjust to the new interface, removing all the handling
      of temporary files.
      * src/tgbatest/readsat.cc: Adjust.
      9c98975c
  6. 06 Feb, 2014 1 commit
  7. 24 Jan, 2014 1 commit
  8. 06 Dec, 2013 2 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
      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
  9. 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
      tests: add some missing "set -e" · cf91a237
      Alexandre Duret-Lutz authored
      * src/ltltest/lbt.test, src/ltltest/utf8.test,
      src/tgbatest/dbacomp.test, src/tgbatest/ltlcross.test,
      src/tgbatest/ltlcross2.test, src/tgbatest/ltlcrossce.test: Add set -e.
      cf91a237
    • 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
  10. 26 Sep, 2013 1 commit
    • 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
  11. 16 Sep, 2013 2 commits
  12. 08 Sep, 2013 4 commits
    • 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
      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
  13. 26 Aug, 2013 14 commits
    • 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
      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
      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
      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
    • Alexandre Duret-Lutz's avatar
      dtbasat: implement dba_sat_minimize() · d9f3ca71
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtbasat.hh: New files.
      * src/tgbaalgos/Makefile.am: Add them.
      * src/tgbatest/ltl2tgba.cc: Add option -RS.
      d9f3ca71
    • Alexandre Duret-Lutz's avatar
      dbacomp: connect only back-links and generalize to tgba · 78e76eb0
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/dbacomp.cc: Here.
      * src/tgbaalgos/dbacomp.hh: Adjust documentation.
      * src/tgbatest/dbacomp.test: New file.
      * src/tgbatest/Makefile.am (TESTS): Add it.
      * src/tgbatest/det.test: Update.
      78e76eb0
    • Alexandre Duret-Lutz's avatar
      tba_determinize: add a cycle_threshold · 63b7cdb6
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh
      (tba_determinize, tba_determinize_check): Add a cycle_threshold
      argument.
      * src/tgbaalgos/postproc.cc: Use it.
      * src/tgbatest/ltl2tgba.cc: Adjust calls.
      63b7cdb6
    • Alexandre Duret-Lutz's avatar
      postproc: use tba_determinize_check() · 0117fc2c
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/postproc.cc: Use tba_determinize_check()
      if option "tba-det" is set.
      * src/tgbaalgos/postproc.hh (tba_determinize_): New attribute.
      * src/tgbatest/det.test: New file.
      * src/tgbatest/Makefile.am (TESTS): Add it.
      0117fc2c
    • Alexandre Duret-Lutz's avatar
      dba_determinize: Add a threshold argument. · 07ab225c
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh
      (dba_determinize, dba_determinize_check): Add a threshold
      argument.
      * src/tgbatest/ltl2tgba.cc (-O, -RQ): Accept a threshold
      argument.
      07ab225c
    • Alexandre Duret-Lutz's avatar
      Implement tba_determinize_check(), following Dax et al. (ATVA'07). · 4ac6468b
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh
      (tba_determinize_check): New function.
      * src/tgbatest/ltl2tgba.cc (-O): Use it.
      4ac6468b
    • Alexandre Duret-Lutz's avatar
      Introduce a dba_complement() function. · bd2e78c1
      Alexandre Duret-Lutz authored
      Loosely based on "Complementing Deterministic Büchi Automata in
      Polynomial Time", R. P. Kurshan, 1987, J. Comp. Syst. Sci. 35.
      
      * src/tgbaalgos/dbacomp.cc, src/tgbaalgos/dbacomp.hh: New files.
      * src/tgbaalgos/Makefile.am: Add them.
      * src/tgbatest/ltl2tgba.cc (-DC): New option to test it.
      bd2e78c1
    • Alexandre Duret-Lutz's avatar
      Implementent tba_determinize(), based on Dax et al (ATVA'07). · ec5bbf4f
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/powerset.hh,
      src/tgbaalgos/powerset.cc (tba_determinize): New function.
      * src/tgbatest/ltl2tgba.cc (-RQ): New option, for testing.
      ec5bbf4f
    • Alexandre Duret-Lutz's avatar
      reachiter: fix the DFS, and add a version with on_stack() · 29bc087d
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/reachiter.hh, src/tgbaalgos/reachiter.cc: Fix the
      tgba_reachable_iterator_depth_first implementation by not making
      inheriting from tgba_reachable_iterator.  Add a
      tgba_reachable_iterator_depth_first_stack
      * src/tgbatest/sim.test, src/tgbatest/dstar.test: Adjust.
      29bc087d
  14. 23 Aug, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      dstar2tgba: new command. · d3b81809
      Alexandre Duret-Lutz authored
      * src/bin/dstar2tgba.cc, src/bin/man/dstar2tgba.x: New files.
      * src/bin/Makefile.am, src/bin/man/Makefile.am: Add them.
      * NEWS: Mention it.
      * src/bin/ltl2tgba.cc, src/tgbaalgos/stats.cc, doc/org/ltl2tgba.org:
      Rename the %S sequence as %c, for consistency with dstar2tgba.
      * src/tgbatest/ltl2dstar.test: Add more tests.
      * src/tgbatest/ltl2dstar2.test: New file.
      * src/tgbatest/Makefile.am: Add it.
      d3b81809