1. 26 Jun, 2003 12 commits
    • Alexandre Duret-Lutz's avatar
      * INSTALL: New file. · 3d129932
      Alexandre Duret-Lutz authored
      3d129932
    • Alexandre Duret-Lutz's avatar
      * src/tgba/ltl2tgba.hh, src/tgba/ltl2tgba.cc: Move ... · 7fdd7861
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ltl2tgba.hh, src/tgbaalgos/ltl2tgba.cc: ... here.
      * src/tgba/Makefile.am, src/tgbaalgos/Makefile.am: Adjust.
      * src/tgba/public.hh: Do not include ltl2tgba.hh.
      * src/tgbatests/explprod.cc, src/tgbatests/ltl2tgba.cc,
      src/tgbatests/ltlprod.cc, src/tgbatests/mixprod.cc,
      src/tgbatests/reach.cc, src/tgbatests/tripprod.cc: Adjust inclusions.
      7fdd7861
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgbabddcoredata.hh: Fix some Doxygen comments. · f4629246
      Alexandre Duret-Lutz authored
      * src/ltlast/formula.hh: More Doxygen comments.
      * src/tgba/tgba.hh: Use <tt> in Doxygen comments.
      f4629246
    • Alexandre Duret-Lutz's avatar
      * doc/mainpage.dox: New file. · ecda9e26
      Alexandre Duret-Lutz authored
      * doc/Makefile.am (EXTRA_DIST): Add mainpage.dox.
      * doc/Doxyfile.in (INPUT): Add @srcdir@/mainpage.dox
      ecda9e26
    • Alexandre Duret-Lutz's avatar
      * src/tgba/succiter.hh: Adjust comments about promises to · 8e3a24ad
      Alexandre Duret-Lutz authored
      refer to accepting conditions.
      * src/tgba/tgbabddconcretefactory.hh: Likewise.
      * src/tgba/tgbabddcoredata.hh: Likewise.
      * src/tgba/dictunion.cc: Likewise.
      * src/tgba/tgba.hh: Likewise.
      8e3a24ad
    • Alexandre Duret-Lutz's avatar
      * doc/Makefile.am (doc): Typo. · 0b3d2c13
      Alexandre Duret-Lutz authored
      * src/ltlvisit/tostring.hh (to_string): Add doxygen comments.
      * src/ltlast/multop.hh (multop::paircmp): Add doxygen comments.
      * src/tgba/tgbaexplicit.hh (tgba_explicit::transtion,
      state_explicit, tgba_explicit_succ_iterator): Add doxygen comments.
      * src/ltlvisit/postfix.hh: Typo.
      0b3d2c13
    • Alexandre Duret-Lutz's avatar
      * doc/Makefile.am (doc): Typo. · 483507f1
      Alexandre Duret-Lutz authored
      * src/ltlvisit/tostring.hh (to_string): Add doxygen comments.
      * src/ltlast/multop.hh (multop::paircmp): Add doxygen comments.
      * src/ltlvisit/postfix.hh: Typo.
      483507f1
    • Alexandre Duret-Lutz's avatar
      * src/ltlast/Makefile.am (ltlastdir, ltlast_HEADERS): New variables. · 05f72410
      Alexandre Duret-Lutz authored
      (libltlast_la_SOURCES): Move all headers to ltlast_HEADERS.
      * src/ltlenv/Makefile.am (ltlenvdir, ltlenv_HEADERS): New variables.
      (libltlenv_la_SOURCES): Move all headers to ltlenv_HEADERS.
      * src/ltlparse/Makefile.am (ltlparsedir, ltlparse_HEADERS): New
      variables.
      (libltlparse_la_SOURCES): Move all public headers to ltlparse_HEADERS.
      * src/ltlvisit/Makefile.am (ltlvisitdir, ltlvisit_HEADERS): New
      variables.
      (libltlvisit_la_SOURCES): Move all headers to ltlparse_HEADERS.
      * src/misc/Makefile.am (include_HEADERS): Rename as ..
      (misc_HEADERS): ... this.
      (miscdir): New variable.
      * src/tgba/Makefile.am (tgbadir, tgba_HEADERS): New variables.
      (libtgba_la_SOURCES): Move all headers to tgba_HEADERS.
      * src/tgbaalgos/Makefile.am (tgbaalgosdir, tgbaalgos_HEADERS):
      New variables.
      (libtgbaalgos_la_SOURCES): Move all headers to tgbaalgos_HEADERS.
      * src/tgbaparse/Makefile.am (tgbaparsedir, tgbaparse_HEADERS): New
      variables.
      (libtgbaparse_la_SOURCES): Move all public headers to
      tgbaparse_HEADERS.
      * src/tgbaparse/public.hh: Include ltlparse/location.hh, not
      location.hh.
      05f72410
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      * m4/buddy.m4 (BUDDY_LDFLAGS): Use $(top_builddir), not $(top_srcdir). · 98a31af4
      Alexandre Duret-Lutz authored
      * src/tgbaparse/Makefile.am (AM_CPPFLAGS): Add $(BUDDY_CPPFLAGS).
      98a31af4
    • Alexandre Duret-Lutz's avatar
      * doc/Makefile.am: Rewrite to run Doxygen whenever Doxyfile.in · 5d26d6f0
      Alexandre Duret-Lutz authored
      or configure.ac changes.  Distribute the html doc.
      * doc/Doxyfile.in (EXCLUDE_PATTERNS): Complete with
      useless Bison classes.
      (FILE_PATTERNS): Remove *.cc files.
      5d26d6f0
    • Alexandre Duret-Lutz's avatar
      Distribute BuDDy. Compile and link with the included version if · 510756cd
      Alexandre Duret-Lutz authored
      explicitely requested (--with-included-buddy) or if there is
      now stuitable version already installed.
      
      * buddy/: New directory.  Contains a patched version of BuDDy 2.2.
      * m4/buddy.m4: Make sure the installed BuDDy supports bdd_mergepairs.
      Honor --with-included-buddy and --without-included-buddy.  Define
      the BUDDY_LDFLAGS and BUDDY_CPPFLAGS output variables, and the
      WITH_INCLUDED_BUDDY Automake conditional
      * Makefile.am [WITH_INCLUDED_BUDDY] (MAYBE_SUBDIRS): New variable.
      (SUBDIRS): Prepend $(MAYBE_SUBDIRS).
      * src/Makefile.am (libspot_LDFLAGS): New variable.
      * src/tgba/Makefile.am (AM_CPPFLAGS): Add $(BUDDY_CPPFLAGS).
      * src/tgbaalgos/Makefile.am (AM_CPPFLAGS): Likewise.
      * src/tgbatest/Makefile.am (AM_CPPFLAGS): Likewise.
      510756cd
  2. 25 Jun, 2003 4 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): · 832a504d
      Alexandre Duret-Lutz authored
      Rewrite using bdd_satoneset.  This time it's for real.  (I hope.)
      * src/tgba/succiterconcrete.hh (current_base_,
      current_base_left_): Delete.
      * tgba/tgbabddcoredata.hh (next_set): New variable.
      * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Adjust
      to update next_set.
      832a504d
    • Alexandre Duret-Lutz's avatar
      * src/tgba/bddprint.hh, src/tgba/tgbabddconcretefactory.hh, · 60bd2d17
      Alexandre Duret-Lutz authored
      src/tgba/tgbaproduct.hh: Fix Doxygen comments.
      60bd2d17
    • Alexandre Duret-Lutz's avatar
      * src/tgba/succiterconcrete.hh (next_succ_set_): Rename as ... · 6d0546c3
      Alexandre Duret-Lutz authored
      (succ_set_left_): ... this.
      (current_base_, current_base_left_): New variables.
      * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::first):
      Reset current_.
      (tgba_succ_iterator_concrete::next): Rewrite.
      (tgba_succ_iterator_concrete::current_state): Simplify.
      (tgba_succ_iterator_concrete::current_accepting_conditions): Remove
      atomic proposition with universal quantification.
      * src/tgba/ltl2tgba.cc (ltl_to_tgba): Normalize the formula.
      * src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::set_init_state):
      Complete the initial state.
      (tgba_bdd_concrete::succ_iter): Do not remove Now variable
      from the BDD passed to the iterator.
      * tgba/tgbabddcoredata.hh (notnow_set, var_set): New variables.
      * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Adjust
      to update notnow_set and var_set.
      6d0546c3
    • Alexandre Duret-Lutz's avatar
      f1af8f96
  3. 24 Jun, 2003 4 commits
  4. 23 Jun, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      Switch from "promises" to "accepting set". Fix the definitions · 25e6cca4
      Alexandre Duret-Lutz authored
      of these accepting set so that they are really usable.  Provide
      a all_accepting_conditions() method for use in the emptyness
      check, and a neg_accepting_conditions() for products.
      Predeclare TGBA accepting conditions is the i/o.
      
      * src/tgba/bddprint.cc (want_prom): Rename as ...
      (want_prom): ... this.
      (print_handler): Adjust to display Acc[].
      (print_acc_handler, bdd_print_acc): New functions.
      * src/tgba/bddprint.hh (print_acc_handler, bdd_print_acc):
      New functions.
      * src/tgba/succiter.hh (current_promise): Rename as ...
      (current_accepting_conditions): ... this.
      * src/tgba/succiterconcrete.cc (current_state):
      Rename next to now.
      (current_promise): Rename as ...
      (current_accepting_conditions): ... this, and compute
      the accepting conditions.
      * src/tgba/dictunion.cc, src/tgba/ltl2tgba.cc,
      src/tgba/succiterconcrete.hh,
      src/tgba/tgbabddconcretefactory.cc,
      src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh,
      src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc,
      src/tgba/tgbabddtranslatefactory.cc,
      src/tgbaalgos/dotty.cc: Adjust to new names.
      * src/tgba/tgba.hh (all_accepting_conditions,
      neg_accepting_conditions): New functions.
      * src/tgba/tgbabddconcretefactory.cc: Adjust to new
      names, and record accepting conditions instead of promises.
      * src/tgba/tgbabddcoredata.hh (accepting_conditions,
      all_accepting_conditions, negacc_set): New variables.
      (notnow_set, notprom_set, declare_promise): Rename as ...
      (notnext_set, notacc_set, declare_accepting_condition): ... these.
      * src/tgba/tgbaexplicit.hh
      (tgba_explicit_succ_iterator::current_promise): Rename as ...
      (tgba_explicit_succ_iterator::current_accepting_conditions): ... this.
      (tgba_explicit::add_promise): Rename as ...
      (tgba_explicit::add_accepting_condition): ... this.
      (tgba_explicit::declare_accepting_condition,
      tgba_explicit::has_accepting_condition): New variables.
      (tgba_explicit::get_promise): Rename as ...
      (tgba_explicit::get_accepting_condition): ... this.
      (tgba_explicit::all_accepting_conditions,
      tgba_explicit::neg_accepting_conditions): Implement them.
      (all_accepting_conditions, neg_accepting_conditions,
      all_accepting_conditions): New variables.
      (tgba_explicit_succ_iterator): Embed all_accepting_conditions_.
      * src/tgba/tgbaexplicit.cc: Likewise.
      * src/tgba/tgbaproduct.hh
      (tgba_product_succ_uterator): Embed left_neg_ and right_neg_.
      (tgba_product::all_accepting_conditions,
      tgba_product::neg_accepting_conditions): Implement them.
      * src/tgba/tgbatranslateproxy.hh:
      (tgba_translate_proxy::all_accepting_conditions,
      tgba_translate_proxy::neg_accepting_conditions): Implement them.
      * src/tgba/tgbatranslateproxy.cc: Likewise.
      * src/tgbaalgos/save.cc (save_rec): Call bdd_print
      (tgba_save_reachable): Output the `acc =' line.
      * src/tgbaparse/tgbaparse.yy: Support the for
      accepting conditions definitions using an "acc =" line
      at the start.  Later, use has_accepting_condition while
      parsing	accepting conditions to ensure they were declared.
      Disallow !cond in accepting conditions.
      * src/tgbaparse/tgbascan.ll (ACC_DEF): New token.
      * src/tgbatest/explicit.cc (main): Declare accepting conditions.
      * src/tgbatest/ltl2tgba.cc (main): Add support for the -a, -A,
      and -R new options.
      * src/tgbatest/tgbaread.cc (main): Really exit on parse error.
      * src/tgbatest/explicit.test, src/tgbatest/explprod.test,
      src/tgbatest/mixprod.test, src/tgbatest/readsave.test,
      src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Reflect
      recent changes.
      25e6cca4
  5. 22 Jun, 2003 1 commit
  6. 19 Jun, 2003 4 commits
  7. 18 Jun, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/tgba/bddprint.cc (print_handler): Quote promises · bacd5a0a
      Alexandre Duret-Lutz authored
      when !want_prom.
      * src/tgbaparse/tgbaparse.yy (prop_list): Accept strings or
      identifiers.  Discard empty strings.
      * src/tgbatest/mixprod.cc, src/tgbatest/mixprod.test: New file.
      * src/tgbatest/Makefile.am (check_PROGRAMS): Add mixprod.
      (mixprod_SOURCES): New variable.
      (TESTS): Add mixprod.test.
      bacd5a0a
  8. 17 Jun, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgbaproduct.cc (state_bdd_product::state_bdd_product): · fd12c023
      Alexandre Duret-Lutz authored
      New constructor.
      * src/tgba/tgbaproduct.hh (state_bdd_product::state_bdd_product):
      New constructor.
      * tgbatest/tripprod.cc, tgbatest/tripprod.test: New files.
      * src/tgbatest/Makefile.am (check_PROGRAMS): Add explprod.
      (tripprod_SOURCES): New variable.
      (CLEANFILES): Add input3.
      (TESTS): Add tripprod.test.
      fd12c023
  9. 16 Jun, 2003 2 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgba/tgbabddprod.cc, src/tgba/tgbabddprod.hh: Rename as ... · 4db70160
      Alexandre Duret-Lutz authored
      * src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: ... these.
      (tgba_bdd_product, tgba_bdd_product_succ_iterator): Rename as ...
      (tgba_product, tgba_product_succ_iterator): ... these, and adjust
      all uses.
      * src/tgba/tgbabddtranslateproxy.cc,
      src/tgba/tgbabddtranslateproxy.hh: Rename as ...
      * src/tgba/tgbatranslateproxy.cc,
      src/tgba/tgbatranslateproxy.hh: ... these.
      (tgba_bdd_translate_proxy, tgba_bdd_translate_proxy_succ_iterator):
      Rename as ...
      (tgba_translate_proxy, tgba_translate_proxy_succ_iterator): ... these,
      and adjust all uses.
      4db70160
    • Alexandre Duret-Lutz's avatar
      Make sure we can multiply two tgba_explicit. · ab09c185
      Alexandre Duret-Lutz authored
      * tgba/state.hh (state::translate, state::clone, state::as_bdd):
      New virtual methods.
      * tgba/stataebdd.cc (state::translate, state::clone): New methods.
      * tgba/stataebdd.hh (state::translate, state::clone): New methods.
      * tgba/tgbabddprod.cc (state_bdd_product::clone,
      tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator):
      New methods.
      (tgba_bdd_product_succ_iterator::first): Reset right_
      if any of left_ or right_ is already done (i.e., is empty).
      (tgba_bdd_product_succ_iterator::done): Return true
      if right_ is NULL.
      (tgba_bdd_product_succ_iterator::current_state,
      tgba_bdd_product::get_init_state): Work	directory with `state's.
      * tgba/tgbabddprod.hh (state_bdd_product::clone,
      tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator):
      New methods.
      * tgba/tgbabddtranslateproxy.cc
      (tgba_bdd_translate_proxy_succ_iterator::
      tgba_bdd_translate_proxy_succ_iterator): Work on any kind of iteraator.
      (tgba_bdd_translate_proxy_succ_iterator::
      ~tgba_bdd_translate_proxy_succ_iterator): New method.
      (tgba_bdd_translate_proxy_succ_iterator::current_state,
      tgba_bdd_translate_proxy::get_init_state,
      tgba_bdd_translate_proxy::succ_iter): Work on `state's and
      `tgba_succ_iterator's directlry.
      (tgba_bdd_translate_proxy::format_state): Delegate formating
      to the proxied automata.
      * tgba/tgbaexplicit.cc (state_explicit::clone): New method.
      * src/tgba/tgbaexplicit.cc (tgba_explicit::get_condition,
      tgba_explicit::get_promise): Call ltl::destroy on existing formulae.
      * tgbatest/Makefile.am (check_PROGRAMS): Add explprod.
      (explprod_SOURCES): New variable.
      (TESTS): Add explprod.test.
      (CLEANFILES): Add input1 and input2.
      ab09c185
  10. 12 Jun, 2003 1 commit
  11. 10 Jun, 2003 1 commit
  12. 06 Jun, 2003 4 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgbatest/bddprod.test: New file. · 0233f31e
      Alexandre Duret-Lutz authored
      * src/tgbatest/Makefile.am (check_PROGRAMS): Add bddprod.
      (bddprod_SOURCES, bddprod_CXXFLAGS): New variables.
      (TESTS): Add bddprod.test.
      * src/tgbatest/ltlprod.c: Handle BDD_CONCRETE_PRODUCT.
      0233f31e
    • Alexandre Duret-Lutz's avatar
      * src/tgba/dictunion.cc (tgba_bdd_dict_union): Clone formulae · 4472a292
      Alexandre Duret-Lutz authored
      while building new dictionary.
      * src/tgbatest/ltlprod.test, src/tgbatest/ltlprod.cc: New files.
      * src/tgbatest/Makefile.am (check_PROGRAMS): Add ltlprod.
      (ltlprod_SOURCES): New variable.
      (TESTS): Add ltlprod.test.
      4472a292
    • Alexandre Duret-Lutz's avatar
      * src/ltlvisit/clone.cc (clone): New const version. · 3991a51a
      Alexandre Duret-Lutz authored
      * src/ltlvisit/clone.hh (clone): Likewise.
      * src/ltlvisit/destroy.cc (destroy): New const version.
      * src/ltlvisit/destroy.hh (destroy): Likewise.
      * src/tgba/tgbabddconcretefactory.cc
      (tgba_bdd_concrete_factory::create_state,
      tgba_bdd_concrete_factory::create_atomic_prop,
      tgba_bdd_concrete_factory::promise): Clone new formulae.
      * src/tgba/tgbabdddict.cc (tgba_bdd_dict::tgba_bdd_dict,
      tgba_bdd_dict::~tgba_bdd_dict, tgba_bdd_dict::operator=): New methods
      that clone and destroy formulae.
      * src/tgbatest/ltl2tgba.test, src/tgbatest/ltl2tgba.cc: New files.
      * src/tgbatest/Makefile.am (check_PROGRAMS): Add ltl2tgba.
      (ltl2tgba_SOURCES): New variable.
      (TESTS): Add ltl2tgba.test.
      3991a51a
    • Alexandre Duret-Lutz's avatar
      * src/ltltest/equals.cc, src/ltltest/readltl.cc, · 578fa26c
      Alexandre Duret-Lutz authored
      src/tgba/bddprint.cc, src/ltltest/tostring.cc: Include <cassert>.
      578fa26c
  13. 05 Jun, 2003 4 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgba/bddprint.cc (dict): Make this variable static. · 19e47ee6
      Alexandre Duret-Lutz authored
      (want_prom): New global static variable.
      (print_handle): Honor want_prom.
      (print_sat_handler, bdd_print_sat, bdd_format_sat): New functions.
      (bdd_print_set, bdd_print_dot, bdd_print_table): Set want_prom.
      * src/tgba/bddprint.hh (bdd_print_sat, bdd_format_sat): New functions.
      * src/tgbaalgos/save.cc, src/tgbaalgos/save.hh,
      src/tgbatest/readsave.cc, src/tgbatest/readsave.test: New files.
      * src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add
      save.cc and save.hh.
      * src/tgbatest/Makefile.am (check_PROGRAMS): Add readsave.
      (readsave_SOURCES): New variable.
      (TESTS): Add readsave.test.
      19e47ee6
    • Alexandre Duret-Lutz's avatar
      * configure.ac: Output src/tgbaparse/Makefile. · 6884a7f9
      Alexandre Duret-Lutz authored
      * src/Makefile.am (SUBDIRS): Add tgbaparse.
      (libspot_la_LDADD): Add tgbaparse/libtgbaparse.la.
      * src/tgba/tgbaexplicit.cc (tgba_explicit::get_condition,
      tgba_explicit::get_promise, tgba_explicit::add_neg_condition,
      tgba_explicit::add_neg_promise): New methods.
      * src/tgba/tgbaexplicit.hh: Declare them.
      * src/tgbaparse/Makefile.am, src/tgbaparse/fmterror.cc,
      src/tgbaparse/parsedecl.hh, src/tgbaparse/public.hh,
      src/tgbaparse/tgbaparse.yy, src/tgbaparse/tgbascan.ll,
      src/tgbatest/tgbaread.cc, src/tgbatest/tgbaread.test: New files.
      * src/tgbatest/Makefile.am (check_PROGRAMS): Add tgbaread.
      (TESTS): Add tgbaread.cc.
      (CLEANFILES): Add input.
      (tgbaread_SOURCES): New variable.
      6884a7f9
    • Alexandre Duret-Lutz's avatar
      cebffb11
    • Alexandre Duret-Lutz's avatar
      * configure.ac: Output src/tgbatest/Makefile and src/tgbatest/defs. · 80dd0ae1
      Alexandre Duret-Lutz authored
      * src/Makefile.am (SUBDIRS): Add tgbatest.
      * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc: New file.
      * src/tgba/Makefile.am (libtgba_la_SOURCES): Add tgbaexplicit.cc
      and tgbaexplicit.hh.
      * src/tgbatest/Makefile.am, src/tgbatest/defs.in,
      src/tgbatest/explicit.cc, src/tgbatest/explicit.test: New files.
      80dd0ae1