diff --git a/NEWS b/NEWS index dea361bc0..cd454c433 100644 --- a/NEWS +++ b/NEWS @@ -84,6 +84,10 @@ New in spot 2.5.3.dev (not yet released) They are most welcome in Python, since we used to redefine them every now and them. + - spot::parity_product() and spot::parity_product_or() were dropped. + The code was buggy, hard to maintain, and these functions do not + seem to be used. + Python: - New spot.jupyter package. This currently contains a function for diff --git a/spot/twaalgos/parity.cc b/spot/twaalgos/parity.cc index d30e30940..497b2fc9a 100644 --- a/spot/twaalgos/parity.cc +++ b/spot/twaalgos/parity.cc @@ -338,350 +338,4 @@ namespace spot return aut; } - namespace - { - using state_history_value_t = unsigned; - - class state_history : public std::vector - { - public: - - using value_t = state_history_value_t; - - state_history(unsigned left_num_sets, unsigned right_num_sets) : - left_num_sets_(left_num_sets), - right_num_sets_(right_num_sets) - { - resize(left_num_sets + right_num_sets, 0); - } - - value_t get_left(value_t right) const - { - return get(right, true); - } - - value_t get_right(value_t left) const - { - return get(left, false); - } - - void set_left(value_t right, value_t val) - { - set(right, true, val); - } - - void set_right(value_t left, value_t val) - { - set(left, false, val); - } - - unsigned get_left_num_sets() const - { - return left_num_sets_; - } - - unsigned get_right_num_sets() const - { - return right_num_sets_; - } - - value_t get_max_acc_set(bool and_cond) const - { - // i is the index of the resulting automaton acceptance set - // If i is even, it means that the according set is a set with - // transitions that need to be infinitly often as the - // acceptance is a parity even. Then k, the index of the - // first automaton must be even too. - unsigned l = right_num_sets_; - while (l-- > 0) - { - auto k = get_left(l); - bool can_jump = and_cond ? (k & l & 1) != 1 : ((k | l) & 1) != 0; - if (!can_jump) - --k; - auto new_l = get_right(k); - if (new_l >= l) - return k + l; - else if (can_jump) - l = new_l + 1; - } - return 0; - } - - state_history make_succ(value_t left_acc_set, - value_t right_acc_set) const - { - auto mat = state_history(left_num_sets_, right_num_sets_); - for (unsigned i = 0; i < right_num_sets_; ++i) - { - auto old = get_left(i); - mat.set_left(i, std::max(left_acc_set, old)); - } - for (unsigned i = 0; i < left_num_sets_; ++i) - { - auto old = get_right(i); - mat.set_right(i, std::max(right_acc_set, old)); - } - return mat; - } - - void clean_here() - { - auto mat = state_history(*this); - for (unsigned l = 0; l < right_num_sets_; ++l) - { - set_left(l, 0); - for (unsigned k = 0; k < left_num_sets_; ++k) - { - if (mat.get_right(k) < l) - set_left(l, std::min(mat.get_left(l), k)); - else - break; - } - } - for (unsigned k = 0; k < left_num_sets_; ++k) - { - set_right(k, 0); - for (unsigned l = 0; l < right_num_sets_; ++l) - { - if (mat.get_left(l) < k) - set_right(k, std::min(mat.get_right(k), l)); - else - break; - } - } - } - - private: - const unsigned left_num_sets_; - const unsigned right_num_sets_; - - value_t get(value_t index, bool first) const - { - return at(index + (first ? 0 : right_num_sets_)); - } - - void set(value_t index, bool first, value_t val) - { - at(index + (first ? 0 : right_num_sets_)) = val; - } - }; - - struct state_history_hash - { - size_t - operator()(const state_history& mat) const noexcept - { - unsigned result = 0; - for (unsigned i = 0; i < mat.get_left_num_sets(); ++i) - result = wang32_hash(result ^ wang32_hash(mat.get_right(i))); - for (unsigned i = 0; i < mat.get_right_num_sets(); ++i) - result = wang32_hash(result ^ wang32_hash(mat.get_left(i))); - return result; - } - }; - - using sh_label_t = unsigned; - - class state_history_set - { - private: - using value_t = state_history::value_t; - - public: - sh_label_t - push_state_history(state_history sh) - { - auto p = sh2l_.emplace(sh, 0); - if (p.second) - { - l2sh_.push_back(p.first); - p.first->second = l2sh_.size() - 1; - } - return p.first->second; - } - - std::pair - push_state_history(sh_label_t label, value_t left_acc_set, - value_t right_acc_set, bool and_cond) - { - state_history new_sh = l2sh_[label]->first; - auto succ = new_sh.make_succ(left_acc_set, right_acc_set); - auto max_acc_set = succ.get_max_acc_set(and_cond); - succ.clean_here(); - return std::make_pair(push_state_history(succ), max_acc_set); - } - - std::pair - get_succ(sh_label_t current_sh, value_t left_acc_set, - value_t right_acc_set, bool and_cond) - { - auto f_args = std::make_tuple(current_sh, left_acc_set, right_acc_set); - auto p = succ_.emplace(f_args, std::make_pair(0, 0)); - if (p.second) - { - p.first->second = - push_state_history(current_sh, left_acc_set, - right_acc_set, and_cond); - } - return p.first->second; - } - - private: - using sh_dict_t = std::unordered_map; - sh_dict_t sh2l_; - - struct sh_succ_hash - { - size_t - operator()(std::tuple x) const noexcept - { - return wang32_hash(std::get<0>(x) ^ wang32_hash(std::get<1>(x) - ^ wang32_hash(std::get<2>(x)))); - } - }; - std::unordered_map, - std::pair, - sh_succ_hash> succ_; - std::vector l2sh_; - }; - - using product_state_t = std::tuple; - - struct product_state_hash - { - size_t - operator()(product_state_t s) const noexcept - { - return wang32_hash(std::get<0>(s) ^ wang32_hash(std::get<1>(s) - ^ wang32_hash(std::get<2>(s)))); - } - }; - - - twa_graph_ptr - parity_product_aux(const const_twa_graph_ptr& first, - const const_twa_graph_ptr& second, - bool and_cond) - { - auto left = change_parity(first, parity_kind_max, parity_style_even); - auto right = change_parity(second, parity_kind_max, parity_style_even); - if (!and_cond) - { - complete_here(left); - complete_here(right); - } - cleanup_parity_here(left, true); - cleanup_parity_here(right, true); - colorize_parity_here(left, true); - colorize_parity_here(right, true); - std::unordered_map s2n; - state_history_set sh_set; - std::queue> todo; - auto res = make_twa_graph(left->get_dict()); - res->copy_ap_of(left); - res->copy_ap_of(right); - unsigned left_num_sets = left->num_sets(); - unsigned right_num_sets = right->num_sets(); - unsigned z_size = left_num_sets + right_num_sets - 1; - auto z = acc_cond::acc_code::parity(true, !and_cond, z_size); - res->set_acceptance(z_size, z); - - auto v = new product_states; - res->set_named_prop("product-states", v); - - auto new_state = - [&](const sh_label_t sh_label, - unsigned left_state, unsigned right_state, - unsigned left_acc_set, unsigned right_acc_set) - -> std::pair - { - auto succ = sh_set.get_succ(sh_label, left_acc_set, right_acc_set, - and_cond); - product_state_t x(left_state, right_state, succ.first); - auto p = s2n.emplace(x, 0); - if (p.second) // This is a new state - { - auto new_state = res->new_state(); - p.first->second = new_state; - v->push_back(std::make_pair(left_state, right_state)); - todo.emplace(x, new_state); - } - return std::make_pair(p.first->second, succ.second); - }; - - state_history init_state_history(left_num_sets, right_num_sets); - auto init_sh_label = sh_set.push_state_history(init_state_history); - product_state_t init_state(left->get_init_state_number(), - right->get_init_state_number(), init_sh_label); - auto init_state_index = res->new_state(); - s2n.emplace(init_state, init_state_index); - todo.emplace(init_state, init_state_index); - res->set_init_state(init_state_index); - - while (!todo.empty()) - { - auto& top = todo.front(); - for (auto& l: left->out(std::get<0>(top.first))) - for (auto& r: right->out(std::get<1>(top.first))) - { - auto cond = l.cond & r.cond; - if (cond == bddfalse) - continue; - auto left_acc = l.acc.max_set() - 1; - auto right_acc = r.acc.max_set() - 1; - auto dst = new_state(std::get<2>(top.first), l.dst, r.dst, - left_acc, right_acc); - auto acc = acc_cond::mark_t{dst.second}; - res->new_edge(top.second, dst.first, cond, acc); - } - todo.pop(); - } - - // The product of two non-deterministic automata could be - // deterministic. likewise for non-complete automata. - if (left->prop_universal() && right->prop_universal()) - res->prop_universal(true); - if (left->prop_complete() && right->prop_complete()) - res->prop_complete(true); - if (left->prop_stutter_invariant() && right->prop_stutter_invariant()) - res->prop_stutter_invariant(true); - if (left->prop_inherently_weak() && right->prop_inherently_weak()) - res->prop_inherently_weak(true); - if (left->prop_weak() && right->prop_weak()) - res->prop_weak(true); - if (left->prop_terminal() && right->prop_terminal()) - res->prop_terminal(true); - res->prop_state_acc(left->prop_state_acc() && right->prop_state_acc()); - return res; - } - } - - twa_graph_ptr - parity_product(const const_twa_graph_ptr& left, - const const_twa_graph_ptr& right) - { - if (left->get_dict() != right->get_dict()) - throw std::runtime_error("parity_product: left and right automata " - "should share their bdd_dict"); - if (!(left->is_existential() && right->is_existential())) - throw std::runtime_error("parity_product() does not support alternating " - "automata"); - return parity_product_aux(left, right, true); - } - - twa_graph_ptr - parity_product_or(const const_twa_graph_ptr& left, - const const_twa_graph_ptr& right) - { - if (left->get_dict() != right->get_dict()) - throw std::runtime_error("parity_product_or: left and right automata " - "should share their bdd_dict"); - if (!(left->is_existential() && right->is_existential())) - throw std::runtime_error("parity_product_or() does not support " - "alternating automata"); - return parity_product_aux(left, right, false); - } } diff --git a/spot/twaalgos/parity.hh b/spot/twaalgos/parity.hh index 672bb5754..cf0f6c4f9 100644 --- a/spot/twaalgos/parity.hh +++ b/spot/twaalgos/parity.hh @@ -133,39 +133,4 @@ namespace spot SPOT_API twa_graph_ptr colorize_parity_here(twa_graph_ptr aut, bool keep_style = false); /// @} - - /// \brief Construct a product performing the intersection of two automata - /// with parity acceptance and keeping their parity acceptance - /// - /// This is based on an algorithm introduced by Olivier Carton (Theoretical - /// Computer Science 161, 1-2 (1996)). The output is a parity max even - /// automaton. The inputs must be automata with a parity acceptance, otherwise - /// an invalid_argument exception is thrown. - /// - /// \param left the first automaton - /// - /// \param right the second automaton - /// - /// \result the product, which is a parity automaton - SPOT_API twa_graph_ptr - parity_product(const const_twa_graph_ptr& left, - const const_twa_graph_ptr& right); - - /// \brief Construct a product performing the union of two automata - /// with parity acceptance and keeping their parity acceptance - /// - /// This is based on an algorithm introduced by Olivier Carton (Theoretical - /// Computer Science 161, 1-2 (1996)). The output is a parity max even - /// automaton. The inputs must be automata with a parity acceptance, otherwise - /// an invalid_argument exception is thrown. - /// - /// \param left the first automaton - /// - /// \param right the second automaton - /// - /// \result the sum which is a parity automaton - SPOT_API twa_graph_ptr - parity_product_or(const const_twa_graph_ptr& left, - const const_twa_graph_ptr& right); - /// @} } diff --git a/tests/core/parity.cc b/tests/core/parity.cc index 64b5f18a2..d9a453ba2 100644 --- a/tests/core/parity.cc +++ b/tests/core/parity.cc @@ -385,75 +385,5 @@ int main() } } - std::random_shuffle(automata_tuples.begin(), automata_tuples.end()); - unsigned num_left = 15; - unsigned num_right = 15; - unsigned acc_index = 0; - - unsigned nb = 0; - // Parity product and sum - for (unsigned left_index = 0; left_index < num_left; ++left_index) - { - auto& aut_tuple_first = automata_tuples[left_index % num_automata]; - auto& left = aut_tuple_first.first; - auto aut_num_sets_first = aut_tuple_first.second; - while (std::get<3>(acceptance_sets[acc_index]) < aut_num_sets_first) - acc_index = (acc_index + 1) % num_acceptance; - auto acc_tuple_first = acceptance_sets[acc_index]; - acc_index = (acc_index + 1) % num_acceptance; - auto acc_first = std::get<0>(acc_tuple_first); - auto acc_num_sets_first = std::get<3>(acc_tuple_first); - left->set_acceptance(acc_num_sets_first, acc_first); - for (unsigned right_index = 0; right_index < num_right; ++right_index) - { - auto& aut_tuple_second = - automata_tuples[(num_left + right_index) % num_automata]; - auto& right = aut_tuple_second.first; - auto aut_num_sets_second = aut_tuple_second.second; - while (std::get<3>(acceptance_sets[acc_index]) < aut_num_sets_second) - acc_index = (acc_index + 1) % num_acceptance; - auto acc_tuple_second = acceptance_sets[acc_index]; - acc_index = (acc_index + 1) % num_acceptance; - auto acc_second = std::get<0>(acc_tuple_second); - auto acc_num_sets_second = std::get<3>(acc_tuple_second); - right->set_acceptance(acc_num_sets_second, acc_second); - auto result_prod = spot::parity_product(left, right); - auto ref_prod = spot::product(left, right); - if (!are_equiv(result_prod, ref_prod)) - { - std::cerr << nb << ": parity_product: Not equivalent.\n" - << "=====First Automaton=====\n"; - spot::print_hoa(std::cerr, left); - std::cerr << "=====Second Automaton=====\n"; - spot::print_hoa(std::cerr, right); - assert(false && "parity_product: Not equivalent.\n"); - } - assert(is_colored_printerr(result_prod) - && "parity_product: not colored."); - assert(is_right_parity(result_prod, spot::parity_kind_any, - spot::parity_style_any, - true, true, 2) - && "parity_product: not a parity acceptance condition"); - - auto result_sum = spot::parity_product_or(left, right); - auto ref_sum = spot::product_or(left, right); - if (!are_equiv(result_sum, ref_sum)) - { - std::cerr << nb << ": parity_product_or: Not equivalent.\n" - << "=====First Automaton=====\n"; - spot::print_hoa(std::cerr, left); - std::cerr << "=====Second Automaton=====\n"; - spot::print_hoa(std::cerr, right); - assert(false && "parity_product_or: Not equivalent.\n"); - } - assert(is_colored_printerr(result_sum) - && "parity_product_or: not colored."); - assert(is_right_parity(result_sum, spot::parity_kind_any, - spot::parity_style_any, - true, true, 2) - && "parity_product_or: not a parity acceptance condition"); - ++nb; - } - } return 0; }