From 7a118426135dd20ff27d25a231ef870d4fbf05a0 Mon Sep 17 00:00:00 2001 From: Laurent XU Date: Mon, 4 Jul 2016 19:22:47 +0200 Subject: [PATCH] parity: add spot::parity_product_or() parity_product_or constructs the sum of two parity automata and it keeps the parity. * spot/twaalgos/parity.cc, spot/twaalgos/parity.hh: Here. * tests/core/parity.cc: Add tests here. --- spot/twaalgos/parity.cc | 55 +++++++++++++++++++++++++++++------------ spot/twaalgos/parity.hh | 17 +++++++++++++ tests/core/parity.cc | 31 ++++++++++++++++++----- 3 files changed, 81 insertions(+), 22 deletions(-) diff --git a/spot/twaalgos/parity.cc b/spot/twaalgos/parity.cc index f9bc1d298..3c83e9725 100644 --- a/spot/twaalgos/parity.cc +++ b/spot/twaalgos/parity.cc @@ -20,6 +20,7 @@ #include #include #include +#include #include #include #include @@ -336,7 +337,7 @@ namespace spot return right_num_sets_; } - value_t get_max_acc_set() const + 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 @@ -347,7 +348,7 @@ namespace spot while (l-- > 0) { auto k = get_left(l); - bool can_jump = (k & l & 1) != 1; + bool can_jump = and_cond ? (k & l & 1) != 1 : ((k | l) & 1) != 0; if (!can_jump) --k; auto new_l = get_right(k); @@ -454,25 +455,26 @@ namespace spot std::pair push_state_history(sh_label_t label, value_t left_acc_set, - value_t right_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(); + 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) + 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); + push_state_history(current_sh, left_acc_set, + right_acc_set, and_cond); } return p.first->second; } @@ -512,8 +514,21 @@ namespace spot twa_graph_ptr - parity_product_aux(twa_graph_ptr& left, twa_graph_ptr& right) + 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; @@ -523,7 +538,7 @@ namespace spot 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, false, z_size); + auto z = acc_cond::acc_code::parity(true, !and_cond, z_size); res->set_acceptance(z_size, z); auto v = new product_states; @@ -535,7 +550,8 @@ namespace spot unsigned left_acc_set, unsigned right_acc_set) -> std::pair { - auto succ = sh_set.get_succ(sh_label, left_acc_set, right_acc_set); + 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 @@ -605,12 +621,19 @@ namespace spot if (!(left->is_existential() && right->is_existential())) throw std::runtime_error("parity_product() does not support alternating " "automata"); - auto first = change_parity(left, parity_kind_max, parity_style_even); - auto second = change_parity(right, parity_kind_max, parity_style_even); - cleanup_parity_here(first, true); - cleanup_parity_here(second, true); - colorize_parity_here(first, true); - colorize_parity_here(second, true); - return parity_product_aux(first, second); + 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 67880892d..5e6e0e6a8 100644 --- a/spot/twaalgos/parity.hh +++ b/spot/twaalgos/parity.hh @@ -147,5 +147,22 @@ namespace spot 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 401a106cd..61983f8e4 100644 --- a/tests/core/parity.cc +++ b/tests/core/parity.cc @@ -27,6 +27,7 @@ #include #include #include +#include #include #include #include @@ -389,7 +390,7 @@ int main() unsigned acc_index = 0; unsigned nb = 0; - // Parity product + // 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]; @@ -415,9 +416,9 @@ int main() 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 = spot::parity_product(left, right); - auto ref = spot::product(left, right); - if (!are_equiv(result, ref)) + 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"; @@ -426,12 +427,30 @@ int main() spot::print_hoa(std::cerr, right); assert(false && "parity_product: Not equivalent.\n"); } - assert(is_colored_printerr(result) + assert(is_colored_printerr(result_prod) && "parity_product: not colored."); - assert(is_right_parity(result, spot::parity_kind_any, + 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; } }