diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc index f5755408a..0d08a8b6c 100644 --- a/spot/ltsmin/ltsmin.cc +++ b/spot/ltsmin/ltsmin.cc @@ -1144,9 +1144,8 @@ namespace spot } }; - //brick::hashset::FastConcurrent ht2; typedef brick::hashset::FastConcurrent cspins_state_map; + cspins_state_hasher> cspins_state_map; //////////////////////////////////////////////////////////////////////// // A manager for Cspins states. @@ -1205,9 +1204,9 @@ namespace spot void dealloc(cspins_state s) { if (compress_) - msp_.deallocate(s, (s[1]+2)*sizeof(int)); + msp_.deallocate(s, (s[1]+2)*sizeof(int)); else - p_.deallocate(s); + p_.deallocate(s); } unsigned int size() const @@ -1249,15 +1248,15 @@ namespace spot { public: cspins_iterator(cspins_state s, - const spot::spins_interface* d, - cspins_state_manager& manager, - cspins_state_map& map, - inner_callback_parameters& inner, - int defvalue, - cube cond, - bool compress, - bool selfloopize, - cubeset& cubeset, int dead_idx) + const spot::spins_interface* d, + cspins_state_manager& manager, + cspins_state_map& map, + inner_callback_parameters& inner, + int defvalue, + cube cond, + bool compress, + bool selfloopize, + cubeset& cubeset, int dead_idx) : current_(0), cond_(cond) { successors_.reserve(10); @@ -1270,41 +1269,41 @@ namespace spot int* ref = s; if (compress) - // already filled by compute_condition - ref = inner.uncompressed_; + // 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); - auto it = inner->map->insert({s}); - inner->succ->push_back(*it); - if (!it.isnew()) - inner->manager->dealloc(s); - }, - &inner); + (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); + auto it = inner->map->insert({s}); + inner->succ->push_back(*it); + if (!it.isnew()) + inner->manager->dealloc(s); + }, + &inner); if (!n && selfloopize) - { - successors_.push_back(s); - if (dead_idx != -1) - cubeset.set_true_var(cond, dead_idx); - } + { + successors_.push_back(s); + if (dead_idx != -1) + cubeset.set_true_var(cond, dead_idx); + } } void recycle(cspins_state s, - const spot::spins_interface* d, - cspins_state_manager& manager, - cspins_state_map& map, - inner_callback_parameters& inner, - int defvalue, - cube cond, - bool compress, - bool selfloopize, - cubeset& cubeset, int dead_idx) + const spot::spins_interface* d, + cspins_state_manager& manager, + cspins_state_map& map, + inner_callback_parameters& inner, + int defvalue, + cube cond, + bool compress, + bool selfloopize, + cubeset& cubeset, int dead_idx) { cond_ = cond; current_ = 0; @@ -1319,35 +1318,35 @@ namespace spot int* ref = s; if (compress) - // Already filled by compute_condition - ref = inner.uncompressed_; + // 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); - auto it = inner->map->insert({s}); - inner->succ->push_back(*it); - if (!it.isnew()) - inner->manager->dealloc(s); - }, - &inner); + (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); + auto it = inner->map->insert({s}); + inner->succ->push_back(*it); + if (!it.isnew()) + inner->manager->dealloc(s); + }, + &inner); if (!n && selfloopize) - { - successors_.push_back(s); - if (dead_idx != -1) - cubeset.set_true_var(cond, dead_idx); - } + { + successors_.push_back(s); + if (dead_idx != -1) + cubeset.set_true_var(cond, dead_idx); + } } ~cspins_iterator() { - // Do not release successors states, the manager - // will do it on time. + // Do not release successors states, the manager + // will do it on time. } void next() @@ -1420,20 +1419,20 @@ namespace spot } ~kripkecube() { - for (auto i: recycle_) - { - cubeset_.release(i->condition()); - delete i; - } - delete inner_.compressed_; - delete inner_.uncompressed_; + for (auto i: recycle_) + { + cubeset_.release(i->condition()); + delete i; + } + delete inner_.compressed_; + delete inner_.uncompressed_; } cspins_state initial() { d_->get_initial_state(inner_.uncompressed_); return manager_.alloc_setup(inner_.uncompressed_, inner_.compressed_, - manager_.size() * 2); + manager_.size() * 2); } std::string to_string(const cspins_state s) const @@ -1442,13 +1441,13 @@ namespace spot cspins_state out = manager_.unbox_state(s); cspins_state ref = out; if (compress_) - { - manager_.decompress(s, inner_.uncompressed_, manager_.size()); - ref = inner_.uncompressed_; - } + { + manager_.decompress(s, inner_.uncompressed_, manager_.size()); + ref = inner_.uncompressed_; + } for (int i = 0; i < d_->get_state_size(); ++i) - res += (d_->get_state_variable_name(i)) + - ("=" + std::to_string(ref[i])) + ","; + res += (d_->get_state_variable_name(i)) + + ("=" + std::to_string(ref[i])) + ","; res.pop_back(); return res; } @@ -1456,20 +1455,20 @@ namespace spot cspins_iterator* succ(const cspins_state s) { if (SPOT_LIKELY(!recycle_.empty())) - { - auto tmp = recycle_.back(); - recycle_.pop_back(); - compute_condition(tmp->condition(), s); - tmp->recycle(s, d_, manager_, map_, inner_, -1, - tmp->condition(), compress_, selfloopize_, - cubeset_, dead_idx_); - return tmp; - } + { + auto tmp = recycle_.back(); + recycle_.pop_back(); + compute_condition(tmp->condition(), s); + tmp->recycle(s, d_, manager_, map_, inner_, -1, + tmp->condition(), compress_, selfloopize_, + cubeset_, dead_idx_); + return tmp; + } cube cond = cubeset_.alloc(); compute_condition(cond, s); return new cspins_iterator(s, d_, manager_, map_, inner_, - -1, cond, compress_, selfloopize_, - cubeset_, dead_idx_); + -1, cond, compress_, selfloopize_, + cubeset_, dead_idx_); } void recycle(cspins_iterator* it) @@ -1518,80 +1517,80 @@ namespace spot // State is compressed, uncompress it if (compress_) { - manager_.decompress(s, inner_.uncompressed_+2, manager_.size()); - vars = inner_.uncompressed_ + 2; + manager_.decompress(s, inner_.uncompressed_+2, manager_.size()); + vars = inner_.uncompressed_ + 2; } for (auto& ap: pset_) { - ++i; - bool cond = false; - switch (ap.op) - { - case OP_EQ_VAR: - cond = (ap.lval == vars[ap.rval]); - break; - case OP_NE_VAR: - cond = (ap.lval != vars[ap.rval]); - break; - case OP_LT_VAR: - cond = (ap.lval < vars[ap.rval]); - break; - case OP_GT_VAR: - cond = (ap.lval > vars[ap.rval]); - break; - case OP_LE_VAR: - cond = (ap.lval <= vars[ap.rval]); - break; - case OP_GE_VAR: - cond = (ap.lval >= vars[ap.rval]); - break; - case VAR_OP_EQ: - cond = (vars[ap.lval] == ap.rval); - break; - case VAR_OP_NE: - cond = (vars[ap.lval] != ap.rval); - break; - case VAR_OP_LT: - cond = (vars[ap.lval] < ap.rval); - break; - case VAR_OP_GT: - cond = (vars[ap.lval] > ap.rval); - break; - case VAR_OP_LE: - cond = (vars[ap.lval] <= ap.rval); - break; - case VAR_OP_GE: - cond = (vars[ap.lval] >= ap.rval); - break; - case VAR_OP_EQ_VAR: - cond = (vars[ap.lval] == vars[ap.rval]); - break; - case VAR_OP_NE_VAR: - cond = (vars[ap.lval] != vars[ap.rval]); - break; - case VAR_OP_LT_VAR: - cond = (vars[ap.lval] < vars[ap.rval]); - break; - case VAR_OP_GT_VAR: - cond = (vars[ap.lval] > vars[ap.rval]); - break; - case VAR_OP_LE_VAR: - cond = (vars[ap.lval] <= vars[ap.rval]); - break; - case VAR_OP_GE_VAR: - cond = (vars[ap.lval] >= vars[ap.rval]); - break; - case VAR_DEAD: - break; - default: - assert(false); - } + ++i; + bool cond = false; + switch (ap.op) + { + case OP_EQ_VAR: + cond = (ap.lval == vars[ap.rval]); + break; + case OP_NE_VAR: + cond = (ap.lval != vars[ap.rval]); + break; + case OP_LT_VAR: + cond = (ap.lval < vars[ap.rval]); + break; + case OP_GT_VAR: + cond = (ap.lval > vars[ap.rval]); + break; + case OP_LE_VAR: + cond = (ap.lval <= vars[ap.rval]); + break; + case OP_GE_VAR: + cond = (ap.lval >= vars[ap.rval]); + break; + case VAR_OP_EQ: + cond = (vars[ap.lval] == ap.rval); + break; + case VAR_OP_NE: + cond = (vars[ap.lval] != ap.rval); + break; + case VAR_OP_LT: + cond = (vars[ap.lval] < ap.rval); + break; + case VAR_OP_GT: + cond = (vars[ap.lval] > ap.rval); + break; + case VAR_OP_LE: + cond = (vars[ap.lval] <= ap.rval); + break; + case VAR_OP_GE: + cond = (vars[ap.lval] >= ap.rval); + break; + case VAR_OP_EQ_VAR: + cond = (vars[ap.lval] == vars[ap.rval]); + break; + case VAR_OP_NE_VAR: + cond = (vars[ap.lval] != vars[ap.rval]); + break; + case VAR_OP_LT_VAR: + cond = (vars[ap.lval] < vars[ap.rval]); + break; + case VAR_OP_GT_VAR: + cond = (vars[ap.lval] > vars[ap.rval]); + break; + case VAR_OP_LE_VAR: + cond = (vars[ap.lval] <= vars[ap.rval]); + break; + case VAR_OP_GE_VAR: + cond = (vars[ap.lval] >= vars[ap.rval]); + break; + case VAR_DEAD: + break; + default: + assert(false); + } - if (cond) - cubeset_.set_true_var(c, i); - else - cubeset_.set_false_var(c, i); + if (cond) + cubeset_.set_true_var(c, i); + else + cubeset_.set_false_var(c, i); } } @@ -1615,10 +1614,10 @@ namespace spot std::unordered_map matcher; for (int i = 0; i < type_count; ++i) { - matcher[d_->get_type_name(i)] = i; - int enum_count = d_->get_type_value_count(i); - for (int j = 0; j < enum_count; ++j) - enum_map[i].emplace(d_->get_type_value_name(i, j), j); + matcher[d_->get_type_name(i)] = i; + int enum_count = d_->get_type_value_count(i); + for (int j = 0; j < enum_count; ++j) + enum_map[i].emplace(d_->get_type_value_name(i, j), j); } // Then we extract the basic atomics propositions from the Kripke @@ -1630,308 +1629,308 @@ namespace spot int i = -1; for (auto ap: aps) { - ++i; + ++i; - // Grab dead property - if (ap.compare(dead_prop) == 0) - { - dead_idx_ = i; - pset_.push_back({i , VAR_DEAD, 0}); - continue; - } + // Grab dead property + if (ap.compare(dead_prop) == 0) + { + dead_idx_ = i; + pset_.push_back({i , VAR_DEAD, 0}); + continue; + } - // Get ap name and remove all extra whitespace - ap.erase(std::remove_if(ap.begin(), ap.end(), - [](char x){ - return std::isspace(x); - }), - ap.end()); + // Get ap name and remove all extra whitespace + ap.erase(std::remove_if(ap.begin(), ap.end(), + [](char x){ + return std::isspace(x); + }), + ap.end()); - // Look if it is a well known atomic proposition - auto it = std::find(k_aps.begin(), k_aps.end(), ap); - if (it != k_aps.end()) - { - // 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}); - continue; - } + // Look if it is a well known atomic proposition + auto it = std::find(k_aps.begin(), k_aps.end(), ap); + if (it != k_aps.end()) + { + // 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}); + continue; + } - // The ap is not known. We distinguish many cases: - // - It is a State name, i.e P_0.S or P_0 == S - // - It refers a specific variable value, i.e. P_0.var == 2, - // P_0.var < 2, P_0.var != 2, ... - // - It's an unknown variable - // Note that we do not support P_0.state1 == 12 since we do not - // know how to interpret such atomic proposition. + // The ap is not known. We distinguish many cases: + // - It is a State name, i.e P_0.S or P_0 == S + // - It refers a specific variable value, i.e. P_0.var == 2, + // P_0.var < 2, P_0.var != 2, ... + // - It's an unknown variable + // Note that we do not support P_0.state1 == 12 since we do not + // know how to interpret such atomic proposition. - // We split the formula according to operators - std::size_t found_op_first = ap.find_first_of("=<>!"); - std::size_t found_op_last = ap.find_last_of("=<>!"); - std::string left; - std::string right; - std::string ap_error; - std::string op; + // We split the formula according to operators + std::size_t found_op_first = ap.find_first_of("=<>!"); + std::size_t found_op_last = ap.find_last_of("=<>!"); + std::string left; + std::string right; + std::string ap_error; + std::string op; - if (found_op_first == 0 || found_op_last == ap.size()-1) - { - err << "Invalid operator use in " << ap << '\n'; - ++errors; - continue; - } + if (found_op_first == 0 || found_op_last == ap.size()-1) + { + err << "Invalid operator use in " << ap << '\n'; + ++errors; + continue; + } - if (std::string::npos == found_op_first) - { - left = ap; - right = ""; - op = ""; - } - else - { - left = ap.substr(0, found_op_first); - right = ap.substr(found_op_last+1, ap.size()-found_op_last); - op = ap.substr(found_op_first, found_op_last+1-found_op_first); - } + if (std::string::npos == found_op_first) + { + left = ap; + right = ""; + op = ""; + } + else + { + left = ap.substr(0, found_op_first); + right = ap.substr(found_op_last+1, ap.size()-found_op_last); + op = ap.substr(found_op_first, found_op_last+1-found_op_first); + } - // Variables to store the left part of the atomic proposition - bool left_is_digit = false; - int lval; + // Variables to store the left part of the atomic proposition + bool left_is_digit = false; + int lval; - // Variables to store the right part of the atomic proposition - bool right_is_digit = false; - int rval; + // Variables to store the right part of the atomic proposition + bool right_is_digit = false; + int rval; - // And finally the operator - relop oper; + // And finally the operator + relop oper; - // Now, left and (possibly) right are should refer atomic - // propositions or specific state inside of a process. - // First check if it is a known atomic proposition - it = std::find(k_aps.begin(), k_aps.end(), left); - if (it != k_aps.end()) - { - // The aps is directly an AP of the system, we will just - // have to detect if the variable is 0 or not. - lval = std::distance(k_aps.begin(), it); - } - else - { - // Detect if it is a process state - std::size_t found_dot = left.find_first_of('.'); - if (std::string::npos != found_dot) - { - std::string proc_name = left.substr(0, found_dot); - std::string st_name = left.substr(found_dot+1, - left.size()-found_dot); + // Now, left and (possibly) right are should refer atomic + // propositions or specific state inside of a process. + // First check if it is a known atomic proposition + it = std::find(k_aps.begin(), k_aps.end(), left); + if (it != k_aps.end()) + { + // The aps is directly an AP of the system, we will just + // have to detect if the variable is 0 or not. + lval = std::distance(k_aps.begin(), it); + } + else + { + // Detect if it is a process state + std::size_t found_dot = left.find_first_of('.'); + if (std::string::npos != found_dot) + { + std::string proc_name = left.substr(0, found_dot); + std::string st_name = left.substr(found_dot+1, + left.size()-found_dot); - auto ni = matcher.find(proc_name); - if (ni == matcher.end()) - { - ap_error = left; - goto error_ap_unknown; - } - int type_num = ni->second; - enum_map_t::const_iterator ei = - enum_map[type_num].find(st_name); - if (ei == enum_map[type_num].end()) - { - ap_error = left; - goto error_ap_unknown; - } + auto ni = matcher.find(proc_name); + if (ni == matcher.end()) + { + ap_error = left; + goto error_ap_unknown; + } + int type_num = ni->second; + enum_map_t::const_iterator ei = + enum_map[type_num].find(st_name); + if (ei == enum_map[type_num].end()) + { + ap_error = left; + goto error_ap_unknown; + } - if (right.compare("") != 0) - { - // We are in the case P.state1 == something.. We don't - // know how to interpret this. - ap_error = op + right; - err << "\nOperation " << op << " in \"" << ap_error - << "\" is not available for process's state" - << " (i.e. " << left << ")\n"; - ++errors; - continue; - } + if (right.compare("") != 0) + { + // We are in the case P.state1 == something.. We don't + // know how to interpret this. + ap_error = op + right; + err << "\nOperation " << op << " in \"" << ap_error + << "\" is not available for process's state" + << " (i.e. " << left << ")\n"; + ++errors; + continue; + } - pset_.push_back({ - (int) std::distance(k_aps.begin(), - std::find(k_aps.begin(), - k_aps.end(), proc_name)), - VAR_OP_EQ, ei->second}); - continue; - } - else - { - // Finally, it's a number... - left_is_digit = true; - for (auto c: left) - if (!isdigit(c)) - left_is_digit = false; + pset_.push_back({ + (int) std::distance(k_aps.begin(), + std::find(k_aps.begin(), + k_aps.end(), proc_name)), + VAR_OP_EQ, ei->second}); + continue; + } + else + { + // Finally, it's a number... + left_is_digit = true; + for (auto c: left) + if (!isdigit(c)) + left_is_digit = false; - if (left_is_digit) - lval = std::strtol (left.c_str(), nullptr, 10); - else - { - // ... or something like: State1 == P_0 - // so it doesn't contains '.' - if (std::string::npos != right.find_first_of('.')) - { - err << "\nOperation \"" << right - << "\" does not refer a process" - << " (i.e. " << left << " is not valid)\n"; - ++errors; - continue; - } + if (left_is_digit) + lval = std::strtol (left.c_str(), nullptr, 10); + else + { + // ... or something like: State1 == P_0 + // so it doesn't contains '.' + if (std::string::npos != right.find_first_of('.')) + { + err << "\nOperation \"" << right + << "\" does not refer a process" + << " (i.e. " << left << " is not valid)\n"; + ++errors; + continue; + } - // or something like: P_0 == State1 - auto ni = matcher.find(right); - if (ni == matcher.end()) - { - ap_error = ap; - goto error_ap_unknown; - } - int type_num = ni->second; - enum_map_t::const_iterator ei = - enum_map[type_num].find(left); - if (ei == enum_map[type_num].end()) - { - ap_error = left; - goto error_ap_unknown; - } - pset_.push_back({ - (int) std::distance(k_aps.begin(), - std::find(k_aps.begin(), - k_aps.end(), right)), - VAR_OP_EQ, ei->second}); - continue; - } - } - } + // or something like: P_0 == State1 + auto ni = matcher.find(right); + if (ni == matcher.end()) + { + ap_error = ap; + goto error_ap_unknown; + } + int type_num = ni->second; + enum_map_t::const_iterator ei = + enum_map[type_num].find(left); + if (ei == enum_map[type_num].end()) + { + ap_error = left; + goto error_ap_unknown; + } + pset_.push_back({ + (int) std::distance(k_aps.begin(), + std::find(k_aps.begin(), + k_aps.end(), right)), + VAR_OP_EQ, ei->second}); + continue; + } + } + } - // Here Left is known. Just detect cases where left is digit there is - // no right part. - if (left_is_digit && right.empty()) - { - ap_error = ap; - goto error_ap_unknown; - } + // Here Left is known. Just detect cases where left is digit there is + // no right part. + if (left_is_digit && right.empty()) + { + ap_error = ap; + goto error_ap_unknown; + } - assert(!right.empty() && !op.empty()); + assert(!right.empty() && !op.empty()); - // Parse right part of the atomic proposition - // Check if it is a known atomic proposition - it = std::find(k_aps.begin(), k_aps.end(), right); - if (it != k_aps.end()) - { - // The aps is directly an AP of the system, we will just - // have to detect if the variable is 0 or not. - rval = std::distance(k_aps.begin(), it); - } - else - { - // We are is the right part, so if it is a process state - // we do not know how to interpret (xxx == P.state1). Abort - std::size_t found_dot = right.find_first_of('.'); - if (std::string::npos != found_dot) - { - ap_error = left + op; - err << "\nOperation " << op << " in \"" << ap_error - << "\" is not available for process's state" - << " (i.e. " << right << ")\n"; - ++errors; - continue; - } - else - { - // Finally, it's a number - right_is_digit = true; - for (auto c: right) - if (!isdigit(c)) - right_is_digit = false; + // Parse right part of the atomic proposition + // Check if it is a known atomic proposition + it = std::find(k_aps.begin(), k_aps.end(), right); + if (it != k_aps.end()) + { + // The aps is directly an AP of the system, we will just + // have to detect if the variable is 0 or not. + rval = std::distance(k_aps.begin(), it); + } + else + { + // We are is the right part, so if it is a process state + // we do not know how to interpret (xxx == P.state1). Abort + std::size_t found_dot = right.find_first_of('.'); + if (std::string::npos != found_dot) + { + ap_error = left + op; + err << "\nOperation " << op << " in \"" << ap_error + << "\" is not available for process's state" + << " (i.e. " << right << ")\n"; + ++errors; + continue; + } + else + { + // Finally, it's a number + right_is_digit = true; + for (auto c: right) + if (!isdigit(c)) + right_is_digit = false; - if (right_is_digit) - rval = std::strtol (right.c_str(), nullptr, 10); - else - { - if (std::string::npos != left.find_first_of('.')) - { - err << "\nProposition \"" << ap - << "\" cannot be interpreted" - << " (i.e. " << op + right << " is not valid)\n"; - ++errors; - continue; - } + if (right_is_digit) + rval = std::strtol (right.c_str(), nullptr, 10); + else + { + if (std::string::npos != left.find_first_of('.')) + { + err << "\nProposition \"" << ap + << "\" cannot be interpreted" + << " (i.e. " << op + right << " is not valid)\n"; + ++errors; + continue; + } - // or something like: P_0 == State1 - auto ni = matcher.find(left); - if (ni == matcher.end()) - { + // or something like: P_0 == State1 + auto ni = matcher.find(left); + if (ni == matcher.end()) + { - ap_error = left; - goto error_ap_unknown; - } - int type_num = ni->second; - enum_map_t::const_iterator ei = - enum_map[type_num].find(right); - if (ei == enum_map[type_num].end()) - { - ap_error = right; - goto error_ap_unknown; - } - pset_.push_back({ - (int) std::distance(k_aps.begin(), - std::find(k_aps.begin(), - k_aps.end(), left)), - VAR_OP_EQ, ei->second}); - continue; - } - } - } + ap_error = left; + goto error_ap_unknown; + } + int type_num = ni->second; + enum_map_t::const_iterator ei = + enum_map[type_num].find(right); + if (ei == enum_map[type_num].end()) + { + ap_error = right; + goto error_ap_unknown; + } + pset_.push_back({ + (int) std::distance(k_aps.begin(), + std::find(k_aps.begin(), + k_aps.end(), left)), + VAR_OP_EQ, ei->second}); + continue; + } + } + } - if (left_is_digit && right_is_digit) - { - err << "\nOperation \"" << op - << "\" between two numbers not available" - << " (i.e. " << right << " and, " - << left << ")\n"; - ++errors; - continue; - } + if (left_is_digit && right_is_digit) + { + err << "\nOperation \"" << op + << "\" between two numbers not available" + << " (i.e. " << right << " and, " + << left << ")\n"; + ++errors; + continue; + } - // 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); - 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); - 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); - 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); - 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); - 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); - else - { - err << "\nOperation \"" << op - << "\" is unknown\n"; - ++errors; - continue; - } + // 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); + 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); + 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); + 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); + 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); + 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); + else + { + err << "\nOperation \"" << op + << "\" is unknown\n"; + ++errors; + continue; + } - pset_.push_back({lval, oper, rval}); - continue; + pset_.push_back({lval, oper, rval}); + continue; error_ap_unknown: - err << "\nProposition \"" << ap_error << "\" does not exist\n"; - ++errors; - continue; + err << "\nProposition \"" << ap_error << "\" does not exist\n"; + ++errors; + continue; } if (errors) diff --git a/spot/mc/ec.hh b/spot/mc/ec.hh index f2ffee636..8bac1f859 100644 --- a/spot/mc/ec.hh +++ b/spot/mc/ec.hh @@ -31,24 +31,24 @@ namespace spot /// emptiness check that has been proposed we opted to implement /// the Gabow's one. template + typename StateHash, typename StateEqual> class ec_renault13lpar : public intersect> + StateHash, StateEqual, + ec_renault13lpar> { // Ease the manipulation using typename intersect>::product_state; + ec_renault13lpar>::product_state; public: ec_renault13lpar(kripkecube& sys, twacube* twa) : intersect>(sys, twa), + ec_renault13lpar>(sys, twa), acc_(twa->acc()) { } @@ -84,13 +84,13 @@ namespace spot /// to true and both \a newtop and \a newtop_dfsnum have inconsistency /// values. bool pop_state(product_state, unsigned top_dfsnum, bool, - product_state, unsigned) + product_state, unsigned) { if (top_dfsnum == roots_.back().dfsnum) - { - roots_.pop_back(); - uf_.markdead(top_dfsnum); - } + { + roots_.pop_back(); + uf_.markdead(top_dfsnum); + } return true; } @@ -101,7 +101,7 @@ namespace spot acc_cond::mark_t cond) { if (uf_.isdead(dst_dfsnum)) - return false; + return false; while (!uf_.sameset(dst_dfsnum, roots_.back().dfsnum)) { @@ -127,18 +127,18 @@ namespace spot // Compute the prefix of the accepting run for (auto& s : this->todo) - res += " " + std::to_string(s.st.st_prop) + - + "*" + this->sys_.to_string(s.st.st_kripke) + "\n"; + res += " " + std::to_string(s.st.st_prop) + + + "*" + this->sys_.to_string(s.st.st_kripke) + "\n"; // Compute the accepting cycle res += "Cycle:\n"; struct ctrx_element { - const product_state* prod_st; - ctrx_element* parent_st; - SuccIterator* it_kripke; - std::shared_ptr it_prop; + const product_state* prod_st; + ctrx_element* parent_st; + SuccIterator* it_kripke; + std::shared_ptr it_prop; }; std::queue bfs; @@ -148,65 +148,65 @@ namespace spot this->sys_.succ(this->todo.back().st.st_kripke), this->twa_->succ(this->todo.back().st.st_prop)})); while (true) - { - here: - auto* front = bfs.front(); - bfs.pop(); - // PUSH all successors of the state. - while (!front->it_kripke->done()) - { - while (!front->it_prop->done()) - { - if (this->twa_->get_cubeset().intersect - (this->twa_->trans_data(front->it_prop).cube_, - front->it_kripke->condition())) - { - const product_state dst = { - front->it_kripke->state(), - this->twa_->trans_storage(front->it_prop).dst - }; + { + here: + auto* front = bfs.front(); + bfs.pop(); + // PUSH all successors of the state. + while (!front->it_kripke->done()) + { + while (!front->it_prop->done()) + { + if (this->twa_->get_cubeset().intersect + (this->twa_->trans_data(front->it_prop).cube_, + front->it_kripke->condition())) + { + const product_state dst = { + front->it_kripke->state(), + this->twa_->trans_storage(front->it_prop).dst + }; - // Skip Unknown states or not same SCC - auto it = this->map.find(dst); - if (it == this->map.end() || - !uf_.sameset(it->second, - this->map[this->todo.back().st])) - { - front->it_prop->next(); - continue; - } + // Skip Unknown states or not same SCC + auto it = this->map.find(dst); + if (it == this->map.end() || + !uf_.sameset(it->second, + this->map[this->todo.back().st])) + { + front->it_prop->next(); + continue; + } - // This is a valid transition. If this transition - // is the one we are looking for, update the counter- - // -example and flush the bfs queue. - auto mark = this->twa_->trans_data(front->it_prop).acc_; - if (!acc.has(mark)) - { - ctrx_element* current = front; - while (current != nullptr) - { - // FIXME also display acc? - res = res + " " + - std::to_string(current->prod_st->st_prop) + - + "*" + - this->sys_. to_string(current->prod_st - ->st_kripke) + - "\n"; - current = current->parent_st; - } + // This is a valid transition. If this transition + // is the one we are looking for, update the counter- + // -example and flush the bfs queue. + auto mark = this->twa_->trans_data(front->it_prop).acc_; + if (!acc.has(mark)) + { + ctrx_element* current = front; + while (current != nullptr) + { + // FIXME also display acc? + res = res + " " + + std::to_string(current->prod_st->st_prop) + + + "*" + + this->sys_. to_string(current->prod_st + ->st_kripke) + + "\n"; + current = current->parent_st; + } - // empty the queue - while (!bfs.empty()) - { - auto* e = bfs.front(); - bfs.pop(); - delete e; - } + // empty the queue + while (!bfs.empty()) + { + auto* e = bfs.front(); + bfs.pop(); + delete e; + } - // update acceptance - acc |= mark; - if (this->twa_->acc().accepting(acc)) - return res; + // update acceptance + acc |= mark; + if (this->twa_->acc().accepting(acc)) + return res; const product_state* q = &(it->first); ctrx_element* root = new ctrx_element({ @@ -242,15 +242,15 @@ namespace spot virtual std::string stats() override { return - std::to_string(this->dfs_number) + " unique states visited\n" + - std::to_string(roots_.size()) + - " strongly connected components in search stack\n" + - std::to_string(this->transitions) + " transitions explored\n"; + std::to_string(this->dfs_number) + " unique states visited\n" + + std::to_string(roots_.size()) + + " strongly connected components in search stack\n" + + std::to_string(this->transitions) + " transitions explored\n"; } private: - bool found_ = false; ///< \brief A counterexample is detected? + bool found_ = false; ///< \brief A counterexample is detected? struct root_element { unsigned dfsnum; diff --git a/spot/mc/intersect.hh b/spot/mc/intersect.hh index 8605ba073..6221b5788 100644 --- a/spot/mc/intersect.hh +++ b/spot/mc/intersect.hh @@ -42,8 +42,8 @@ namespace spot /// The other template parameters allows to consider any kind /// of state (and so any kind of kripke structures). template + typename StateHash, typename StateEqual, + typename EmptinessCheck> class SPOT_API intersect { public: @@ -78,64 +78,64 @@ namespace spot self().setup(); product_state initial = {sys_.initial(), twa_->get_initial()}; if (SPOT_LIKELY(self().push_state(initial, dfs_number+1, 0U))) - { - todo.push_back({initial, sys_.succ(initial.st_kripke), - twa_->succ(initial.st_prop)}); + { + todo.push_back({initial, sys_.succ(initial.st_kripke), + twa_->succ(initial.st_prop)}); - // Not going further! It's a product with a single state. - if (todo.back().it_prop->done()) - return false; + // Not going further! It's a product with a single state. + if (todo.back().it_prop->done()) + return false; - forward_iterators(true); - map[initial] = ++dfs_number; - } + forward_iterators(true); + 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(self().pop_state(todo.back().st, - map[todo.back().st], - is_init, - newtop, - map[newtop]))) - { - sys_.recycle(todo.back().it_kripke); - // 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).dst - }; - auto acc = twa_->trans_data(todo.back().it_prop).acc_; - forward_iterators(false); - 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), - twa_->succ(dst.st_prop)}); - forward_iterators(true); - } - } - else if (SPOT_UNLIKELY(self().update(todo.back().st, - dfs_number, - dst, map[dst], acc))) - return true; - } - } + { + // 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); + // 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).dst + }; + auto acc = twa_->trans_data(todo.back().it_prop).acc_; + forward_iterators(false); + 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), + twa_->succ(dst.st_prop)}); + forward_iterators(true); + } + } + else if (SPOT_UNLIKELY(self().update(todo.back().st, + dfs_number, + dst, map[dst], acc))) + return true; + } + } return false; } @@ -158,8 +158,8 @@ namespace spot virtual std::string stats() { return - std::to_string(dfs_number) + " unique states visited\n" + - std::to_string(transitions) + " transitions explored\n"; + std::to_string(dfs_number) + " unique states visited\n" + + std::to_string(transitions) + " transitions explored\n"; } protected: @@ -175,37 +175,37 @@ namespace spot // Sometimes kripke state may have no successors. if (todo.back().it_kripke->done()) - return; + return; // The state has just been push and the 2 iterators intersect. // There is no need to move iterators forward. assert(!(todo.back().it_prop->done())); if (just_pushed && twa_->get_cubeset() - .intersect(twa_->trans_data(todo.back().it_prop).cube_, - todo.back().it_kripke->condition())) - return; + .intersect(twa_->trans_data(todo.back().it_prop).cube_, + todo.back().it_kripke->condition())) + return; // Otherwise we have to compute the next valid successor (if it exits). // This requires two loops. The most inner one is for the twacube since // its costless if (todo.back().it_prop->done()) - todo.back().it_prop->reset(); + todo.back().it_prop->reset(); else - todo.back().it_prop->next(); + todo.back().it_prop->next(); while (!todo.back().it_kripke->done()) - { - while (!todo.back().it_prop->done()) - { - if (SPOT_UNLIKELY(twa_->get_cubeset() - .intersect(twa_->trans_data(todo.back().it_prop).cube_, - todo.back().it_kripke->condition()))) - return; - todo.back().it_prop->next(); - } - todo.back().it_prop->reset(); - todo.back().it_kripke->next(); - } + { + while (!todo.back().it_prop->done()) + { + if (SPOT_UNLIKELY(twa_->get_cubeset() + .intersect(twa_->trans_data(todo.back().it_prop).cube_, + todo.back().it_kripke->condition()))) + return; + todo.back().it_prop->next(); + } + todo.back().it_prop->reset(); + todo.back().it_kripke->next(); + } } public: @@ -219,11 +219,11 @@ namespace spot { bool operator()(const product_state lhs, - const product_state rhs) const + const product_state rhs) const { - StateEqual equal; - return (lhs.st_prop == rhs.st_prop) && - equal(lhs.st_kripke, rhs.st_kripke); + StateEqual equal; + return (lhs.st_prop == rhs.st_prop) && + equal(lhs.st_kripke, rhs.st_kripke); } }; @@ -232,10 +232,10 @@ namespace spot size_t operator()(const product_state that) const { - // FIXME! wang32_hash(that.st_prop) could have - // been pre-calculated! - StateHash hasher; - return wang32_hash(that.st_prop) ^ hasher(that.st_kripke); + // FIXME! wang32_hash(that.st_prop) could have + // been pre-calculated! + StateHash hasher; + return wang32_hash(that.st_prop) ^ hasher(that.st_kripke); } }; @@ -249,8 +249,8 @@ namespace spot twacube* twa_; std::vector todo; typedef std::unordered_map visited_map; + product_state_hash, + product_state_equal> visited_map; visited_map map; unsigned int dfs_number = 0; unsigned int transitions = 0; diff --git a/spot/mc/reachability.hh b/spot/mc/reachability.hh index 97dd09fa5..77648549b 100644 --- a/spot/mc/reachability.hh +++ b/spot/mc/reachability.hh @@ -27,8 +27,8 @@ namespace spot /// of a kripkecube. The algorithm uses a single DFS since it /// is the most efficient in a sequential setting template + typename StateHash, typename StateEqual, + typename Visitor> class SPOT_API seq_reach_kripke { public: @@ -59,32 +59,32 @@ namespace spot visited[initial] = ++dfs_number; self().push(initial, dfs_number); while (!todo.empty()) - { - if (todo.back().it->done()) - { - sys_.recycle(todo.back().it); - todo.pop_back(); - } - else - { - ++transitions; - State dst = todo.back().it->state(); - auto it = visited.insert({dst, dfs_number+1}); - if (it.second) - { - ++dfs_number; - self().push(dst, dfs_number); - self().edge(visited[todo.back().s], dfs_number); - todo.back().it->next(); - todo.push_back({dst, sys_.succ(dst)}); - } - else - { - self().edge(visited[todo.back().s], visited[dst]); - todo.back().it->next(); - } - } - } + { + if (todo.back().it->done()) + { + sys_.recycle(todo.back().it); + todo.pop_back(); + } + else + { + ++transitions; + State dst = todo.back().it->state(); + auto it = visited.insert({dst, dfs_number+1}); + if (it.second) + { + ++dfs_number; + self().push(dst, dfs_number); + self().edge(visited[todo.back().s], dfs_number); + todo.back().it->next(); + todo.push_back({dst, sys_.succ(dst)}); + } + else + { + self().edge(visited[todo.back().s], visited[dst]); + todo.back().it->next(); + } + } + } self().finalize(); } @@ -109,7 +109,7 @@ namespace spot // FIXME: The system already handle a set of visited states so // this map is redundant: an we avoid this new map? typedef std::unordered_map visited_map; + StateHash, StateEqual> visited_map; visited_map visited; unsigned int dfs_number = 0; unsigned int transitions = 0; diff --git a/spot/mc/unionfind.cc b/spot/mc/unionfind.cc index e0ce9f089..27bb6ac77 100644 --- a/spot/mc/unionfind.cc +++ b/spot/mc/unionfind.cc @@ -69,7 +69,7 @@ namespace spot else { id[root2] = root1; if (rk1 == rk2) - id[root1] = -(rk1 + 1); + id[root1] = -(rk1 + 1); } return true; } diff --git a/spot/mc/utils.hh b/spot/mc/utils.hh index d3468365b..293d0276d 100644 --- a/spot/mc/utils.hh +++ b/spot/mc/utils.hh @@ -27,18 +27,18 @@ namespace spot { template + typename StateHash, typename StateEqual> class SPOT_API kripke_to_twa : public seq_reach_kripke> + StateHash, StateEqual, + kripke_to_twa> { public: kripke_to_twa(kripkecube& sys, bdd_dict_ptr dict) : seq_reach_kripke>(sys), + kripke_to_twa>(sys), dict_(dict) {} @@ -57,10 +57,10 @@ namespace spot // Compute the reverse binder. auto aps = this->sys_.get_ap(); for (unsigned i = 0; i < aps.size(); ++i) - { - auto k = res_->register_ap(aps[i]); - reverse_binder_.insert({i, k}); - } + { + auto k = res_->register_ap(aps[i]); + reverse_binder_.insert({i, k}); + } } void push(State s, unsigned i) @@ -74,7 +74,7 @@ namespace spot { cubeset cs(this->sys_.get_ap().size()); bdd cond = cube_to_bdd(this->todo.back().it->condition(), - cs, reverse_binder_); + cs, reverse_binder_); res_->new_edge(src, dst, cond); } @@ -101,25 +101,25 @@ namespace spot template + typename StateHash, typename StateEqual> class SPOT_API product_to_twa : public intersect> + StateHash, StateEqual, + product_to_twa> { // Ease the manipulation using typename intersect>::product_state; + product_to_twa>::product_state; public: product_to_twa(kripkecube& sys, twacube* twa) : intersect>(sys, twa) + product_to_twa>(sys, twa) { } @@ -141,50 +141,50 @@ namespace spot int i = 0; for (auto ap : this->twa_->get_ap()) - { - auto idx = res_->register_ap(ap); - std::cout << ap << idx << std::endl; - reverse_binder_[i++] = idx; - } + { + auto idx = res_->register_ap(ap); + std::cout << ap << idx << std::endl; + reverse_binder_[i++] = idx; + } } 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()) - { - auto c = this->twa_->get_cubeset() - .intersection(this->twa_->trans_data - (this->todo.back().it_prop).cube_, - this->todo.back().it_kripke->condition()); + { + auto c = this->twa_->get_cubeset() + .intersection(this->twa_->trans_data + (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, - this->twa_->trans_data - (this->todo.back().it_prop).acc_); - } + 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, + this->twa_->trans_data + (this->todo.back().it_prop).acc_); + } unsigned st = res_->new_state(); names_->push_back(this->sys_.to_string(s.st_kripke) + - ('*' + std::to_string(s.st_prop))); + ('*' + std::to_string(s.st_prop))); assert(st+1 == i); return true; } bool update(product_state, unsigned src, - product_state, unsigned dst, - acc_cond::mark_t cond) + 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()); + .intersection(this->twa_->trans_data + (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_); + reverse_binder_); this->twa_->get_cubeset().release(c); res_->new_edge(src-1, dst-1, x, cond); return false; diff --git a/spot/twacube/cube.cc b/spot/twacube/cube.cc index c5985c8af..25101dfb6 100644 --- a/spot/twacube/cube.cc +++ b/spot/twacube/cube.cc @@ -79,9 +79,9 @@ namespace spot bool incompatible = false; for (unsigned int i = 0; i < uint_size_ && !incompatible; ++i) { - true_elt = *(lhs+i) | *(rhs+i); - false_elt = *(lhs+i+uint_size_) | *(rhs+i+uint_size_); - incompatible |= (true_elt & false_elt); + true_elt = *(lhs+i) | *(rhs+i); + false_elt = *(lhs+i+uint_size_) | *(rhs+i+uint_size_); + incompatible |= (true_elt & false_elt); } return !incompatible; } @@ -91,8 +91,8 @@ namespace spot auto* res = new unsigned int[2*uint_size_]; for (unsigned int i = 0; i < uint_size_; ++i) { - res[i] = *(lhs+i) | *(rhs+i); - res[i+uint_size_] = *(lhs+i+uint_size_) | *(rhs+i+uint_size_); + res[i] = *(lhs+i) | *(rhs+i); + res[i+uint_size_] = *(lhs+i+uint_size_) | *(rhs+i+uint_size_); } return res; } @@ -119,11 +119,11 @@ namespace spot { for (unsigned int i = 0; i < 2*uint_size_; ++i) { - if (i == uint_size_) - std::cout << '\n'; + if (i == uint_size_) + std::cout << '\n'; - for (unsigned x = 0; x < nb_bits_; ++x) - std::cout << ((*(c+i) >> x) & 1); + for (unsigned x = 0; x < nb_bits_; ++x) + std::cout << ((*(c+i) >> x) & 1); } std::cout << '\n'; } @@ -135,24 +135,24 @@ namespace spot unsigned int cpt = 0; for (unsigned int i = 0; i < uint_size_; ++i) { - for (unsigned x = 0; x < nb_bits_ && cpt != size_; ++x) - { - bool true_var = (*(c+i) >> x) & 1; - bool false_var = (*(c+i+uint_size_) >> x) & 1; - if (true_var) - { - oss << aps[cpt] - << (cpt != (size_ - 1) ? "&": ""); - all_free = false; - } - else if (false_var) - { - oss << '!' << aps[cpt] - << (cpt != (size_ - 1) ? "&": ""); - all_free = false; - } - ++cpt; - } + for (unsigned x = 0; x < nb_bits_ && cpt != size_; ++x) + { + bool true_var = (*(c+i) >> x) & 1; + bool false_var = (*(c+i+uint_size_) >> x) & 1; + if (true_var) + { + oss << aps[cpt] + << (cpt != (size_ - 1) ? "&": ""); + all_free = false; + } + else if (false_var) + { + oss << '!' << aps[cpt] + << (cpt != (size_ - 1) ? "&": ""); + all_free = false; + } + ++cpt; + } } if (all_free) oss << '1'; diff --git a/spot/twacube/twacube.cc b/spot/twacube/twacube.cc index 63abc22e2..8a49c29ab 100644 --- a/spot/twacube/twacube.cc +++ b/spot/twacube/twacube.cc @@ -42,7 +42,7 @@ namespace spot { } transition::transition(const cube& cube, - acc_cond::mark_t acc): + acc_cond::mark_t acc): cube_(cube), acc_(acc) { } @@ -104,7 +104,7 @@ namespace spot void twacube::create_transition(unsigned int src, const cube& cube, - const acc_cond::mark_t& mark, unsigned int dst) + const acc_cond::mark_t& mark, unsigned int dst) { theg_.new_edge(src, dst, cube, mark); } @@ -121,24 +121,24 @@ namespace spot unsigned int i = 1; while (i <= theg_.num_edges()) { - unsigned int j = i; + unsigned int j = i; - // Walk first bucket of successors - while (j <= theg_.num_edges() && - theg_.edge_storage(i).src == theg_.edge_storage(j).src) - ++j; + // Walk first bucket of successors + while (j <= theg_.num_edges() && + theg_.edge_storage(i).src == theg_.edge_storage(j).src) + ++j; - // Remove the next bucket - unsigned int itmp = j; + // Remove the next bucket + unsigned int itmp = j; - // Look if there are some transitions missing in this bucket. - while (j <= theg_.num_edges()) - { - if (theg_.edge_storage(i).src == theg_.edge_storage(j).src) - return false; - ++j; - } - i = itmp; + // Look if there are some transitions missing in this bucket. + while (j <= theg_.num_edges()) + { + if (theg_.edge_storage(i).src == theg_.edge_storage(j).src) + return false; + ++j; + } + i = itmp; } return true; } @@ -150,10 +150,10 @@ namespace spot os << "init : " << twa.init_ << '\n'; for (unsigned int i = 1; i <= twa.theg_.num_edges(); ++i) os << twa.theg_.edge_storage(i).src << "->" - << twa.theg_.edge_storage(i).dst << " : " - << cs.dump(twa.theg_.edge_data(i).cube_, twa.aps_) - << ' ' << twa.theg_.edge_data(i).acc_ - << '\n'; + << twa.theg_.edge_storage(i).dst << " : " + << cs.dump(twa.theg_.edge_data(i).cube_, twa.aps_) + << ' ' << twa.theg_.edge_data(i).acc_ + << '\n'; return os; } } diff --git a/spot/twacube/twacube.hh b/spot/twacube/twacube.hh index 21513ca9c..865594387 100644 --- a/spot/twacube/twacube.hh +++ b/spot/twacube/twacube.hh @@ -91,7 +91,7 @@ namespace spot // no-swarming : since twacube are dedicated for parallelism, i.e. // swarming, we expect swarming is activated. if (SPOT_UNLIKELY(!seed)) - return idx_; + return idx_; // swarming. return (((idx_-st_.succ+1)*seed) % (st_.succ_tail-st_.succ+1)) + st_.succ; } @@ -115,7 +115,7 @@ namespace spot unsigned int get_initial(); cstate* state_from_int(unsigned int i); void create_transition(unsigned int src, const cube& cube, - const acc_cond::mark_t& mark, unsigned int dst); + const acc_cond::mark_t& mark, unsigned int dst); const cubeset& get_cubeset() const; bool succ_contiguous() const; typedef digraph graph_t; @@ -126,12 +126,12 @@ namespace spot typedef graph_t::edge_storage_t edge_storage_t; const graph_t::edge_storage_t& trans_storage(std::shared_ptr ci, - unsigned int seed = 0) const + unsigned int seed = 0) const { return theg_.edge_storage(ci->current(seed)); } const transition& trans_data(std::shared_ptr ci, - unsigned int seed = 0) const + unsigned int seed = 0) const { return theg_.edge_data(ci->current(seed)); } @@ -142,7 +142,7 @@ namespace spot } friend SPOT_API std::ostream& operator<<(std::ostream& os, - const twacube& twa); + const twacube& twa); private: unsigned int init_; acc_cond acc_; diff --git a/spot/twacube_algos/convert.cc b/spot/twacube_algos/convert.cc index b8bf42266..44aeb9e49 100644 --- a/spot/twacube_algos/convert.cc +++ b/spot/twacube_algos/convert.cc @@ -23,45 +23,45 @@ namespace spot { spot::cube satone_to_cube(bdd one, cubeset& cubeset, - std::unordered_map& binder) + std::unordered_map& binder) { auto cube = cubeset.alloc(); while (one != bddtrue) { - if (bdd_high(one) == bddfalse) - { - assert(binder.find(bdd_var(one)) != binder.end()); - cubeset.set_false_var(cube, binder[bdd_var(one)]); - one = bdd_low(one); - } - else - { - assert(binder.find(bdd_var(one)) != binder.end()); - cubeset.set_true_var(cube, binder[bdd_var(one)]); - one = bdd_high(one); - } + if (bdd_high(one) == bddfalse) + { + assert(binder.find(bdd_var(one)) != binder.end()); + cubeset.set_false_var(cube, binder[bdd_var(one)]); + one = bdd_low(one); + } + else + { + assert(binder.find(bdd_var(one)) != binder.end()); + cubeset.set_true_var(cube, binder[bdd_var(one)]); + one = bdd_high(one); + } } return cube; } bdd cube_to_bdd(spot::cube cube, const cubeset& cubeset, - std::unordered_map& reverse_binder) + std::unordered_map& reverse_binder) { bdd result = bddtrue; for (unsigned int i = 0; i < cubeset.size(); ++i) { - assert(reverse_binder.find(i) != reverse_binder.end()); - if (cubeset.is_false_var(cube, i)) - result &= bdd_nithvar(reverse_binder[i]); - if (cubeset.is_true_var(cube, i)) - result &= bdd_ithvar(reverse_binder[i]); + assert(reverse_binder.find(i) != reverse_binder.end()); + if (cubeset.is_false_var(cube, i)) + result &= bdd_nithvar(reverse_binder[i]); + if (cubeset.is_true_var(cube, i)) + result &= bdd_ithvar(reverse_binder[i]); } return result; } spot::twacube* twa_to_twacube(spot::twa_graph_ptr& aut, - std::unordered_map& ap_binder, - std::vector& aps) + std::unordered_map& ap_binder, + std::vector& aps) { // Declare the twa cube spot::twacube* tg = new spot::twacube(aps); @@ -86,29 +86,29 @@ namespace spot // spot::cube cube(aps); for (unsigned n = 0; n < aut->num_states(); ++n) for (auto& t: aut->out(n)) - { - bdd cond = t.cond; + { + bdd cond = t.cond; - // Special case for bddfalse - if (cond == bddfalse) - { - spot::cube cube = tg->get_cubeset().alloc(); - for (unsigned int i = 0; i < cs.size(); ++i) - cs.set_false_var(cube, i); // FIXME ! use fill! - tg->create_transition(st_binder[n], cube, - t.acc, st_binder[t.dst]); - } - else - // Split the bdd into multiple transitions - while (cond != bddfalse) - { - bdd one = bdd_satone(cond); - cond -= one; - spot::cube cube =spot::satone_to_cube(one, cs, ap_binder); - tg->create_transition(st_binder[n], cube, t.acc, - st_binder[t.dst]); - } - } + // Special case for bddfalse + if (cond == bddfalse) + { + spot::cube cube = tg->get_cubeset().alloc(); + for (unsigned int i = 0; i < cs.size(); ++i) + cs.set_false_var(cube, i); // FIXME ! use fill! + tg->create_transition(st_binder[n], cube, + t.acc, st_binder[t.dst]); + } + else + // Split the bdd into multiple transitions + while (cond != bddfalse) + { + bdd one = bdd_satone(cond); + cond -= one; + spot::cube cube =spot::satone_to_cube(one, cs, ap_binder); + tg->create_transition(st_binder[n], cube, t.acc, + st_binder[t.dst]); + } + } // Must be contiguous to support swarming. assert(tg->succ_contiguous()); return tg; @@ -116,17 +116,17 @@ namespace spot std::vector* extract_aps(spot::twa_graph_ptr& aut, - std::unordered_map& ap_binder) + std::unordered_map& ap_binder) { std::vector* aps = new std::vector(); for (auto f: aut->ap()) { - int size = aps->size(); - if (std::find(aps->begin(), aps->end(), f.ap_name()) == aps->end()) - { - aps->push_back(f.ap_name()); - ap_binder.insert({aut->get_dict()->var_map[f], size}); - } + int size = aps->size(); + if (std::find(aps->begin(), aps->end(), f.ap_name()) == aps->end()) + { + aps->push_back(f.ap_name()); + ap_binder.insert({aut->get_dict()->var_map[f], size}); + } } return aps; } @@ -153,26 +153,26 @@ namespace spot // Build all resulting states for (unsigned int i = 0; i < theg.num_states(); ++i) { - unsigned st = res->new_state(); - (void) st; - assert(st == i); + unsigned st = res->new_state(); + (void) st; + assert(st == i); } // Build all resulting conditions. for (unsigned int i = 1; i <= theg.num_edges(); ++i) { - bdd cond = bddtrue; - for (unsigned j = 0; j < cs.size(); ++j) - { - if (cs.is_true_var(theg.edge_data(i).cube_, j)) - cond &= bdd_ithvar(bdds_ref[j]); - else if (cs.is_false_var(theg.edge_data(i).cube_, j)) - cond &= bdd_nithvar(bdds_ref[j]); - // otherwise it 's a free variable do nothing - } + bdd cond = bddtrue; + for (unsigned j = 0; j < cs.size(); ++j) + { + if (cs.is_true_var(theg.edge_data(i).cube_, j)) + cond &= bdd_ithvar(bdds_ref[j]); + else if (cs.is_false_var(theg.edge_data(i).cube_, j)) + cond &= bdd_nithvar(bdds_ref[j]); + // otherwise it 's a free variable do nothing + } - res->new_edge(theg.edge_storage(i).src, theg.edge_storage(i).dst, - cond, theg.edge_data(i).acc_); + res->new_edge(theg.edge_storage(i).src, theg.edge_storage(i).dst, + cond, theg.edge_data(i).acc_); } // Fix the initial state diff --git a/spot/twacube_algos/convert.hh b/spot/twacube_algos/convert.hh index 5c6f2569d..bcba3a671 100644 --- a/spot/twacube_algos/convert.hh +++ b/spot/twacube_algos/convert.hh @@ -33,23 +33,23 @@ namespace spot /// into a \a cube cube passed in parameter. The parameter /// \a binder map bdd indexes to cube indexes. SPOT_API spot::cube satone_to_cube(bdd one, cubeset& cubeset, - std::unordered_map& binder); + std::unordered_map& binder); /// \brief Transform a \a cube cube into bdd using the map /// that bind cube indexes to bdd indexes. SPOT_API bdd cube_to_bdd(spot::cube cube, const cubeset& cubeset, - std::unordered_map& reverse_binder); + std::unordered_map& reverse_binder); /// \brief Extract the atomic propositions from the automaton SPOT_API std::vector* extract_aps(spot::twa_graph_ptr& aut, - std::unordered_map& ap_binder); + std::unordered_map& ap_binder); /// \brief Convert a twa into a twacube SPOT_API spot::twacube* twa_to_twacube(spot::twa_graph_ptr& aut, - std::unordered_map& ap_binder, - std::vector& aps); + std::unordered_map& ap_binder, + std::vector& aps); /// \brief Convert a twacube into a twa SPOT_API spot::twa_graph_ptr diff --git a/tests/core/bricks.cc b/tests/core/bricks.cc index 089015ac1..f698fdd0b 100644 --- a/tests/core/bricks.cc +++ b/tests/core/bricks.cc @@ -62,10 +62,10 @@ int main() for (int i = 0; i < 6; i++) workers. push_back(std::thread([&ht2](int tid) - { - for (int i = 0; i< 2000; ++i) - ht2.insert({i, tid}); - }, i)); + { + for (int i = 0; i< 2000; ++i) + ht2.insert({i, tid}); + }, i)); // Wait the end of all threads. for (auto& t: workers) @@ -75,6 +75,6 @@ int main() for (unsigned i = 0; i < ht2.size(); ++ i) if (ht2.valid(i)) std::cout << i << ": {" - << ht2[i].x << ',' << ht2[i].y << "}\n"; + << ht2[i].x << ',' << ht2[i].y << "}\n"; return 0; } diff --git a/tests/core/cube.cc b/tests/core/cube.cc index cfcf77f99..03bf53f81 100644 --- a/tests/core/cube.cc +++ b/tests/core/cube.cc @@ -31,9 +31,9 @@ static bool test_translation(bdd& input, spot::cubeset& cubeset, - std::unordered_map& binder, - std::unordered_map& reverse_binder, - std::vector& aps) + std::unordered_map& binder, + std::unordered_map& reverse_binder, + std::vector& aps) { // The BDD used to detect if the convertion works bdd res = bddfalse; diff --git a/tests/core/twacube.cc b/tests/core/twacube.cc index c67ffbbab..28d8cacfc 100644 --- a/tests/core/twacube.cc +++ b/tests/core/twacube.cc @@ -63,9 +63,9 @@ int main() auto& t = aut->trans_storage(it, seed); auto& d = aut->trans_data(it, seed); std::cout << t.src << ' ' << t.dst << ' ' - << ' ' << aut->get_cubeset().dump(d.cube_, *aps) - << ' ' << d.acc_ - << std::endl; + << ' ' << aut->get_cubeset().dump(d.cube_, *aps) + << ' ' << d.acc_ + << std::endl; } spot::print_dot(std::cout, spot::twacube_to_twa(aut)); diff --git a/tests/ltsmin/modelcheck.cc b/tests/ltsmin/modelcheck.cc index 63ca36cea..34525a9d3 100644 --- a/tests/ltsmin/modelcheck.cc +++ b/tests/ltsmin/modelcheck.cc @@ -75,17 +75,17 @@ parse_opt_finput(int key, char* arg, struct argp_state*) break; case 'd': if (strcmp(arg, "model") == 0) - mc_options.dot_output |= DOT_MODEL; + mc_options.dot_output |= DOT_MODEL; else if (strcmp(arg, "product") == 0) - mc_options.dot_output |= DOT_PRODUCT; + mc_options.dot_output |= DOT_PRODUCT; else if (strcmp(arg, "formula") == 0) - mc_options.dot_output |= DOT_FORMULA; + mc_options.dot_output |= DOT_FORMULA; else - { - std::cerr << "Unknown argument: '" << arg - << "' for option --dot\n"; - return ARGP_ERR_UNKNOWN; - } + { + std::cerr << "Unknown argument: '" << arg + << "' for option --dot\n"; + return ARGP_ERR_UNKNOWN; + } break; case 'e': mc_options.is_empty = true; @@ -154,8 +154,8 @@ static const argp_option options[] = }; const struct argp finput_argp = { options, parse_opt_finput, - nullptr, nullptr, nullptr, - nullptr, nullptr }; + nullptr, nullptr, nullptr, + nullptr, nullptr }; const struct argp_child children[] = { @@ -184,12 +184,12 @@ static int checked_main() if (mc_options.selfloopize) { if (mc_options.dead_ap == nullptr || - !strcasecmp(mc_options.dead_ap, "true")) - deadf = spot::formula::tt(); + !strcasecmp(mc_options.dead_ap, "true")) + deadf = spot::formula::tt(); else if (!strcasecmp(mc_options.dead_ap, "false")) - deadf = spot::formula::ff(); + deadf = spot::formula::ff(); else - deadf = env.require(mc_options.dead_ap); + deadf = env.require(mc_options.dead_ap); } @@ -197,39 +197,39 @@ static int checked_main() { tm.start("parsing formula"); { - auto pf = spot::parse_infix_psl(mc_options.formula, env, false); - exit_code = pf.format_errors(std::cerr); - f = pf.f; + auto pf = spot::parse_infix_psl(mc_options.formula, env, false); + exit_code = pf.format_errors(std::cerr); + f = pf.f; } tm.stop("parsing formula"); tm.start("translating formula"); { - spot::translator trans(dict); - // if (deterministic) FIXME - // trans.set_pref(spot::postprocessor::Deterministic); - prop = trans.run(&f); + spot::translator trans(dict); + // if (deterministic) FIXME + // trans.set_pref(spot::postprocessor::Deterministic); + prop = trans.run(&f); } tm.stop("translating formula"); atomic_prop_collect(f, &ap); if (mc_options.dot_output & DOT_FORMULA) - { - tm.start("dot output"); - spot::print_dot(std::cout, prop); - tm.stop("dot output"); - } + { + tm.start("dot output"); + spot::print_dot(std::cout, prop); + tm.stop("dot output"); + } } if (mc_options.model != nullptr) { tm.start("loading ltsmin model"); try - { - model = spot::ltsmin_model::load(mc_options.model) - .kripke(&ap, dict, deadf, mc_options.compress); - } + { + model = spot::ltsmin_model::load(mc_options.model) + .kripke(&ap, dict, deadf, mc_options.compress); + } catch (std::runtime_error& e) { std::cerr << e.what() << '\n'; @@ -237,23 +237,23 @@ static int checked_main() tm.stop("loading ltsmin model"); if (!model) - { - exit_code = 2; - goto safe_exit; - } + { + exit_code = 2; + goto safe_exit; + } if (mc_options.dot_output & DOT_MODEL) - { - tm.start("dot output"); - spot::print_dot(std::cout, model); - tm.stop("dot output"); - } + { + tm.start("dot output"); + spot::print_dot(std::cout, model); + tm.stop("dot output"); + } if (mc_options.kripke_output) - { - tm.start("kripke output"); - spot::print_hoa(std::cout, model); - tm.stop("kripke output"); - } + { + tm.start("kripke output"); + spot::print_hoa(std::cout, model); + tm.stop("kripke output"); + } } if (mc_options.formula != nullptr && @@ -262,92 +262,92 @@ static int checked_main() product = spot::otf_product(model, prop); if (mc_options.is_empty) - { - const char* err; - echeck_inst = spot::make_emptiness_check_instantiator("Cou99", &err); - if (!echeck_inst) - { - std::cerr << "Unknown emptiness check algorihm `" - << err << "'\n"; - exit_code = 1; - goto safe_exit; - } + { + const char* err; + echeck_inst = spot::make_emptiness_check_instantiator("Cou99", &err); + if (!echeck_inst) + { + std::cerr << "Unknown emptiness check algorihm `" + << err << "'\n"; + exit_code = 1; + goto safe_exit; + } - auto ec = echeck_inst->instantiate(product); - assert(ec); - int memused = spot::memusage(); - tm.start("running emptiness check"); - spot::emptiness_check_result_ptr res; - try - { - res = ec->check(); - } - catch (std::bad_alloc) - { - std::cerr << "Out of memory during emptiness check." - << std::endl; - if (!mc_options.compress) - std::cerr << "Try option -z for state compression." << std::endl; - exit_code = 2; - exit(exit_code); - } - tm.stop("running emptiness check"); - memused = spot::memusage() - memused; + auto ec = echeck_inst->instantiate(product); + assert(ec); + int memused = spot::memusage(); + tm.start("running emptiness check"); + spot::emptiness_check_result_ptr res; + try + { + res = ec->check(); + } + catch (std::bad_alloc) + { + std::cerr << "Out of memory during emptiness check." + << std::endl; + if (!mc_options.compress) + std::cerr << "Try option -z for state compression." << std::endl; + exit_code = 2; + exit(exit_code); + } + tm.stop("running emptiness check"); + memused = spot::memusage() - memused; - ec->print_stats(std::cout); - std::cout << memused << " pages allocated for emptiness check" - << std::endl; + ec->print_stats(std::cout); + std::cout << memused << " pages allocated for emptiness check" + << std::endl; - if (!res) - { - std::cout << "no accepting run found"; - } - else if (!mc_options.compute_counterexample) - { - std::cout << "an accepting run exists " - << "(use -c to print it)" << std::endl; - exit_code = 1; - } - else - { - exit_code = 1; - spot::twa_run_ptr run; - tm.start("computing accepting run"); - try - { - run = res->accepting_run(); - } - catch (std::bad_alloc) - { - std::cerr << "Out of memory while looking for counterexample." - << std::endl; - exit_code = 2; - exit(exit_code); - } - tm.stop("computing accepting run"); + if (!res) + { + std::cout << "no accepting run found"; + } + else if (!mc_options.compute_counterexample) + { + std::cout << "an accepting run exists " + << "(use -c to print it)" << std::endl; + exit_code = 1; + } + else + { + exit_code = 1; + spot::twa_run_ptr run; + tm.start("computing accepting run"); + try + { + run = res->accepting_run(); + } + catch (std::bad_alloc) + { + std::cerr << "Out of memory while looking for counterexample." + << std::endl; + exit_code = 2; + exit(exit_code); + } + tm.stop("computing accepting run"); - if (!run) - { - std::cout << "an accepting run exists" << std::endl; - } - else - { - tm.start("reducing accepting run"); - run = run->reduce(); - tm.stop("reducing accepting run"); - tm.start("printing accepting run"); - std::cout << *run; - tm.stop("printing accepting run"); - } - } - } + if (!run) + { + std::cout << "an accepting run exists" << std::endl; + } + else + { + tm.start("reducing accepting run"); + run = run->reduce(); + tm.stop("reducing accepting run"); + tm.start("printing accepting run"); + std::cout << *run; + tm.stop("printing accepting run"); + } + } + } if (mc_options.dot_output & DOT_PRODUCT) - { - tm.start("dot output"); - spot::print_dot(std::cout, product); - tm.stop("dot output"); - } + { + tm.start("dot output"); + spot::print_dot(std::cout, product); + tm.stop("dot output"); + } } safe_exit: @@ -363,7 +363,7 @@ main(int argc, char** argv) { setup(argv); const argp ap = { nullptr, nullptr, nullptr, - argp_program_doc, children, nullptr, nullptr }; + argp_program_doc, children, nullptr, nullptr }; if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) exit(err);