diff --git a/python/spot/impl.i b/python/spot/impl.i index 88bdcf5c4..502770fcb 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -520,6 +520,7 @@ namespace std { %template(vectorbdd) vector; %template(aliasvector) vector>; %template(vectorstring) vector; + %template(vectorint) vector; %template(pair_formula_vectorstring) pair>; %template(atomic_prop_set) set; %template(relabeling_map) map; diff --git a/spot/twaalgos/parity.cc b/spot/twaalgos/parity.cc index 9428d7bb5..c8507ac53 100644 --- a/spot/twaalgos/parity.cc +++ b/spot/twaalgos/parity.cc @@ -387,27 +387,15 @@ namespace spot return aut; } - twa_graph_ptr - reduce_parity(const const_twa_graph_ptr& aut, bool colored, bool layered) + reduce_parity_data::reduce_parity_data(const const_twa_graph_ptr& aut, + bool layered) { - return reduce_parity_here(make_twa_graph(aut, twa::prop_set::all()), - colored, layered); - } - - twa_graph_ptr - reduce_parity_here(twa_graph_ptr aut, bool colored, bool layered) - { - unsigned num_sets = aut->num_sets(); - if (!colored && num_sets == 0) - return aut; - - bool current_max; - bool current_odd; - if (!aut->acc().is_parity(current_max, current_odd, true)) - input_is_not_parity("reduce_parity"); + if (!aut->acc().is_parity(parity_max, parity_odd, true)) + input_is_not_parity("reduce_parity_data"); if (!aut->is_existential()) throw std::runtime_error - ("reduce_parity_here() does not support alternation"); + ("reduce_parity_data() does not support alternation"); + unsigned num_sets = aut->num_sets(); // The algorithm assumes "max odd" or "max even" parity. "min" // parity is handled by converting it to "max" while the algorithm @@ -466,8 +454,8 @@ namespace spot // // -2 means the edge was never assigned a color. unsigned evs = aut->edge_vector().size(); - std::vector piprime1(evs, -2); // k=1 - std::vector piprime2(evs, -2); // k=0 + piprime1.resize(evs, -2); // k=1 + piprime2.resize(evs, -2); // k=0 bool sba = aut->prop_state_acc().is_true(); auto rec = @@ -481,7 +469,7 @@ namespace spot { int piri; // π(Rᵢ) int color; // corresponding color, to deal with "min" kind - if (current_max) + if (parity_max) { piri = color = si.acc_sets_of(scc).max_set() - 1; } @@ -538,11 +526,28 @@ namespace spot }; scc_and_mark_filter filter1(aut, {}); rec(filter1, rec); + } + + twa_graph_ptr + reduce_parity(const const_twa_graph_ptr& aut, bool colored, bool layered) + { + return reduce_parity_here(make_twa_graph(aut, twa::prop_set::all()), + colored, layered); + } + + twa_graph_ptr + reduce_parity_here(twa_graph_ptr aut, bool colored, bool layered) + { + unsigned num_sets = aut->num_sets(); + if (!colored && num_sets == 0) + return aut; + + reduce_parity_data pd(aut, layered); // compute the used range for each vector. int min1 = num_sets; int max1 = -2; - for (int m : piprime1) + for (int m : pd.piprime1) { if (m <= -2) continue; @@ -559,7 +564,7 @@ namespace spot } int min2 = num_sets; int max2 = -2; - for (int m : piprime2) + for (int m : pd.piprime2) { if (m <= -2) continue; @@ -575,13 +580,13 @@ namespace spot { std::swap(size1, size2); std::swap(min1, min2); - std::swap(piprime1, piprime2); + std::swap(pd.piprime1, pd.piprime2); } unsigned new_num_sets = size1; - if (current_max) + if (pd.parity_max) { - for (int& m : piprime1) + for (int& m : pd.piprime1) if (m > -2) m -= min1; else @@ -589,7 +594,7 @@ namespace spot } else { - for (int& m : piprime1) + for (int& m : pd.piprime1) if (m > -2) m = new_num_sets - (m - min1) - 1; else @@ -597,8 +602,8 @@ namespace spot } // The parity style changes if we shift colors by an odd number. - bool new_odd = current_odd ^ (min1 & 1); - if (!current_max) + bool new_odd = pd.parity_odd ^ (min1 & 1); + if (!pd.parity_max) // Switching from min<->max changes the parity style every time // the number of colors is even. If the input was "min", we // switched once to "max" to apply the reduction and once again @@ -607,7 +612,7 @@ namespace spot new_odd ^= !(num_sets & 1) ^ !(new_num_sets & 1); if (!colored) { - new_odd ^= current_max; + new_odd ^= pd.parity_max; new_num_sets -= 1; // It seems we have nothing to win by changing automata with a @@ -617,18 +622,18 @@ namespace spot } aut->set_acceptance(new_num_sets, - acc_cond::acc_code::parity(current_max, new_odd, + acc_cond::acc_code::parity(pd.parity_max, new_odd, new_num_sets)); if (colored) for (auto& e: aut->edges()) { unsigned n = aut->edge_number(e); - e.acc = acc_cond::mark_t({unsigned(piprime1[n])}); + e.acc = acc_cond::mark_t({unsigned(pd.piprime1[n])}); } - else if (current_max) + else if (pd.parity_max) for (auto& e: aut->edges()) { - unsigned n = piprime1[aut->edge_number(e)]; + unsigned n = pd.piprime1[aut->edge_number(e)]; if (n == 0) e.acc = acc_cond::mark_t({}); else @@ -637,7 +642,7 @@ namespace spot else for (auto& e: aut->edges()) { - unsigned n = piprime1[aut->edge_number(e)]; + unsigned n = pd.piprime1[aut->edge_number(e)]; if (n >= new_num_sets) e.acc = acc_cond::mark_t({}); else diff --git a/spot/twaalgos/parity.hh b/spot/twaalgos/parity.hh index 44d7cca7e..188e92483 100644 --- a/spot/twaalgos/parity.hh +++ b/spot/twaalgos/parity.hh @@ -21,6 +21,7 @@ #include #include +#include namespace spot { @@ -194,5 +195,27 @@ namespace spot SPOT_API twa_graph_ptr reduce_parity_here(twa_graph_ptr aut, bool colored = false, bool layered = false); + + /// @} + + /// \brief Internal data computed by the reduce_parity function + /// + /// `piprime1` and `piprime2` have the size of `aut`'s edge vector, + /// represent two possible colorations of the edges. piprime1 assumes + /// that terminal cases of the recursion are odd, and piprime2 assumes + /// they are even. + /// + /// reduce_parity() actually compare the range of values in these + /// two vectors to limit the number of colors. + struct SPOT_API reduce_parity_data + { + bool parity_max; ///< Whether the input automaton is parity max + bool parity_odd; ///< Whether the input automaton is parity odd + std::vector piprime1; + std::vector piprime2; + + reduce_parity_data(const const_twa_graph_ptr& aut, bool layered = false); + }; + /// @} }