1. 25 Feb, 2008 1 commit
  2. 21 Sep, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/sanity/style.test: Warn about places where size() is used · c30823f7
      Alexandre Duret-Lutz authored
      instead of empty().
      * src/misc/bddalloc.cc (bdd_allocator::extend): Use empty() rather
      than size() when checking emptiness of lists.
      * src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/minimalce.cc,
      src/ltlvisit/basicreduce.cc, src/ltlvisit/reduce.cc,
      src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/ltl2tgba_fm.cc,
      src/misc/minato.cc: Likewise.
      * src/ltlast/multop.cc (multop::instance): Call ->size() only once.
      c30823f7
  3. 17 May, 2004 1 commit
  4. 18 Mar, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      Move the free_list management into a separate class for reuse. · cf6602a3
      Alexandre Duret-Lutz authored
      * src/misc/freelist.hh, src/misc/freelist.cc: New files.
      * src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them.
      * src/misc/bddalloc.hh (bdd_allocator): Inherit from free_list and
      make dump_free_list visible.
      * src/misc/bddalloc.cc (bdd_allocator::allocate_variables): Move
      all the code into free_list::register_n() and
      bdd_allocator::extend(), and call the former.
      (bdd_allocator::release_variables): Move all the code into
      free_list::release_n() and call it.
      (bdd_allocator::extend): New method.
      * src/tgba/bdddict.cc (bdd_dict::dump): Call dump_free_list;
      cf6602a3
  5. 21 Nov, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      * COPYING: New file. · 43a91a15
      Alexandre Duret-Lutz authored
      * Makefile.am, configure.ac, doc/Makefile.am, iface/Makefile.am,
      iface/gspn/Makefile.am, iface/gspn/common.cc,
      iface/gspn/common.hh, iface/gspn/dottyeesrg.cc,
      iface/gspn/dottygspn.cc, iface/gspn/eesrg.cc, iface/gspn/eesrg.hh,
      iface/gspn/gspn.cc, iface/gspn/gspn.hh, iface/gspn/ltlgspn.cc,
      src/Makefile.am, src/ltlast/Makefile.am, src/ltlast/allnodes.hh,
      src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
      src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/constant.cc,
      src/ltlast/constant.hh, src/ltlast/formula.cc,
      src/ltlast/formula.hh, src/ltlast/multop.cc, src/ltlast/multop.hh,
      src/ltlast/predecl.hh, src/ltlast/refformula.cc,
      src/ltlast/refformula.hh, src/ltlast/unop.cc, src/ltlast/unop.hh,
      src/ltlast/visitor.hh, src/ltlenv/Makefile.am,
      src/ltlenv/defaultenv.cc, src/ltlenv/defaultenv.hh,
      src/ltlenv/environment.hh, src/ltlparse/Makefile.am,
      src/ltlparse/fmterror.cc, src/ltlparse/ltlparse.yy,
      src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh,
      src/ltlparse/public.hh, src/ltltest/Makefile.am,
      src/ltltest/defs.in, src/ltltest/equals.cc,
      src/ltltest/equals.test, src/ltltest/lunabbrev.test,
      src/ltltest/nenoform.test, src/ltltest/parse.test,
      src/ltltest/parseerr.test, src/ltltest/readltl.cc,
      src/ltltest/tostring.cc, src/ltltest/tostring.test,
      src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test,
      src/ltlvisit/Makefile.am, src/ltlvisit/clone.cc,
      src/ltlvisit/clone.hh, src/ltlvisit/destroy.cc,
      src/ltlvisit/destroy.hh, src/ltlvisit/dotty.cc,
      src/ltlvisit/dotty.hh, src/ltlvisit/dump.cc, src/ltlvisit/dump.hh,
      src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh,
      src/ltlvisit/nenoform.cc, src/ltlvisit/nenoform.hh,
      src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh,
      src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh,
      src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh,
      src/misc/Makefile.am, src/misc/bddalloc.cc, src/misc/bddalloc.hh,
      src/misc/bddlt.hh, src/misc/hash.hh, src/misc/minato.cc,
      src/misc/minato.hh, src/misc/version.cc, src/misc/version.hh,
      src/tgba/Makefile.am, src/tgba/bdddict.cc, src/tgba/bdddict.hh,
      src/tgba/bddprint.cc, src/tgba/bddprint.hh, src/tgba/public.hh,
      src/tgba/state.hh, src/tgba/statebdd.cc, src/tgba/statebdd.hh,
      src/tgba/succiter.hh, src/tgba/succiterconcrete.cc,
      src/tgba/succiterconcrete.hh, src/tgba/tgba.cc, src/tgba/tgba.hh,
      src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh,
      src/tgba/tgbabddconcretefactory.cc,
      src/tgba/tgbabddconcretefactory.hh,
      src/tgba/tgbabddconcreteproduct.cc,
      src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddcoredata.cc,
      src/tgba/tgbabddcoredata.hh, src/tgba/tgbabddfactory.hh,
      src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh,
      src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh,
      src/tgba/tgbatba.cc, src/tgba/tgbatba.hh,
      src/tgbaalgos/Makefile.am, src/tgbaalgos/dotty.cc,
      src/tgbaalgos/dotty.hh, src/tgbaalgos/dupexp.cc,
      src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptinesscheck.cc,
      src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/lbtt.cc,
      src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.cc,
      src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/magic.cc,
      src/tgbaalgos/magic.hh, src/tgbaalgos/reachiter.cc,
      src/tgbaalgos/reachiter.hh, src/tgbaalgos/save.cc,
      src/tgbaalgos/save.hh, 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/Makefile.am,
      src/tgbatest/bddprod.test, src/tgbatest/defs.in,
      src/tgbatest/dupexp.test, src/tgbatest/emptchk.test,
      src/tgbatest/emptchke.test, src/tgbatest/explicit.test,
      src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
      src/tgbatest/explprod.test, src/tgbatest/ltl2tgba.test,
      src/tgbatest/ltlprod.test, src/tgbatest/mixprod.test,
      src/tgbatest/readsave.test, src/tgbatest/spotlbtt.test,
      src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test,
      wrap/Makefile.am, wrap/python/Makefile.am, wrap/python/buddy.i,
      wrap/python/spot.i, wrap/python/cgi/Makefile.am,
      wrap/python/cgi/ltl2tgba.in, wrap/python/tests/Makefile.am,
      wrap/python/tests/bddnqueen.py, wrap/python/tests/interdep.py,
      wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltl2tgba.test,
      wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py,
      wrap/python/tests/run.in: Add Copyright license.
      43a91a15
  6. 14 Oct, 2003 1 commit
  7. 15 Aug, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      varnum can be augmented by other allocator. Keep track · 256d8005
      Alexandre Duret-Lutz authored
      of a local varnum (lvarnum) in each allocator.
      * src/misc/bddalloc.cc (bdd_allocator::bdd_allocator): Initialize
      lvarnum.
      (bdd_allocator::extvarnum): New method.
      (bdd_allocator::allocate_variables): Use lvarnum and extvarnum.
      * src/misc/bddalloc.hh (bdd_allocator::extvarnum): New mathod.
      (bdd_allocator::lvarnum): New variable.
      256d8005
  8. 14 Jul, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      Before this change, all automata would construct their own · cab3be97
      Alexandre Duret-Lutz authored
      dictionaries (map of BDD variables to LTL formulae).  This was
      cumbersome, because to multiply two automata we had to build a
      common dictionary (the union of the two LTL formula spaces), and
      install wrappers to translate each automaton's BDD answers into
      the common dictionary.  This translation, that had to be repeated
      when several products were nested, was time consuming and was a
      hindrance for some optimizations.
      In the new scheme, all automata involved in a product must
      share the same dictionary.  An empty dictionary should be
      constructed by the user and passed to the automaton' constructors
      as necessary.
      This huge change removes most code than it adds.
      
      * src/Makefile.am (libspot_la_LIBADD): Add misc/libmisc.la.
      * src/misc/bddalloc.hh, src/misc/bddalloc.cc: New files.  These
      partly replace src/tgba/bddfactory.hh and src/tgba/bddfactory.cc.
      * src/misc/Makefile.am: Adjust to build bddalloc.hh and bddalloc.cc.
      * src/tgba/bddfactory.hh, src/tgba/bddfactory.cc,
      src/tgba/dictunion.hh, src/tgba/dictunion.cc,
      src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc,
      src/tgba/tgbabddtranslatefactory.hh,
      src/tgba/tgbabddtranslatefactory.cc,
      src/tgba/tgbatranslateproxy.hh, src/tgba/tgbatranslateproxy.cc:
      Delete.
      * src/tgba/bdddict.hh, src/tgba/bdddict.cc: New files.  These
      replaces tgbabdddict.hh and tgbabdddict.cc, and also part of
      bddfactory.hh and bddfactory.cc.
      * src/tgba/bddprint.cc, src/tgba/bddprint.hh: Adjust to
      use bdd_dict* instead of tgba_bdd_dict&.
      * src/tgba/succiterconcrete.cc (succ_iter_concrete::next()):
      Get next_to_now from the dictionary.
      * src/tgba/tgba.hh (tgba::get_dict): Return a bdd_dict*,
      not a const tgba_bdd_dict*.
      * src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh:
      Adjust to use the new dictionary, stored in data_.
      * src/tgba/tgbabddconcretefactory.cc,
      src/tgba/tgbabddconcretefactory.hh: Likewise.  Plus
      now_to_next_ is now also stored in the dictionary.
      * src/tgba/tgbabddconcreteproduct.cc: Likewise.  Now
      that both operand share the same product, there is not
      point in using tgba_bdd_translate_factory.
      * src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh:
      Store a bdd_dict (taken as constructor argument).
      (tgba_bdd_core_data::~tgba_bdd_core_data): Remove.
      (tgba_bdd_core_data::translate): Remove.
      (tgba_bdd_core_data::next_to_now): Remove (now in dict).
      (tgba_bdd_core_data::dict): New pointer.
      * src/tgba/tgbabddfactory.hh: (tgba_bdd_factory::get_dict): Remove.
      * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh:
      Adjust to use the new dictionary.
      * src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: Likewise.  Do
      not use tgba_bdd_dict_union and tgba_bdd_translate_proxy anymore.
      * src/tgbaalgos/lbtt.cc, src/tgbaalgos/save.cc: Adjust to
      use bdd_dict* instead of tgba_bdd_dict&.
      * src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.cc: Likewise.
      (ltl_to_tgba): Take a dict argument.
      * src/tgbaparse/public.hh (tgba_parse): Take a dict argument.
      * src/tgbaparse/tgbaparse.yy (tgba_parse): Take a dict argument.
      * src/tgbatest/explicit.cc, src/tgbatest/explprod.cc,
      src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc,
      src/tgbatest/readsave.cc, src/tgbatest/spotlbtt.cc,
      src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc: Instantiate
      a dictionary, and pass it to the automata' constructors.
      * src/tgbatest/ltl2tgba.cc: Likewise, and remove the -o (defrag)
      option.
      * iface/gspn/gspn.hh (tgba_gspn::tgba_gspn): Take a bdd_dict argument.
      (tgba_gspn::get_dict): Adjust return type.
      * iface/gspn/gspn.cc: Do not use bdd_factory, adjust to
      use the new dictionary instead.
      cab3be97