1. 02 Sep, 2009 5 commits
    • Alexandre Duret-Lutz's avatar
      Use Automake 1.11's parallel-tests feature. · 1098c62d
      Alexandre Duret-Lutz authored
      * configure.ac: Enable parallel-tests.
      * src/eltltest/defs.in, src/evtgbatest/defs.in,
      src/ltltest/defs.in, src/tgbatest/defs.in: Always output verbose
      tests.  Make a subdirectory for each test case.
      * src/ltltest/Makefile.am, src/eltltest/Makefile.am,
      src/tgbatest/Makefile.am, src/evtgbatest/Makefile.am: Remove
      CLEANFILES and clean the test subdirectories in a distclean-local
      rule instead.
      * src/eltltest/acc.test, src/eltltest/nfa.test,
      src/evtgbatest/explicit.test, src/evtgbatest/ltl2evtgba.test,
      src/evtgbatest/product.test, src/evtgbatest/readsave.test,
      src/ltltest/equals.test, src/ltltest/lunabbrev.test,
      src/ltltest/nenoform.test, src/ltltest/parse.test,
      src/ltltest/parseerr.test, src/ltltest/reduc.test,
      src/ltltest/reduccmp.test, src/ltltest/syntimpl.test,
      src/ltltest/tostring.test, src/ltltest/tunabbrev.test,
      src/ltltest/tunenoform.test, src/tgbatest/bddprod.test,
      src/tgbatest/complementation.test, src/tgbatest/dfs.test,
      src/tgbatest/dupexp.test, src/tgbatest/eltl2tgba.test,
      src/tgbatest/emptchk.test, src/tgbatest/emptchke.test,
      src/tgbatest/emptchkr.test, src/tgbatest/explicit.test,
      src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
      src/tgbatest/explpro4.test, src/tgbatest/explprod.test,
      src/tgbatest/ltl2neverclaim.test, src/tgbatest/ltl2tgba.test,
      src/tgbatest/ltlprod.test, src/tgbatest/mixprod.test,
      src/tgbatest/readsave.test, src/tgbatest/reduccmp.test,
      src/tgbatest/reductgba.test, src/tgbatest/scc.test,
      src/tgbatest/spotlbtt.test, src/tgbatest/tgbaread.test,
      src/tgbatest/tripprod.test: Adjust to run from a subdirectory.
      1098c62d
    • Alexandre Duret-Lutz's avatar
      more files to ignore · 1f7aa90d
      Alexandre Duret-Lutz authored
      1f7aa90d
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      [buddy] configure.ac: Switch from Libtool 1.5.x to Libtool 2.x, and add an... · 43ba3f83
      Alexandre Duret-Lutz authored
      [buddy] configure.ac: Switch from Libtool 1.5.x to Libtool 2.x, and add an AC_CONFIG_MACRO_DIR call.
      43ba3f83
    • Alexandre Duret-Lutz's avatar
      * configure.ac: Switch from Libtool 1.5.x to Libtool 2.x, and · 9eecd6ae
      Alexandre Duret-Lutz authored
      add an AC_CONFIG_MACRO_DIR call.
      * m4/libtool.m4, tools/ltmain.sh: Remove.
      9eecd6ae
  2. 30 Jul, 2009 1 commit
  3. 09 Jul, 2009 1 commit
  4. 08 Jul, 2009 2 commits
    • Guillaume Sadegh's avatar
      fd9ec017
    • Flix Abecassis's avatar
      Add 2 benchmarks directories. · 414956c5
      Flix Abecassis authored
      Add an algorithm to split an automaton in several automata.
      
      * bench/scc-stats: New directory.  Contains input files and test
      program for computing statistics.
      * bench/split-product: New directory.  Contains test program for
      synchronised product on splitted automata.
      * bench/split-product/models: New directory.  Contains Promela
      files and LTL formulae that should be verified by the models.
      * src/tgba/tgbafromfile.cc, src/tgba/tgbafromfile.hh:
      New files.  Small class to avoid long initializations with numerous
      constants when translating to TGBA many LTL formulae from a
      given file.
      * src/tgbaalgos/cutscc.cc, src/tgbaalgos/cutscc.hh:
      New file.  From a single automaton, create, at most,
      X sub automata.
      * src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh:
      Adjust to compute self-loops count.
      414956c5
  5. 07 Jul, 2009 1 commit
  6. 17 Jun, 2009 1 commit
  7. 12 Jun, 2009 3 commits
  8. 11 Jun, 2009 1 commit
  9. 10 Jun, 2009 4 commits
  10. 09 Jun, 2009 1 commit
  11. 05 Jun, 2009 3 commits
    • Guillaume Sadegh's avatar
      Remove generated files that git follows. · 78f8f164
      Guillaume Sadegh authored
              * INSTALL, lbtt/INSTALL, lbtt/doc/texinfo.tex: Do not track
      	anymore these generated files.
      78f8f164
    • Guillaume Sadegh's avatar
      Add an algorithm to complement Büchi automata. · c5f8eafb
      Guillaume Sadegh authored
      	* src/tgba/tgbacomplement.hh, src/tgba/tgbacomplement.cc: New
      	files. The complementation algorithm.
      	* src/tgba/Makefile.am: Adjust.
      	* src/tgbatest/complementation.test,
      	src/tgbatest/complementation.cc: New files. Test suite for the
      	complementation algorithm.
      	* src/tgbatest/Makefile.am: Adjust.
      	* src/tgbaalgos/Makefile.am: Reformat the header using 80
      	columns.
      c5f8eafb
    • Damien Lefortier's avatar
      Modify the ELTL parser to be able to support PSL operators. Add a · e48338e8
      Damien Lefortier authored
      new keyword in the ELTL format: finish, which applies to an
      automaton operator and tells whether it just completed.
      
      * src/eltlparse/eltlparse.yy: Clean it. Add finish.
      * src/eltlparse/eltlscan.ll: Add finish.
      * src/formula_tree.cc, src/formula_tree.hh: New files. Define a
      small AST representing formulae where atomic props are unknown
      which is used in the ELTL parser.
      * src/ltlast/automatop.cc, ltlast/automatop.hh, ltlast/nfa.cc,
      ltlast/nfa.hh: Adjust.
      * src/ltlast/unop.cc, src/ltlast/unop.hh: Finish is an unop.
      * src/ltlvisit/basicreduce.cc, src/ltlvisit/nenoform.cc,
      src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc,
      src/ltlvisit/tostring.cc, src/ltlvisit/tunabbrev.cc,
      src/tgba/formula2bdd.cc, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/ltl2tgba_lacim.cc: Handle finish in switches.
      * src/tgbaalgos/eltl2tgba_lacim.cc: Translate finish.
      * src/tgbatest/eltl2tgba.test: More tests.
      e48338e8
  12. 02 Jun, 2009 3 commits
  13. 31 May, 2009 2 commits
  14. 28 May, 2009 8 commits
    • Alexandre Duret-Lutz's avatar
      Test "ltl2tgba -FC" and plug the memory leaks of scc_map. · 35298429
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/scc.hh (scc_map::~scc_map): Declare it.
      * src/tgbaalgos/scc.cc (scc_map::~scc_map): Implement it.
      (scc_map::build_map): Delete duplicate states.
      * src/tbbatest/ltl2tgba.test: Run ltl2tgba -FV to catch
      memory leaks with valgrind.
      35298429
    • Alexandre Duret-Lutz's avatar
      Implement spot::future_conditions_collector. · d74578ef
      Alexandre Duret-Lutz authored
      * src/tgba/futurecondcol.hh, src/tgba/futurecondcol.cc:
      New files.
      * src/tgba/Makefile.am: Adjust.
      * src/tgbatest/ltl2tgba.cc: Add option -FC.
      d74578ef
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/scc.cc (dump_scc_dot): Use a bit vector instead of · a375972f
      Alexandre Duret-Lutz authored
      a map to track visited SCC since they are sequentially numbered.
      a375972f
    • Alexandre Duret-Lutz's avatar
      Number states using negative values and SCCs using nonnegative · 15b3b9e0
      Alexandre Duret-Lutz authored
      values.
      
      Before this change states were numbered using positive values and
      SCCs using negative values.  That meant the user had to work with
      negative values.  With this changes, the nonnegative values used
      to label SCCs can also directly be used as index in the scc_map_.
      
      * src/tgbaalgos/scc.hh (scc_map::scc_of_state,
      scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of,
      scc_map::initial, scc_map::scc_type, scc_map::succ,
      scc_map::accepting): Adjust prototypes to take or return unsigned
      arguments.
      * src/tgbaalgos/scc.cc: Adjust prototypes of the above functions.
      (scc_map::build_map, scc_map::relabel_component): Number states
      using negative values, and SCCs using nonnegative values.
      (dump_scc_dot): Adjust to use nonnegative values.
      15b3b9e0
    • Alexandre Duret-Lutz's avatar
      Store the scc_map_ as a vector instead of a std::map. There is no · 96a7a49c
      Alexandre Duret-Lutz authored
      point in using a map since the SCC are numbered in sequence.
      
      * src/tgbaalgos/scc.hh (scc_map::relabel_component): Return the
      number of the SCC instead of taking it as argument.
      (scc_map::scc_num_): Delete this variable.  scc_map_.size() gives
      the same information.
      (scc_map::scc_map_type): Define using std::vector instead of
      std::map.
      * src/tgbaalgos/scc.cc: Adjust all uses.
      96a7a49c
    • Alexandre Duret-Lutz's avatar
      Keep track of conditions in SCC, and add a more verbose dump. · 07ead613
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/scc.hh (scc_map::scc_of_state,
      scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of):
      New functions.
      (scc_map::scc::conds): New attribute.
      (dump_scc_dot): Take an optional VERBOSE argument.
      * src/tgbaalgos/scc.cc (scc_map::scc_of_state,
      scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of):
      Implement these new functions.
      (dump_scc_dot): Display number of states, conditions and
      acceptance conditions, with VERBOSE is set.
      (build_map): Fill the new scc_map::scc::cond field.
      07ead613
    • Alexandre Duret-Lutz's avatar
      Fix assertion in scc.cc · cbfdcca1
      Alexandre Duret-Lutz authored
      cbfdcca1
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgba.hh (format_state): s/automata who/automata that/. · 6142441f
      Alexandre Duret-Lutz authored
      * src/evtgba/evtgba.hh (format_state): Likewise.
      * src/evtgba/product.hh (format_state): Likewise.
      6142441f
  15. 26 Apr, 2009 1 commit
    • Damien Lefortier's avatar
      Extend the ELTL parser to support more complex aliases of · b06c9cd5
      Damien Lefortier authored
      automaton operators such as Strong=G(F($0))->G(F($1)) and
      G=R(false, $0).
      
      * src/eltlparse/eltlparse.yy, src/eltlparse/eltlscan.ll: Add
      support for more complex aliases.
      * src/eltltest/acc.cc, src/eltltest/acc.test: Adjust.
      * src/ltlast/nfa.cc, src/ltlast/nfa.hh (arity): Now returns an
      unsigned value.
      * src/tgbatest/eltl2tgba.test: Adjust.
      * src/tgbalagos/eltl2tgba_lacim.cc: Fix sanity.
      b06c9cd5
  16. 09 Apr, 2009 1 commit
    • Guillaume Sadegh's avatar
      Minor fixes to compile with GCC 4.4. · bbbc1acc
      Guillaume Sadegh authored
      2009-04-09  Guillaume SADEGH  <sadegh@lrde.epita.fr>
      
      	* src/eltlparse/eltlparse.yy (subformula): Avoid a comparaison
      	between a signed and an unsigned value.
      	* src/ltlast/automatop.hh, src/ltlast/automatop.cc (nfa): Avoid
      	a name clash with the `nfa' class.
      bbbc1acc
  17. 08 Apr, 2009 1 commit
    • Damien Lefortier's avatar
      Correct LaCIM for ELTL and make it work with LBTT. · 7643c49c
      Damien Lefortier authored
      * src/eltlparse/eltlparse.yy: Adjust.
      * src/ltlast/automatop.cc, src/ltlast/automatop.hh,
      src/ltlvisit/clone.cc, src/ltlvisit/nenoform.cc: Clean the way we
      handle the negation of automaton operators.
      * src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh: Add an
      optional argument to output a fully parenthesized string.
      * src/tgbaalgos/eltl2tgba_lacim.cc: Fix it.
      * src/tgbatest/eltl2tgba.cc: Add a new option (-L) to read formulae
      from an LBTT-compatible file.
      * src/tgbatest/eltl2tgba.test: A new tests.
      * src/tgbatest/spotlbtt.test: Add LaCIM for ELTL.
      7643c49c
  18. 04 Apr, 2009 1 commit
    • Damien Lefortier's avatar
      Extend the ELTL parser to support basic aliases of automaton · 355461ae
      Damien Lefortier authored
      operators such as F=U(true,$0) or R=!U(!$0,!$1), and infix
      notation for binary automaton operators.
      
      * README: Document the ELTL directories.
      * src/eltlparse/eltlparse.yy, src/eltlparse/eltlscan.ll: Add
      support for aliases and infix notation.
      * src/eltlparse/public.hh, src/ltlast/nfa.cc, src/ltlast/nfa.hh:
      Clean them.
      * src/eltltest/acc.test, src/tgbatest/eltl2tgba.test: Add tests
      for the ELTL parser's extensions.
      * src/tgbatest/eltl2tgba.cc: Adjust.
      355461ae