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; }