From cab3be97952c865d3b14a2c10f146a4c32d2992c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 14 Jul 2003 21:42:59 +0000 Subject: [PATCH] Before this change, all automata would construct their own 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. --- ChangeLog | 75 +++++++- iface/gspn/gspn.cc | 72 ++++---- iface/gspn/gspn.hh | 16 +- src/Makefile.am | 1 + src/misc/.cvsignore | 3 + src/misc/Makefile.am | 12 +- src/misc/bddalloc.cc | 123 +++++++++++++ src/misc/bddalloc.hh | 32 ++++ src/tgba/Makefile.am | 16 +- src/tgba/bdddict.cc | 271 ++++++++++++++++++++++++++++ src/tgba/bdddict.hh | 122 +++++++++++++ src/tgba/bddfactory.cc | 48 ----- src/tgba/bddfactory.hh | 60 ------ src/tgba/bddprint.cc | 28 +-- src/tgba/bddprint.hh | 16 +- src/tgba/dictunion.cc | 80 -------- src/tgba/dictunion.hh | 13 -- src/tgba/succiterconcrete.cc | 2 +- src/tgba/tgba.hh | 4 +- src/tgba/tgbabddconcrete.cc | 13 +- src/tgba/tgbabddconcrete.hh | 3 +- src/tgba/tgbabddconcretefactory.cc | 54 ++---- src/tgba/tgbabddconcretefactory.hh | 10 +- src/tgba/tgbabddconcreteproduct.cc | 24 ++- src/tgba/tgbabddcoredata.cc | 34 +--- src/tgba/tgbabddcoredata.hh | 15 +- src/tgba/tgbabdddict.cc | 103 ----------- src/tgba/tgbabdddict.hh | 40 ---- src/tgba/tgbabddfactory.hh | 3 - src/tgba/tgbabddtranslatefactory.cc | 81 --------- src/tgba/tgbabddtranslatefactory.hh | 43 ----- src/tgba/tgbaexplicit.cc | 77 ++++---- src/tgba/tgbaexplicit.hh | 11 +- src/tgba/tgbaproduct.cc | 37 +--- src/tgba/tgbaproduct.hh | 6 +- src/tgba/tgbatranslateproxy.cc | 159 ---------------- src/tgba/tgbatranslateproxy.hh | 69 ------- src/tgbaalgos/lbtt.cc | 4 +- src/tgbaalgos/ltl2tgba.cc | 32 ++-- src/tgbaalgos/ltl2tgba.hh | 2 +- src/tgbaalgos/save.cc | 6 +- src/tgbaparse/public.hh | 2 + src/tgbaparse/tgbaparse.yy | 25 +-- src/tgbatest/explicit.cc | 39 ++-- src/tgbatest/explprod.cc | 7 +- src/tgbatest/ltl2tgba.cc | 16 +- src/tgbatest/ltlprod.cc | 6 +- src/tgbatest/mixprod.cc | 7 +- src/tgbatest/readsave.cc | 13 +- src/tgbatest/spotlbtt.cc | 7 +- src/tgbatest/tgbaread.cc | 13 +- src/tgbatest/tripprod.cc | 9 +- 52 files changed, 930 insertions(+), 1034 deletions(-) create mode 100644 src/misc/bddalloc.cc create mode 100644 src/misc/bddalloc.hh create mode 100644 src/tgba/bdddict.cc create mode 100644 src/tgba/bdddict.hh delete mode 100644 src/tgba/bddfactory.cc delete mode 100644 src/tgba/bddfactory.hh delete mode 100644 src/tgba/dictunion.cc delete mode 100644 src/tgba/dictunion.hh delete mode 100644 src/tgba/tgbabdddict.cc delete mode 100644 src/tgba/tgbabdddict.hh delete mode 100644 src/tgba/tgbabddtranslatefactory.cc delete mode 100644 src/tgba/tgbabddtranslatefactory.hh delete mode 100644 src/tgba/tgbatranslateproxy.cc delete mode 100644 src/tgba/tgbatranslateproxy.hh diff --git a/ChangeLog b/ChangeLog index 6357317ab..4cbf8daed 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,4 +1,77 @@ -2003-07-13 Alexandre Duret-Lutz +2003-07-14 Alexandre Duret-Lutz + + Before this change, all automata would construct their own + 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. + +2003-07-13 Alexandre Duret-Lutz * configure.ac: Bump version to 0.0e. diff --git a/iface/gspn/gspn.cc b/iface/gspn/gspn.cc index cd2b31ca7..a230563fc 100644 --- a/iface/gspn/gspn.cc +++ b/iface/gspn/gspn.cc @@ -4,7 +4,6 @@ #include "gspnlib.h" #include "gspn.hh" #include "ltlvisit/destroy.hh" -#include "tgba/bddfactory.hh" namespace spot { @@ -12,52 +11,59 @@ namespace spot // tgba_gspn_private_ ////////////////////////////////////////////////////////////////////// - struct tgba_gspn_private_ : public bdd_factory + struct tgba_gspn_private_ { int refs; // reference count - tgba_bdd_dict dict; + bdd_dict* dict; typedef std::pair ab_pair; typedef std::map prop_map; prop_map prop_dict; AtomicProp *all_indexes; size_t index_count; - tgba_gspn_private_(const gspn_environment& env) - : refs(0) + tgba_gspn_private_(bdd_dict* dict, const gspn_environment& env) + : refs(0), dict(dict) { const gspn_environment::prop_map& p = env.get_prop_map(); - for (gspn_environment::prop_map::const_iterator i = p.begin(); - i != p.end(); ++i) + try { - int var = create_node(); - i->second->ref(); - dict.var_map[i->second] = var; - dict.var_formula_map[var] = i->second; + for (gspn_environment::prop_map::const_iterator i = p.begin(); + i != p.end(); ++i) + { + int var = dict->register_proposition(i->second, this); + AtomicProp index; + int err = prop_index(i->first.c_str(), &index); + if (err) + throw gspn_exeption(err); + AtomicPropKind kind; + err = prop_kind(index, &kind); + if (err) + throw gspn_exeption(err); - AtomicProp index; - int err = prop_index(i->first.c_str(), &index); - if (err) - throw gspn_exeption(err); - AtomicPropKind kind; - err = prop_kind(index, &kind); - if (err) - throw gspn_exeption(err); + prop_dict[index] = ab_pair(kind, bdd_ithvar(var)); + } - prop_dict[index] = ab_pair(kind, ithvar(var)); + index_count = prop_dict.size(); + all_indexes = new AtomicProp[index_count]; + + unsigned idx = 0; + for (prop_map::const_iterator i = prop_dict.begin(); + i != prop_dict.end(); ++i) + all_indexes[idx++] = i->first; } - // If an exception occurs during the loop, dict will - // be cleaned and that will dereferenciate the formula - // it contains. No need to handle anything explicitely. + catch (...) + { + // If an exception occurs during the loop, we need to clean + // all BDD variables which have been registered so far. + dict->unregister_all_my_variables(this); + } + } - index_count = prop_dict.size(); - all_indexes = new AtomicProp[index_count]; - - unsigned idx = 0; - for (prop_map::const_iterator i = prop_dict.begin(); - i != prop_dict.end(); ++i) - all_indexes[idx++] = i->first; + tgba_gspn_private_::~tgba_gspn_private_() + { + dict->unregister_all_my_variables(this); } bdd index_to_bdd(AtomicProp index) const @@ -239,9 +245,9 @@ namespace spot ////////////////////////////////////////////////////////////////////// - tgba_gspn::tgba_gspn(const gspn_environment& env) + tgba_gspn::tgba_gspn(bdd_dict* dict, const gspn_environment& env) { - data_ = new tgba_gspn_private_(env); + data_ = new tgba_gspn_private_(dict, env); } tgba_gspn::tgba_gspn(const tgba_gspn& other) @@ -299,7 +305,7 @@ namespace spot return new tgba_succ_iterator_gspn(state_conds, s->get_state(), data_); } - const tgba_bdd_dict& + bdd_dict* tgba_gspn::get_dict() const { return data_->dict; diff --git a/iface/gspn/gspn.hh b/iface/gspn/gspn.hh index c2e225079..0be9967f2 100644 --- a/iface/gspn/gspn.hh +++ b/iface/gspn/gspn.hh @@ -2,7 +2,7 @@ # define SPOT_IFACE_GSPN_HH // Try not to include gspnlib.h here, or it will polute the user's -// namespace with internal C symbols. +// namespace with internal C symbols. # include # include "tgba/tgba.hh" @@ -20,7 +20,7 @@ namespace spot : err(err) { } - + int get_err() const { @@ -29,7 +29,7 @@ namespace spot private: int err; }; - + class gspn_environment : public ltl::environment { @@ -42,11 +42,11 @@ namespace spot bool declare(const std::string& prop_str); virtual ltl::formula* require(const std::string& prop_str); - + /// Get the name of the environment. virtual const std::string& name(); - typedef std::map prop_map; + typedef std::map prop_map; /// Get the map of atomic proposition known to this environment. const prop_map& get_prop_map() const; @@ -62,20 +62,20 @@ namespace spot class tgba_gspn: public tgba { public: - tgba_gspn(const gspn_environment& env); + tgba_gspn(bdd_dict* dict, const gspn_environment& env); tgba_gspn(const tgba_gspn& other); tgba_gspn& operator=(const tgba_gspn& other); virtual ~tgba_gspn(); virtual state* get_init_state() const; virtual tgba_succ_iterator* succ_iter(const state* state) const; - virtual const tgba_bdd_dict& get_dict() const; + virtual bdd_dict* get_dict() const; virtual std::string format_state(const state* state) const; virtual bdd all_accepting_conditions() const; virtual bdd neg_accepting_conditions() const; private: tgba_gspn_private_* data_; }; - + } #endif // SPOT_IFACE_GSPN_HH diff --git a/src/Makefile.am b/src/Makefile.am index 7fd5d8473..ac3f6e81c 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -9,6 +9,7 @@ lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = libspot_la_LDFLAGS = $(BUDDY_LDFLAGS) libspot_la_LIBADD = \ + misc/libmisc.la \ ltlenv/libltlenv.la \ ltlparse/libltlparse.la \ ltlvisit/libltlvisit.la \ diff --git a/src/misc/.cvsignore b/src/misc/.cvsignore index 051d1bd50..6e5ca7ed4 100644 --- a/src/misc/.cvsignore +++ b/src/misc/.cvsignore @@ -1,3 +1,6 @@ Makefile Makefile.in .deps +.libs +*.lo +*.la diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am index af56982b2..56b4be474 100644 --- a/src/misc/Makefile.am +++ b/src/misc/Makefile.am @@ -1,2 +1,12 @@ +AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) + miscdir = $(pkgincludedir)/misc -misc_HEADERS = const_sel.hh + +misc_HEADERS = \ + bddalloc.hh \ + const_sel.hh + +noinst_LTLIBRARIES = libmisc.la +libmisc_la_SOURCES = \ + bddalloc.cc diff --git a/src/misc/bddalloc.cc b/src/misc/bddalloc.cc new file mode 100644 index 000000000..e57d8d7dd --- /dev/null +++ b/src/misc/bddalloc.cc @@ -0,0 +1,123 @@ +#include +#include +#include "bddalloc.hh" + +namespace spot +{ + bool bdd_allocator::initialized = false; + int bdd_allocator::varnum = 2; + + bdd_allocator::bdd_allocator() + { + initialize(); + free_list.push_front(pos_lenght_pair(0, varnum)); + } + + void + bdd_allocator::initialize() + { + if (initialized) + return; + initialized = true; + bdd_init(50000, 5000); + bdd_setvarnum(varnum); + } + + int + bdd_allocator::allocate_variables(int n) + { + // Browse the free list until we find N consecutive variables. We + // try not to fragment the list my allocating the variables in the + // smallest free range we find. + free_list_type::iterator best = free_list.end(); + free_list_type::iterator cur; + for (cur = free_list.begin(); cur != free_list.end(); ++cur) + { + if (cur->second < n) + continue; + if (n == cur->second) + { + best = cur; + break; + } + if (best == free_list.end() + || cur->second < best->second) + best = cur; + } + + // We have found enough free variables. + if (best != free_list.end()) + { + int result = best->first; + best->second -= n; + assert(best->second >= 0); + // Erase the range if it's now empty. + if (best->second == 0) + free_list.erase(best); + else + best->first += n; + return result; + } + + // We haven't found enough adjacent free variables; + // ask BuDDy for some more. + + // If we already have some free variable at the end + // of the variable space, allocate just the difference. + if (free_list.size() > 0 + && free_list.back().first + free_list.back().second == varnum) + { + int res = free_list.back().first; + int endvar = free_list.back().second; + assert(n > endvar); + bdd_extvarnum(n - endvar); + varnum += n - endvar; + free_list.pop_back(); + return res; + } + else + { + // Otherwise, allocate as much variables as we need. + int res = varnum; + bdd_extvarnum(n); + varnum += n; + return res; + } + } + + void + bdd_allocator::release_variables(int base, int n) + { + free_list_type::iterator cur; + int end = base + n; + for (cur = free_list.begin(); cur != free_list.end(); ++cur) + { + // Append to a range ... + if (cur->first + cur->second == base) + { + cur->second += n; + // Maybe the next item on the list can be merged. + free_list_type::iterator next = cur; + ++next; + if (next != free_list.end() + && next->first == end) + { + cur->second += next->second; + free_list.erase(next); + } + return; + } + // ... or prepend to a range ... + if (cur->first == end) + { + cur->first -= n; + cur->second += n; + return; + } + // ... or insert a new range. + if (cur->first > end) + break; + } + free_list.insert(cur, pos_lenght_pair(base, n)); + } +} diff --git a/src/misc/bddalloc.hh b/src/misc/bddalloc.hh new file mode 100644 index 000000000..68b66a7e1 --- /dev/null +++ b/src/misc/bddalloc.hh @@ -0,0 +1,32 @@ +#ifndef SPOT_MISC_BDDALLOC_HH +# define SPOT_MISC_BDDALLOC_HH + +#include +#include + +namespace spot +{ + + /// Manage ranges of variables. + class bdd_allocator + { + protected: + /// Default constructor. + bdd_allocator(); + /// Initialize the BDD library. + static void initialize(); + /// Allocate \a n BDD variables. + int allocate_variables(int n); + /// Release \a n BDD variables starting at \a base. + void release_variables(int base, int n); + + static bool initialized; ///< Whether the BDD library has been initialized. + static int varnum; ///< number of variable in use in the BDD library. + typedef std::pair pos_lenght_pair; + typedef std::list free_list_type; + free_list_type free_list; ///< Tracks unused BDD variables. + }; + +} + +#endif // SPOT_MISC_BDDALLOC_HH diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 64711678c..24ec0d0cb 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -4,9 +4,8 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) tgbadir = $(pkgincludedir)/tgba tgba_HEADERS = \ - bddfactory.hh \ + bdddict.hh \ bddprint.hh \ - dictunion.hh \ public.hh \ state.hh \ statebdd.hh \ @@ -17,26 +16,19 @@ tgba_HEADERS = \ tgbabddconcretefactory.hh \ tgbabddconcreteproduct.hh \ tgbabddcoredata.hh \ - tgbabdddict.hh \ tgbabddfactory.hh \ - tgbabddtranslatefactory.hh \ tgbaexplicit.hh \ - tgbaproduct.hh \ - tgbatranslateproxy.hh + tgbaproduct.hh noinst_LTLIBRARIES = libtgba.la libtgba_la_SOURCES = \ - bddfactory.cc \ + bdddict.cc \ bddprint.cc \ - dictunion.cc \ statebdd.cc \ succiterconcrete.cc \ tgbabddconcrete.cc \ tgbabddconcretefactory.cc \ tgbabddconcreteproduct.cc \ tgbabddcoredata.cc \ - tgbabdddict.cc \ - tgbabddtranslatefactory.cc \ tgbaexplicit.cc \ - tgbaproduct.cc \ - tgbatranslateproxy.cc + tgbaproduct.cc diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc new file mode 100644 index 000000000..4b12092b0 --- /dev/null +++ b/src/tgba/bdddict.cc @@ -0,0 +1,271 @@ +#include +#include +#include +#include +#include "bdddict.hh" + +namespace spot +{ + bdd_dict::bdd_dict() + : bdd_allocator(), + next_to_now(bdd_newpair()), + now_to_next(bdd_newpair()) + { + } + + bdd_dict::~bdd_dict() + { + assert_emptiness(); + bdd_freepair(next_to_now); + bdd_freepair(now_to_next); + } + + int + bdd_dict::register_proposition(const ltl::formula* f, const void* for_me) + { + int num; + // Do not build a variable that already exists. + fv_map::iterator sii = var_map.find(f); + if (sii != var_map.end()) + { + num = sii->second; + } + else + { + f = clone(f); + num = allocate_variables(1); + var_map[f] = num; + var_formula_map[num] = f; + } + var_refs[num].insert(for_me); + return num; + } + + int + bdd_dict::register_state(const ltl::formula* f, const void* for_me) + { + int num; + // Do not build a state that already exists. + fv_map::iterator sii = now_map.find(f); + if (sii != now_map.end()) + { + num = sii->second; + } + else + { + f = ltl::clone(f); + num = allocate_variables(2); + now_map[f] = num; + now_formula_map[num] = f; + // Record that num+1 should be renamed as num when + // the next state becomes current. + bdd_setpair(next_to_now, num + 1, num); + bdd_setpair(now_to_next, num, num + 1); + } + var_refs[num].insert(for_me); + return num; + } + + int + bdd_dict::register_accepting_variable(const ltl::formula* f, + const void* for_me) + { + int num; + // Do not build an accepting variable that already exists. + fv_map::iterator sii = acc_map.find(f); + if (sii != acc_map.end()) + { + num = sii->second; + } + else + { + f = clone(f); + num = allocate_variables(1); + acc_map[f] = num; + acc_formula_map[num] = f; + } + var_refs[num].insert(for_me); + return num; + } + + void + bdd_dict::register_all_variables_of(const void* from_other, + const void* for_me) + { + vr_map::iterator i; + for (i = var_refs.begin(); i != var_refs.end(); ++i) + { + ref_set& s = i->second; + if (s.find(from_other) != s.end()) + s.insert(for_me); + } + } + + void + bdd_dict::unregister_all_my_variables(const void* me) + { + vr_map::iterator i; + for (i = var_refs.begin(); i != var_refs.end();) + { + // Increment i++ now, we will possibly erase + // the current node (which would invalidate the iterator). + vr_map::iterator cur = i++; + + ref_set& s = cur->second; + ref_set::iterator si = s.find(me); + if (si == s.end()) + continue; + s.erase(si); + if (! s.empty()) + continue; + // ME was the last user of this variable. + // Let's free it. First, we need to find + // if this is a Now, a Var, or an Acc variable. + int var = cur->first; + int n = 1; + const ltl::formula* f; + vf_map::iterator vi = var_formula_map.find(var); + if (vi != var_formula_map.end()) + { + f = vi->second; + var_map.erase(f); + var_formula_map.erase(vi); + } + else + { + vi = now_formula_map.find(var); + if (vi != now_formula_map.end()) + { + f = vi->second; + now_map.erase(f); + now_formula_map.erase(vi); + n = 2; + bdd_setpair(next_to_now, var + 1, var + 1); + bdd_setpair(now_to_next, var, var); + } + else + { + vi = acc_formula_map.find(var); + f = vi->second; + assert(vi != now_formula_map.end()); + acc_map.erase(f); + acc_formula_map.erase(vi); + } + } + // Actually release the associated BDD variables, and the + // formula itself. + release_variables(var, n); + ltl::destroy(f); + var_refs.erase(cur); + } + } + + bool + bdd_dict::is_registered(const ltl::formula* f, const void* by_me) + { + int var; + fv_map::iterator fi = var_map.find(f); + if (fi != var_map.end()) + { + var = fi->second; + } + else + { + fi = now_map.find(f); + if (fi != now_map.end()) + { + var = fi->second; + } + else + { + fi = acc_map.find(f); + if (fi == acc_map.end()) + return false; + var = fi->second; + } + } + ref_set& s = var_refs[var]; + return s.find(by_me) != s.end(); + } + + std::ostream& + bdd_dict::dump(std::ostream& os) const + { + fv_map::const_iterator fi; + os << "Atomic Propositions:" << std::endl; + for (fi = var_map.begin(); fi != var_map.end(); ++fi) + { + os << " " << fi->second << " (x" + << var_refs.find(fi->second)->second.size() << "): "; + to_string(fi->first, os) << std::endl; + } + os << "States:" << std::endl; + for (fi = now_map.begin(); fi != now_map.end(); ++fi) + { + int refs = var_refs.find(fi->second)->second.size(); + os << " " << fi->second << " (x" << refs << "): Now["; + to_string(fi->first, os) << "]" << std::endl; + os << " " << fi->second + 1 << " (x" << refs << "): Next["; + to_string(fi->first, os) << "]" << std::endl; + } + os << "Accepting Conditions:" << std::endl; + for (fi = acc_map.begin(); fi != acc_map.end(); ++fi) + { + os << " " << fi->second << " (x" + << var_refs.find(fi->second)->second.size() << "): Acc["; + to_string(fi->first, os) << "]" << std::endl; + } + os << "Free list:" << std::endl; + free_list_type::const_iterator i; + for (i = free_list.begin(); i != free_list.end(); ++i) + os << " (" << i->first << ", " << i->second << ")"; + os << std::endl; + return os; + } + + void + bdd_dict::assert_emptiness() const + { + bool fail = false; + if (var_map.empty() + && now_map.empty() + && acc_map.empty()) + { + if (! var_formula_map.empty()) + { + std::cerr << "var_map is empty but var_formula_map is not" + << std::endl; + fail = true; + } + if (! now_formula_map.empty()) + { + std::cerr << "now_map is empty but now_formula_map is not" + << std::endl; + fail = true; + } + if (! acc_formula_map.empty()) + { + std::cerr << "acc_map is empty but acc_formula_map is not" + << std::endl; + fail = true; + } + if (! var_refs.empty()) + { + std::cerr << "maps are empty but var_refs is not" << std::endl; + fail = true; + vr_map::const_iterator i; + for (i = var_refs.begin(); i != var_refs.end(); ++i) + std::cerr << " " << i->first << ":" << i->second.size(); + std::cerr << std::endl; + } + if (! fail) + return; + } + else + { + std::cerr << "some maps are not empty" << std::endl; + } + dump(std::cerr); + assert(0); + } +} diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh new file mode 100644 index 000000000..a0a8a10a0 --- /dev/null +++ b/src/tgba/bdddict.hh @@ -0,0 +1,122 @@ +#ifndef SPOT_TGBA_BDDDICT_HH +# define SPOT_TGBA_BDDDICT_HH + +#include +#include +#include +#include +#include +#include "ltlast/formula.hh" +#include "misc/bddalloc.hh" + +namespace spot +{ + + /// Map BDD variables to formulae. + class bdd_dict: public bdd_allocator + { + public: + + bdd_dict(); + ~bdd_dict(); + + /// Formula-to-BDD-variable maps. + typedef std::map fv_map; + /// BDD-variable-to-formula maps. + typedef std::map vf_map; + + fv_map now_map; ///< Maps formulae to "Now" BDD variables + vf_map now_formula_map; ///< Maps "Now" BDD variables to formulae + fv_map var_map; ///< Maps atomic propisitions to BDD variables + vf_map var_formula_map; ///< Maps BDD variables to atomic propisitions + fv_map acc_map; ///< Maps accepting conditions to BDD variables + vf_map acc_formula_map; ///< Maps BDD variables to accepting conditions + + /// \brief Map Next variables to Now variables. + /// + /// Use with BuDDy's bdd_replace() function. + bddPair* next_to_now; + /// \brief Map Now variables to Next variables. + /// + /// Use with BuDDy's bdd_replace() function. + bddPair* now_to_next; + + /// \brief Register an atomic proposition. + /// + /// Return (and maybe allocate) a BDD variable designating formula + /// \a f. The \a for_me argument should point to the object using + /// this BDD variable, this is used for reference counting. It is + /// perfectly safe to call this function several time with the same + /// arguments. + /// + /// \return The variable number. Use bdd_ithvar() or bdd_nithvar() + /// to convert this to a BDD. + int register_proposition(const ltl::formula* f, const void* for_me); + + /// \brief Register a couple of Now/Next variables + /// + /// Return (and maybe allocate) two BDD variables for a state + /// associated to formula \a f. The \a for_me argument should point + /// to the object using this BDD variable, this is used for + /// reference counting. It is perfectly safe to call this + /// function several time with the same arguments. + /// + /// \return The first variable number. Add one to get the second + /// variable. Use bdd_ithvar() or bdd_nithvar() to convert this + /// to a BDD. + int register_state(const ltl::formula* f, const void* for_me); + + /// \brief Register an atomic proposition. + /// + /// Return (and maybe allocate) a BDD variable designating an + /// accepting set associated to formula \a f. The \a for_me + /// argument should point to the object using this BDD variable, + /// this is used for reference counting. It is perfectly safe to + /// call this function several time with the same arguments. + /// + /// \return The variable number. Use bdd_ithvar() or bdd_nithvar() + /// to convert this to a BDD. + int register_accepting_variable(const ltl::formula* f, const void* for_me); + + /// \brief Duplicate the variable usage of another object. + /// + /// This tells this dictionary that the \a for_me object + /// will be using the same BDD variables as the \a from_other objects. + /// This ensure that the variables won't be freed when \a from_other + /// is deleted if \a from_other is still alive. + void register_all_variables_of(const void* from_other, const void* for_me); + + /// \brief Release the variables used by object. + /// + /// Usually called in the destructor if \a me. + void unregister_all_my_variables(const void* me); + + /// Check whether formula \a f has already been registered by \a by_me. + bool is_registered(const ltl::formula* f, const void* by_me); + + /// \brief Dump all variables for debugging. + /// \param os The output stream. + std::ostream& dump(std::ostream& os) const; + + /// \brief Make sure the dictionary is empty. + /// + /// This will print diagnostics and abort if the dictionary + /// is not empty. Use for debugging. + void assert_emptiness() const; + + protected: + /// BDD-variable reference counts. + typedef std::set ref_set; + typedef std::map vr_map; + vr_map var_refs; + + private: + // Disallow copy. + bdd_dict(const bdd_dict& other); + bdd_dict& operator=(const bdd_dict& other); + }; + + +} + +#endif // SPOT_TGBA_BDDDICT_HH diff --git a/src/tgba/bddfactory.cc b/src/tgba/bddfactory.cc deleted file mode 100644 index 5bef3476f..000000000 --- a/src/tgba/bddfactory.cc +++ /dev/null @@ -1,48 +0,0 @@ -#include "bddfactory.hh" - -namespace spot -{ - bdd_factory::bdd_factory() - : varused(0) - { - initialize(); - } - - int - bdd_factory::create_node() - { - return create_nodes(1); - } - - int - bdd_factory::create_pair() - { - return create_nodes(2); - } - - int - bdd_factory::create_nodes(int i) - { - int res = varused; - varused += i; - if (varnum < varused) - { - bdd_extvarnum(varused - varnum); - varnum = varused; - } - return res; - } - - void - bdd_factory::initialize() - { - if (initialized) - return; - initialized = true; - bdd_init(50000, 5000); - bdd_setvarnum(varnum); - } - - bool bdd_factory::initialized = false; - int bdd_factory::varnum = 2; -} diff --git a/src/tgba/bddfactory.hh b/src/tgba/bddfactory.hh deleted file mode 100644 index bde475499..000000000 --- a/src/tgba/bddfactory.hh +++ /dev/null @@ -1,60 +0,0 @@ -#ifndef SPOT_TGBA_BDDFACTORY_HH -# define SPOT_TGBA_BDDFACTORY_HH - -#include - -namespace spot -{ - - /// \brief Help construct BDDs by reusing existing variables. - /// - /// Spot uses BuDDy as BDD library, and BuDDy needs to - /// know the number of BDD variables in use. As a rule - /// of thumb: the more BDD variables the slowere. So - /// creating new BDD variables each time we build a new - /// Automata won't do. - /// - /// To avoid variable explosion, we reuse existing variables - /// when building new automata, and only allocate new variables - /// when we ran out of existing variables. This class helps - /// reusing variables this way. - /// - /// Using the same variables in different automata is not a - /// problem until an operation is performed on both automata. - /// In this case some homogenization of BDD variable will be - /// required. Such operation is out of the scope of this class. - class bdd_factory - { - public: - bdd_factory(); - - /// \brief Allocate a BDD variable. - /// - /// The returned integer can be converted to a BDD using ithvar(). - int create_node(); - - /// \brief Allocate a pair BDD variable. - /// - /// The returned integer is the first variable of the pair, - /// it's successor (i.e., n + 1) is the second variable. - /// They can be converted to BDDs using ithvar(). - int create_pair(); - - /// Convert a variable number into a BDD. - static bdd - ithvar(int i) - { - return bdd_ithvar(i); - } - - protected: - static void initialize(); ///< Initialize the BDD library. - int create_nodes(int i); ///< Create \a i variables. - - static bool initialized; ///< Whether the BDD library has been initialized. - static int varnum; ///< number of variable in use in the BDD library. - int varused; ///< Number of variables used for this construction. - }; -} - -#endif // SPOT_TGBA_BDDFACTORY_HH diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc index e8fe12288..09be5ab18 100644 --- a/src/tgba/bddprint.cc +++ b/src/tgba/bddprint.cc @@ -6,7 +6,7 @@ namespace spot { /// Global dictionary used by print_handler() to lookup variables. - static const tgba_bdd_dict* dict; + static const bdd_dict* dict; /// Global flag to enable Acc[x] output (instead of `x'). static bool want_acc; @@ -15,7 +15,7 @@ namespace spot static void print_handler(std::ostream& o, int var) { - tgba_bdd_dict::vf_map::const_iterator isi = + bdd_dict::vf_map::const_iterator isi = dict->var_formula_map.find(var); if (isi != dict->var_formula_map.end()) to_string(isi->second, o); @@ -80,9 +80,9 @@ namespace spot } std::ostream& - bdd_print_sat(std::ostream& os, const tgba_bdd_dict& d, bdd b) + bdd_print_sat(std::ostream& os, const bdd_dict* d, bdd b) { - dict = &d; + dict = d; where = &os; want_acc = false; assert(bdd_satone(b) == b); @@ -106,9 +106,9 @@ namespace spot } std::ostream& - bdd_print_acc(std::ostream& os, const tgba_bdd_dict& d, bdd b) + bdd_print_acc(std::ostream& os, const bdd_dict* d, bdd b) { - dict = &d; + dict = d; where = &os; want_acc = false; bdd_allsat(b, print_acc_handler); @@ -116,7 +116,7 @@ namespace spot } std::string - bdd_format_sat(const tgba_bdd_dict& d, bdd b) + bdd_format_sat(const bdd_dict* d, bdd b) { std::ostringstream os; bdd_print_sat(os, d, b); @@ -124,9 +124,9 @@ namespace spot } std::ostream& - bdd_print_set(std::ostream& os, const tgba_bdd_dict& d, bdd b) + bdd_print_set(std::ostream& os, const bdd_dict* d, bdd b) { - dict = &d; + dict = d; want_acc = true; bdd_strm_hook(print_handler); os << bddset << b; @@ -135,7 +135,7 @@ namespace spot } std::string - bdd_format_set(const tgba_bdd_dict& d, bdd b) + bdd_format_set(const bdd_dict* d, bdd b) { std::ostringstream os; bdd_print_set(os, d, b); @@ -143,9 +143,9 @@ namespace spot } std::ostream& - bdd_print_dot(std::ostream& os, const tgba_bdd_dict& d, bdd b) + bdd_print_dot(std::ostream& os, const bdd_dict* d, bdd b) { - dict = &d; + dict = d; want_acc = true; bdd_strm_hook(print_handler); os << bdddot << b; @@ -154,9 +154,9 @@ namespace spot } std::ostream& - bdd_print_table(std::ostream& os, const tgba_bdd_dict& d, bdd b) + bdd_print_table(std::ostream& os, const bdd_dict* d, bdd b) { - dict = &d; + dict = d; want_acc = true; bdd_strm_hook(print_handler); os << bddtable << b; diff --git a/src/tgba/bddprint.hh b/src/tgba/bddprint.hh index 9408caddb..858e2c6e6 100644 --- a/src/tgba/bddprint.hh +++ b/src/tgba/bddprint.hh @@ -3,7 +3,7 @@ #include #include -#include "tgbabdddict.hh" +#include "bdddict.hh" #include namespace spot @@ -16,7 +16,7 @@ namespace spot /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. std::ostream& bdd_print_sat(std::ostream& os, - const tgba_bdd_dict& dict, bdd b); + const bdd_dict* dict, bdd b); /// \brief Format a BDD as a list of literals. /// @@ -24,7 +24,7 @@ namespace spot /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. /// \return The BDD formated as a string. - std::string bdd_format_sat(const tgba_bdd_dict& dict, bdd b); + std::string bdd_format_sat(const bdd_dict* dict, bdd b); /// \brief Print a BDD as a list of accepting conditions. /// @@ -34,33 +34,33 @@ namespace spot /// \param b The BDD to print. /// \return The BDD formated as a string. std::ostream& bdd_print_acc(std::ostream& os, - const tgba_bdd_dict& dict, bdd b); + const bdd_dict* dict, bdd b); /// \brief Print a BDD as a set. /// \param os The output stream. /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. std::ostream& bdd_print_set(std::ostream& os, - const tgba_bdd_dict& dict, bdd b); + const bdd_dict* dict, bdd b); /// \brief Format a BDD as a set. /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. /// \return The BDD formated as a string. - std::string bdd_format_set(const tgba_bdd_dict& dict, bdd b); + std::string bdd_format_set(const bdd_dict* dict, bdd b); /// \brief Print a BDD as a diagram in dotty format. /// \param os The output stream. /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. std::ostream& bdd_print_dot(std::ostream& os, - const tgba_bdd_dict& dict, bdd b); + const bdd_dict* dict, bdd b); /// \brief Print a BDD as a table. /// \param os The output stream. /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. std::ostream& bdd_print_table(std::ostream& os, - const tgba_bdd_dict& dict, bdd b); + const bdd_dict* dict, bdd b); } diff --git a/src/tgba/dictunion.cc b/src/tgba/dictunion.cc deleted file mode 100644 index 5c745db92..000000000 --- a/src/tgba/dictunion.cc +++ /dev/null @@ -1,80 +0,0 @@ -#include -#include "dictunion.hh" -#include "ltlvisit/clone.hh" -#include -#include - -namespace spot -{ - - tgba_bdd_dict - tgba_bdd_dict_union(const tgba_bdd_dict& l, const tgba_bdd_dict& r) - { - std::set now; - std::set var; - std::set acc; - - tgba_bdd_dict::fv_map::const_iterator i; - - // Merge Now variables. - for (i = l.now_map.begin(); i != l.now_map.end(); ++i) - now.insert(i->first); - for (i = r.now_map.begin(); i != r.now_map.end(); ++i) - now.insert(i->first); - - // Merge atomic propositions. - for (i = l.var_map.begin(); i != l.var_map.end(); ++i) - var.insert(i->first); - for (i = r.var_map.begin(); i != r.var_map.end(); ++i) - var.insert(i->first); - - // Merge accepting conditions. - for (i = l.acc_map.begin(); i != l.acc_map.end(); ++i) - acc.insert(i->first); - for (i = r.acc_map.begin(); i != r.acc_map.end(); ++i) - acc.insert(i->first); - - // Ensure we have enough BDD variables. - int have = bdd_extvarnum(0); - int want = now.size() * 2 + var.size() + acc.size(); - if (have < want) - bdd_setvarnum(want); - - // Fill in the "defragmented" union dictionary. - - // FIXME: Make some experiments with ordering of acc/var/now variables. - // Maybe there is one order that usually produces smaller BDDs? - - // Next BDD variable to use. - int v = 0; - - tgba_bdd_dict res; - - std::set::const_iterator f; - for (f = acc.begin(); f != acc.end(); ++f) - { - clone(*f); - res.acc_map[*f] = v; - res.acc_formula_map[v] = *f; - ++v; - } - for (f = var.begin(); f != var.end(); ++f) - { - clone(*f); - res.var_map[*f] = v; - res.var_formula_map[v] = *f; - ++v; - } - for (f = now.begin(); f != now.end(); ++f) - { - clone(*f); - res.now_map[*f] = v; - res.now_formula_map[v] = *f; - v += 2; - } - - assert (v == want); - return res; - } - -} diff --git a/src/tgba/dictunion.hh b/src/tgba/dictunion.hh deleted file mode 100644 index cc03d1f34..000000000 --- a/src/tgba/dictunion.hh +++ /dev/null @@ -1,13 +0,0 @@ -#ifndef SPOT_TGBA_DICTUNION_HH -# define SPOT_TGBA_DICTUNION_HH - -#include "tgbabdddict.hh" - -namespace spot -{ - /// Build the union of two dictionaries. - tgba_bdd_dict - tgba_bdd_dict_union(const tgba_bdd_dict& l, const tgba_bdd_dict& r); -} - -#endif // SPOT_TGBA_DICTUNION_HH diff --git a/src/tgba/succiterconcrete.cc b/src/tgba/succiterconcrete.cc index 8dedbadb6..91c34a78c 100644 --- a/src/tgba/succiterconcrete.cc +++ b/src/tgba/succiterconcrete.cc @@ -140,7 +140,7 @@ namespace spot // successor (a dead node) and we can skip it. We need to // compute current_state_ anyway, so this test costs us nothing. assert(dest == bdd_exist(current_, data_.notnext_set)); - current_state_ = bdd_replace(dest, data_.next_to_now); + current_state_ = bdd_replace(dest, data_.dict->next_to_now); } while ((current_state_ & data_.relation) == bddfalse); } diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index be7cc723f..f3ee66368 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -3,7 +3,7 @@ #include "state.hh" #include "succiter.hh" -#include "tgbabdddict.hh" +#include "bdddict.hh" namespace spot { @@ -64,7 +64,7 @@ namespace spot /// This is useful when dealing with several automata (which /// may use the same BDD variable for different formula), /// or simply when printing. - virtual const tgba_bdd_dict& get_dict() const = 0; + virtual bdd_dict* get_dict() const = 0; /// \brief Format the state as a string for printing. /// diff --git a/src/tgba/tgbabddconcrete.cc b/src/tgba/tgbabddconcrete.cc index 0b68839c5..8cc3a7c5a 100644 --- a/src/tgba/tgbabddconcrete.cc +++ b/src/tgba/tgbabddconcrete.cc @@ -5,18 +5,21 @@ namespace spot { tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact) - : data_(fact.get_core_data()), dict_(fact.get_dict()) + : data_(fact.get_core_data()) { + get_dict()->register_all_variables_of(&fact, this); } tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init) - : data_(fact.get_core_data()), dict_(fact.get_dict()) + : data_(fact.get_core_data()) { + get_dict()->register_all_variables_of(&fact, this); set_init_state(init); } tgba_bdd_concrete::~tgba_bdd_concrete() { + get_dict()->unregister_all_my_variables(this); } void @@ -81,13 +84,13 @@ namespace spot { const state_bdd* s = dynamic_cast(state); assert(s); - return bdd_format_set(dict_, s->as_bdd()); + return bdd_format_set(get_dict(), s->as_bdd()); } - const tgba_bdd_dict& + bdd_dict* tgba_bdd_concrete::get_dict() const { - return dict_; + return data_.dict; } bdd diff --git a/src/tgba/tgbabddconcrete.hh b/src/tgba/tgbabddconcrete.hh index 29ad84436..788462979 100644 --- a/src/tgba/tgbabddconcrete.hh +++ b/src/tgba/tgbabddconcrete.hh @@ -43,7 +43,7 @@ namespace spot std::string format_state(const state* state) const; - const tgba_bdd_dict& get_dict() const; + bdd_dict* get_dict() const; /// \brief Get the core data associated to this automaton. /// @@ -57,7 +57,6 @@ namespace spot protected: tgba_bdd_core_data data_; ///< Core data associated to the automaton. - tgba_bdd_dict dict_; ///< Dictionary used by the automaton. bdd init_; ///< Initial state. }; } diff --git a/src/tgba/tgbabddconcretefactory.cc b/src/tgba/tgbabddconcretefactory.cc index d7101f50d..f9ee4337c 100644 --- a/src/tgba/tgbabddconcretefactory.cc +++ b/src/tgba/tgbabddconcretefactory.cc @@ -3,8 +3,8 @@ #include "tgbabddconcretefactory.hh" namespace spot { - tgba_bdd_concrete_factory::tgba_bdd_concrete_factory() - : now_to_next_(bdd_newpair()) + tgba_bdd_concrete_factory::tgba_bdd_concrete_factory(bdd_dict* dict) + : data_(dict) { } @@ -13,50 +13,26 @@ namespace spot acc_map_::iterator ai; for (ai = acc_.begin(); ai != acc_.end(); ++ai) destroy(ai->first); + get_dict()->unregister_all_my_variables(this); } int tgba_bdd_concrete_factory::create_state(const ltl::formula* f) { - // Do not build a state that already exists. - tgba_bdd_dict::fv_map::iterator sii = dict_.now_map.find(f); - if (sii != dict_.now_map.end()) - return sii->second; - - f = clone(f); - - int num = create_pair(); - dict_.now_map[f] = num; - dict_.now_formula_map[num] = f; - - // Record that num+1 should be renamed as num when - // the next state becomes current. - bdd_setpair(data_.next_to_now, num + 1, num); - bdd_setpair(now_to_next_, num, num + 1); - + int num = get_dict()->register_state(f, this); // Keep track of all "Now" variables for easy // existential quantification. - data_.declare_now_next (ithvar(num), ithvar(num + 1)); + data_.declare_now_next (bdd_ithvar(num), bdd_ithvar(num + 1)); return num; } int tgba_bdd_concrete_factory::create_atomic_prop(const ltl::formula* f) { - // Do not build a variable that already exists. - tgba_bdd_dict::fv_map::iterator sii = dict_.var_map.find(f); - if (sii != dict_.var_map.end()) - return sii->second; - - f = clone(f); - - int num = create_node(); - dict_.var_map[f] = num; - dict_.var_formula_map[num] = f; - + int num = get_dict()->register_proposition(f, this); // Keep track of all atomic proposition for easy // existential quantification. - data_.declare_atomic_prop(ithvar(num)); + data_.declare_atomic_prop(bdd_ithvar(num)); return num; } @@ -86,18 +62,14 @@ namespace spot for (ai = acc_.begin(); ai != acc_.end(); ++ai) { // Register a BDD variable for this accepting condition. - int a = create_node(); - const ltl::formula* f = clone(ai->first); // The associated formula. - dict_.acc_map[f] = a; - dict_.acc_formula_map[a] = f; - bdd acc = ithvar(a); + int num = get_dict()->register_accepting_variable(ai->first, this); // Keep track of all accepting conditions for easy // existential quantification. - data_.declare_accepting_condition(acc); + data_.declare_accepting_condition(bdd_ithvar(num)); } for (ai = acc_.begin(); ai != acc_.end(); ++ai) { - bdd acc = ithvar(dict_.acc_map[ai->first]); + bdd acc = bdd_ithvar(get_dict()->acc_map[ai->first]); // Complete acc with all the other accepting conditions negated. acc &= bdd_exist(data_.negacc_set, acc); @@ -119,7 +91,7 @@ namespace spot // state: the combination exists but won't allow further exploration // because it fails the constraints.) data_.relation &= bdd_replace(bdd_exist(data_.relation, data_.notnow_set), - now_to_next_); + get_dict()->now_to_next); } const tgba_bdd_core_data& @@ -128,10 +100,10 @@ namespace spot return data_; } - const tgba_bdd_dict& + bdd_dict* tgba_bdd_concrete_factory::get_dict() const { - return dict_; + return data_.dict; } void diff --git a/src/tgba/tgbabddconcretefactory.hh b/src/tgba/tgbabddconcretefactory.hh index a8c180868..45bd89ed5 100644 --- a/src/tgba/tgbabddconcretefactory.hh +++ b/src/tgba/tgbabddconcretefactory.hh @@ -2,17 +2,16 @@ # define SPOT_TGBA_TGBABDDCONCRETEFACTORY_HH #include "ltlast/formula.hh" -#include "bddfactory.hh" #include "tgbabddfactory.hh" #include namespace spot { /// Helper class to build a spot::tgba_bdd_concrete object. - class tgba_bdd_concrete_factory: public bdd_factory, public tgba_bdd_factory + class tgba_bdd_concrete_factory: public tgba_bdd_factory { public: - tgba_bdd_concrete_factory(); + tgba_bdd_concrete_factory(bdd_dict* dict); virtual ~tgba_bdd_concrete_factory(); @@ -50,7 +49,7 @@ namespace spot void declare_accepting_condition(bdd b, const ltl::formula* a); const tgba_bdd_core_data& get_core_data() const; - const tgba_bdd_dict& get_dict() const; + bdd_dict* get_dict() const; /// Add a new constraint to the relation. void constrain_relation(bdd new_rel); @@ -64,12 +63,9 @@ namespace spot private: tgba_bdd_core_data data_; ///< Core data for the new automata. - tgba_bdd_dict dict_; ///< Dictionary for the new automata. typedef std::map acc_map_; acc_map_ acc_; ///< BDD associated to each accepting condition - bddPair *now_to_next_; ///< \brief Rewriting pairs to transform - /// Now variables into Next variables. }; } diff --git a/src/tgba/tgbabddconcreteproduct.cc b/src/tgba/tgbabddconcreteproduct.cc index 135a6bdc9..5a6de7526 100644 --- a/src/tgba/tgbabddconcreteproduct.cc +++ b/src/tgba/tgbabddconcreteproduct.cc @@ -1,6 +1,5 @@ +#include #include "tgbabddconcreteproduct.hh" -#include "tgbabddtranslatefactory.hh" -#include "dictunion.hh" namespace spot { @@ -14,13 +13,13 @@ namespace spot public: tgba_bdd_product_factory(const tgba_bdd_concrete& left, const tgba_bdd_concrete& right) - : dict_(tgba_bdd_dict_union(left.get_dict(), - right.get_dict())), - fact_left_(left, dict_), - fact_right_(right, dict_), - data_(fact_left_.get_core_data(), fact_right_.get_core_data()), - init_(fact_left_.get_init_state() & fact_right_.get_init_state()) + : dict_(left.get_dict()), + left_(left), + right_(right), + data_(left_.get_core_data(), right_.get_core_data()), + init_(left_.get_init_bdd() & right_.get_init_bdd()) { + assert(dict_ == right.get_dict()); } virtual @@ -34,7 +33,7 @@ namespace spot return data_; } - const tgba_bdd_dict& + bdd_dict* get_dict() const { return dict_; @@ -47,9 +46,9 @@ namespace spot } private: - tgba_bdd_dict dict_; - tgba_bdd_translate_factory fact_left_; - tgba_bdd_translate_factory fact_right_; + bdd_dict* dict_; + const tgba_bdd_concrete& left_; + const tgba_bdd_concrete& right_; tgba_bdd_core_data data_; bdd init_; }; @@ -57,7 +56,6 @@ namespace spot tgba_bdd_concrete product(const tgba_bdd_concrete& left, const tgba_bdd_concrete& right) { - tgba_bdd_product_factory p(left, right); return tgba_bdd_concrete(p, p.get_init_state()); } diff --git a/src/tgba/tgbabddcoredata.cc b/src/tgba/tgbabddcoredata.cc index 0c0a0d010..b172b9f73 100644 --- a/src/tgba/tgbabddcoredata.cc +++ b/src/tgba/tgbabddcoredata.cc @@ -1,8 +1,9 @@ +#include #include "tgbabddcoredata.hh" namespace spot { - tgba_bdd_core_data::tgba_bdd_core_data() + tgba_bdd_core_data::tgba_bdd_core_data(bdd_dict* dict) : relation(bddtrue), accepting_conditions(bddfalse), all_accepting_conditions(bddfalse), @@ -17,7 +18,7 @@ namespace spot acc_set(bddtrue), notacc_set(bddtrue), negacc_set(bddtrue), - next_to_now(bdd_newpair()) + dict(dict) { } @@ -36,7 +37,7 @@ namespace spot acc_set(copy.acc_set), notacc_set(copy.notacc_set), negacc_set(copy.negacc_set), - next_to_now(bdd_copypair(copy.next_to_now)) + dict(copy.dict) { } @@ -59,8 +60,9 @@ namespace spot acc_set(left.acc_set & right.acc_set), notacc_set(left.notacc_set & right.notacc_set), negacc_set(left.negacc_set & right.negacc_set), - next_to_now(bdd_mergepairs(left.next_to_now, right.next_to_now)) + dict(left.dict) { + assert(dict == right.dict); } const tgba_bdd_core_data& @@ -74,11 +76,6 @@ namespace spot return *this; } - tgba_bdd_core_data::~tgba_bdd_core_data() - { - bdd_freepair(next_to_now); - } - void tgba_bdd_core_data::declare_now_next(bdd now, bdd next) { @@ -112,23 +109,4 @@ namespace spot acc_set &= acc; negacc_set &= !acc; } - - void - tgba_bdd_core_data::translate(bddPair* rewrite) - { - relation = bdd_replace(relation, rewrite); - accepting_conditions = bdd_replace(accepting_conditions, rewrite); - all_accepting_conditions = bdd_replace(all_accepting_conditions, rewrite); - now_set = bdd_replace(now_set, rewrite); - next_set = bdd_replace(next_set, rewrite); - nownext_set = bdd_replace(nownext_set, rewrite); - notnow_set = bdd_replace(notnow_set, rewrite); - notnext_set = bdd_replace(notnext_set, rewrite); - notvar_set = bdd_replace(notvar_set, rewrite); - var_set = bdd_replace(var_set, rewrite); - varandnext_set = bdd_replace(varandnext_set, rewrite); - acc_set = bdd_replace(acc_set, rewrite); - notacc_set = bdd_replace(notacc_set, rewrite); - negacc_set = bdd_replace(negacc_set, rewrite); - } } diff --git a/src/tgba/tgbabddcoredata.hh b/src/tgba/tgbabddcoredata.hh index e2eea8d42..46e70ac72 100644 --- a/src/tgba/tgbabddcoredata.hh +++ b/src/tgba/tgbabddcoredata.hh @@ -2,6 +2,7 @@ # define SPOT_TGBA_TGBABDDCOREDATA_HH #include +#include "bdddict.hh" namespace spot { @@ -92,13 +93,13 @@ namespace spot /// conditions. bdd negacc_set; - /// Record pairings between Next and Now variables. - bddPair* next_to_now; + /// The dictionary used by the automata. + bdd_dict* dict; /// \brief Default constructor. /// /// Initially all variable set are empty and the \c relation is true. - tgba_bdd_core_data(); + tgba_bdd_core_data(bdd_dict* dict); /// Copy constructor. tgba_bdd_core_data(const tgba_bdd_core_data& copy); @@ -111,8 +112,6 @@ namespace spot const tgba_bdd_core_data& operator= (const tgba_bdd_core_data& copy); - ~tgba_bdd_core_data(); - /// \brief Update the variable sets to take a new pair of variables into /// account. void declare_now_next(bdd now, bdd next); @@ -122,12 +121,6 @@ namespace spot /// \brief Update the variable sets to take a new accepting condition /// into account. void declare_accepting_condition(bdd prom); - - /// \brief Translate BDD variables. - /// - /// Rewrite the variables according to \a rewrite. - /// This used by spot::tgba_bdd_translate_factory. - void translate(bddPair* rewrite); }; } diff --git a/src/tgba/tgbabdddict.cc b/src/tgba/tgbabdddict.cc deleted file mode 100644 index d21a2cb10..000000000 --- a/src/tgba/tgbabdddict.cc +++ /dev/null @@ -1,103 +0,0 @@ -#include "tgbabdddict.hh" -#include "ltlvisit/tostring.hh" -#include "ltlvisit/clone.hh" -#include "ltlvisit/destroy.hh" - -namespace spot -{ - std::ostream& - tgba_bdd_dict::dump(std::ostream& os) const - { - fv_map::const_iterator sii; - os << "Atomic Propositions:" << std::endl; - for (sii = var_map.begin(); sii != var_map.end(); ++sii) - { - os << " " << sii->second << ": "; - to_string(sii->first, os) << std::endl; - } - os << "States:" << std::endl; - for (sii = now_map.begin(); sii != now_map.end(); ++sii) - { - os << " " << sii->second << ": Now["; - to_string(sii->first, os) << "]" << std::endl; - os << " " << sii->second + 1 << ": Next["; - to_string(sii->first, os) << "]" << std::endl; - } - os << "Accepting Conditions:" << std::endl; - for (sii = acc_map.begin(); sii != acc_map.end(); ++sii) - { - os << " " << sii->second << ": "; - to_string(sii->first, os) << std::endl; - } - return os; - } - - bool - tgba_bdd_dict::contains(const tgba_bdd_dict& other) const - { - fv_map::const_iterator i; - for (i = other.var_map.begin(); i != other.var_map.end(); ++i) - { - fv_map::const_iterator i2 = var_map.find(i->first); - if (i2 == var_map.end() || i->second != i2->second) - return false; - } - for (i = other.now_map.begin(); i != other.now_map.end(); ++i) - { - fv_map::const_iterator i2 = now_map.find(i->first); - if (i2 == now_map.end() || i->second != i2->second) - return false; - } - for (i = other.acc_map.begin(); i != other.acc_map.end(); ++i) - { - fv_map::const_iterator i2 = acc_map.find(i->first); - if (i2 == acc_map.end() || i->second != i2->second) - return false; - } - return true; - } - - tgba_bdd_dict::tgba_bdd_dict() - { - } - - tgba_bdd_dict::tgba_bdd_dict(const tgba_bdd_dict& other) - : now_map(other.now_map), - now_formula_map(other.now_formula_map), - var_map(other.var_map), - var_formula_map(other.var_formula_map), - acc_map(other.acc_map), - acc_formula_map(other.acc_formula_map) - { - fv_map::iterator i; - for (i = now_map.begin(); i != now_map.end(); ++i) - ltl::clone(i->first); - for (i = var_map.begin(); i != var_map.end(); ++i) - ltl::clone(i->first); - for (i = acc_map.begin(); i != acc_map.end(); ++i) - ltl::clone(i->first); - } - - tgba_bdd_dict& - tgba_bdd_dict::operator=(const tgba_bdd_dict& other) - { - if (this != &other) - { - this->~tgba_bdd_dict(); - new (this) tgba_bdd_dict(other); - } - return *this; - } - - tgba_bdd_dict::~tgba_bdd_dict() - { - fv_map::iterator i; - for (i = now_map.begin(); i != now_map.end(); ++i) - ltl::destroy(i->first); - for (i = var_map.begin(); i != var_map.end(); ++i) - ltl::destroy(i->first); - for (i = acc_map.begin(); i != acc_map.end(); ++i) - ltl::destroy(i->first); - } - -} diff --git a/src/tgba/tgbabdddict.hh b/src/tgba/tgbabdddict.hh deleted file mode 100644 index 97a51fc22..000000000 --- a/src/tgba/tgbabdddict.hh +++ /dev/null @@ -1,40 +0,0 @@ -#ifndef SPOT_TGBA_TGBABDDDICT_H -# define SPOT_TGBA_TGBABDDDICT_H - -#include -#include -#include "ltlast/formula.hh" - -namespace spot -{ - - /// Dictionary of BDD variables. - struct tgba_bdd_dict - { - /// Formula-to-BDD-variable maps. - typedef std::map fv_map; - /// BDD-variable-to-formula maps. - typedef std::map vf_map; - - fv_map now_map; ///< Maps formulae to "Now" BDD variables - vf_map now_formula_map; ///< Maps "Now" BDD variables to formulae - fv_map var_map; ///< Maps atomic propisitions to BDD variables - vf_map var_formula_map; ///< Maps BDD variables to atomic propisitions - fv_map acc_map; ///< Maps accepting conditions to BDD variables - vf_map acc_formula_map; ///< Maps BDD variables to accepting conditions - - /// \brief Dump all variables for debugging. - /// \param os The output stream. - std::ostream& dump(std::ostream& os) const; - - /// Whether this dictionary contains \a other. - bool contains(const tgba_bdd_dict& other) const; - - tgba_bdd_dict(); - tgba_bdd_dict(const tgba_bdd_dict& other); - tgba_bdd_dict& operator=(const tgba_bdd_dict& other); - ~tgba_bdd_dict(); - }; -} - -#endif // SPOT_TGBA_TGBABDDDICT_H diff --git a/src/tgba/tgbabddfactory.hh b/src/tgba/tgbabddfactory.hh index d6e260b6f..75233ee80 100644 --- a/src/tgba/tgbabddfactory.hh +++ b/src/tgba/tgbabddfactory.hh @@ -2,7 +2,6 @@ # define SPOT_TGBA_TGBABDDFACTORY_H #include "tgbabddcoredata.hh" -#include "tgbabdddict.hh" namespace spot { @@ -15,8 +14,6 @@ namespace spot public: /// Get the core data for the new automata. virtual const tgba_bdd_core_data& get_core_data() const = 0; - /// Get the dictionary for the new automata. - virtual const tgba_bdd_dict& get_dict() const = 0; }; } diff --git a/src/tgba/tgbabddtranslatefactory.cc b/src/tgba/tgbabddtranslatefactory.cc deleted file mode 100644 index 506c0e39f..000000000 --- a/src/tgba/tgbabddtranslatefactory.cc +++ /dev/null @@ -1,81 +0,0 @@ -#include "tgbabddtranslatefactory.hh" -#include "dictunion.hh" -#include - -namespace spot -{ - tgba_bdd_translate_factory::tgba_bdd_translate_factory - (const tgba_bdd_concrete& from, const tgba_bdd_dict& to) - : data_(from.get_core_data()), dict_(to) - { - bddPair* rewrite = compute_pairs(from.get_dict()); - data_.translate(rewrite); - init_ = bdd_replace(from.get_init_bdd(), rewrite); - bdd_freepair(rewrite); - } - - tgba_bdd_translate_factory::~tgba_bdd_translate_factory() - { - } - - bddPair* - tgba_bdd_translate_factory::compute_pairs(const tgba_bdd_dict& from) - { - bddPair* rewrite = bdd_newpair(); - - tgba_bdd_dict::fv_map::const_iterator i_from; - tgba_bdd_dict::fv_map::const_iterator i_to; - - for (i_from = from.now_map.begin(); i_from != from.now_map.end(); ++i_from) - { - i_to = dict_.now_map.find(i_from->first); - assert(i_to != dict_.now_map.end()); - bdd_setpair(rewrite, i_from->second, i_to->second); - bdd_setpair(rewrite, i_from->second + 1, i_to->second + 1); - bdd_setpair(data_.next_to_now, i_to->second + 1, i_to->second); - } - for (i_from = from.var_map.begin(); i_from != from.var_map.end(); ++i_from) - { - i_to = dict_.var_map.find(i_from->first); - assert(i_to != dict_.var_map.end()); - bdd_setpair(rewrite, i_from->second, i_to->second); - } - for (i_from = from.acc_map.begin(); - i_from != from.acc_map.end(); - ++i_from) - { - i_to = dict_.acc_map.find(i_from->first); - assert(i_to != dict_.acc_map.end()); - bdd_setpair(rewrite, i_from->second, i_to->second); - } - return rewrite; - } - - const tgba_bdd_core_data& - tgba_bdd_translate_factory::get_core_data() const - { - return data_; - } - - const tgba_bdd_dict& - tgba_bdd_translate_factory::get_dict() const - { - return dict_; - } - - bdd - tgba_bdd_translate_factory::get_init_state() const - { - return init_; - } - - - tgba_bdd_concrete - defrag(const tgba_bdd_concrete& a) - { - const tgba_bdd_dict& ad = a.get_dict(); - tgba_bdd_dict u = tgba_bdd_dict_union(ad, ad); - tgba_bdd_translate_factory f(a, u); - return tgba_bdd_concrete(f, f.get_init_state()); - } -} diff --git a/src/tgba/tgbabddtranslatefactory.hh b/src/tgba/tgbabddtranslatefactory.hh deleted file mode 100644 index 1e34c0be5..000000000 --- a/src/tgba/tgbabddtranslatefactory.hh +++ /dev/null @@ -1,43 +0,0 @@ -#ifndef SPOT_TGBA_TGBABDDTRANSLATEFACTORY_HH -# define SPOT_TGBA_TGBABDDTRANSLATEFACTORY_HH - -#include "tgbabddfactory.hh" -#include "tgbabddconcrete.hh" - -namespace spot -{ - - /// A spot::tgba_bdd_factory than renumber BDD variables. - class tgba_bdd_translate_factory: public tgba_bdd_factory - { - public: - ///\brief Construct a spot::tgba_bdd_translate_factory - /// - /// \param from The Automata to copy. - /// \param to The dictionary of variable number to use. - tgba_bdd_translate_factory(const tgba_bdd_concrete& from, - const tgba_bdd_dict& to); - - virtual ~tgba_bdd_translate_factory(); - - const tgba_bdd_core_data& get_core_data() const; - const tgba_bdd_dict& get_dict() const; - - /// Get the new initial state. - bdd get_init_state() const; - - protected: - /// Compute renaming pairs. - bddPair* compute_pairs(const tgba_bdd_dict& from); - - private: - tgba_bdd_core_data data_; - tgba_bdd_dict dict_; - bdd init_; - }; - - /// Reorder the variables of an automata. - tgba_bdd_concrete defrag(const tgba_bdd_concrete& a); -} - -#endif // SPOT_TGBA_TGBABDDTRANSLATEFACTORY_HH diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index 9c03f6573..d74c56963 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -80,13 +80,38 @@ namespace spot // tgba_explicit - tgba_explicit::tgba_explicit() - : init_(0), all_accepting_conditions_(bddfalse), + tgba_explicit::tgba_explicit(bdd_dict* dict) + : dict_(dict), init_(0), all_accepting_conditions_(bddfalse), neg_accepting_conditions_(bddtrue), all_accepting_conditions_computed_(false) { } + tgba_explicit::tgba_explicit(const tgba_explicit& other) + : tgba(), + name_state_map_(other.name_state_map_), + state_name_map_(other.state_name_map_), + dict_(other.dict_), + init_(other.init_), + all_accepting_conditions_(other.all_accepting_conditions_), + neg_accepting_conditions_(other.neg_accepting_conditions_), + all_accepting_conditions_computed_(other. + all_accepting_conditions_computed_) + { + dict_->register_all_variables_of(&other, this); + } + + tgba_explicit& + tgba_explicit::operator=(const tgba_explicit& other) + { + if (&other != this) + { + this->~tgba_explicit(); + new (this) tgba_explicit(other); + } + return *this; + } + tgba_explicit::~tgba_explicit() { ns_map::iterator i; @@ -97,6 +122,7 @@ namespace spot delete *i2; delete i->second; } + dict_->unregister_all_my_variables(this); } tgba_explicit::state* @@ -136,20 +162,9 @@ namespace spot tgba_explicit::get_condition(ltl::formula* f) { assert(dynamic_cast(f)); - tgba_bdd_dict::fv_map::iterator i = dict_.var_map.find(f); - int v; - if (i == dict_.var_map.end()) - { - v = create_node(); - dict_.var_map[f] = v; - dict_.var_formula_map[v] = f; - } - else - { - ltl::destroy(f); - v = i->second; - } - return ithvar(v); + int v = dict_->register_proposition(f, this); + ltl::destroy(f); + return bdd_ithvar(v); } void @@ -167,22 +182,15 @@ namespace spot void tgba_explicit::declare_accepting_condition(ltl::formula* f) { - tgba_bdd_dict::fv_map::iterator i = dict_.acc_map.find(f); - if (i == dict_.acc_map.end()) - { - int v; - v = create_node(); - dict_.acc_map[f] = v; - dict_.acc_formula_map[v] = f; - neg_accepting_conditions_ &= !ithvar(v); - } + int v = dict_->register_accepting_variable(f, this); + ltl::destroy(f); + neg_accepting_conditions_ &= bdd_nithvar(v); } bool tgba_explicit::has_accepting_condition(ltl::formula* f) const { - tgba_bdd_dict::fv_map::const_iterator i = dict_.acc_map.find(f); - return i != dict_.acc_map.end(); + return dict_->is_registered(f, this); } bdd @@ -201,11 +209,10 @@ namespace spot /* Unreachable code. */ assert(0); } - - tgba_bdd_dict::fv_map::iterator i = dict_.acc_map.find(f); - assert (i != dict_.acc_map.end()); + bdd_dict::fv_map::iterator i = dict_->acc_map.find(f); + assert(i != dict_->acc_map.end()); ltl::destroy(f); - bdd v = ithvar(i->second); + bdd v = bdd_ithvar(i->second); v &= bdd_exist(neg_accepting_conditions_, v); return v; } @@ -232,7 +239,7 @@ namespace spot all_accepting_conditions()); } - const tgba_bdd_dict& + bdd_dict* tgba_explicit::get_dict() const { return dict_; @@ -254,10 +261,10 @@ namespace spot if (!all_accepting_conditions_computed_) { bdd all = bddfalse; - tgba_bdd_dict::fv_map::const_iterator i; - for (i = dict_.acc_map.begin(); i != dict_.acc_map.end(); ++i) + bdd_dict::fv_map::const_iterator i; + for (i = dict_->acc_map.begin(); i != dict_->acc_map.end(); ++i) { - bdd v = ithvar(i->second); + bdd v = bdd_ithvar(i->second); all |= v & bdd_exist(neg_accepting_conditions_, v); } all_accepting_conditions_ = all; diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 87cb826e6..c14b831fe 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -5,7 +5,6 @@ #include #include "tgba.hh" #include "ltlast/formula.hh" -#include "bddfactory.hh" namespace spot { @@ -14,10 +13,12 @@ namespace spot class tgba_explicit_succ_iterator; /// Explicit representation of a spot::tgba. - class tgba_explicit : public tgba, public bdd_factory + class tgba_explicit: public tgba { public: - tgba_explicit(); + tgba_explicit(bdd_dict* dict); + tgba_explicit(const tgba_explicit& other); + tgba_explicit& tgba_explicit::operator=(const tgba_explicit& other); struct transition; typedef std::list state; @@ -44,7 +45,7 @@ namespace spot virtual spot::state* get_init_state() const; virtual tgba_succ_iterator* succ_iter(const spot::state* state) const; - virtual const tgba_bdd_dict& get_dict() const; + virtual bdd_dict* get_dict() const; virtual std::string format_state(const spot::state* state) const; virtual bdd all_accepting_conditions() const; @@ -59,7 +60,7 @@ namespace spot typedef std::map sn_map; ns_map name_state_map_; sn_map state_name_map_; - tgba_bdd_dict dict_; + bdd_dict* dict_; tgba_explicit::state* init_; mutable bdd all_accepting_conditions_; bdd neg_accepting_conditions_; diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index abc9db54e..8cd41abbf 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/tgba/tgbaproduct.cc @@ -1,6 +1,4 @@ #include "tgbaproduct.hh" -#include "tgbatranslateproxy.hh" -#include "dictunion.hh" #include #include @@ -146,31 +144,9 @@ namespace spot // tgba_product tgba_product::tgba_product(const tgba& left, const tgba& right) - : dict_(tgba_bdd_dict_union(left.get_dict(), right.get_dict())) + : dict_(left.get_dict()), left_(&left), right_(&right) { - // Translate the left automaton if needed. - if (dict_.contains(left.get_dict())) - { - left_ = &left; - left_should_be_freed_ = false; - } - else - { - left_ = new tgba_translate_proxy(left, dict_); - left_should_be_freed_ = true; - } - - // Translate the right automaton if needed. - if (dict_.contains(right.get_dict())) - { - right_ = &right; - right_should_be_freed_ = false; - } - else - { - right_ = new tgba_translate_proxy(right, dict_); - right_should_be_freed_ = true; - } + assert(dict_ == right.get_dict()); all_accepting_conditions_ = ((left_->all_accepting_conditions() & right_->neg_accepting_conditions()) @@ -178,14 +154,13 @@ namespace spot & left_->neg_accepting_conditions())); neg_accepting_conditions_ = (left_->neg_accepting_conditions() & right_->neg_accepting_conditions()); + dict_->register_all_variables_of(&left_, this); + dict_->register_all_variables_of(&right_, this); } tgba_product::~tgba_product() { - if (left_should_be_freed_) - delete left_; - if (right_should_be_freed_) - delete right_; + dict_->unregister_all_my_variables(this); } state* @@ -208,7 +183,7 @@ namespace spot right_->neg_accepting_conditions()); } - const tgba_bdd_dict& + bdd_dict* tgba_product::get_dict() const { return dict_; diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index 415adbf2f..54cef2929 100644 --- a/src/tgba/tgbaproduct.hh +++ b/src/tgba/tgbaproduct.hh @@ -103,7 +103,7 @@ namespace spot virtual tgba_product_succ_iterator* succ_iter(const state* state) const; - virtual const tgba_bdd_dict& get_dict() const; + virtual bdd_dict* get_dict() const; virtual std::string format_state(const state* state) const; @@ -111,11 +111,9 @@ namespace spot virtual bdd neg_accepting_conditions() const; private: + bdd_dict* dict_; const tgba* left_; - bool left_should_be_freed_; const tgba* right_; - bool right_should_be_freed_; - tgba_bdd_dict dict_; bdd all_accepting_conditions_; bdd neg_accepting_conditions_; }; diff --git a/src/tgba/tgbatranslateproxy.cc b/src/tgba/tgbatranslateproxy.cc deleted file mode 100644 index 2944801dc..000000000 --- a/src/tgba/tgbatranslateproxy.cc +++ /dev/null @@ -1,159 +0,0 @@ -#include "tgbatranslateproxy.hh" -#include "bddprint.hh" -#include - -namespace spot -{ - - // tgba_translate_proxy_succ_iterator - // -------------------------------------- - - tgba_translate_proxy_succ_iterator:: - tgba_translate_proxy_succ_iterator(tgba_succ_iterator* it, - bddPair* rewrite) - : iter_(it), rewrite_(rewrite) - { - } - - tgba_translate_proxy_succ_iterator::~tgba_translate_proxy_succ_iterator() - { - delete iter_; - } - - void - tgba_translate_proxy_succ_iterator::first() - { - iter_->first(); - } - - void - tgba_translate_proxy_succ_iterator::next() - { - iter_->next(); - } - - bool - tgba_translate_proxy_succ_iterator::done() const - { - return iter_->done(); - } - - state* - tgba_translate_proxy_succ_iterator::current_state() const - { - state* s = iter_->current_state(); - s->translate(rewrite_); - return s; - } - - bdd - tgba_translate_proxy_succ_iterator::current_condition() const - { - return bdd_replace(iter_->current_condition(), rewrite_); - } - - bdd - tgba_translate_proxy_succ_iterator::current_accepting_conditions() const - { - return bdd_replace(iter_->current_accepting_conditions(), rewrite_); - } - - - // tgba_translate_proxy - // ------------------------ - - tgba_translate_proxy::tgba_translate_proxy(const tgba& from, - const tgba_bdd_dict& to) - : from_(from), to_(to) - { - const tgba_bdd_dict& f = from.get_dict(); - rewrite_to_ = bdd_newpair(); - rewrite_from_ = bdd_newpair(); - - tgba_bdd_dict::fv_map::const_iterator i_from; - tgba_bdd_dict::fv_map::const_iterator i_to; - - for (i_from = f.now_map.begin(); i_from != f.now_map.end(); ++i_from) - { - i_to = to_.now_map.find(i_from->first); - assert(i_to != to_.now_map.end()); - bdd_setpair(rewrite_to_, i_from->second, i_to->second); - bdd_setpair(rewrite_to_, i_from->second + 1, i_to->second + 1); - bdd_setpair(rewrite_from_, i_to->second, i_from->second); - bdd_setpair(rewrite_from_, i_to->second + 1, i_from->second + 1); - } - for (i_from = f.var_map.begin(); i_from != f.var_map.end(); ++i_from) - { - i_to = to_.var_map.find(i_from->first); - assert(i_to != to_.var_map.end()); - bdd_setpair(rewrite_to_, i_from->second, i_to->second); - bdd_setpair(rewrite_from_, i_to->second, i_from->second); - } - for (i_from = f.acc_map.begin(); i_from != f.acc_map.end(); ++i_from) - { - i_to = to_.acc_map.find(i_from->first); - assert(i_to != to_.acc_map.end()); - bdd_setpair(rewrite_to_, i_from->second, i_to->second); - bdd_setpair(rewrite_from_, i_to->second, i_from->second); - } - - all_accepting_conditions_ = bdd_replace(from.all_accepting_conditions(), - rewrite_to_); - neg_accepting_conditions_ = bdd_replace(from.neg_accepting_conditions(), - rewrite_to_); - } - - tgba_translate_proxy::~tgba_translate_proxy() - { - bdd_freepair(rewrite_from_); - bdd_freepair(rewrite_to_); - } - - state* - tgba_translate_proxy::get_init_state() const - { - state* s = from_.get_init_state(); - s->translate(rewrite_to_); - return s; - } - - tgba_translate_proxy_succ_iterator* - tgba_translate_proxy::succ_iter(const state* s) const - { - state* s2 = s->clone(); - s2->translate(rewrite_from_); - tgba_translate_proxy_succ_iterator *res = - new tgba_translate_proxy_succ_iterator(from_.succ_iter(s2), - rewrite_to_); - delete s2; - return res; - } - - const tgba_bdd_dict& - tgba_translate_proxy::get_dict() const - { - return to_; - } - - std::string - tgba_translate_proxy::format_state(const state* s) const - { - state* s2 = s->clone(); - s2->translate(rewrite_from_); - std::string res = from_.format_state(s2); - delete s2; - return res; - } - - bdd - tgba_translate_proxy::all_accepting_conditions() const - { - return all_accepting_conditions_; - } - - bdd tgba_translate_proxy::neg_accepting_conditions() const - { - return neg_accepting_conditions_; - } - -} diff --git a/src/tgba/tgbatranslateproxy.hh b/src/tgba/tgbatranslateproxy.hh deleted file mode 100644 index 3f2cb24ea..000000000 --- a/src/tgba/tgbatranslateproxy.hh +++ /dev/null @@ -1,69 +0,0 @@ -#ifndef SPOT_TGBA_TGBATRANSLATEPROXY_HH -# define SPOT_TGBA_TGBATRANSLATEPROXY_HH - -#include "tgba.hh" - -namespace spot -{ - /// \brief Proxy for a spot::tgba_succ_iterator_concrete that renumber - /// BDD variables on the fly. - class tgba_translate_proxy_succ_iterator: public tgba_succ_iterator - { - public: - tgba_translate_proxy_succ_iterator(tgba_succ_iterator* it, - bddPair* rewrite); - virtual ~tgba_translate_proxy_succ_iterator(); - - // iteration - void first(); - void next(); - bool done() const; - - // inspection - state* current_state() const; - bdd current_condition() const; - bdd current_accepting_conditions() const; - protected: - tgba_succ_iterator* iter_; - bddPair* rewrite_; - }; - - - /// \brief Proxy for a spot::tgba_bdd_concrete that renumber BDD variables - /// on the fly. - class tgba_translate_proxy: public tgba - { - public: - /// \brief Constructor. - /// \param from The spot::tgba to masquerade. - /// \param to The new dictionary to use. - tgba_translate_proxy(const tgba& from, - const tgba_bdd_dict& to); - - virtual ~tgba_translate_proxy(); - - virtual state* get_init_state() const; - - virtual tgba_translate_proxy_succ_iterator* - succ_iter(const state* state) const; - - virtual const tgba_bdd_dict& get_dict() const; - - virtual std::string format_state(const state* state) const; - - virtual bdd all_accepting_conditions() const; - - virtual bdd neg_accepting_conditions() const; - - private: - const tgba& from_; ///< The spot::tgba to masquerade. - tgba_bdd_dict to_; ///< The new dictionar to use. - bddPair* rewrite_to_; ///< The rewriting pair for from->to. - bddPair* rewrite_from_; ///< The rewriting pair for to->from. - bdd all_accepting_conditions_; - bdd neg_accepting_conditions_; - }; - -} - -#endif // SPOT_TGBA_TGBATRANSLATEPROXY_HH diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index ddbb19167..9736b34be 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -64,7 +64,7 @@ namespace spot // Conjunctions are printed by bdd_format_sat, so we just have // to handle the other cases. static std::string - bdd_to_lbtt(bdd b, const tgba_bdd_dict& d) + bdd_to_lbtt(bdd b, const bdd_dict* d) { if (b == bddfalse) return "f"; @@ -178,7 +178,7 @@ namespace spot std::ostream& lbtt_reachable(std::ostream& os, const tgba& g) { - const tgba_bdd_dict& d = g.get_dict(); + const bdd_dict* d = g.get_dict(); std::ostringstream body; seen_map seen; diff --git a/src/tgbaalgos/ltl2tgba.cc b/src/tgbaalgos/ltl2tgba.cc index 00c1383c6..a48f48158 100644 --- a/src/tgbaalgos/ltl2tgba.cc +++ b/src/tgbaalgos/ltl2tgba.cc @@ -38,7 +38,7 @@ namespace spot void visit(const atomic_prop* node) { - res_ = fact_.ithvar(fact_.create_atomic_prop(node)); + res_ = bdd_ithvar(fact_.create_atomic_prop(node)); } void @@ -70,8 +70,8 @@ namespace spot now <=> x | next */ int v = fact_.create_state(node); - bdd now = fact_.ithvar(v); - bdd next = fact_.ithvar(v + 1); + bdd now = bdd_ithvar(v); + bdd next = bdd_ithvar(v + 1); bdd x = recurse(node->child()); fact_.constrain_relation(bdd_apply(now, x | next, bddop_biimp)); /* @@ -101,8 +101,8 @@ namespace spot } // Gx <=> x && XGx int v = fact_.create_state(node); - bdd now = fact_.ithvar(v); - bdd next = fact_.ithvar(v + 1); + bdd now = bdd_ithvar(v); + bdd next = bdd_ithvar(v + 1); fact_.constrain_relation(bdd_apply(now, child & next, bddop_biimp)); res_ = now; @@ -116,8 +116,8 @@ namespace spot case unop::X: { int v = fact_.create_state(node->child()); - bdd now = fact_.ithvar(v); - bdd next = fact_.ithvar(v + 1); + bdd now = bdd_ithvar(v); + bdd next = bdd_ithvar(v + 1); fact_.constrain_relation(bdd_apply(now, recurse(node->child()), bddop_biimp)); res_ = next; @@ -153,8 +153,8 @@ namespace spot now <=> f2 | (f1 & next) */ int v = fact_.create_state(node); - bdd now = fact_.ithvar(v); - bdd next = fact_.ithvar(v + 1); + bdd now = bdd_ithvar(v); + bdd next = bdd_ithvar(v + 1); fact_.constrain_relation(bdd_apply(now, f2 | (f1 & next), bddop_biimp)); /* @@ -175,8 +175,8 @@ namespace spot now <=> f2 & (f1 | next) */ int v = fact_.create_state(node); - bdd now = fact_.ithvar(v); - bdd next = fact_.ithvar(v + 1); + bdd now = bdd_ithvar(v); + bdd next = bdd_ithvar(v + 1); fact_.constrain_relation(bdd_apply(now, f2 & (f1 | next), bddop_biimp)); res_ = now; @@ -231,18 +231,18 @@ namespace spot }; tgba_bdd_concrete - ltl_to_tgba(const ltl::formula* f) + ltl_to_tgba(const ltl::formula* f, bdd_dict* dict) { - // Normalize the formula. We want all the negation on - // the atomic proposition. We also suppress logic - // abbreviation such as <=>, =>, or XOR, since they + // Normalize the formula. We want all the negations on + // the atomic propositions. We also suppress logic + // abbreviations such as <=>, =>, or XOR, since they // would involve negations at the BDD level. const ltl::formula* f1 = ltl::unabbreviate_logic(f); const ltl::formula* f2 = ltl::negative_normal_form(f1); ltl::destroy(f1); // Traverse the formula and draft the automaton in a factory. - tgba_bdd_concrete_factory fact; + tgba_bdd_concrete_factory fact(dict); ltl_trad_visitor v(fact, true); f2->accept(v); ltl::destroy(f2); diff --git a/src/tgbaalgos/ltl2tgba.hh b/src/tgbaalgos/ltl2tgba.hh index a5c0fd71f..7e7c682b8 100644 --- a/src/tgbaalgos/ltl2tgba.hh +++ b/src/tgbaalgos/ltl2tgba.hh @@ -7,7 +7,7 @@ namespace spot { /// Build a spot::tgba_bdd_concrete from an LTL formula. - tgba_bdd_concrete ltl_to_tgba(const ltl::formula* f); + tgba_bdd_concrete ltl_to_tgba(const ltl::formula* f, bdd_dict* dict); } #endif // SPOT_TGBA_LTL2TGBA_HH diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc index ed0436388..4d28b1883 100644 --- a/src/tgbaalgos/save.cc +++ b/src/tgbaalgos/save.cc @@ -42,10 +42,10 @@ namespace spot std::ostream& tgba_save_reachable(std::ostream& os, const tgba& g) { - const tgba_bdd_dict& d = g.get_dict(); + const bdd_dict* d = g.get_dict(); os << "acc ="; - for (tgba_bdd_dict::fv_map::const_iterator ai = d.acc_map.begin(); - ai != d.acc_map.end(); ++ai) + for (bdd_dict::fv_map::const_iterator ai = d->acc_map.begin(); + ai != d->acc_map.end(); ++ai) { os << " \""; ltl::to_string(ai->first, os) << "\""; diff --git a/src/tgbaparse/public.hh b/src/tgbaparse/public.hh index 924ba1cea..b1ffdc399 100644 --- a/src/tgbaparse/public.hh +++ b/src/tgbaparse/public.hh @@ -20,6 +20,7 @@ namespace spot /// \param filename The name of the file to parse. /// \param error_list A list that will be filled with /// parse errors that occured during parsing. + /// \param dict The BDD dictionary where to use. /// \param env The environment into which parsing should take place. /// \param debug When true, causes the parser to trace its execution. /// \return A pointer to the tgba built from \a filename, or @@ -33,6 +34,7 @@ namespace spot /// \warning This function is not reentrant. tgba_explicit* tgba_parse(const std::string& filename, tgba_parse_error_list& error_list, + bdd_dict* dict, ltl::environment& env = ltl::default_environment::instance(), bool debug = false); diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy index 50ab0568d..14cff5e1b 100644 --- a/src/tgbaparse/tgbaparse.yy +++ b/src/tgbaparse/tgbaparse.yy @@ -155,22 +155,23 @@ namespace spot tgba_explicit* tgba_parse(const std::string& name, tgba_parse_error_list& error_list, + bdd_dict* dict, environment& env, bool debug) { if (tgbayyopen(name)) - { - error_list.push_back - (tgba_parse_error(yy::Location(), - std::string("Cannot open file ") + name)); - return 0; - } - tgba_explicit* result = new tgba_explicit; - tgbayy::Parser parser(debug, yy::Location(), error_list, env, result); - parser.parse(); - tgbayyclose(); - return result; - } + { + error_list.push_back + (tgba_parse_error(yy::Location(), + std::string("Cannot open file ") + name)); + return 0; + } + tgba_explicit* result = new tgba_explicit(dict); + tgbayy::Parser parser(debug, yy::Location(), error_list, env, result); + parser.parse(); + tgbayyclose(); + return result; + } } // Local Variables: diff --git a/src/tgbatest/explicit.cc b/src/tgbatest/explicit.cc index fef0f047d..7a836e132 100644 --- a/src/tgbatest/explicit.cc +++ b/src/tgbatest/explicit.cc @@ -1,29 +1,40 @@ #include +#include #include "ltlenv/defaultenv.hh" #include "tgba/tgbaexplicit.hh" #include "tgbaalgos/dotty.hh" +#include "ltlast/allnodes.hh" int main() { + spot::bdd_dict* dict = new spot::bdd_dict(); + spot::ltl::default_environment& e = spot::ltl::default_environment::instance(); - spot::tgba_explicit a; + spot::tgba_explicit* a = new spot::tgba_explicit(dict); typedef spot::tgba_explicit::transition trans; - trans* t1 = a.create_transition("state 0", "state 1"); - trans* t2 = a.create_transition("state 1", "state 2"); - trans* t3 = a.create_transition("state 2", "state 0"); - a.add_condition(t2, e.require("a")); - a.add_condition(t3, e.require("b")); - a.add_condition(t3, e.require("c")); - a.declare_accepting_condition(e.require("p")); - a.declare_accepting_condition(e.require("q")); - a.declare_accepting_condition(e.require("r")); - a.add_accepting_condition(t1, e.require("p")); - a.add_accepting_condition(t1, e.require("q")); - a.add_accepting_condition(t2, e.require("r")); + trans* t1 = a->create_transition("state 0", "state 1"); + trans* t2 = a->create_transition("state 1", "state 2"); + trans* t3 = a->create_transition("state 2", "state 0"); + a->add_condition(t2, e.require("a")); + a->add_condition(t3, e.require("b")); + a->add_condition(t3, e.require("c")); + a->declare_accepting_condition(e.require("p")); + a->declare_accepting_condition(e.require("q")); + a->declare_accepting_condition(e.require("r")); + a->add_accepting_condition(t1, e.require("p")); + a->add_accepting_condition(t1, e.require("q")); + a->add_accepting_condition(t2, e.require("r")); - spot::dotty_reachable(std::cout, a); + spot::dotty_reachable(std::cout, *a); + + delete a; + delete dict; + assert(spot::ltl::atomic_prop::instance_count() == 0); + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); } diff --git a/src/tgbatest/explprod.cc b/src/tgbatest/explprod.cc index 82cde4605..719da7d52 100644 --- a/src/tgbatest/explprod.cc +++ b/src/tgbatest/explprod.cc @@ -22,13 +22,15 @@ main(int argc, char** argv) if (argc != 3) syntax(argv[0]); + spot::bdd_dict* dict = new spot::bdd_dict(); + spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::tgba_parse_error_list pel1; - spot::tgba_explicit* a1 = spot::tgba_parse(argv[1], pel1, env); + spot::tgba_explicit* a1 = spot::tgba_parse(argv[1], pel1, dict, env); if (spot::format_tgba_parse_errors(std::cerr, pel1)) return 2; spot::tgba_parse_error_list pel2; - spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, env); + spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, dict, env); if (spot::format_tgba_parse_errors(std::cerr, pel2)) return 2; @@ -44,5 +46,6 @@ main(int argc, char** argv) delete a1; delete a2; assert(spot::ltl::atomic_prop::instance_count() == 0); + delete dict; return exit_code; } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index c28cb90f6..97af56acc 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -5,7 +5,6 @@ #include "ltlparse/public.hh" #include "tgbaalgos/ltl2tgba.hh" #include "tgba/bddprint.hh" -#include "tgba/tgbabddtranslatefactory.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/lbtt.hh" @@ -19,7 +18,6 @@ syntax(char* prog) << std::endl << " -A same as -a, but as a set" << std::endl << " -d turn on traces during parsing" << std::endl - << " -o re-order BDD variables in the automata" << std::endl << " -r display the relation BDD, not the reachability graph" << std::endl << " -R same as -r, but as a set" << std::endl @@ -35,7 +33,6 @@ main(int argc, char** argv) int exit_code = 0; bool debug_opt = false; - bool defrag_opt = false; int output = 0; int formula_index = 0; @@ -58,10 +55,6 @@ main(int argc, char** argv) { debug_opt = true; } - else if (!strcmp(argv[formula_index], "-o")) - { - defrag_opt = true; - } else if (!strcmp(argv[formula_index], "-r")) { output = 1; @@ -84,7 +77,6 @@ main(int argc, char** argv) } } - spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::parse_error_list pel; spot::ltl::formula* f = spot::ltl::parse(argv[formula_index], @@ -93,12 +85,11 @@ main(int argc, char** argv) exit_code = spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel); + spot::bdd_dict* dict = new spot::bdd_dict(); if (f) { - spot::tgba_bdd_concrete a = spot::ltl_to_tgba(f); + spot::tgba_bdd_concrete a = spot::ltl_to_tgba(f, dict); spot::ltl::destroy(f); - if (defrag_opt) - a = spot::defrag(a); switch (output) { case 0: @@ -121,7 +112,7 @@ main(int argc, char** argv) a.get_core_data().accepting_conditions); break; case 5: - a.get_dict().dump(std::cout); + a.get_dict()->dump(std::cout); break; case 6: spot::lbtt_reachable(std::cout, a); @@ -139,5 +130,6 @@ main(int argc, char** argv) assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0); assert(spot::ltl::multop::instance_count() == 0); + delete dict; return exit_code; } diff --git a/src/tgbatest/ltlprod.cc b/src/tgbatest/ltlprod.cc index 7c6833b13..556c95124 100644 --- a/src/tgbatest/ltlprod.cc +++ b/src/tgbatest/ltlprod.cc @@ -37,9 +37,10 @@ main(int argc, char** argv) if (spot::ltl::format_parse_errors(std::cerr, argv[2], pel2)) return 2; + spot::bdd_dict* dict = new spot::bdd_dict(); { - spot::tgba_bdd_concrete a1 = spot::ltl_to_tgba(f1); - spot::tgba_bdd_concrete a2 = spot::ltl_to_tgba(f2); + spot::tgba_bdd_concrete a1 = spot::ltl_to_tgba(f1, dict); + spot::tgba_bdd_concrete a2 = spot::ltl_to_tgba(f2, dict); spot::ltl::destroy(f1); spot::ltl::destroy(f2); @@ -56,5 +57,6 @@ main(int argc, char** argv) assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0); assert(spot::ltl::multop::instance_count() == 0); + delete dict; return exit_code; } diff --git a/src/tgbatest/mixprod.cc b/src/tgbatest/mixprod.cc index 9f7d932e0..3125452e0 100644 --- a/src/tgbatest/mixprod.cc +++ b/src/tgbatest/mixprod.cc @@ -24,6 +24,8 @@ main(int argc, char** argv) if (argc != 3) syntax(argv[0]); + spot::bdd_dict* dict = new spot::bdd_dict(); + spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::parse_error_list pel1; @@ -32,12 +34,12 @@ main(int argc, char** argv) return 2; spot::tgba_parse_error_list pel2; - spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, env); + spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, dict, env); if (spot::format_tgba_parse_errors(std::cerr, pel2)) return 2; { - spot::tgba_bdd_concrete a1 = spot::ltl_to_tgba(f1); + spot::tgba_bdd_concrete a1 = spot::ltl_to_tgba(f1, dict); spot::ltl::destroy(f1); spot::tgba_product p(a1, *a2); @@ -49,5 +51,6 @@ main(int argc, char** argv) assert(spot::ltl::multop::instance_count() == 0); delete a2; assert(spot::ltl::atomic_prop::instance_count() == 0); + delete dict; return exit_code; } diff --git a/src/tgbatest/readsave.cc b/src/tgbatest/readsave.cc index 0077eb61d..c8bb52674 100644 --- a/src/tgbatest/readsave.cc +++ b/src/tgbatest/readsave.cc @@ -1,7 +1,9 @@ #include +#include #include "tgbaparse/public.hh" #include "tgba/tgbaexplicit.hh" #include "tgbaalgos/save.hh" +#include "ltlast/allnodes.hh" void syntax(char* prog) @@ -29,10 +31,12 @@ main(int argc, char** argv) filename_index = 2; } + spot::bdd_dict* dict = new spot::bdd_dict(); + spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::tgba_parse_error_list pel; spot::tgba_explicit* a = spot::tgba_parse(argv[filename_index], - pel, env, debug); + pel, dict, env, debug); exit_code = spot::format_tgba_parse_errors(std::cerr, pel); @@ -46,5 +50,12 @@ main(int argc, char** argv) { exit_code = 1; } + + delete dict; + assert(spot::ltl::atomic_prop::instance_count() == 0); + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); + return exit_code; } diff --git a/src/tgbatest/spotlbtt.cc b/src/tgbatest/spotlbtt.cc index 7fe43233f..3e471836d 100644 --- a/src/tgbatest/spotlbtt.cc +++ b/src/tgbatest/spotlbtt.cc @@ -35,9 +35,11 @@ main(int argc, char** argv) if (! std::getline(fin, input, '\0')) { std::cerr << "Cannot read " << argv[1] << std::endl; - exit(2); + exit(2); } + spot::bdd_dict* dict = new spot::bdd_dict(); + spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::parse_error_list pel; spot::ltl::formula* f = spot::ltl::parse(input, pel, env); @@ -46,7 +48,7 @@ main(int argc, char** argv) if (f) { - spot::tgba_bdd_concrete a = spot::ltl_to_tgba(f); + spot::tgba_bdd_concrete a = spot::ltl_to_tgba(f, dict); spot::ltl::destroy(f); spot::lbtt_reachable(std::cout, a); } @@ -59,5 +61,6 @@ main(int argc, char** argv) assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0); assert(spot::ltl::multop::instance_count() == 0); + delete dict; return exit_code; } diff --git a/src/tgbatest/tgbaread.cc b/src/tgbatest/tgbaread.cc index 3449fb865..3408775cb 100644 --- a/src/tgbatest/tgbaread.cc +++ b/src/tgbatest/tgbaread.cc @@ -1,7 +1,9 @@ #include +#include #include "tgbaparse/public.hh" #include "tgba/tgbaexplicit.hh" #include "tgbaalgos/dotty.hh" +#include "ltlast/allnodes.hh" void syntax(char* prog) @@ -29,10 +31,12 @@ main(int argc, char** argv) filename_index = 2; } + spot::bdd_dict* dict = new spot::bdd_dict(); + spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::tgba_parse_error_list pel; spot::tgba_explicit* a = spot::tgba_parse(argv[filename_index], - pel, env, debug); + pel, dict, env, debug); if (spot::format_tgba_parse_errors(std::cerr, pel)) return 2; @@ -46,5 +50,12 @@ main(int argc, char** argv) { return 1; } + + delete dict; + assert(spot::ltl::atomic_prop::instance_count() == 0); + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); + return 0; } diff --git a/src/tgbatest/tripprod.cc b/src/tgbatest/tripprod.cc index 65a8fe40d..f9fa6eab8 100644 --- a/src/tgbatest/tripprod.cc +++ b/src/tgbatest/tripprod.cc @@ -22,17 +22,19 @@ main(int argc, char** argv) if (argc != 4) syntax(argv[0]); + spot::bdd_dict* dict = new spot::bdd_dict(); + spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::tgba_parse_error_list pel1; - spot::tgba_explicit* a1 = spot::tgba_parse(argv[1], pel1, env); + spot::tgba_explicit* a1 = spot::tgba_parse(argv[1], pel1, dict, env); if (spot::format_tgba_parse_errors(std::cerr, pel1)) return 2; spot::tgba_parse_error_list pel2; - spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, env); + spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, dict, env); if (spot::format_tgba_parse_errors(std::cerr, pel2)) return 2; spot::tgba_parse_error_list pel3; - spot::tgba_explicit* a3 = spot::tgba_parse(argv[3], pel3, env); + spot::tgba_explicit* a3 = spot::tgba_parse(argv[3], pel3, dict, env); if (spot::format_tgba_parse_errors(std::cerr, pel3)) return 2; @@ -50,5 +52,6 @@ main(int argc, char** argv) delete a2; delete a3; assert(spot::ltl::atomic_prop::instance_count() == 0); + delete dict; return exit_code; }