diff --git a/spot/ltsmin/spins_kripke.hh b/spot/ltsmin/spins_kripke.hh index d790ac258..7e9eac374 100644 --- a/spot/ltsmin/spins_kripke.hh +++ b/spot/ltsmin/spins_kripke.hh @@ -33,7 +33,6 @@ /// to build a kripke that is thread safe namespace spot { - /// \brief A Spins state is represented as an array of integer /// Note that this array has two reserved slots (position 0 an 1). /// @@ -64,16 +63,33 @@ namespace spot /// \brief The management of states (i.e. allocation/deallocation) can /// be painless since every time we have to consider wether the state will - /// be compressed or not. This class aims to simplify this management + /// be compressed or not. This class aims to simplify this management. class cspins_state_manager final { public: + /// \brief Build a manager for a state of \a state_size variables + /// and indicate wether compression should be used: + /// - 1 for handle large models + /// - 2 (faster) assume all values in [0 .. 2^28-1] cspins_state_manager(unsigned int state_size, int compress); + + /// \brief Get Rid of the internal representation of the state int* unbox_state(cspins_state s) const; - // cmp is the area we can use to compute the compressed rep of dst. - cspins_state alloc_setup(int *dst, int* cmp, size_t cmpsize); + + /// \brief Builder for a state from a raw description given in \a dst + /// + /// \a cmp is the area we can use to compute the compressed + /// representatation of dst. + /// \a cmpsize the size of the previous area + cspins_state alloc_setup(int* dst, int* cmp, size_t cmpsize); + + /// \brief Helper to decompress a state void decompress(cspins_state s, int* uncompressed, unsigned size) const; + + /// \brief Help the manager to reclam the memory of a state void dealloc(cspins_state s); + + /// \brief The size of a state unsigned int size() const; private: @@ -85,56 +101,67 @@ namespace spot void (*fn_decompress_)(const int*, size_t, int*, size_t); }; - - // This structure is used as a parameter during callback when - // generating states from the shared librarie produced by LTSmin + // \brief This structure is used as a parameter during callback when + // generating states from the shared librarie produced by LTSmin. struct inner_callback_parameters { cspins_state_manager* manager; // The state manager std::vector* succ; // The successors of a state - int* compressed_; - int* uncompressed_; - bool compress; - bool selfloopize; + int* compressed; // Area to store compressed state + int* uncompressed; // Area to store uncompressed state + bool compress; // Should the state be compressed? + bool selfloopize; // Should the state be selfloopized }; - // This class provides an iterator over the successors of a state. - // All successors are computed once when an iterator is recycled or - // created. + /// \brief This class provides an iterator over the successors of a state. + /// All successors are computed once when an iterator is recycled or + /// created. + /// + /// Note: Two threads will explore sucessors with two different orders class cspins_iterator final { public: + // Inner struct used to pack the various arguments required by the iterator + struct cspins_iterator_param + { + cspins_state s; + const spot::spins_interface* d; + cspins_state_manager& manager; + inner_callback_parameters& inner; + cube cond; + bool compress; + bool selfloopize; + spot::cubeset& cubeset; + int dead_idx; + unsigned tid; + }; + cspins_iterator(const cspins_iterator&) = delete; cspins_iterator(cspins_iterator&) = delete; - cspins_iterator(cspins_state s, - const spot::spins_interface* d, - cspins_state_manager& manager, - inner_callback_parameters& inner, - cube cond, - bool compress, - bool selfloopize, - cubeset& cubeset, - int dead_idx, unsigned tid); - - void recycle(cspins_state s, - const spot::spins_interface* d, - cspins_state_manager& manager, - inner_callback_parameters& inner, - cube cond, - bool compress, - bool selfloopize, - cubeset& cubeset, int dead_idx, unsigned tid); + cspins_iterator(cspins_iterator_param& p); + void recycle(cspins_iterator_param& p); ~cspins_iterator(); + void next(); bool done() const; cspins_state state() const; cube condition() const; private: - /// Compute the real index in the successor vector + /// \brief Compute the real index in the successor vector unsigned compute_index() const; + inline void setup_iterator(cspins_state s, + const spot::spins_interface* d, + cspins_state_manager& manager, + inner_callback_parameters& inner, + cube& cond, + bool compress, + bool selfloopize, + cubeset& cubeset, + int dead_idx); + std::vector successors_; unsigned int current_; cube cond_; @@ -146,20 +173,36 @@ namespace spot template<> class kripkecube final { - - typedef enum { - OP_EQ_VAR, OP_NE_VAR, OP_LT_VAR, OP_GT_VAR, OP_LE_VAR, OP_GE_VAR, - VAR_OP_EQ, VAR_OP_NE, VAR_OP_LT, VAR_OP_GT, VAR_OP_LE, VAR_OP_GE, - VAR_OP_EQ_VAR, VAR_OP_NE_VAR, VAR_OP_LT_VAR, - VAR_OP_GT_VAR, VAR_OP_LE_VAR, VAR_OP_GE_VAR, VAR_DEAD - } relop; + // Define operators that are available for atomic proposition + enum class relop + { + OP_EQ_VAR, // 1 == a + OP_NE_VAR, // 1 != a + OP_LT_VAR, // 1 < a + OP_GT_VAR, // 1 > a + OP_LE_VAR, // 1 <= a + OP_GE_VAR, // 1 >= a + VAR_OP_EQ, // a == 1 + VAR_OP_NE, // a != 1 + VAR_OP_LT, // a < 1 + VAR_OP_GT, // a >= 1 + VAR_OP_LE, // a <= 1 + VAR_OP_GE, // a >= 1 + VAR_OP_EQ_VAR, // a == b + VAR_OP_NE_VAR, // a != b + VAR_OP_LT_VAR, // a < b + VAR_OP_GT_VAR, // a > b + VAR_OP_LE_VAR, // a <= b + VAR_OP_GE_VAR, // a >= b + VAR_DEAD // The atomic proposition used to label deadlock + }; // Structure for complex atomic proposition struct one_prop { - int lval; - relop op; - int rval; + int lval; // Index of left variable or raw number + relop op; // The operator + int rval; // Index or right variable or raw number }; // Data structure to store complex atomic propositions @@ -176,29 +219,36 @@ namespace spot std::string to_string(const cspins_state s, unsigned tid = 0) const; cspins_iterator* succ(const cspins_state s, unsigned tid); void recycle(cspins_iterator* it, unsigned tid); + + /// \brief List the atomic propositions used by *this* kripke const std::vector get_ap(); + + /// \brief The number of thread used by *this* kripke unsigned get_threads(); private: - /// Parse the set of atomic proposition to have a more + /// \brief Parse the set of atomic proposition to have a more /// efficient data strucure for computation void match_aps(std::vector& aps, std::string dead_prop); - /// Compute the cube associated to each state. The cube + /// \brief Compute the cube associated to each state. The cube /// will then be given to all iterators. void compute_condition(cube c, cspins_state s, unsigned tid = 0); - spins_interface_ptr sip_; + spins_interface_ptr sip_; // The interface to the shared library const spot::spins_interface* d_; // To avoid numerous sip_.get() - cspins_state_manager* manager_; - bool compress_; + cspins_state_manager* manager_; // One manager per thread + bool compress_; // Should a compression be performed + + // One per threads to store no longer used iterators (and save memory) std::vector> recycle_; - inner_callback_parameters* inner_; - cubeset cubeset_; - bool selfloopize_; - int dead_idx_; - std::vector aps_; - unsigned int nb_threads_; + + inner_callback_parameters* inner_; // One callback per thread + cubeset cubeset_; // A single cubeset to manipulate cubes + bool selfloopize_; // Should selfloopize be performed + int dead_idx_; // If yes, index of the "dead ap" + std::vector aps_; // All the atomic propositions + unsigned int nb_threads_; // The number of threads used }; /// \brief shortcut to manipulate the kripke below diff --git a/spot/ltsmin/spins_kripke.hxx b/spot/ltsmin/spins_kripke.hxx index ff6457654..67697aca4 100644 --- a/spot/ltsmin/spins_kripke.hxx +++ b/spot/ltsmin/spins_kripke.hxx @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Développement de +// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de // l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -95,22 +95,35 @@ namespace spot return state_size_; } - - // This class provides an iterator over the successors of a state. - // All successors are computed once when an iterator is recycled or - // created. - cspins_iterator::cspins_iterator(cspins_state s, - const spot::spins_interface* d, - cspins_state_manager& manager, - inner_callback_parameters& inner, - cube cond, - bool compress, - bool selfloopize, - cubeset& cubeset, - int dead_idx, unsigned tid) - : current_(0), cond_(cond), tid_(tid) + cspins_iterator::cspins_iterator(cspins_iterator_param& p) + : current_(0), cond_(p.cond), tid_(p.tid) { successors_.reserve(10); + setup_iterator(p.s, p.d, p.manager, p.inner, p.cond, p.compress, + p.selfloopize, p.cubeset, p.dead_idx); + } + + void cspins_iterator::recycle(cspins_iterator_param& p) + { + tid_ = p.tid; + cond_ = p.cond; + current_ = 0; + // Constant time since int* is is_trivially_destructible + successors_.clear(); + setup_iterator(p.s, p.d, p.manager, p.inner, p.cond, p.compress, + p.selfloopize, p.cubeset, p.dead_idx); + } + + void cspins_iterator::setup_iterator(cspins_state s, + const spot::spins_interface* d, + cspins_state_manager& manager, + inner_callback_parameters& inner, + cube& cond, + bool compress, + bool selfloopize, + cubeset& cubeset, + int dead_idx) + { inner.manager = &manager; inner.succ = &successors_; inner.compress = compress; @@ -119,7 +132,7 @@ namespace spot if (compress) // already filled by compute_condition - ref = inner.uncompressed_; + ref = inner.uncompressed; int n = d->get_successors (nullptr, manager.unbox_state(ref), @@ -127,7 +140,7 @@ namespace spot inner_callback_parameters* inner = static_cast(arg); cspins_state s = - inner->manager->alloc_setup(dst, inner->compressed_, + inner->manager->alloc_setup(dst, inner->compressed, inner->manager->size() * 2); inner->succ->push_back(s); }, @@ -138,49 +151,7 @@ namespace spot if (dead_idx != -1) cubeset.set_true_var(cond, dead_idx); } - } - void cspins_iterator::recycle(cspins_state s, - const spot::spins_interface* d, - cspins_state_manager& manager, - inner_callback_parameters& inner, - cube cond, - bool compress, - bool selfloopize, - cubeset& cubeset, int dead_idx, unsigned tid) - { - tid_ = tid; - cond_ = cond; - current_ = 0; - // Constant time since int* is is_trivially_destructible - successors_.clear(); - inner.manager = &manager; - inner.succ = &successors_; - inner.compress = compress; - inner.selfloopize = selfloopize; - int* ref = s; - - if (compress) - // Already filled by compute_condition - ref = inner.uncompressed_; - - int n = d->get_successors - (nullptr, manager.unbox_state(ref), - [](void* arg, transition_info_t*, int *dst){ - inner_callback_parameters* inner = - static_cast(arg); - cspins_state s = - inner->manager->alloc_setup(dst, inner->compressed_, - inner->manager->size() * 2); - inner->succ->push_back(s); - }, - &inner); - if (!n && selfloopize) - { - successors_.push_back(s); - if (dead_idx != -1) - cubeset.set_true_var(cond, dead_idx); - } } cspins_iterator::~cspins_iterator() @@ -240,8 +211,8 @@ namespace spot recycle_.back().reserve(2000000); new (&manager_[i]) cspins_state_manager(d_->get_state_size(), compress); - inner_[i].compressed_ = new int[d_->get_state_size() * 2]; - inner_[i].uncompressed_ = new int[d_->get_state_size()+30]; + inner_[i].compressed = new int[d_->get_state_size() * 2]; + inner_[i].uncompressed = new int[d_->get_state_size()+30]; } dead_idx_ = -1; match_aps(visible_aps, dead_prop); @@ -262,8 +233,8 @@ namespace spot for (unsigned i = 0; i < nb_threads_; ++i) { manager_[i].~cspins_state_manager(); - delete[] inner_[i].compressed_; - delete[] inner_[i].uncompressed_; + delete[] inner_[i].compressed; + delete[] inner_[i].uncompressed; } ::operator delete(manager_); delete[] inner_; @@ -271,9 +242,9 @@ namespace spot cspins_state kripkecube::initial(unsigned tid) { - d_->get_initial_state(inner_[tid].uncompressed_); - return manager_[tid].alloc_setup(inner_[tid].uncompressed_, - inner_[tid].compressed_, + d_->get_initial_state(inner_[tid].uncompressed); + return manager_[tid].alloc_setup(inner_[tid].uncompressed, + inner_[tid].compressed, manager_[tid].size() * 2); } @@ -286,9 +257,9 @@ namespace spot cspins_state ref = out; if (compress_) { - manager_[tid].decompress(s, inner_[tid].uncompressed_, + manager_[tid].decompress(s, inner_[tid].uncompressed, manager_[tid].size()); - ref = inner_[tid].uncompressed_; + ref = inner_[tid].uncompressed; } for (int i = 0; i < d_->get_state_size(); ++i) res += (d_->get_state_variable_name(i)) + @@ -301,21 +272,26 @@ namespace spot kripkecube::succ(const cspins_state s, unsigned tid) { + cspins_iterator::cspins_iterator_param p = + { + s, d_, manager_[tid], inner_[tid], + nullptr, compress_, selfloopize_, + cubeset_, dead_idx_, tid + }; + if (SPOT_LIKELY(!recycle_[tid].empty())) { auto tmp = recycle_[tid].back(); recycle_[tid].pop_back(); - compute_condition(tmp->condition(), s, tid); - tmp->recycle(s, d_, manager_[tid], inner_[tid], - tmp->condition(), compress_, selfloopize_, - cubeset_, dead_idx_, tid); + p.cond = tmp->condition(); + compute_condition(p.cond, s, tid); + tmp->recycle(p); return tmp; } cube cond = cubeset_.alloc(); + p.cond = cond; compute_condition(cond, s, tid); - return new cspins_iterator(s, d_, manager_[tid], inner_[tid], - cond, compress_, selfloopize_, - cubeset_, dead_idx_, tid); + return new cspins_iterator(p); } void @@ -346,9 +322,9 @@ namespace spot // State is compressed, uncompress it if (compress_) { - manager_[tid].decompress(s, inner_[tid].uncompressed_+2, + manager_[tid].decompress(s, inner_[tid].uncompressed+2, manager_[tid].size()); - vars = inner_[tid].uncompressed_ + 2; + vars = inner_[tid].uncompressed + 2; } for (auto& ap: pset_) @@ -357,61 +333,61 @@ namespace spot bool cond = false; switch (ap.op) { - case OP_EQ_VAR: + case relop::OP_EQ_VAR: cond = (ap.lval == vars[ap.rval]); break; - case OP_NE_VAR: + case relop::OP_NE_VAR: cond = (ap.lval != vars[ap.rval]); break; - case OP_LT_VAR: + case relop::OP_LT_VAR: cond = (ap.lval < vars[ap.rval]); break; - case OP_GT_VAR: + case relop::OP_GT_VAR: cond = (ap.lval > vars[ap.rval]); break; - case OP_LE_VAR: + case relop::OP_LE_VAR: cond = (ap.lval <= vars[ap.rval]); break; - case OP_GE_VAR: + case relop::OP_GE_VAR: cond = (ap.lval >= vars[ap.rval]); break; - case VAR_OP_EQ: + case relop::VAR_OP_EQ: cond = (vars[ap.lval] == ap.rval); break; - case VAR_OP_NE: + case relop::VAR_OP_NE: cond = (vars[ap.lval] != ap.rval); break; - case VAR_OP_LT: + case relop::VAR_OP_LT: cond = (vars[ap.lval] < ap.rval); break; - case VAR_OP_GT: + case relop::VAR_OP_GT: cond = (vars[ap.lval] > ap.rval); break; - case VAR_OP_LE: + case relop::VAR_OP_LE: cond = (vars[ap.lval] <= ap.rval); break; - case VAR_OP_GE: + case relop::VAR_OP_GE: cond = (vars[ap.lval] >= ap.rval); break; - case VAR_OP_EQ_VAR: + case relop::VAR_OP_EQ_VAR: cond = (vars[ap.lval] == vars[ap.rval]); break; - case VAR_OP_NE_VAR: + case relop::VAR_OP_NE_VAR: cond = (vars[ap.lval] != vars[ap.rval]); break; - case VAR_OP_LT_VAR: + case relop::VAR_OP_LT_VAR: cond = (vars[ap.lval] < vars[ap.rval]); break; - case VAR_OP_GT_VAR: + case relop::VAR_OP_GT_VAR: cond = (vars[ap.lval] > vars[ap.rval]); break; - case VAR_OP_LE_VAR: + case relop::VAR_OP_LE_VAR: cond = (vars[ap.lval] <= vars[ap.rval]); break; - case VAR_OP_GE_VAR: + case relop::VAR_OP_GE_VAR: cond = (vars[ap.lval] >= vars[ap.rval]); break; - case VAR_DEAD: + case relop::VAR_DEAD: break; default: SPOT_ASSERT(false); @@ -465,7 +441,7 @@ namespace spot if (ap.compare(dead_prop) == 0) { dead_idx_ = i; - pset_.push_back({i , VAR_DEAD, 0}); + pset_.push_back({i , relop::VAR_DEAD, 0}); continue; } @@ -483,7 +459,7 @@ namespace spot // The aps is directly an AP of the system, we will just // have to detect if the variable is 0 or not. pset_.push_back({(int)std::distance(k_aps.begin(), it), - VAR_OP_NE, 0}); + relop::VAR_OP_NE, 0}); continue; } @@ -534,7 +510,6 @@ namespace spot // And finally the operator relop oper; - // Now, left and (possibly) right may refer atomic // propositions or specific state inside of a process. // First check if it is a known atomic proposition @@ -586,7 +561,7 @@ namespace spot (int) std::distance(k_aps.begin(), std::find(k_aps.begin(), k_aps.end(), proc_name)), - VAR_OP_EQ, ei->second}); + relop::VAR_OP_EQ, ei->second}); continue; } else @@ -631,7 +606,7 @@ namespace spot (int) std::distance(k_aps.begin(), std::find(k_aps.begin(), k_aps.end(), right)), - VAR_OP_EQ, ei->second}); + relop::VAR_OP_EQ, ei->second}); continue; } } @@ -711,7 +686,7 @@ namespace spot (int) std::distance(k_aps.begin(), std::find(k_aps.begin(), k_aps.end(), left)), - VAR_OP_EQ, ei->second}); + relop::VAR_OP_EQ, ei->second}); continue; } } @@ -729,23 +704,23 @@ namespace spot // Left and Right are know, just analyse the operator. if (op.compare("==") == 0) - oper = !left_is_digit && !right_is_digit? VAR_OP_EQ_VAR : - (left_is_digit? OP_EQ_VAR : VAR_OP_EQ); + oper = !left_is_digit && !right_is_digit? relop::VAR_OP_EQ_VAR : + (left_is_digit? relop::OP_EQ_VAR : relop::VAR_OP_EQ); else if (op.compare("!=") == 0) - oper = !left_is_digit && !right_is_digit? VAR_OP_NE_VAR : - (left_is_digit? OP_NE_VAR : VAR_OP_NE); + oper = !left_is_digit && !right_is_digit? relop::VAR_OP_NE_VAR : + (left_is_digit? relop::OP_NE_VAR : relop::VAR_OP_NE); else if (op.compare("<") == 0) - oper = !left_is_digit && !right_is_digit? VAR_OP_LT_VAR : - (left_is_digit? OP_LT_VAR : VAR_OP_LT); + oper = !left_is_digit && !right_is_digit? relop::VAR_OP_LT_VAR : + (left_is_digit? relop::OP_LT_VAR : relop::VAR_OP_LT); else if (op.compare(">") == 0) - oper = !left_is_digit && !right_is_digit? VAR_OP_GT_VAR : - (left_is_digit? OP_GT_VAR : VAR_OP_GT); + oper = !left_is_digit && !right_is_digit? relop::VAR_OP_GT_VAR : + (left_is_digit? relop::OP_GT_VAR : relop::VAR_OP_GT); else if (op.compare("<=") == 0) - oper = !left_is_digit && !right_is_digit? VAR_OP_LE_VAR : - (left_is_digit? OP_LE_VAR : VAR_OP_LE); + oper = !left_is_digit && !right_is_digit? relop::VAR_OP_LE_VAR : + (left_is_digit? relop::OP_LE_VAR : relop::VAR_OP_LE); else if (op.compare(">=") == 0) - oper = !left_is_digit && !right_is_digit? VAR_OP_GE_VAR : - (left_is_digit? OP_GE_VAR : VAR_OP_GE); + oper = !left_is_digit && !right_is_digit? relop::VAR_OP_GE_VAR : + (left_is_digit? relop::OP_GE_VAR : relop::VAR_OP_GE); else { err << "\nOperation \"" << op