From b92320cc332807825db46ce4f7ba3f1b93868a62 Mon Sep 17 00:00:00 2001 From: Laurent XU Date: Wed, 15 Feb 2017 00:25:11 +0100 Subject: [PATCH] parity: add spot::parity_product() Compute the synchronized product of two parity automata, this product keeps the parity acceptance. * spot/twaalgos/parity.cc, spot/twaalgos/parity.hh: Here * tests/core/parity.cc: Add tests for spot::parity_product() --- spot/twaalgos/parity.cc | 216 ++++++++++++++++++++++++++++++++++++++++ spot/twaalgos/parity.hh | 17 ++++ tests/core/parity.cc | 53 ++++++++++ 3 files changed, 286 insertions(+) diff --git a/spot/twaalgos/parity.cc b/spot/twaalgos/parity.cc index af1c8585a..2dbb9c8a9 100644 --- a/spot/twaalgos/parity.cc +++ b/spot/twaalgos/parity.cc @@ -288,4 +288,220 @@ namespace spot } return aut; } + + namespace + { + class state_history : public std::vector + { + public: + 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 * 2, false); + } + + bool get_e(unsigned left, unsigned right) const + { + return get(left, right, true); + } + + bool get_f(unsigned left, unsigned right) const + { + return get(left, right, false); + } + + void set_e(unsigned left, unsigned right, bool val) + { + set(left, right, true, val); + } + + void set_f(unsigned left, unsigned right, bool val) + { + set(left, right, false, val); + } + + unsigned get_left_num_sets() const + { + return left_num_sets_; + } + + unsigned get_right_num_sets() const + { + return right_num_sets_; + } + + private: + unsigned left_num_sets_; + unsigned right_num_sets_; + + bool get(unsigned left, unsigned right, bool first) const + { + return at(left * right_num_sets_ * 2 + right * 2 + (first ? 1 : 0)); + } + + void set(unsigned left, unsigned right, bool first, bool val) + { + at(left * right_num_sets_ * 2 + right * 2 + (first ? 1 : 0)) = val; + } + }; + + typedef std::tuple + product_state; + + struct product_state_hash + { + size_t + operator()(product_state s) const + { + auto result = wang32_hash(std::get<0>(s) ^ wang32_hash(std::get<1>(s))); + return result ^ (std::hash>()(std::get<2>(s)) << 1); + } + }; + + twa_graph_ptr + parity_product_aux(twa_graph_ptr& left, twa_graph_ptr& right) + { + std::unordered_map, + product_state_hash> s2n; + 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, false, z_size); + res->set_acceptance(z_size, z); + + auto v = new product_states; + res->set_named_prop("product-states", v); + + auto new_state = + [&](const state_history& current_history, + unsigned left_state, unsigned right_state, + unsigned left_acc_set, unsigned right_acc_set) + -> std::pair + { + product_state x(left_state, right_state, current_history); + auto& mat = std::get<2>(x); + for (unsigned i = 0; i < left_num_sets; ++i) + for (unsigned j = 0; j < right_num_sets; ++j) + { + auto e_ij = current_history.get_e(i, j); + auto f_ij = current_history.get_f(i, j); + auto left_in_i = left_acc_set >= i; + auto right_in_j = right_acc_set >= j; + if (e_ij && f_ij) + { + mat.set_e(i, j, left_in_i); + mat.set_f(i, j, right_in_j); + } + else + { + mat.set_e(i, j, e_ij || left_in_i); + mat.set_f(i, j, f_ij || right_in_j); + } + } + auto p = s2n.emplace(x, std::make_pair(0, 0)); + if (p.second) // This is a new state + { + p.first->second.first = res->new_state(); + p.first->second.second = 0; + for (unsigned i = z_size - 1; i > 0 + && p.first->second.second == 0; --i) + { + // 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 k = 0; + if (i >= right_num_sets) + k = i - right_num_sets + 1; + unsigned var = 2 - i % 2; + k += k & ~var & 1; + unsigned max_k = std::min(i + 1, left_num_sets); + while (k < max_k) + { + unsigned l = i - k; + if (mat.get_e(k, l) && mat.get_f(k, l)) + { + p.first->second.second = i; + break; + } + k += var; + } + v->push_back(std::make_pair(left_state, right_state)); + } + todo.emplace(x, p.first->second.first); + } + return p.first->second; + }; + + state_history init_state_history(left_num_sets, right_num_sets); + product_state init_state(left->get_init_state_number(), + right->get_init_state_number(), + init_state_history); + auto init_state_index = res->new_state(); + s2n.emplace(init_state, std::make_pair(init_state_index, 0)); + 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"); + 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); + } } diff --git a/spot/twaalgos/parity.hh b/spot/twaalgos/parity.hh index 34b0c3a6d..67880892d 100644 --- a/spot/twaalgos/parity.hh +++ b/spot/twaalgos/parity.hh @@ -130,5 +130,22 @@ 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); /// @} } diff --git a/tests/core/parity.cc b/tests/core/parity.cc index 5e5194c4a..401a106cd 100644 --- a/tests/core/parity.cc +++ b/tests/core/parity.cc @@ -382,5 +382,58 @@ 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 + 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 = spot::parity_product(left, right); + auto ref = spot::product(left, right); + if (!are_equiv(result, ref)) + { + 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) + && "parity_product: not colored."); + assert(is_right_parity(result, spot::parity_kind_any, + spot::parity_style_any, + true, true, 2) + && "parity_product: not a parity acceptance condition"); + ++nb; + } + } return 0; }