diff --git a/spot/mc/utils.hh b/spot/mc/utils.hh index 6124f55fa..8ffdc6831 100644 --- a/spot/mc/utils.hh +++ b/spot/mc/utils.hh @@ -97,145 +97,14 @@ namespace spot std::unordered_map reverse_binder_; }; - // FIXME: should be merge into the next algorithm. - /// \brief This class explores (with a DFS) a product between a - /// system and a twa. This exploration is performed on-the-fly. - /// Since this exploration aims to be a generic we need to define - /// hooks to the various emptiness checks. - /// Actually, we use "mixins templates" in order to efficiently - /// call emptiness check procedure. This means that we add - /// a template \a EmptinessCheck that will be called though - /// four functions: - /// - setup: called before any operation - /// - push: called for every new state - /// - pop: called every time a state leave the DFS stack - /// - update: called for every closing edge - /// - trace: must return a counterexample (if exists) - /// - /// The other template parameters allows to consider any kind - /// of state (and so any kind of kripke structures). + + + /// \brief convert a (cube) product automaton into a twa + /// Note that this algorithm cannot be run in parallel. template - class SPOT_API intersect + typename StateHash, typename StateEqual> + class SPOT_API product_to_twa { - public: - intersect(const intersect& i) = default; - - intersect(kripkecube& sys, - twacube_ptr twa, unsigned tid, bool& stop): - sys_(sys), twa_(twa), tid_(tid), stop_(stop) - { - static_assert(spot::is_a_kripkecube_ptr::value, - "error: does not match the kripkecube requirements"); - map.reserve(2000000); - todo.reserve(100000); - } - - ~intersect() - { - map.clear(); - } - - /// \brief In order to implement "mixin paradigm", we - /// must be abble to access the acual definition of - /// the emptiness check that, in turn, has to access - /// local variables. - EmptinessCheck& self() - { - return static_cast(*this); - } - - /// \brief The main function that will perform the - /// product on-the-fly and call the emptiness check - /// when necessary. - bool run() - { - self().setup(); - product_state initial = {sys_.initial(tid_), twa_->get_initial()}; - if (SPOT_LIKELY(self().push_state(initial, dfs_number+1, {}))) - { - todo.push_back({initial, sys_.succ(initial.st_kripke, tid_), - twa_->succ(initial.st_prop)}); - - // Not going further! It's a product with a single state. - if (todo.back().it_prop->done()) - return false; - - forward_iterators(sys_, twa_, todo.back().it_kripke, - todo.back().it_prop, true, 0); - map[initial] = ++dfs_number; - } - while (!todo.empty() && !stop_) - { - // Check the kripke is enough since it's the outer loop. More - // details in forward_iterators. - if (todo.back().it_kripke->done()) - { - bool is_init = todo.size() == 1; - auto newtop = is_init? todo.back().st: todo[todo.size() -2].st; - if (SPOT_LIKELY(self().pop_state(todo.back().st, - map[todo.back().st], - is_init, - newtop, - map[newtop]))) - { - sys_.recycle(todo.back().it_kripke, tid_); - // FIXME a local storage for twacube iterator? - todo.pop_back(); - if (SPOT_UNLIKELY(self().counterexample_found())) - return true; - } - } - else - { - ++transitions; - product_state dst = { - todo.back().it_kripke->state(), - twa_->trans_storage(todo.back().it_prop, tid_).dst - }; - auto acc = twa_->trans_data(todo.back().it_prop, tid_).acc_; - forward_iterators(sys_, twa_, todo.back().it_kripke, - todo.back().it_prop, false, 0); - auto it = map.find(dst); - if (it == map.end()) - { - if (SPOT_LIKELY(self().push_state(dst, dfs_number+1, acc))) - { - map[dst] = ++dfs_number; - todo.push_back({dst, sys_.succ(dst.st_kripke, tid_), - twa_->succ(dst.st_prop)}); - forward_iterators(sys_, twa_, todo.back().it_kripke, - todo.back().it_prop, true, 0); - } - } - else if (SPOT_UNLIKELY(self().update(todo.back().st, - dfs_number, - dst, map[dst], acc))) - return true; - } - } - return false; - } - - unsigned int states() - { - return dfs_number; - } - - unsigned int trans() - { - return transitions; - } - - std::string counterexample() - { - return self().trace(); - } - - public: struct product_state { State st_kripke; @@ -257,80 +126,94 @@ namespace spot struct product_state_hash { size_t - operator()(const product_state that) const noexcept + operator()(const product_state lhs) const noexcept { - // FIXME! wang32_hash(that.st_prop) could have - // been pre-calculated! - StateHash hasher; - return wang32_hash(that.st_prop) ^ hasher(that.st_kripke); + unsigned u = hash(lhs.st_kripke) % (1<<30); + u = wang32_hash(lhs.st_prop) ^ u; + u = u % (1<<30); + return u; } }; - struct todo_element - { - product_state st; - SuccIterator* it_kripke; - std::shared_ptr it_prop; - }; - kripkecube& sys_; - twacube_ptr twa_; - std::vector todo; - typedef std::unordered_map visited_map; - visited_map map; - unsigned int dfs_number = 0; - unsigned int transitions = 0; - unsigned tid_; - bool& stop_; // Do not need to be atomic. - }; - - - - - - - - - - - - - - - - - - - - - - template - class SPOT_API product_to_twa : - public intersect> - { - // Ease the manipulation - using typename intersect>::product_state; - public: product_to_twa(kripkecube& sys, - twacube_ptr twa) - : intersect>(sys, twa) - { - } + twacube_ptr twa): + sys_(sys), twa_(twa) + { + static_assert(spot::is_a_kripkecube_ptr::value, + "error: does not match the kripkecube requirements"); + } - ~product_to_twa() - { - } + virtual ~product_to_twa() + { + map.clear(); + } + + bool run() + { + setup(); + product_state initial = {sys_.initial(0), twa_->get_initial()}; + if (SPOT_LIKELY(push_state(initial, dfs_number_+1, {}))) + { + todo_.push_back({initial, sys_.succ(initial.st_kripke, 0), + twa_->succ(initial.st_prop)}); + + // Not going further! It's a product with a single state. + if (todo_.back().it_prop->done()) + return false; + + forward_iterators(sys_, twa_, todo_.back().it_kripke, + todo_.back().it_prop, true, 0); + map[initial] = ++dfs_number_; + } + while (!todo_.empty()) + { + // Check the kripke is enough since it's the outer loop. More + // details in forward_iterators. + if (todo_.back().it_kripke->done()) + { + bool is_init = todo_.size() == 1; + auto newtop = is_init? todo_.back().st: todo_[todo_.size() -2].st; + if (SPOT_LIKELY(pop_state(todo_.back().st, + map[todo_.back().st], + is_init, + newtop, + map[newtop]))) + { + sys_.recycle(todo_.back().it_kripke, 0); + todo_.pop_back(); + } + } + else + { + ++transitions_; + product_state dst = { + todo_.back().it_kripke->state(), + twa_->trans_storage(todo_.back().it_prop, 0).dst + }; + auto acc = twa_->trans_data(todo_.back().it_prop, 0).acc_; + forward_iterators(sys_, twa_, todo_.back().it_kripke, + todo_.back().it_prop, false, 0); + auto it = map.find(dst); + if (it == map.end()) + { + if (SPOT_LIKELY(push_state(dst, dfs_number_+1, acc))) + { + map[dst] = ++dfs_number_; + todo_.push_back({dst, sys_.succ(dst.st_kripke, 0), + twa_->succ(dst.st_prop)}); + forward_iterators(sys_, twa_, todo_.back().it_kripke, + todo_.back().it_prop, true, 0); + } + } + else if (SPOT_UNLIKELY(update(todo_.back().st, dfs_number_, + dst, map[dst], acc))) + return true; + } + } + return false; + } twa_graph_ptr twa() { @@ -355,19 +238,19 @@ namespace spot bool push_state(product_state s, unsigned i, acc_cond::mark_t) { // push also implies edge (when it's not the initial state) - if (this->todo.size()) + if (this->todo_.size()) { auto c = this->twa_->get_cubeset() .intersection(this->twa_->trans_data - (this->todo.back().it_prop).cube_, - this->todo.back().it_kripke->condition()); + (this->todo_.back().it_prop).cube_, + this->todo_.back().it_kripke->condition()); bdd x = spot::cube_to_bdd(c, this->twa_->get_cubeset(), reverse_binder_); this->twa_->get_cubeset().release(c); - res_->new_edge(this->map[this->todo.back().st]-1, i-1, x, + res_->new_edge(this->map[this->todo_.back().st]-1, i-1, x, this->twa_->trans_data - (this->todo.back().it_prop).acc_); + (this->todo_.back().it_prop).acc_); } unsigned st = res_->new_state(); @@ -377,15 +260,14 @@ namespace spot return true; } - bool update(product_state, unsigned src, product_state, unsigned dst, acc_cond::mark_t cond) { auto c = this->twa_->get_cubeset() .intersection(this->twa_->trans_data - (this->todo.back().it_prop).cube_, - this->todo.back().it_kripke->condition()); + (this->todo_.back().it_prop).cube_, + this->todo_.back().it_kripke->condition()); bdd x = spot::cube_to_bdd(c, this->twa_->get_cubeset(), reverse_binder_); @@ -394,23 +276,29 @@ namespace spot return false; } - // These callbacks are useless here - bool counterexample_found() - { - return false; - } - - std::string trace() - { - return ""; - } - bool pop_state(product_state, unsigned, bool, product_state, unsigned) { return true; } private: + struct todo__element + { + product_state st; + SuccIterator* it_kripke; + std::shared_ptr it_prop; + }; + + typedef std::unordered_map visited_map; + + kripkecube& sys_; + twacube_ptr twa_; + std::vector todo_; + visited_map map; + unsigned int dfs_number_ = 0; + unsigned int transitions_ = 0; spot::twa_graph_ptr res_; std::vector* names_; std::unordered_map reverse_binder_;