diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 3b31cefbf..d92353026 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -1290,3 +1290,30 @@ class scc_and_mark_filter: def __exit__(self, exc_type, exc_value, traceback): self.restore_acceptance() + + +def to_parity(aut, **kwargs): + option = car_option() + if "search_ex" in kwargs: + option.search_ex = kwargs.get("search_ex") + if "use_last" in kwargs: + option.use_last = kwargs.get("use_last") + if "force_order" in kwargs: + option.force_order = kwargs.get("force_order") + if "partial_degen" in kwargs: + option.partial_degen = kwargs.get("partial_degen") + if "acc_clean" in kwargs: + option.acc_clean = kwargs.get("acc_clean") + if "parity_equiv" in kwargs: + option.parity_equiv = kwargs.get("parity_equiv") + if "parity_prefix" in kwargs: + option.parity_prefix = kwargs.get("parity_prefix") + if "rabin_to_buchi" in kwargs: + option.rabin_to_buchi = kwargs.get("rabin_to_buchi") + if "reduce_col_deg" in kwargs: + option.reduce_col_deg = kwargs.get("reduce_col_deg") + if "propagate_col" in kwargs: + option.propagate_col = kwargs.get("propagate_col") + if "pretty_print" in kwargs: + option.pretty_print = kwargs.get("pretty_print") + return impl.to_parity(aut, option) diff --git a/python/spot/impl.i b/python/spot/impl.i index d9296f76f..d5e4bb415 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -160,9 +160,7 @@ #include #include #include -#include #include -#include #include @@ -682,9 +680,7 @@ def state_is_accepting(self, src) -> "bool": %include %template(list_bdd) std::list; %include -%include %include -%include %pythonprepend spot::twa::dtwa_complement %{ from warnings import warn diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index f3bd3d717..adbecbd82 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -59,7 +59,6 @@ twaalgos_HEADERS = \ isunamb.hh \ isweakscc.hh \ langmap.hh \ - car.hh \ lbtt.hh \ ltl2taa.hh \ ltl2tgba_fm.hh \ @@ -72,7 +71,6 @@ twaalgos_HEADERS = \ postproc.hh \ powerset.hh \ product.hh \ - rabin2parity.hh \ randomgraph.hh \ randomize.hh \ reachiter.hh \ @@ -129,7 +127,6 @@ libtwaalgos_la_SOURCES = \ isunamb.cc \ isweakscc.cc \ langmap.cc \ - car.cc \ lbtt.cc \ ltl2taa.cc \ ltl2tgba_fm.cc \ @@ -143,7 +140,6 @@ libtwaalgos_la_SOURCES = \ postproc.cc \ powerset.cc \ product.cc \ - rabin2parity.cc \ randomgraph.cc \ randomize.cc \ reachiter.cc \ diff --git a/spot/twaalgos/car.cc b/spot/twaalgos/car.cc deleted file mode 100644 index 07952c020..000000000 --- a/spot/twaalgos/car.cc +++ /dev/null @@ -1,1291 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2012-2020 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include "config.h" -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include - -#include - -namespace spot -{ -namespace -{ -struct node -{ - // A color of the permutation or a state. - unsigned label; - std::vector children; - // is_leaf is true if the label is a state of res_. - bool is_leaf; - - node() - : node(0, 0){ - } - - node(int label_, bool is_leaf_) - : label(label_) - , children(0) - , is_leaf(is_leaf_){ - } - - ~node() - { - for (auto c : children) - delete c; - } - - // Add a permutation to the tree. - void - add_new_perm(const std::vector& permu, int pos, unsigned state) - { - if (pos == -1) - children.push_back(new node(state, true)); - else - { - auto lab = permu[pos]; - auto child = std::find_if(children.begin(), children.end(), - [lab](node* n){ - return n->label == lab; - }); - if (child == children.end()) - { - node* new_child = new node(lab, false); - children.push_back(new_child); - new_child->add_new_perm(permu, pos - 1, state); - } - else - (*child)->add_new_perm(permu, pos - 1, state); - } - } - - // Gives a state of res_ (if it exists) reachable from this node. - // If use_last is true, we take the most recent, otherwise we take - // the oldest. - unsigned - get_end(bool use_last) - { - if (children.empty()) - { - if (!is_leaf) - return -1U; - return label; - } - if (use_last) - return children[children.size() - 1]->get_end(use_last); - return children[0]->get_end(use_last); - } - - // Try to find a state compatible with the permu when seen_nb colors are - // moved. - unsigned - get_existing(const std::vector& permu, unsigned seen_nb, int pos, - bool use_last) - { - if (pos < (int) seen_nb) - return get_end(use_last); - else - { - auto lab = permu[pos]; - auto child = std::find_if(children.begin(), children.end(), - [lab](node* n){ - return n->label == lab; - }); - if (child == children.end()) - return -1U; - return (*child)->get_existing(permu, seen_nb, pos - 1, use_last); - } - } -}; - -class state_2_car_scc -{ -std::vector nodes; - -public: -state_2_car_scc(unsigned nb_states) - : nodes(nb_states, node()){ -} - -unsigned -get_res_state(unsigned state, const std::vector& permu, - unsigned seen_nb, bool use_last) -{ - return nodes[state].get_existing(permu, seen_nb, - permu.size() - 1, use_last); -} - -void -add_res_state(unsigned initial, unsigned state, - const std::vector& permu) -{ - nodes[initial].add_new_perm(permu, ((int) permu.size()) - 1, state); -} -}; - -class car_generator -{ -enum algorithm { - // Try to have a Büchi condition if we have Rabin. - Rabin_to_Buchi, - Streett_to_Buchi, - // IAR - IAR_Streett, - IAR_Rabin, - // CAR - CAR, - // Changing colors transforms acceptance to max even/odd copy. - Copy_even, - Copy_odd, - // If a condition is "t" or "f", we just have to copy the automaton. - False_clean, - True_clean, - None -}; - - -static std::string -algorithm_to_str(algorithm algo) -{ - std::string algo_str; - switch (algo) - { - case IAR_Streett: - algo_str = "IAR (Streett)"; - break; - case IAR_Rabin: - algo_str = "IAR (Rabin)"; - break; - case CAR: - algo_str = "CAR"; - break; - case Copy_even: - algo_str = "Copy even"; - break; - case Copy_odd: - algo_str = "Copy odd"; - break; - case False_clean: - algo_str = "False clean"; - break; - case True_clean: - algo_str = "True clean"; - break; - case Streett_to_Buchi: - algo_str = "Streett to Büchi"; - break; - case Rabin_to_Buchi: - algo_str = "Rabin to Büchi"; - break; - default: - algo_str = "None"; - break; - } - return algo_str; -} - -using perm_t = std::vector; - -struct car_state -{ - // State of the original automaton - unsigned state; - // We create a new automaton for each SCC of the original automaton - // so we keep a link between a car_state and the state of the - // subautomaton. - unsigned state_scc; - // Permutation used by IAR and CAR. - perm_t perm; - - bool - operator<(const car_state &other) const - { - if (state < other.state) - return true; - if (state > other.state) - return false; - if (perm < other.perm) - return true; - if (perm > other.perm) - return false; - return state_scc < other.state_scc; - } - - std::string - to_string(algorithm algo) const - { - std::stringstream s; - s << state; - unsigned ps = perm.size(); - if (ps > 0) - { - s << " ["; - for (unsigned i = 0; i != ps; ++i) - { - if (i > 0) - s << ','; - s << perm[i]; - } - s << ']'; - } - s << ", "; - s << algorithm_to_str(algo); - return s.str(); - } -}; - -const acc_cond::mark_t & -fin(const std::vector& pairs, unsigned k, algorithm algo) -const -{ - if (algo == IAR_Rabin) - return pairs[k].fin; - else - return pairs[k].inf; -} - -acc_cond::mark_t -inf(const std::vector& pairs, unsigned k, algorithm algo) -const -{ - if (algo == IAR_Rabin) - return pairs[k].inf; - else - return pairs[k].fin; -} - -std::vector> -get_inputs_states(const twa_graph_ptr& aut) -{ - auto used = aut->acc().get_acceptance().used_sets(); - std::vector> inputs(aut->num_states()); - for (auto e : aut->edges()) - { - auto elements = e.acc & used; - if (elements.count() > 1) - inputs[e.dst].insert(elements); - } - return inputs; -} - -std::vector>> -get_inputs_iar(const twa_graph_ptr& aut, algorithm algo, - const std::set& perm_elem, - const std::vector& pairs) -{ - std::vector>> inputs(aut->num_states()); - for (auto e : aut->edges()) - { - auto acc = e.acc; - std::vector new_vect; - for (unsigned k : perm_elem) - if (acc & fin(pairs, k, algo)) - new_vect.push_back(k); - std::sort(std::begin(new_vect), std::end(new_vect)); - inputs[e.dst].insert(new_vect); - } - return inputs; -} - -std::vector -group_to_vector(const std::set& group) -{ - std::vector group_vect(group.begin(), group.end()); - - std::sort(group_vect.begin(), group_vect.end(), - [](const acc_cond::mark_t left, const acc_cond::mark_t right) - { - return (left & right) == left; - }); - std::vector result; - for (auto mark : group_vect) - { - for (unsigned col : mark.sets()) - if (std::find(result.begin(), result.end(), col) == result.end()) - result.push_back(col); - } - return result; -} - -std::vector -group_to_vector_iar(const std::set>& group) -{ - std::vector> group_vect(group.begin(), group.end()); - for (auto& vec : group_vect) - std::sort(std::begin(vec), std::end(vec)); - std::sort(group_vect.begin(), group_vect.end(), - [](const std::vector left, - const std::vector right) - { - return std::includes(right.begin(), right.end(), - left.begin(), left.end()); - }); - std::vector result; - for (auto vec : group_vect) - for (unsigned col : vec) - if (std::find(result.begin(), result.end(), col) == result.end()) - result.push_back(col); - return result; -} - -std::map> -get_groups(const std::set& marks_input) -{ - std::map> result; - - std::vector> groups; - for (acc_cond::mark_t mark : marks_input) - { - bool added = false; - for (unsigned group = 0; group < groups.size(); ++group) - { - if (std::all_of(groups[group].begin(), groups[group].end(), - [mark](acc_cond::mark_t element) - { - return ((element | mark) == mark) - || ((element | mark) == element); - })) - { - groups[group].insert(mark); - added = true; - break; - } - } - if (!added) - groups.push_back({mark}); - } - for (auto& group : groups) - { - auto new_vector = group_to_vector(group); - for (auto mark : group) - result.insert(std::pair>( - mark, new_vector)); - } - return result; -} - -std::map, std::vector> -get_groups_iar(const std::set>& marks_input) -{ - std::map, std::vector> result; - - std::vector>> groups; - for (auto vect : marks_input) - { - bool added = false; - for (unsigned group = 0; group < groups.size(); ++group) - if (std::all_of(groups[group].begin(), groups[group].end(), - [vect](std::vector element) - { - return std::includes(vect.begin(), vect.end(), - element.begin(), element.end()) - || std::includes(element.begin(), element.end(), - vect.begin(), vect.end()); - })) - { - groups[group].insert(vect); - added = true; - break; - } - if (!added) - groups.push_back({vect}); - } - for (auto& group : groups) - { - auto new_vector = group_to_vector_iar(group); - for (auto vect : group) - result.insert( - std::pair, std::vector>( - vect, new_vector)); - } - return result; -} - -std::vector>> -get_mark_to_vector(const twa_graph_ptr& aut) -{ - std::vector>> result; - auto inputs = get_inputs_states(aut); - for (unsigned state = 0; state < inputs.size(); ++state) - { - std::map> state_map; - auto map = get_groups(inputs[state]); - result.push_back(map); - } - return result; -} - -std::vector, std::vector>> -get_iar_to_vector(const twa_graph_ptr& aut, algorithm algo, - const std::set& perm_elem, - const std::vector& pairs) -{ - std::vector, std::vector>> result; - auto inputs = get_inputs_iar(aut, algo, perm_elem, pairs); - for (unsigned state = 0; state < inputs.size(); ++state) - { - std::map, std::vector> state_map; - auto map = get_groups_iar(inputs[state]); - result.push_back(map); - } - return result; -} - -public: -explicit car_generator(const const_twa_graph_ptr &a, car_option options) - : aut_(a) - , scc_(scc_info(a)) - , is_odd(false) - , options(options) -{ - if (options.pretty_print) - names = new std::vector(); - else - names = nullptr; -} - -unsigned -apply_false_true_clean(const twa_graph_ptr &sub_automaton, bool is_true, - const std::vector& inf_fin_prefix, - unsigned max_free_color, - std::map& state2car_local, - std::map& car2num_local) -{ - std::vector* init_states = sub_automaton-> - get_named_prop>("original-states"); - - for (unsigned state = 0; state < sub_automaton->num_states(); ++state) - { - unsigned s_aut = (*init_states)[state]; - - car_state new_car = { s_aut, state, perm_t() }; - auto new_state = res_->new_state(); - car2num_local[new_car] = new_state; - num2car.insert(num2car.begin() + new_state, new_car); - if (options.pretty_print) - names->push_back( - new_car.to_string(is_true ? True_clean : False_clean)); - state2car_local[s_aut] = new_car; - } - for (unsigned state = 0; state < sub_automaton->num_states(); ++state) - { - auto col = is_true ^ !is_odd; - if (((unsigned) col) > max_free_color) - throw std::runtime_error("CAR needs more sets"); - unsigned s_aut = (*init_states)[state]; - car_state src = { s_aut, state, perm_t() }; - unsigned src_state = car2num_local[src]; - for (auto e : aut_->out(s_aut)) - { - if (scc_.scc_of(s_aut) == scc_.scc_of(e.dst)) - { - for (auto c : e.acc.sets()) - if (inf_fin_prefix[c] + is_odd > col) - col = inf_fin_prefix[c] + is_odd; - acc_cond::mark_t cond = { (unsigned) col }; - res_->new_edge( - src_state, car2num_local[state2car_local[e.dst]], - e.cond, cond); - } - } - } - return sub_automaton->num_states(); -} - -unsigned -apply_copy(const twa_graph_ptr &sub_automaton, - const std::vector &permut, - bool copy_odd, - const std::vector& inf_fin_prefix, - std::map& state2car_local, - std::map& car2num_local) -{ - std::vector* init_states = sub_automaton - ->get_named_prop>("original-states"); - for (unsigned state = 0; state < sub_automaton->num_states(); ++state) - { - car_state new_car = { (*init_states)[state], state, perm_t() }; - auto new_state = res_->new_state(); - car2num_local[new_car] = new_state; - num2car.insert(num2car.begin() + new_state, new_car); - state2car_local[(*init_states)[state]] = new_car; - if (options.pretty_print) - names->push_back( - new_car.to_string(copy_odd ? Copy_odd : Copy_even)); - } - auto cond_col = sub_automaton->acc().get_acceptance().used_sets(); - for (unsigned s = 0; s < sub_automaton->num_states(); ++s) - { - for (auto e : sub_automaton->out(s)) - { - acc_cond::mark_t mark = { }; - int max_edge = -1; - for (auto col : e.acc.sets()) - { - if (cond_col.has(col)) - max_edge = std::max(max_edge, (int) permut[col]); - if (inf_fin_prefix[col] + (is_odd || copy_odd) > max_edge) - max_edge = inf_fin_prefix[col] + (is_odd || copy_odd); - } - if (max_edge != -1) - mark.set((unsigned) max_edge); - car_state src = { (*init_states)[s], s, perm_t() }, - dst = { (*init_states)[e.dst], e.dst, perm_t() }; - unsigned src_state = car2num_local[src], - dst_state = car2num_local[dst]; - res_->new_edge(src_state, dst_state, e.cond, mark); - } - } - return sub_automaton->num_states(); -} - -unsigned -apply_to_Buchi(const twa_graph_ptr& sub_automaton, - const twa_graph_ptr& buchi, - bool is_streett_to_buchi, - const std::vector& inf_fin_prefix, - unsigned max_free_color, - std::map& state2car_local, - std::map&car2num_local) -{ - std::vector* init_states = sub_automaton - ->get_named_prop>("original-states"); - - for (unsigned state = 0; state < buchi->num_states(); ++state) - { - car_state new_car = { (*init_states)[state], state, perm_t() }; - auto new_state = res_->new_state(); - car2num_local[new_car] = new_state; - num2car.insert(num2car.begin() + new_state, new_car); - state2car_local[(*init_states)[state]] = new_car; - if (options.pretty_print) - names->push_back(new_car.to_string( - is_streett_to_buchi ? Streett_to_Buchi : Rabin_to_Buchi)); - } - auto g = buchi->get_graph(); - for (unsigned s = 0; s < buchi->num_states(); ++s) - { - unsigned b = g.state_storage(s).succ; - while (b) - { - auto& e = g.edge_storage(b); - auto acc = e.acc; - acc <<= (is_odd + is_streett_to_buchi); - if ((is_odd || is_streett_to_buchi) && acc == acc_cond::mark_t{ }) - acc = { (unsigned) (is_streett_to_buchi && is_odd) }; - car_state src = { (*init_states)[s], s, perm_t() }, - dst = { (*init_states)[e.dst], e.dst, perm_t() }; - unsigned src_state = car2num_local[src], - dst_state = car2num_local[dst]; - int col = ((int) acc.max_set()) - 1; - if (col > (int) max_free_color) - throw std::runtime_error("CAR needs more sets"); - auto& e2 = sub_automaton->get_graph().edge_storage(b); - for (auto c : e2.acc.sets()) - { - if (inf_fin_prefix[c] + is_odd > col) - col = inf_fin_prefix[c] + is_odd; - } - if (col != -1) - acc = { (unsigned) col }; - else - acc = {}; - res_->new_edge(src_state, dst_state, e.cond, acc); - b = e.next_succ; - } - } - return buchi->num_states(); -} - -void -initial_perm_iar(std::set &perm_elem, perm_t &p0, - algorithm algo, const acc_cond::mark_t &colors, - const std::vector &pairs) -{ - for (unsigned k = 0; k != pairs.size(); ++k) - if (!inf(pairs, k, algo) || (colors & (pairs[k].fin | pairs[k].inf))) - { - perm_elem.insert(k); - p0.push_back(k); - } -} - -// Create a permutation for the first state of a SCC (CAR) -void -initial_perm_car(perm_t &p0, const acc_cond::mark_t &colors) -{ - auto cont = colors.sets(); - p0.assign(cont.begin(), cont.end()); -} - -void -find_new_perm_iar(perm_t &new_perm, - const std::vector &pairs, - const acc_cond::mark_t &acc, - algorithm algo, const std::set &perm_elem, - unsigned &seen_nb) -{ - for (unsigned k : perm_elem) - if (acc & fin(pairs, k, algo)) - { - ++seen_nb; - auto it = std::find(new_perm.begin(), new_perm.end(), k); - - // move the pair in front of the permutation - std::rotate(new_perm.begin(), it, it + 1); - } -} - -// Given the set acc of colors appearing on an edge, create a new -// permutation new_perm, and give the number seen_nb of colors moved to -// the head of the permutation. -void -find_new_perm_car(perm_t &new_perm, const acc_cond::mark_t &acc, - unsigned &seen_nb, unsigned &h) -{ - for (unsigned k : acc.sets()) - { - auto it = std::find(new_perm.begin(), new_perm.end(), k); - if (it != new_perm.end()) - { - h = std::max(h, unsigned(it - new_perm.begin()) + 1); - std::rotate(new_perm.begin(), it, it + 1); - ++seen_nb; - } - } -} - -void -get_acceptance_iar(algorithm algo, const perm_t ¤t_perm, - const std::vector &pairs, - const acc_cond::mark_t &e_acc, acc_cond::mark_t &acc) -{ - unsigned delta_acc = (algo == IAR_Streett) && is_odd; - - // find the maximal index encountered by this transition - unsigned maxint = -1U; - - for (int k = current_perm.size() - 1; k >= 0; --k) - { - unsigned pk = current_perm[k]; - - if (!inf(pairs, pk, - algo) - || (e_acc & (pairs[pk].fin | pairs[pk].inf))) - { - maxint = k; - break; - } - } - unsigned value; - - if (maxint == -1U) - value = delta_acc; - else if (e_acc & fin(pairs, current_perm[maxint], algo)) - value = 2 * maxint + 2 + delta_acc; - else - value = 2 * maxint + 1 + delta_acc; - acc = { value }; -} - -void -get_acceptance_car(const acc_cond &sub_aut_cond, const perm_t &new_perm, - unsigned h, acc_cond::mark_t &acc) -{ - acc_cond::mark_t m(new_perm.begin(), new_perm.begin() + h); - bool rej = !sub_aut_cond.accepting(m); - unsigned value = 2 * h + rej + is_odd; - acc = { value }; -} - -unsigned -apply_lar(const twa_graph_ptr &sub_automaton, - unsigned init, std::vector &pairs, - algorithm algo, unsigned scc_num, - const std::vector& inf_fin_prefix, - unsigned max_free_color, - std::map& state2car_local, - std::map& car2num_local, - unsigned max_states) -{ - auto maps = get_mark_to_vector(sub_automaton); - unsigned nb_created_states = 0; - auto state_2_car = state_2_car_scc(sub_automaton->num_states()); - std::vector* init_states = sub_automaton-> - get_named_prop>("original-states"); - std::deque todo; - auto get_state = - [&](const car_state &s){ - auto it = car2num_local.find(s); - - if (it == car2num_local.end()) - { - ++nb_created_states; - unsigned nb = res_->new_state(); - if (options.search_ex) - state_2_car.add_res_state(s.state_scc, nb, s.perm); - car2num_local[s] = nb; - num2car.insert(num2car.begin() + nb, s); - - todo.push_back(s); - if (options.pretty_print) - names->push_back(s.to_string(algo)); - return nb; - } - return it->second; - }; - - auto colors = sub_automaton->acc().get_acceptance().used_sets(); - std::set perm_elem; - - perm_t p0 = { }; - switch (algo) - { - case IAR_Streett: - case IAR_Rabin: - initial_perm_iar(perm_elem, p0, algo, colors, pairs); - break; - case CAR: - initial_perm_car(p0, colors); - break; - default: - assert(false); - break; - } - - std::vector, std::vector>> - iar_maps; - if (algo == IAR_Streett || algo == IAR_Rabin) - iar_maps = get_iar_to_vector(sub_automaton, algo, perm_elem, pairs); - - car_state s0{ (*init_states)[init], init, p0 }; - get_state(s0); // put s0 in todo - - // the main loop - while (!todo.empty()) - { - car_state current = todo.front(); - todo.pop_front(); - - unsigned src_num = get_state(current); - for (const auto &e : sub_automaton->out(current.state_scc)) - { - perm_t new_perm = current.perm; - - // Count pairs whose fin-part is seen on this transition - unsigned seen_nb = 0; - - // consider the pairs for this SCC only - unsigned h = 0; - - switch (algo) - { - case IAR_Rabin: - case IAR_Streett: - find_new_perm_iar(new_perm, pairs, e.acc, algo, - perm_elem, seen_nb); - break; - case CAR: - find_new_perm_car(new_perm, e.acc, seen_nb, h); - break; - default: - assert(false); - } - - if (options.force_order) - { - if (algo == CAR && seen_nb > 1) - { - auto map = maps[e.dst]; - acc_cond::mark_t first_vals( - new_perm.begin(), new_perm.begin() + seen_nb); - auto new_start = map.find(first_vals); - assert(new_start->second.size() >= seen_nb); - assert(new_start != map.end()); - for (unsigned i = 0; i < seen_nb; ++i) - new_perm[i] = new_start->second[i]; - } - else if ((algo == IAR_Streett || algo == IAR_Rabin) - && seen_nb > 1) - { - auto map = iar_maps[e.dst]; - std::vector first_vals( - new_perm.begin(), new_perm.begin() + seen_nb); - std::sort(std::begin(first_vals), std::end(first_vals)); - auto new_start = map.find(first_vals); - assert(new_start->second.size() >= seen_nb); - assert(new_start != map.end()); - for (unsigned i = 0; i < seen_nb; ++i) - new_perm[i] = new_start->second[i]; - } - } - - // Optimization: when several indices are seen in the - // transition, they move at the front of new_perm in any - // order. Check whether there already exists an car_state - // that matches this condition. - car_state dst; - unsigned dst_num = -1U; - - if (options.search_ex) - dst_num = state_2_car.get_res_state(e.dst, new_perm, seen_nb, - options.use_last); - - if (dst_num == -1U) - { - auto dst = car_state{ (*init_states)[e.dst], e.dst, new_perm }; - dst_num = get_state(dst); - if (nb_created_states > max_states) - return -1U; - } - - acc_cond::mark_t acc = { }; - - switch (algo) - { - case IAR_Rabin: - case IAR_Streett: - get_acceptance_iar(algo, current.perm, pairs, e.acc, acc); - break; - case CAR: - get_acceptance_car(sub_automaton->acc(), new_perm, h, acc); - break; - default: - assert(false); - } - - unsigned acc_col = acc.min_set() - 1; - if (options.parity_prefix) - { - if (acc_col > max_free_color) - throw std::runtime_error("CAR needs more sets"); - // parity prefix - for (auto col : e.acc.sets()) - { - if (inf_fin_prefix[col] + is_odd > (int) acc_col) - acc_col = (unsigned) inf_fin_prefix[col] + is_odd; - } - } - res_->new_edge(src_num, dst_num, e.cond, { acc_col }); - } - } - auto leaving_edge = - [&](unsigned d){ - return scc_.scc_of(num2car.at(d).state) != scc_num; - }; - auto filter_edge = - [](const twa_graph::edge_storage_t &, - unsigned dst, - void* filter_data){ - decltype(leaving_edge) *data = - static_cast(filter_data); - - if ((*data)(dst)) - return scc_info::edge_filter_choice::ignore; - - return scc_info::edge_filter_choice::keep; - }; - scc_info sub_scc(res_, get_state(s0), filter_edge, &leaving_edge); - - // SCCs are numbered in reverse topological order, so the bottom SCC has - // index 0. - const unsigned bscc = 0; - assert(sub_scc.scc_count() != 0); - assert(sub_scc.succ(0).empty()); - assert( - [&](){ - for (unsigned s = 1; s != sub_scc.scc_count(); ++s) - if (sub_scc.succ(s).empty()) - return false; - - return true; - } ()); - - assert(sub_scc.states_of(bscc).size() >= sub_automaton->num_states()); - - // update state2car - for (unsigned scc_state : sub_scc.states_of(bscc)) - { - car_state &car = num2car.at(scc_state); - - if (state2car_local.find(car.state) == state2car_local.end()) - state2car_local[car.state] = car; - } - return sub_scc.states_of(bscc).size(); -} - -algorithm -chooseAlgo(twa_graph_ptr &sub_automaton, - twa_graph_ptr &rabin_aut, - std::vector &pairs, - std::vector &permut) -{ - auto scc_condition = sub_automaton->acc(); - if (options.parity_equiv) - { - if (scc_condition.is_f()) - return False_clean; - if (scc_condition.is_t()) - return True_clean; - std::vector permut_tmp(scc_condition.all_sets().max_set(), -1); - - if (!is_odd && scc_condition.is_parity_max_equiv(permut_tmp, true)) - { - for (auto c : permut_tmp) - permut.push_back((unsigned) c); - - scc_condition.apply_permutation(permut); - sub_automaton->apply_permutation(permut); - return Copy_even; - } - std::fill(permut_tmp.begin(), permut_tmp.end(), -1); - if (scc_condition.is_parity_max_equiv(permut_tmp, false)) - { - for (auto c : permut_tmp) - permut.push_back((unsigned) c); - scc_condition.apply_permutation(permut); - sub_automaton->apply_permutation(permut); - return Copy_odd; - } - } - - if (options.rabin_to_buchi) - { - auto ra = rabin_to_buchi_if_realizable(sub_automaton); - if (ra != nullptr) - { - rabin_aut = ra; - return Rabin_to_Buchi; - } - else - { - bool streett_buchi = false; - auto sub_cond = sub_automaton->get_acceptance(); - sub_automaton->set_acceptance(sub_cond.complement()); - auto ra = rabin_to_buchi_if_realizable(sub_automaton); - streett_buchi = (ra != nullptr); - sub_automaton->set_acceptance(sub_cond); - if (streett_buchi) - { - rabin_aut = ra; - return Streett_to_Buchi; - } - } - } - - auto pairs1 = std::vector(); - auto pairs2 = std::vector(); - std::sort(pairs1.begin(), pairs1.end()); - pairs1.erase(std::unique(pairs1.begin(), pairs1.end()), pairs1.end()); - std::sort(pairs2.begin(), pairs2.end()); - pairs2.erase(std::unique(pairs2.begin(), pairs2.end()), pairs2.end()); - bool is_r_like = scc_condition.is_rabin_like(pairs1); - bool is_s_like = scc_condition.is_streett_like(pairs2); - unsigned num_cols = scc_condition.get_acceptance().used_sets().count(); - if (is_r_like) - { - if ((is_s_like && pairs1.size() < pairs2.size()) || !is_s_like) - { - if (pairs1.size() > num_cols) - return CAR; - pairs = pairs1; - return IAR_Rabin; - } - else if (is_s_like) - { - if (pairs2.size() > num_cols) - return CAR; - pairs = pairs2; - return IAR_Streett; - } - } - else - { - if (is_s_like) - { - if (pairs2.size() > num_cols) - return CAR; - pairs = pairs2; - return IAR_Streett; - } - } - return CAR; -} - -unsigned -build_scc(twa_graph_ptr &sub_automaton, - unsigned scc_num, - std::map& state2car_local, - std::map&car2num_local, - algorithm& algo, - unsigned max_states = -1U) -{ - - std::vector parity_prefix_colors (SPOT_MAX_ACCSETS, -1); - unsigned min_prefix_color = SPOT_MAX_ACCSETS + 1; - if (options.parity_prefix) - { - auto new_acc = sub_automaton->acc(); - auto colors = std::vector(); - bool inf_start = - sub_automaton->acc().has_parity_prefix(new_acc, colors); - sub_automaton->set_acceptance(new_acc); - for (unsigned i = 0; i < colors.size(); ++i) - parity_prefix_colors[colors[i]] = - SPOT_MAX_ACCSETS - 4 - i - !inf_start; - if (colors.size() > 0) - min_prefix_color = - SPOT_MAX_ACCSETS - 4 - colors.size() - 1 - !inf_start; - } - --min_prefix_color; - - unsigned init = 0; - - std::vector pairs = { }; - auto permut = std::vector(); - twa_graph_ptr rabin_aut = nullptr; - algo = chooseAlgo(sub_automaton, rabin_aut, pairs, permut); - switch (algo) - { - case False_clean: - case True_clean: - return apply_false_true_clean(sub_automaton, (algo == True_clean), - parity_prefix_colors, min_prefix_color, - state2car_local, car2num_local); - break; - case IAR_Streett: - case IAR_Rabin: - case CAR: - return apply_lar(sub_automaton, init, pairs, algo, scc_num, - parity_prefix_colors, min_prefix_color, - state2car_local, car2num_local, max_states); - break; - case Copy_odd: - case Copy_even: - return apply_copy(sub_automaton, permut, algo == Copy_odd, - parity_prefix_colors, state2car_local, - car2num_local); - break; - case Rabin_to_Buchi: - case Streett_to_Buchi: - return apply_to_Buchi(sub_automaton, rabin_aut, - (algo == Streett_to_Buchi), - parity_prefix_colors, min_prefix_color, - state2car_local, car2num_local); - break; - default: - break; - } - return -1U; -} - -public: -twa_graph_ptr -run() -{ - res_ = make_twa_graph(aut_->get_dict()); - res_->copy_ap_of(aut_); - for (unsigned scc = 0; scc < scc_.scc_count(); ++scc) - { - if (!scc_.is_useful_scc(scc)) - continue; - auto sub_automata = scc_.split_on_sets(scc, { }, true); - if (sub_automata.empty()) - { - for (auto state : scc_.states_of(scc)) - { - auto new_state = res_->new_state(); - car_state new_car = { state, state, perm_t() }; - car2num[new_car] = new_state; - num2car.insert(num2car.begin() + new_state, new_car); - if (options.pretty_print) - names->push_back(new_car.to_string(None)); - state2car[state] = new_car; - } - continue; - } - - auto sub_automaton = sub_automata[0]; - auto deg = sub_automaton; - if (options.acc_clean) - simplify_acceptance_here(sub_automaton); - bool has_degeneralized = false; - if (options.partial_degen) - { - std::vector forbid; - auto m = - is_partially_degeneralizable(sub_automaton, true, - true, forbid); - while (m != acc_cond::mark_t {}) - { - auto tmp = partial_degeneralize(deg, m); - simplify_acceptance_here(tmp); - if (tmp->get_acceptance().used_sets().count() - < deg->get_acceptance().used_sets().count() || - !(options.reduce_col_deg)) - { - deg = tmp; - has_degeneralized = true; - } - else - forbid.push_back(m); - m = is_partially_degeneralizable(deg, true, true, forbid); - } - } - - if (options.propagate_col) - { - propagate_marks_here(sub_automaton); - propagate_marks_here(deg); - } - - std::map state2car_sub, state2car_deg; - std::map car2num_sub, car2num_deg; - - unsigned nb_states_deg = -1U, - nb_states_sub = -1U; - - algorithm algo_sub, algo_deg; - unsigned max_states_sub_car = -1U; - - if (has_degeneralized) - { - nb_states_deg = - build_scc(deg, scc, state2car_deg, car2num_deg, algo_deg); - // We suppose that if we see nb_states_deg + 1000 states when - // when construct the version without degeneralization during the - // construction, we will not be able to have nb_states_deg after - // removing useless states. So we will stop the execution. - max_states_sub_car = - 10000 + nb_states_deg - 1; - } - nb_states_sub = - build_scc(sub_automaton, scc, state2car_sub, car2num_sub, - algo_sub, max_states_sub_car); - if (nb_states_deg < nb_states_sub) - { - state2car.insert(state2car_deg.begin(), state2car_deg.end()); - car2num.insert(car2num_deg.begin(), car2num_deg.end()); - algo_sub = algo_deg; - } - else - { - state2car.insert(state2car_sub.begin(), state2car_sub.end()); - car2num.insert(car2num_sub.begin(), car2num_sub.end()); - } - if ((algo_sub == IAR_Rabin || algo_sub == Copy_odd) && !is_odd) - { - is_odd = true; - for (auto &edge : res_->edges()) - { - if (scc_.scc_of(num2car[edge.src].state) != scc - && scc_.scc_of(num2car[edge.dst].state) != scc) - { - if (edge.acc == acc_cond::mark_t{}) - edge.acc = { 0 }; - else - edge.acc <<= 1; - } - } - } - } - - for (unsigned state = 0; state < res_->num_states(); ++state) - { - unsigned original_state = num2car.at(state).state; - auto state_scc = scc_.scc_of(original_state); - for (auto edge : aut_->out(original_state)) - { - if (scc_.scc_of(edge.dst) != state_scc) - { - auto car = state2car.find(edge.dst); - if (car != state2car.end()) - { - unsigned res_dst = car2num.at(car->second); - res_->new_edge(state, res_dst, edge.cond, { }); - } - } - } - } - unsigned initial_state = aut_->get_init_state_number(); - auto initial_car = state2car.find(initial_state); - auto initial_state_res = car2num.find(initial_car->second); - if (initial_state_res != car2num.end()) - res_->set_init_state(initial_state_res->second); - else - res_->new_state(); - res_->set_acceptance( - acc_cond::acc_code::parity_max(is_odd, SPOT_MAX_ACCSETS)); - if (options.pretty_print) - res_->set_named_prop("state-names", names); - reduce_parity_here(res_); - res_->purge_unreachable_states(); - return res_; -} - -private: -const const_twa_graph_ptr &aut_; -const scc_info scc_; -twa_graph_ptr res_; -bool is_odd; - -std::vector num2car; -std::map state2car; -std::map car2num; - -car_option options; - -std::vector* names; -}; // car_generator - -}// namespace - -twa_graph_ptr -remove_false_transitions(const twa_graph_ptr a) -{ - auto res_ = make_twa_graph(a->get_dict()); - res_->copy_ap_of(a); - for (unsigned state = 0; state < a->num_states(); ++state) - res_->new_state(); - for (unsigned state = 0; state < a->num_states(); ++state) - for (auto edge : a->out(state)) - if (edge.cond != bddfalse) - res_->new_edge(state, edge.dst, edge.cond, edge.acc); - res_->set_init_state(a->get_init_state_number()); - res_->set_acceptance(a->get_acceptance()); - return res_; -} - -twa_graph_ptr -to_parity(const twa_graph_ptr &aut, const car_option options) -{ - return car_generator(remove_false_transitions(aut), options).run(); -} -} \ No newline at end of file diff --git a/spot/twaalgos/car.hh b/spot/twaalgos/car.hh deleted file mode 100644 index de7598625..000000000 --- a/spot/twaalgos/car.hh +++ /dev/null @@ -1,69 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2012-2019 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#pragma once - -#include - -namespace spot -{ - struct car_option -{ - bool search_ex = true; - bool use_last = true; - bool force_order = true; - bool partial_degen = true; - bool acc_clean = true; - bool parity_equiv = true; - bool parity_prefix = true; - bool rabin_to_buchi = true; - bool reduce_col_deg = false; - bool propagate_col = true; - bool pretty_print = true; -}; - - - -/// \ingroup twa_acc_transform -/// \brief Take an automaton with any acceptance condition and return an -/// equivalent parity automaton. -/// -/// The parity condition of the returned automaton is max even or -/// max odd. -/// If \a search_ex is true, when we move several elements, we -/// try to find an order such that the new permutation already exists. -/// If \a partial_degen is true, we apply a partial degeneralization to remove -// occurences of Fin | Fin and Inf & Inf. -/// If \a scc_acc_clean is true, we remove for each SCC the colors that don't -// appear. -/// If \a parity_equiv is true, we check if there exists a permutations of -// colors such that the acceptance -/// condition is a partity condition. -/// If \a use_last is true, we use the most recent state when looking for an -// existing state. -/// If \a pretty_print is true, we give a name to the states describing the -// state of the aut_ and the permutation. - -SPOT_API twa_graph_ptr -remove_false_transitions(const twa_graph_ptr a); - -SPOT_API twa_graph_ptr -to_parity(const twa_graph_ptr &aut, const car_option options = car_option()); - -} // namespace spot \ No newline at end of file diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 6165ac834..ed35040cb 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -38,8 +38,8 @@ #include #include #include -#include #include +#include namespace spot { @@ -280,7 +280,7 @@ namespace spot twa_graph_ptr b = nullptr; if (want_parity && is_deterministic(a) && !a->acc().is_generalized_buchi()) - b = iar_maybe(a); + b = to_parity(a); // possible only if a was deterministic and (Rabin-like or Streett-like) // and we want parity and a is not a TGBA // NB: on a TGBA, degeneralization is better than IAR diff --git a/spot/twaalgos/rabin2parity.cc b/spot/twaalgos/rabin2parity.cc deleted file mode 100644 index 32cecb819..000000000 --- a/spot/twaalgos/rabin2parity.cc +++ /dev/null @@ -1,361 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement -// de l'Epita. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include "config.h" -#include -#include -#include - -namespace spot -{ - namespace - { - - using perm_t = std::vector; - struct iar_state - { - unsigned state; - perm_t perm; - - bool - operator<(const iar_state& other) const - { - return state == other.state ? perm < other.perm : state < other.state; - } - }; - - template - class iar_generator - { - // helper functions: access fin and inf parts of the pairs - // these functions negate the Streett condition to see it as a Rabin one - const acc_cond::mark_t& - fin(unsigned k) const - { - if (is_rabin) - return pairs_[k].fin; - else - return pairs_[k].inf; - } - acc_cond::mark_t - inf(unsigned k) const - { - if (is_rabin) - return pairs_[k].inf; - else - return pairs_[k].fin; - } - public: - explicit iar_generator(const const_twa_graph_ptr& a, - const std::vector& p, - const bool pretty_print) - : aut_(a) - , pairs_(p) - , scc_(scc_info(a)) - , pretty_print_(pretty_print) - , state2pos_iar_states(aut_->num_states(), -1U) - {} - - twa_graph_ptr - run() - { - res_ = make_twa_graph(aut_->get_dict()); - res_->copy_ap_of(aut_); - - build_iar_scc(scc_.initial()); - - { - // resulting automaton has acceptance condition: parity max odd - // for Rabin-like input and parity max even for Streett-like input. - // with priorities ranging from 0 to 2*(nb pairs) - // /!\ priorities are shifted by -1 compared to the original paper - unsigned sets = 2 * pairs_.size() + 1; - res_->set_acceptance(sets, acc_cond::acc_code::parity_max(is_rabin, - sets)); - } - { - unsigned s = iar2num.at(state2iar.at(aut_->get_init_state_number())); - res_->set_init_state(s); - } - - // there could be quite a number of unreachable states, prune them - res_->purge_unreachable_states(); - - if (pretty_print_) - { - unsigned nstates = res_->num_states(); - auto names = new std::vector(nstates); - for (auto e : res_->edges()) - { - unsigned s = e.src; - iar_state iar = num2iar.at(s); - std::ostringstream st; - st << iar.state << ' '; - if (iar.perm.empty()) - st << '['; - char sep = '['; - for (unsigned h: iar.perm) - { - st << sep << h; - sep = ','; - } - st << ']'; - (*names)[s] = st.str(); - } - res_->set_named_prop("state-names", names); - } - - return res_; - } - - void - build_iar_scc(unsigned scc_num) - { - // we are working on an SCC: the state we start from does not matter - unsigned init = scc_.one_state_of(scc_num); - - std::deque todo; - auto get_state = [&](const iar_state& s) - { - auto it = iar2num.find(s); - if (it == iar2num.end()) - { - unsigned nb = res_->new_state(); - iar2num[s] = nb; - num2iar[nb] = s; - unsigned iar_pos = iar_states.size(); - unsigned old_newest_pos = state2pos_iar_states[s.state]; - state2pos_iar_states[s.state] = iar_pos; - iar_states.push_back( - std::pair(s, old_newest_pos)); - todo.push_back(s); - return nb; - } - return it->second; - }; - - auto get_other_scc = [this](unsigned state) - { - auto it = state2iar.find(state); - // recursively build the destination SCC if we detect that it has - // not been already built. - if (it == state2iar.end()) - build_iar_scc(scc_.scc_of(state)); - return iar2num.at(state2iar.at(state)); - }; - - if (scc_.is_trivial(scc_num)) - { - iar_state iar_s{init, perm_t()}; - state2iar[init] = iar_s; - unsigned src_num = get_state(iar_s); - // Do not forget to connect to subsequent SCCs - for (const auto& e : aut_->out(init)) - res_->new_edge(src_num, get_other_scc(e.dst), e.cond); - return; - } - - // determine the pairs that appear in the SCC - auto colors = scc_.acc_sets_of(scc_num); - std::set scc_pairs; - for (unsigned k = 0; k != pairs_.size(); ++k) - if (!inf(k) || (colors & (pairs_[k].fin | pairs_[k].inf))) - scc_pairs.insert(k); - - perm_t p0; - for (unsigned k : scc_pairs) - p0.push_back(k); - - iar_state s0{init, p0}; - get_state(s0); // put s0 in todo - - // the main loop - while (!todo.empty()) - { - iar_state current = todo.front(); - todo.pop_front(); - - unsigned src_num = get_state(current); - - for (const auto& e : aut_->out(current.state)) - { - // connect to the appropriate state - if (scc_.scc_of(e.dst) != scc_num) - res_->new_edge(src_num, get_other_scc(e.dst), e.cond); - else - { - // find the new permutation - perm_t new_perm = current.perm; - // Count pairs whose fin-part is seen on this transition - unsigned seen_nb = 0; - // consider the pairs for this SCC only - for (unsigned k : scc_pairs) - if (e.acc & fin(k)) - { - ++seen_nb; - auto it = std::find(new_perm.begin(), - new_perm.end(), - k); - // move the pair in front of the permutation - std::rotate(new_perm.begin(), it, it+1); - } - - iar_state dst; - unsigned dst_num = -1U; - - // Optimization: when several indices are seen in the - // transition, they move at the front of new_perm in any - // order. Check whether there already exists an iar_state - // that matches this condition. - - auto iar_pos = state2pos_iar_states[e.dst]; - while (iar_pos != -1U) - { - iar_state& tmp = iar_states[iar_pos].first; - iar_pos = iar_states[iar_pos].second; - if (std::equal(new_perm.begin() + seen_nb, - new_perm.end(), - tmp.perm.begin() + seen_nb)) - { - dst = tmp; - dst_num = iar2num[dst]; - break; - } - } - // if such a state was not found, build it - if (dst_num == -1U) - { - dst = iar_state{e.dst, new_perm}; - dst_num = get_state(dst); - } - - // find the maximal index encountered by this transition - unsigned maxint = -1U; - for (int k = current.perm.size() - 1; k >= 0; --k) - { - unsigned pk = current.perm[k]; - if (!inf(pk) || - (e.acc & (pairs_[pk].fin | pairs_[pk].inf))) { - maxint = k; - break; - } - } - - acc_cond::mark_t acc = {}; - if (maxint == -1U) - acc = {0}; - else if (e.acc & fin(current.perm[maxint])) - acc = {2*maxint+2}; - else - acc = {2*maxint+1}; - - res_->new_edge(src_num, dst_num, e.cond, acc); - } - } - } - - // Optimization: find the bottom SCC of the sub-automaton we have just - // built. To that end, we have to ignore edges going out of scc_num. - auto leaving_edge = [&](unsigned d) - { - return scc_.scc_of(num2iar.at(d).state) != scc_num; - }; - auto filter_edge = [](const twa_graph::edge_storage_t&, - unsigned dst, - void* filter_data) - { - decltype(leaving_edge)* data = - static_cast(filter_data); - - if ((*data)(dst)) - return scc_info::edge_filter_choice::ignore; - return scc_info::edge_filter_choice::keep; - }; - scc_info sub_scc(res_, get_state(s0), filter_edge, &leaving_edge); - // SCCs are numbered in reverse topological order, so the bottom SCC has - // index 0. - const unsigned bscc = 0; - assert(sub_scc.succ(0).empty()); - assert( - [&]() - { - for (unsigned s = 1; s != sub_scc.scc_count(); ++s) - if (sub_scc.succ(s).empty()) - return false; - return true; - } ()); - - assert(sub_scc.states_of(bscc).size() - >= scc_.states_of(scc_num).size()); - - // update state2iar - for (unsigned scc_state : sub_scc.states_of(bscc)) - { - iar_state& iar = num2iar.at(scc_state); - if (state2iar.find(iar.state) == state2iar.end()) - state2iar[iar.state] = iar; - } - } - - private: - const const_twa_graph_ptr& aut_; - const std::vector& pairs_; - const scc_info scc_; - twa_graph_ptr res_; - bool pretty_print_; - - // to be used when entering a new SCC - // maps a state of aut_ onto an iar_state with the appropriate perm - std::map state2iar; - - std::map iar2num; - std::map num2iar; - - std::vector state2pos_iar_states; - std::vector> iar_states; - }; - } - - twa_graph_ptr - iar_maybe(const const_twa_graph_ptr& aut, bool pretty_print) - { - std::vector pairs; - if (!aut->acc().is_rabin_like(pairs)) - if (!aut->acc().is_streett_like(pairs)) - return nullptr; - else - { - iar_generator gen(aut, pairs, pretty_print); - return gen.run(); - } - else - { - iar_generator gen(aut, pairs, pretty_print); - return gen.run(); - } - } - - twa_graph_ptr - iar(const const_twa_graph_ptr& aut, bool pretty_print) - { - if (auto res = iar_maybe(aut, pretty_print)) - return res; - throw std::runtime_error("iar() expects Rabin-like or Streett-like input"); - } -} diff --git a/spot/twaalgos/rabin2parity.hh b/spot/twaalgos/rabin2parity.hh deleted file mode 100644 index 36c6c6d98..000000000 --- a/spot/twaalgos/rabin2parity.hh +++ /dev/null @@ -1,55 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement de l'Epita. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#pragma once - -#include - -namespace spot -{ - /// \ingroup twa_acc_transform - /// \brief Turn a Rabin-like or Streett-like automaton into a parity automaton - /// based on the index appearence record (IAR) - /// - /// If the input automaton has n states and k pairs, the output automaton has - /// at most k!*n states and 2k+1 colors. If the input automaton is - /// deterministic, the output automaton is deterministic as well, which is the - /// intended use case for this function. If the input automaton is - /// non-deterministic, the result is still correct, but way larger than an - /// equivalent Büchi automaton. - /// If the input automaton is Rabin-like (resp. Streett-like), the output - /// automaton has max odd (resp. min even) acceptance condition. - /// Details on the algorithm can be found in: - /// https://arxiv.org/pdf/1701.05738.pdf (published at TACAS 2017) - /// - /// Throws an std::runtime_error if the input is neither Rabin-like nor - /// Street-like. - SPOT_API - twa_graph_ptr - iar(const const_twa_graph_ptr& aut, bool pretty_print = false); - - /// \ingroup twa_acc_transform - /// \brief Turn a Rabin-like or Streett-like automaton into a parity automaton - /// based on the index appearence record (IAR) - /// - /// Returns nullptr if the input automaton is neither Rabin-like nor - /// Streett-like, and calls spot::iar() otherwise. - SPOT_API - twa_graph_ptr - iar_maybe(const const_twa_graph_ptr& aut, bool pretty_print = false); -} diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc index 51046fadd..12f152819 100644 --- a/spot/twaalgos/toparity.cc +++ b/spot/twaalgos/toparity.cc @@ -22,13 +22,1619 @@ #include #include -#include -#include -#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include namespace spot { +// Old version of IAR. +namespace + { + + using perm_t = std::vector; + struct iar_state + { + unsigned state; + perm_t perm; + + bool + operator<(const iar_state& other) const + { + return state == other.state ? perm < other.perm : state < other.state; + } + }; + + template + class iar_generator + { + // helper functions: access fin and inf parts of the pairs + // these functions negate the Streett condition to see it as a Rabin one + const acc_cond::mark_t& + fin(unsigned k) const + { + if (is_rabin) + return pairs_[k].fin; + else + return pairs_[k].inf; + } + acc_cond::mark_t + inf(unsigned k) const + { + if (is_rabin) + return pairs_[k].inf; + else + return pairs_[k].fin; + } + public: + explicit iar_generator(const const_twa_graph_ptr& a, + const std::vector& p, + const bool pretty_print) + : aut_(a) + , pairs_(p) + , scc_(scc_info(a)) + , pretty_print_(pretty_print) + , state2pos_iar_states(aut_->num_states(), -1U) + {} + + twa_graph_ptr + run() + { + res_ = make_twa_graph(aut_->get_dict()); + res_->copy_ap_of(aut_); + + build_iar_scc(scc_.initial()); + + { + // resulting automaton has acceptance condition: parity max odd + // for Rabin-like input and parity max even for Streett-like input. + // with priorities ranging from 0 to 2*(nb pairs) + // /!\ priorities are shifted by -1 compared to the original paper + unsigned sets = 2 * pairs_.size() + 1; + res_->set_acceptance(sets, acc_cond::acc_code::parity_max(is_rabin, + sets)); + } + { + unsigned s = iar2num.at(state2iar.at(aut_->get_init_state_number())); + res_->set_init_state(s); + } + + // there could be quite a number of unreachable states, prune them + res_->purge_unreachable_states(); + + if (pretty_print_) + { + unsigned nstates = res_->num_states(); + auto names = new std::vector(nstates); + for (auto e : res_->edges()) + { + unsigned s = e.src; + iar_state iar = num2iar.at(s); + std::ostringstream st; + st << iar.state << ' '; + if (iar.perm.empty()) + st << '['; + char sep = '['; + for (unsigned h: iar.perm) + { + st << sep << h; + sep = ','; + } + st << ']'; + (*names)[s] = st.str(); + } + res_->set_named_prop("state-names", names); + } + + return res_; + } + + void + build_iar_scc(unsigned scc_num) + { + // we are working on an SCC: the state we start from does not matter + unsigned init = scc_.one_state_of(scc_num); + + std::deque todo; + auto get_state = [&](const iar_state& s) + { + auto it = iar2num.find(s); + if (it == iar2num.end()) + { + unsigned nb = res_->new_state(); + iar2num[s] = nb; + num2iar[nb] = s; + unsigned iar_pos = iar_states.size(); + unsigned old_newest_pos = state2pos_iar_states[s.state]; + state2pos_iar_states[s.state] = iar_pos; + iar_states.push_back( + std::pair(s, old_newest_pos)); + todo.push_back(s); + return nb; + } + return it->second; + }; + + auto get_other_scc = [this](unsigned state) + { + auto it = state2iar.find(state); + // recursively build the destination SCC if we detect that it has + // not been already built. + if (it == state2iar.end()) + build_iar_scc(scc_.scc_of(state)); + return iar2num.at(state2iar.at(state)); + }; + + if (scc_.is_trivial(scc_num)) + { + iar_state iar_s{init, perm_t()}; + state2iar[init] = iar_s; + unsigned src_num = get_state(iar_s); + // Do not forget to connect to subsequent SCCs + for (const auto& e : aut_->out(init)) + res_->new_edge(src_num, get_other_scc(e.dst), e.cond); + return; + } + + // determine the pairs that appear in the SCC + auto colors = scc_.acc_sets_of(scc_num); + std::set scc_pairs; + for (unsigned k = 0; k != pairs_.size(); ++k) + if (!inf(k) || (colors & (pairs_[k].fin | pairs_[k].inf))) + scc_pairs.insert(k); + + perm_t p0; + for (unsigned k : scc_pairs) + p0.push_back(k); + + iar_state s0{init, p0}; + get_state(s0); // put s0 in todo + + // the main loop + while (!todo.empty()) + { + iar_state current = todo.front(); + todo.pop_front(); + + unsigned src_num = get_state(current); + + for (const auto& e : aut_->out(current.state)) + { + // connect to the appropriate state + if (scc_.scc_of(e.dst) != scc_num) + res_->new_edge(src_num, get_other_scc(e.dst), e.cond); + else + { + // find the new permutation + perm_t new_perm = current.perm; + // Count pairs whose fin-part is seen on this transition + unsigned seen_nb = 0; + // consider the pairs for this SCC only + for (unsigned k : scc_pairs) + if (e.acc & fin(k)) + { + ++seen_nb; + auto it = std::find(new_perm.begin(), + new_perm.end(), + k); + // move the pair in front of the permutation + std::rotate(new_perm.begin(), it, it+1); + } + + iar_state dst; + unsigned dst_num = -1U; + + // Optimization: when several indices are seen in the + // transition, they move at the front of new_perm in any + // order. Check whether there already exists an iar_state + // that matches this condition. + + auto iar_pos = state2pos_iar_states[e.dst]; + while (iar_pos != -1U) + { + iar_state& tmp = iar_states[iar_pos].first; + iar_pos = iar_states[iar_pos].second; + if (std::equal(new_perm.begin() + seen_nb, + new_perm.end(), + tmp.perm.begin() + seen_nb)) + { + dst = tmp; + dst_num = iar2num[dst]; + break; + } + } + // if such a state was not found, build it + if (dst_num == -1U) + { + dst = iar_state{e.dst, new_perm}; + dst_num = get_state(dst); + } + + // find the maximal index encountered by this transition + unsigned maxint = -1U; + for (int k = current.perm.size() - 1; k >= 0; --k) + { + unsigned pk = current.perm[k]; + if (!inf(pk) || + (e.acc & (pairs_[pk].fin | pairs_[pk].inf))) { + maxint = k; + break; + } + } + + acc_cond::mark_t acc = {}; + if (maxint == -1U) + acc = {0}; + else if (e.acc & fin(current.perm[maxint])) + acc = {2*maxint+2}; + else + acc = {2*maxint+1}; + + res_->new_edge(src_num, dst_num, e.cond, acc); + } + } + } + + // Optimization: find the bottom SCC of the sub-automaton we have just + // built. To that end, we have to ignore edges going out of scc_num. + auto leaving_edge = [&](unsigned d) + { + return scc_.scc_of(num2iar.at(d).state) != scc_num; + }; + auto filter_edge = [](const twa_graph::edge_storage_t&, + unsigned dst, + void* filter_data) + { + decltype(leaving_edge)* data = + static_cast(filter_data); + + if ((*data)(dst)) + return scc_info::edge_filter_choice::ignore; + return scc_info::edge_filter_choice::keep; + }; + scc_info sub_scc(res_, get_state(s0), filter_edge, &leaving_edge); + // SCCs are numbered in reverse topological order, so the bottom SCC has + // index 0. + const unsigned bscc = 0; + assert(sub_scc.succ(0).empty()); + assert( + [&]() + { + for (unsigned s = 1; s != sub_scc.scc_count(); ++s) + if (sub_scc.succ(s).empty()) + return false; + return true; + } ()); + + assert(sub_scc.states_of(bscc).size() + >= scc_.states_of(scc_num).size()); + + // update state2iar + for (unsigned scc_state : sub_scc.states_of(bscc)) + { + iar_state& iar = num2iar.at(scc_state); + if (state2iar.find(iar.state) == state2iar.end()) + state2iar[iar.state] = iar; + } + } + + private: + const const_twa_graph_ptr& aut_; + const std::vector& pairs_; + const scc_info scc_; + twa_graph_ptr res_; + bool pretty_print_; + + // to be used when entering a new SCC + // maps a state of aut_ onto an iar_state with the appropriate perm + std::map state2iar; + + std::map iar2num; + std::map num2iar; + + std::vector state2pos_iar_states; + std::vector> iar_states; + }; + } + + twa_graph_ptr + iar_maybe_old(const const_twa_graph_ptr& aut, bool pretty_print) + { + std::vector pairs; + if (!aut->acc().is_rabin_like(pairs)) + if (!aut->acc().is_streett_like(pairs)) + return nullptr; + else + { + iar_generator gen(aut, pairs, pretty_print); + return gen.run(); + } + else + { + iar_generator gen(aut, pairs, pretty_print); + return gen.run(); + } + } + + twa_graph_ptr + iar_old(const const_twa_graph_ptr& aut, bool pretty_print) + { + if (auto res = iar_maybe_old(aut, pretty_print)) + return res; + throw std::runtime_error("iar() expects Rabin-like or Streett-like input"); + } + +// New version for paritizing +namespace +{ +struct node +{ + // A color of the permutation or a state. + unsigned label; + std::vector children; + // is_leaf is true if the label is a state of res_. + bool is_leaf; + + node() + : node(0, 0){ + } + + node(int label_, bool is_leaf_) + : label(label_) + , children(0) + , is_leaf(is_leaf_){ + } + + ~node() + { + for (auto c : children) + delete c; + } + + // Add a permutation to the tree. + void + add_new_perm(const std::vector& permu, int pos, unsigned state) + { + if (pos == -1) + children.push_back(new node(state, true)); + else + { + auto lab = permu[pos]; + auto child = std::find_if(children.begin(), children.end(), + [lab](node* n){ + return n->label == lab; + }); + if (child == children.end()) + { + node* new_child = new node(lab, false); + children.push_back(new_child); + new_child->add_new_perm(permu, pos - 1, state); + } + else + (*child)->add_new_perm(permu, pos - 1, state); + } + } + + // Gives a state of res_ (if it exists) reachable from this node. + // If use_last is true, we take the most recent, otherwise we take + // the oldest. + unsigned + get_end(bool use_last) + { + if (children.empty()) + { + if (!is_leaf) + return -1U; + return label; + } + if (use_last) + return children[children.size() - 1]->get_end(use_last); + return children[0]->get_end(use_last); + } + + // Try to find a state compatible with the permu when seen_nb colors are + // moved. + unsigned + get_existing(const std::vector& permu, unsigned seen_nb, int pos, + bool use_last) + { + if (pos < (int) seen_nb) + return get_end(use_last); + else + { + auto lab = permu[pos]; + auto child = std::find_if(children.begin(), children.end(), + [lab](node* n){ + return n->label == lab; + }); + if (child == children.end()) + return -1U; + return (*child)->get_existing(permu, seen_nb, pos - 1, use_last); + } + } +}; + +class state_2_car_scc +{ +std::vector nodes; + +public: +state_2_car_scc(unsigned nb_states) + : nodes(nb_states, node()){ +} + +unsigned +get_res_state(unsigned state, const std::vector& permu, + unsigned seen_nb, bool use_last) +{ + return nodes[state].get_existing(permu, seen_nb, + permu.size() - 1, use_last); +} + +void +add_res_state(unsigned initial, unsigned state, + const std::vector& permu) +{ + nodes[initial].add_new_perm(permu, ((int) permu.size()) - 1, state); +} +}; + +class car_generator +{ +enum algorithm { + // Try to have a Büchi condition if we have Rabin. + Rabin_to_Buchi, + Streett_to_Buchi, + // IAR + IAR_Streett, + IAR_Rabin, + // CAR + CAR, + // Changing colors transforms acceptance to max even/odd copy. + Copy_even, + Copy_odd, + // If a condition is "t" or "f", we just have to copy the automaton. + False_clean, + True_clean, + None +}; + + +static std::string +algorithm_to_str(algorithm algo) +{ + std::string algo_str; + switch (algo) + { + case IAR_Streett: + algo_str = "IAR (Streett)"; + break; + case IAR_Rabin: + algo_str = "IAR (Rabin)"; + break; + case CAR: + algo_str = "CAR"; + break; + case Copy_even: + algo_str = "Copy even"; + break; + case Copy_odd: + algo_str = "Copy odd"; + break; + case False_clean: + algo_str = "False clean"; + break; + case True_clean: + algo_str = "True clean"; + break; + case Streett_to_Buchi: + algo_str = "Streett to Büchi"; + break; + case Rabin_to_Buchi: + algo_str = "Rabin to Büchi"; + break; + default: + algo_str = "None"; + break; + } + return algo_str; +} + +using perm_t = std::vector; + +struct car_state +{ + // State of the original automaton + unsigned state; + // We create a new automaton for each SCC of the original automaton + // so we keep a link between a car_state and the state of the + // subautomaton. + unsigned state_scc; + // Permutation used by IAR and CAR. + perm_t perm; + + bool + operator<(const car_state &other) const + { + if (state < other.state) + return true; + if (state > other.state) + return false; + if (perm < other.perm) + return true; + if (perm > other.perm) + return false; + return state_scc < other.state_scc; + } + + std::string + to_string(algorithm algo) const + { + std::stringstream s; + s << state; + unsigned ps = perm.size(); + if (ps > 0) + { + s << " ["; + for (unsigned i = 0; i != ps; ++i) + { + if (i > 0) + s << ','; + s << perm[i]; + } + s << ']'; + } + s << ", "; + s << algorithm_to_str(algo); + return s.str(); + } +}; + +const acc_cond::mark_t & +fin(const std::vector& pairs, unsigned k, algorithm algo) +const +{ + if (algo == IAR_Rabin) + return pairs[k].fin; + else + return pairs[k].inf; +} + +acc_cond::mark_t +inf(const std::vector& pairs, unsigned k, algorithm algo) +const +{ + if (algo == IAR_Rabin) + return pairs[k].inf; + else + return pairs[k].fin; +} + +std::vector> +get_inputs_states(const twa_graph_ptr& aut) +{ + auto used = aut->acc().get_acceptance().used_sets(); + std::vector> inputs(aut->num_states()); + for (auto e : aut->edges()) + { + auto elements = e.acc & used; + if (elements.count() > 1) + inputs[e.dst].insert(elements); + } + return inputs; +} + +std::vector>> +get_inputs_iar(const twa_graph_ptr& aut, algorithm algo, + const std::set& perm_elem, + const std::vector& pairs) +{ + std::vector>> inputs(aut->num_states()); + for (auto e : aut->edges()) + { + auto acc = e.acc; + std::vector new_vect; + for (unsigned k : perm_elem) + if (acc & fin(pairs, k, algo)) + new_vect.push_back(k); + std::sort(std::begin(new_vect), std::end(new_vect)); + inputs[e.dst].insert(new_vect); + } + return inputs; +} + +std::vector +group_to_vector(const std::set& group) +{ + std::vector group_vect(group.begin(), group.end()); + + std::sort(group_vect.begin(), group_vect.end(), + [](const acc_cond::mark_t left, const acc_cond::mark_t right) + { + return (left & right) == left; + }); + std::vector result; + for (auto mark : group_vect) + { + for (unsigned col : mark.sets()) + if (std::find(result.begin(), result.end(), col) == result.end()) + result.push_back(col); + } + return result; +} + +std::vector +group_to_vector_iar(const std::set>& group) +{ + std::vector> group_vect(group.begin(), group.end()); + for (auto& vec : group_vect) + std::sort(std::begin(vec), std::end(vec)); + std::sort(group_vect.begin(), group_vect.end(), + [](const std::vector left, + const std::vector right) + { + return std::includes(right.begin(), right.end(), + left.begin(), left.end()); + }); + std::vector result; + for (auto vec : group_vect) + for (unsigned col : vec) + if (std::find(result.begin(), result.end(), col) == result.end()) + result.push_back(col); + return result; +} + +// Créé les groupes à partir d'un ensemble de mark_t +std::map> +get_groups(const std::set& marks_input) +{ + std::map> result; + + std::vector> groups; + // Pour toutes les mark_t à traiter + for (acc_cond::mark_t mark : marks_input) + { + // added teste si la mark peut être ajoutée à un group déjà + // existant. + bool added = false; + for (unsigned group = 0; group < groups.size(); ++group) + { + if (std::all_of(groups[group].begin(), groups[group].end(), + [mark](acc_cond::mark_t element) + { + return ((element | mark) == mark) + || ((element | mark) == element); + })) + { + groups[group].insert(mark); + added = true; + break; + } + } + if (!added) + groups.push_back({mark}); + } + for (auto& group : groups) + { + auto new_vector = group_to_vector(group); + for (auto mark : group) + result.insert(std::pair>( + mark, new_vector)); + } + return result; +} + +std::map, std::vector> +get_groups_iar(const std::set>& marks_input) +{ + std::map, std::vector> result; + + std::vector>> groups; + for (auto vect : marks_input) + { + bool added = false; + for (unsigned group = 0; group < groups.size(); ++group) + if (std::all_of(groups[group].begin(), groups[group].end(), + [vect](std::vector element) + { + return std::includes(vect.begin(), vect.end(), + element.begin(), element.end()) + || std::includes(element.begin(), element.end(), + vect.begin(), vect.end()); + })) + { + groups[group].insert(vect); + added = true; + break; + } + if (!added) + groups.push_back({vect}); + } + for (auto& group : groups) + { + auto new_vector = group_to_vector_iar(group); + for (auto vect : group) + result.insert( + std::pair, std::vector>( + vect, new_vector)); + } + return result; +} + +// Donne pour chaque état l'ensemble des combinaisons entre mark et vector +std::vector>> +get_mark_to_vector(const twa_graph_ptr& aut) +{ + std::vector>> result; + auto inputs = get_inputs_states(aut); + for (unsigned state = 0; state < inputs.size(); ++state) + { + std::map> state_map; + auto map = get_groups(inputs[state]); + result.push_back(map); + } + return result; +} + +std::vector, std::vector>> +get_iar_to_vector(const twa_graph_ptr& aut, algorithm algo, + const std::set& perm_elem, + const std::vector& pairs) +{ + std::vector, std::vector>> result; + auto inputs = get_inputs_iar(aut, algo, perm_elem, pairs); + for (unsigned state = 0; state < inputs.size(); ++state) + { + std::map, std::vector> state_map; + auto map = get_groups_iar(inputs[state]); + result.push_back(map); + } + return result; +} + +public: +explicit car_generator(const const_twa_graph_ptr &a, car_option options) + : aut_(a) + , scc_(scc_info(a)) + , is_odd(false) + , options(options) +{ + if (options.pretty_print) + names = new std::vector(); + else + names = nullptr; +} + +unsigned +apply_false_true_clean(const twa_graph_ptr &sub_automaton, bool is_true, + const std::vector& inf_fin_prefix, + unsigned max_free_color, + std::map& state2car_local, + std::map& car2num_local) +{ + std::vector* init_states = sub_automaton-> + get_named_prop>("original-states"); + + for (unsigned state = 0; state < sub_automaton->num_states(); ++state) + { + unsigned s_aut = (*init_states)[state]; + + car_state new_car = { s_aut, state, perm_t() }; + auto new_state = res_->new_state(); + car2num_local[new_car] = new_state; + num2car.insert(num2car.begin() + new_state, new_car); + if (options.pretty_print) + names->push_back( + new_car.to_string(is_true ? True_clean : False_clean)); + state2car_local[s_aut] = new_car; + } + for (unsigned state = 0; state < sub_automaton->num_states(); ++state) + { + auto col = is_true ^ !is_odd; + if (((unsigned) col) > max_free_color) + throw std::runtime_error("CAR needs more sets"); + unsigned s_aut = (*init_states)[state]; + car_state src = { s_aut, state, perm_t() }; + unsigned src_state = car2num_local[src]; + for (auto e : aut_->out(s_aut)) + { + if (scc_.scc_of(s_aut) == scc_.scc_of(e.dst)) + { + for (auto c : e.acc.sets()) + if (inf_fin_prefix[c] + is_odd > col) + col = inf_fin_prefix[c] + is_odd; + acc_cond::mark_t cond = { (unsigned) col }; + res_->new_edge( + src_state, car2num_local[state2car_local[e.dst]], + e.cond, cond); + } + } + } + return sub_automaton->num_states(); +} + +unsigned +apply_copy(const twa_graph_ptr &sub_automaton, + const std::vector &permut, + bool copy_odd, + const std::vector& inf_fin_prefix, + std::map& state2car_local, + std::map& car2num_local) +{ + std::vector* init_states = sub_automaton + ->get_named_prop>("original-states"); + for (unsigned state = 0; state < sub_automaton->num_states(); ++state) + { + car_state new_car = { (*init_states)[state], state, perm_t() }; + auto new_state = res_->new_state(); + car2num_local[new_car] = new_state; + num2car.insert(num2car.begin() + new_state, new_car); + state2car_local[(*init_states)[state]] = new_car; + if (options.pretty_print) + names->push_back( + new_car.to_string(copy_odd ? Copy_odd : Copy_even)); + } + auto cond_col = sub_automaton->acc().get_acceptance().used_sets(); + for (unsigned s = 0; s < sub_automaton->num_states(); ++s) + { + for (auto e : sub_automaton->out(s)) + { + acc_cond::mark_t mark = { }; + int max_edge = -1; + for (auto col : e.acc.sets()) + { + if (cond_col.has(col)) + max_edge = std::max(max_edge, (int) permut[col]); + if (inf_fin_prefix[col] + (is_odd || copy_odd) > max_edge) + max_edge = inf_fin_prefix[col] + (is_odd || copy_odd); + } + if (max_edge != -1) + mark.set((unsigned) max_edge); + car_state src = { (*init_states)[s], s, perm_t() }, + dst = { (*init_states)[e.dst], e.dst, perm_t() }; + unsigned src_state = car2num_local[src], + dst_state = car2num_local[dst]; + res_->new_edge(src_state, dst_state, e.cond, mark); + } + } + return sub_automaton->num_states(); +} + +unsigned +apply_to_Buchi(const twa_graph_ptr& sub_automaton, + const twa_graph_ptr& buchi, + bool is_streett_to_buchi, + const std::vector& inf_fin_prefix, + unsigned max_free_color, + std::map& state2car_local, + std::map&car2num_local) +{ + std::vector* init_states = sub_automaton + ->get_named_prop>("original-states"); + + for (unsigned state = 0; state < buchi->num_states(); ++state) + { + car_state new_car = { (*init_states)[state], state, perm_t() }; + auto new_state = res_->new_state(); + car2num_local[new_car] = new_state; + num2car.insert(num2car.begin() + new_state, new_car); + state2car_local[(*init_states)[state]] = new_car; + if (options.pretty_print) + names->push_back(new_car.to_string( + is_streett_to_buchi ? Streett_to_Buchi : Rabin_to_Buchi)); + } + auto g = buchi->get_graph(); + for (unsigned s = 0; s < buchi->num_states(); ++s) + { + unsigned b = g.state_storage(s).succ; + while (b) + { + auto& e = g.edge_storage(b); + auto acc = e.acc; + acc <<= (is_odd + is_streett_to_buchi); + if ((is_odd || is_streett_to_buchi) && acc == acc_cond::mark_t{ }) + acc = { (unsigned) (is_streett_to_buchi && is_odd) }; + car_state src = { (*init_states)[s], s, perm_t() }, + dst = { (*init_states)[e.dst], e.dst, perm_t() }; + unsigned src_state = car2num_local[src], + dst_state = car2num_local[dst]; + int col = ((int) acc.max_set()) - 1; + if (col > (int) max_free_color) + throw std::runtime_error("CAR needs more sets"); + auto& e2 = sub_automaton->get_graph().edge_storage(b); + for (auto c : e2.acc.sets()) + { + if (inf_fin_prefix[c] + is_odd > col) + col = inf_fin_prefix[c] + is_odd; + } + if (col != -1) + acc = { (unsigned) col }; + else + acc = {}; + res_->new_edge(src_state, dst_state, e.cond, acc); + b = e.next_succ; + } + } + return buchi->num_states(); +} + +void +initial_perm_iar(std::set &perm_elem, perm_t &p0, + algorithm algo, const acc_cond::mark_t &colors, + const std::vector &pairs) +{ + for (unsigned k = 0; k != pairs.size(); ++k) + if (!inf(pairs, k, algo) || (colors & (pairs[k].fin | pairs[k].inf))) + { + perm_elem.insert(k); + p0.push_back(k); + } +} + +// Create a permutation for the first state of a SCC (CAR) +void +initial_perm_car(perm_t &p0, const acc_cond::mark_t &colors) +{ + auto cont = colors.sets(); + p0.assign(cont.begin(), cont.end()); +} + +void +find_new_perm_iar(perm_t &new_perm, + const std::vector &pairs, + const acc_cond::mark_t &acc, + algorithm algo, const std::set &perm_elem, + unsigned &seen_nb) +{ + for (unsigned k : perm_elem) + if (acc & fin(pairs, k, algo)) + { + ++seen_nb; + auto it = std::find(new_perm.begin(), new_perm.end(), k); + + // move the pair in front of the permutation + std::rotate(new_perm.begin(), it, it + 1); + } +} + +// Given the set acc of colors appearing on an edge, create a new +// permutation new_perm, and give the number seen_nb of colors moved to +// the head of the permutation. +void +find_new_perm_car(perm_t &new_perm, const acc_cond::mark_t &acc, + unsigned &seen_nb, unsigned &h) +{ + for (unsigned k : acc.sets()) + { + auto it = std::find(new_perm.begin(), new_perm.end(), k); + if (it != new_perm.end()) + { + h = std::max(h, unsigned(it - new_perm.begin()) + 1); + std::rotate(new_perm.begin(), it, it + 1); + ++seen_nb; + } + } +} + +void +get_acceptance_iar(algorithm algo, const perm_t ¤t_perm, + const std::vector &pairs, + const acc_cond::mark_t &e_acc, acc_cond::mark_t &acc) +{ + unsigned delta_acc = (algo == IAR_Streett) && is_odd; + + // find the maximal index encountered by this transition + unsigned maxint = -1U; + + for (int k = current_perm.size() - 1; k >= 0; --k) + { + unsigned pk = current_perm[k]; + + if (!inf(pairs, pk, + algo) + || (e_acc & (pairs[pk].fin | pairs[pk].inf))) + { + maxint = k; + break; + } + } + unsigned value; + + if (maxint == -1U) + value = delta_acc; + else if (e_acc & fin(pairs, current_perm[maxint], algo)) + value = 2 * maxint + 2 + delta_acc; + else + value = 2 * maxint + 1 + delta_acc; + acc = { value }; +} + +void +get_acceptance_car(const acc_cond &sub_aut_cond, const perm_t &new_perm, + unsigned h, acc_cond::mark_t &acc) +{ + acc_cond::mark_t m(new_perm.begin(), new_perm.begin() + h); + bool rej = !sub_aut_cond.accepting(m); + unsigned value = 2 * h + rej + is_odd; + acc = { value }; +} + +unsigned +apply_lar(const twa_graph_ptr &sub_automaton, + unsigned init, std::vector &pairs, + algorithm algo, unsigned scc_num, + const std::vector& inf_fin_prefix, + unsigned max_free_color, + std::map& state2car_local, + std::map& car2num_local, + unsigned max_states) +{ + auto maps = get_mark_to_vector(sub_automaton); + unsigned nb_created_states = 0; + auto state_2_car = state_2_car_scc(sub_automaton->num_states()); + std::vector* init_states = sub_automaton-> + get_named_prop>("original-states"); + std::deque todo; + auto get_state = + [&](const car_state &s){ + auto it = car2num_local.find(s); + + if (it == car2num_local.end()) + { + ++nb_created_states; + unsigned nb = res_->new_state(); + if (options.search_ex) + state_2_car.add_res_state(s.state_scc, nb, s.perm); + car2num_local[s] = nb; + num2car.insert(num2car.begin() + nb, s); + + todo.push_back(s); + if (options.pretty_print) + names->push_back(s.to_string(algo)); + return nb; + } + return it->second; + }; + + auto colors = sub_automaton->acc().get_acceptance().used_sets(); + std::set perm_elem; + + perm_t p0 = { }; + switch (algo) + { + case IAR_Streett: + case IAR_Rabin: + initial_perm_iar(perm_elem, p0, algo, colors, pairs); + break; + case CAR: + initial_perm_car(p0, colors); + break; + default: + assert(false); + break; + } + + std::vector, std::vector>> + iar_maps; + if (algo == IAR_Streett || algo == IAR_Rabin) + iar_maps = get_iar_to_vector(sub_automaton, algo, perm_elem, pairs); + + car_state s0{ (*init_states)[init], init, p0 }; + get_state(s0); // put s0 in todo + + // the main loop + while (!todo.empty()) + { + car_state current = todo.front(); + todo.pop_front(); + + unsigned src_num = get_state(current); + for (const auto &e : sub_automaton->out(current.state_scc)) + { + perm_t new_perm = current.perm; + + // Count pairs whose fin-part is seen on this transition + unsigned seen_nb = 0; + + // consider the pairs for this SCC only + unsigned h = 0; + + switch (algo) + { + case IAR_Rabin: + case IAR_Streett: + find_new_perm_iar(new_perm, pairs, e.acc, algo, + perm_elem, seen_nb); + break; + case CAR: + find_new_perm_car(new_perm, e.acc, seen_nb, h); + break; + default: + assert(false); + } + + if (options.force_order) + { + if (algo == CAR && seen_nb > 1) + { + auto map = maps[e.dst]; + acc_cond::mark_t first_vals( + new_perm.begin(), new_perm.begin() + seen_nb); + auto new_start = map.find(first_vals); + assert(new_start->second.size() >= seen_nb); + assert(new_start != map.end()); + for (unsigned i = 0; i < seen_nb; ++i) + new_perm[i] = new_start->second[i]; + } + else if ((algo == IAR_Streett || algo == IAR_Rabin) + && seen_nb > 1) + { + auto map = iar_maps[e.dst]; + std::vector first_vals( + new_perm.begin(), new_perm.begin() + seen_nb); + std::sort(std::begin(first_vals), std::end(first_vals)); + auto new_start = map.find(first_vals); + assert(new_start->second.size() >= seen_nb); + assert(new_start != map.end()); + for (unsigned i = 0; i < seen_nb; ++i) + new_perm[i] = new_start->second[i]; + } + } + + // Optimization: when several indices are seen in the + // transition, they move at the front of new_perm in any + // order. Check whether there already exists an car_state + // that matches this condition. + car_state dst; + unsigned dst_num = -1U; + + if (options.search_ex) + dst_num = state_2_car.get_res_state(e.dst, new_perm, seen_nb, + options.use_last); + + if (dst_num == -1U) + { + auto dst = car_state{ (*init_states)[e.dst], e.dst, new_perm }; + dst_num = get_state(dst); + if (nb_created_states > max_states) + return -1U; + } + + acc_cond::mark_t acc = { }; + + switch (algo) + { + case IAR_Rabin: + case IAR_Streett: + get_acceptance_iar(algo, current.perm, pairs, e.acc, acc); + break; + case CAR: + get_acceptance_car(sub_automaton->acc(), new_perm, h, acc); + break; + default: + assert(false); + } + + unsigned acc_col = acc.min_set() - 1; + if (options.parity_prefix) + { + if (acc_col > max_free_color) + throw std::runtime_error("CAR needs more sets"); + // parity prefix + for (auto col : e.acc.sets()) + { + if (inf_fin_prefix[col] + is_odd > (int) acc_col) + acc_col = (unsigned) inf_fin_prefix[col] + is_odd; + } + } + res_->new_edge(src_num, dst_num, e.cond, { acc_col }); + } + } + auto leaving_edge = + [&](unsigned d){ + return scc_.scc_of(num2car.at(d).state) != scc_num; + }; + auto filter_edge = + [](const twa_graph::edge_storage_t &, + unsigned dst, + void* filter_data){ + decltype(leaving_edge) *data = + static_cast(filter_data); + + if ((*data)(dst)) + return scc_info::edge_filter_choice::ignore; + + return scc_info::edge_filter_choice::keep; + }; + scc_info sub_scc(res_, get_state(s0), filter_edge, &leaving_edge); + + // SCCs are numbered in reverse topological order, so the bottom SCC has + // index 0. + const unsigned bscc = 0; + assert(sub_scc.scc_count() != 0); + assert(sub_scc.succ(0).empty()); + assert( + [&](){ + for (unsigned s = 1; s != sub_scc.scc_count(); ++s) + if (sub_scc.succ(s).empty()) + return false; + + return true; + } ()); + + assert(sub_scc.states_of(bscc).size() >= sub_automaton->num_states()); + + // update state2car + for (unsigned scc_state : sub_scc.states_of(bscc)) + { + car_state &car = num2car.at(scc_state); + + if (state2car_local.find(car.state) == state2car_local.end()) + state2car_local[car.state] = car; + } + return sub_scc.states_of(bscc).size(); +} + +algorithm +chooseAlgo(twa_graph_ptr &sub_automaton, + twa_graph_ptr &rabin_aut, + std::vector &pairs, + std::vector &permut) +{ + auto scc_condition = sub_automaton->acc(); + if (options.parity_equiv) + { + if (scc_condition.is_f()) + return False_clean; + if (scc_condition.is_t()) + return True_clean; + std::vector permut_tmp(scc_condition.all_sets().max_set(), -1); + + if (!is_odd && scc_condition.is_parity_max_equiv(permut_tmp, true)) + { + for (auto c : permut_tmp) + permut.push_back((unsigned) c); + + scc_condition.apply_permutation(permut); + sub_automaton->apply_permutation(permut); + return Copy_even; + } + std::fill(permut_tmp.begin(), permut_tmp.end(), -1); + if (scc_condition.is_parity_max_equiv(permut_tmp, false)) + { + for (auto c : permut_tmp) + permut.push_back((unsigned) c); + scc_condition.apply_permutation(permut); + sub_automaton->apply_permutation(permut); + return Copy_odd; + } + } + + if (options.rabin_to_buchi) + { + auto ra = rabin_to_buchi_if_realizable(sub_automaton); + if (ra != nullptr) + { + rabin_aut = ra; + return Rabin_to_Buchi; + } + else + { + bool streett_buchi = false; + auto sub_cond = sub_automaton->get_acceptance(); + sub_automaton->set_acceptance(sub_cond.complement()); + auto ra = rabin_to_buchi_if_realizable(sub_automaton); + streett_buchi = (ra != nullptr); + sub_automaton->set_acceptance(sub_cond); + if (streett_buchi) + { + rabin_aut = ra; + return Streett_to_Buchi; + } + } + } + + auto pairs1 = std::vector(); + auto pairs2 = std::vector(); + std::sort(pairs1.begin(), pairs1.end()); + pairs1.erase(std::unique(pairs1.begin(), pairs1.end()), pairs1.end()); + std::sort(pairs2.begin(), pairs2.end()); + pairs2.erase(std::unique(pairs2.begin(), pairs2.end()), pairs2.end()); + bool is_r_like = scc_condition.is_rabin_like(pairs1); + bool is_s_like = scc_condition.is_streett_like(pairs2); + unsigned num_cols = scc_condition.get_acceptance().used_sets().count(); + if (is_r_like) + { + if ((is_s_like && pairs1.size() < pairs2.size()) || !is_s_like) + { + if (pairs1.size() > num_cols) + return CAR; + pairs = pairs1; + return IAR_Rabin; + } + else if (is_s_like) + { + if (pairs2.size() > num_cols) + return CAR; + pairs = pairs2; + return IAR_Streett; + } + } + else + { + if (is_s_like) + { + if (pairs2.size() > num_cols) + return CAR; + pairs = pairs2; + return IAR_Streett; + } + } + return CAR; +} + +unsigned +build_scc(twa_graph_ptr &sub_automaton, + unsigned scc_num, + std::map& state2car_local, + std::map&car2num_local, + algorithm& algo, + unsigned max_states = -1U) +{ + + std::vector parity_prefix_colors (SPOT_MAX_ACCSETS, -1); + unsigned min_prefix_color = SPOT_MAX_ACCSETS + 1; + if (options.parity_prefix) + { + auto new_acc = sub_automaton->acc(); + auto colors = std::vector(); + bool inf_start = + sub_automaton->acc().has_parity_prefix(new_acc, colors); + sub_automaton->set_acceptance(new_acc); + for (unsigned i = 0; i < colors.size(); ++i) + parity_prefix_colors[colors[i]] = + SPOT_MAX_ACCSETS - 4 - i - !inf_start; + if (colors.size() > 0) + min_prefix_color = + SPOT_MAX_ACCSETS - 4 - colors.size() - 1 - !inf_start; + } + --min_prefix_color; + + unsigned init = 0; + + std::vector pairs = { }; + auto permut = std::vector(); + twa_graph_ptr rabin_aut = nullptr; + algo = chooseAlgo(sub_automaton, rabin_aut, pairs, permut); + switch (algo) + { + case False_clean: + case True_clean: + return apply_false_true_clean(sub_automaton, (algo == True_clean), + parity_prefix_colors, min_prefix_color, + state2car_local, car2num_local); + break; + case IAR_Streett: + case IAR_Rabin: + case CAR: + return apply_lar(sub_automaton, init, pairs, algo, scc_num, + parity_prefix_colors, min_prefix_color, + state2car_local, car2num_local, max_states); + break; + case Copy_odd: + case Copy_even: + return apply_copy(sub_automaton, permut, algo == Copy_odd, + parity_prefix_colors, state2car_local, + car2num_local); + break; + case Rabin_to_Buchi: + case Streett_to_Buchi: + return apply_to_Buchi(sub_automaton, rabin_aut, + (algo == Streett_to_Buchi), + parity_prefix_colors, min_prefix_color, + state2car_local, car2num_local); + break; + default: + break; + } + return -1U; +} + +public: +twa_graph_ptr +run() +{ + res_ = make_twa_graph(aut_->get_dict()); + res_->copy_ap_of(aut_); + for (unsigned scc = 0; scc < scc_.scc_count(); ++scc) + { + if (!scc_.is_useful_scc(scc)) + continue; + auto sub_automata = scc_.split_on_sets(scc, { }, true); + if (sub_automata.empty()) + { + for (auto state : scc_.states_of(scc)) + { + auto new_state = res_->new_state(); + car_state new_car = { state, state, perm_t() }; + car2num[new_car] = new_state; + num2car.insert(num2car.begin() + new_state, new_car); + if (options.pretty_print) + names->push_back(new_car.to_string(None)); + state2car[state] = new_car; + } + continue; + } + + auto sub_automaton = sub_automata[0]; + auto deg = sub_automaton; + if (options.acc_clean) + simplify_acceptance_here(sub_automaton); + bool has_degeneralized = false; + if (options.partial_degen) + { + std::vector forbid; + auto m = + is_partially_degeneralizable(sub_automaton, true, + true, forbid); + while (m != acc_cond::mark_t {}) + { + auto tmp = partial_degeneralize(deg, m); + simplify_acceptance_here(tmp); + if (tmp->get_acceptance().used_sets().count() + < deg->get_acceptance().used_sets().count() || + !(options.reduce_col_deg)) + { + deg = tmp; + has_degeneralized = true; + } + else + forbid.push_back(m); + m = is_partially_degeneralizable(deg, true, true, forbid); + } + } + + if (options.propagate_col) + { + propagate_marks_here(sub_automaton); + propagate_marks_here(deg); + } + + std::map state2car_sub, state2car_deg; + std::map car2num_sub, car2num_deg; + + unsigned nb_states_deg = -1U, + nb_states_sub = -1U; + + algorithm algo_sub, algo_deg; + unsigned max_states_sub_car = -1U; + + if (has_degeneralized) + { + nb_states_deg = + build_scc(deg, scc, state2car_deg, car2num_deg, algo_deg); + // We suppose that if we see nb_states_deg + 1000 states when + // when construct the version without degeneralization during the + // construction, we will not be able to have nb_states_deg after + // removing useless states. So we will stop the execution. + max_states_sub_car = + 10000 + nb_states_deg - 1; + } + nb_states_sub = + build_scc(sub_automaton, scc, state2car_sub, car2num_sub, + algo_sub, max_states_sub_car); + if (nb_states_deg < nb_states_sub) + { + state2car.insert(state2car_deg.begin(), state2car_deg.end()); + car2num.insert(car2num_deg.begin(), car2num_deg.end()); + algo_sub = algo_deg; + } + else + { + state2car.insert(state2car_sub.begin(), state2car_sub.end()); + car2num.insert(car2num_sub.begin(), car2num_sub.end()); + } + if ((algo_sub == IAR_Rabin || algo_sub == Copy_odd) && !is_odd) + { + is_odd = true; + for (auto &edge : res_->edges()) + { + if (scc_.scc_of(num2car[edge.src].state) != scc + && scc_.scc_of(num2car[edge.dst].state) != scc) + { + if (edge.acc == acc_cond::mark_t{}) + edge.acc = { 0 }; + else + edge.acc <<= 1; + } + } + } + } + + for (unsigned state = 0; state < res_->num_states(); ++state) + { + unsigned original_state = num2car.at(state).state; + auto state_scc = scc_.scc_of(original_state); + for (auto edge : aut_->out(original_state)) + { + if (scc_.scc_of(edge.dst) != state_scc) + { + auto car = state2car.find(edge.dst); + if (car != state2car.end()) + { + unsigned res_dst = car2num.at(car->second); + res_->new_edge(state, res_dst, edge.cond, { }); + } + } + } + } + unsigned initial_state = aut_->get_init_state_number(); + auto initial_car = state2car.find(initial_state); + auto initial_state_res = car2num.find(initial_car->second); + if (initial_state_res != car2num.end()) + res_->set_init_state(initial_state_res->second); + else + res_->new_state(); + res_->set_acceptance( + acc_cond::acc_code::parity_max(is_odd, SPOT_MAX_ACCSETS)); + if (options.pretty_print) + res_->set_named_prop("state-names", names); + reduce_parity_here(res_); + res_->purge_unreachable_states(); + return res_; +} + +private: +const const_twa_graph_ptr &aut_; +const scc_info scc_; +twa_graph_ptr res_; +bool is_odd; + +std::vector num2car; +std::map state2car; +std::map car2num; + +car_option options; + +std::vector* names; +}; // car_generator + +}// namespace + +twa_graph_ptr +remove_false_transitions(const twa_graph_ptr a) +{ + auto res_ = make_twa_graph(a->get_dict()); + res_->copy_ap_of(a); + for (unsigned state = 0; state < a->num_states(); ++state) + res_->new_state(); + for (unsigned state = 0; state < a->num_states(); ++state) + for (auto edge : a->out(state)) + if (edge.cond != bddfalse) + res_->new_edge(state, edge.dst, edge.cond, edge.acc); + res_->set_init_state(a->get_init_state_number()); + res_->set_acceptance(a->get_acceptance()); + return res_; +} + +twa_graph_ptr +to_parity(const twa_graph_ptr &aut, const car_option options) +{ + return car_generator(remove_false_transitions(aut), options).run(); +} + + // Old version of CAR. namespace { struct lar_state @@ -154,7 +1760,7 @@ namespace spot } twa_graph_ptr - to_parity(const const_twa_graph_ptr& aut, bool pretty_print) + to_parity_old(const const_twa_graph_ptr& aut, bool pretty_print) { if (!aut->is_existential()) throw std::runtime_error("LAR does not handle alternation"); diff --git a/spot/twaalgos/toparity.hh b/spot/twaalgos/toparity.hh index c9c22985f..e9ad49907 100644 --- a/spot/twaalgos/toparity.hh +++ b/spot/twaalgos/toparity.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2018 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -23,11 +23,91 @@ namespace spot { + // The version that combines CAR, IAR and multiple optimizations. + struct car_option +{ + bool search_ex = true; + bool use_last = true; + bool force_order = true; + bool partial_degen = true; + bool acc_clean = true; + bool parity_equiv = true; + bool parity_prefix = true; + bool rabin_to_buchi = true; + bool reduce_col_deg = false; + bool propagate_col = true; + bool pretty_print = false; +}; + + + +/// \ingroup twa_acc_transform +/// \brief Take an automaton with any acceptance condition and return an +/// equivalent parity automaton. +/// +/// The parity condition of the returned automaton is max even or +/// max odd. +/// If \a search_ex is true, when we move several elements, we +/// try to find an order such that the new permutation already exists. +/// If \a partial_degen is true, we apply a partial degeneralization to remove +// occurences of Fin | Fin and Inf & Inf. +/// If \a scc_acc_clean is true, we remove for each SCC the colors that don't +// appear. +/// If \a parity_equiv is true, we check if there exists a permutations of +// colors such that the acceptance +/// condition is a partity condition. +/// If \a use_last is true, we use the most recent state when looking for an +// existing state. +/// If \a pretty_print is true, we give a name to the states describing the +// state of the aut_ and the permutation. + + SPOT_API twa_graph_ptr + remove_false_transitions(const twa_graph_ptr a); + + SPOT_API twa_graph_ptr + to_parity(const twa_graph_ptr &aut, const car_option options = car_option()); + + + // Old version of CAR + /// \ingroup twa_acc_transform /// \brief Take an automaton with any acceptance condition and return an /// equivalent parity automaton. /// /// The parity condition of the returned automaton is max even. SPOT_API twa_graph_ptr - to_parity(const const_twa_graph_ptr& aut, bool pretty_print=false); -} + to_parity_old(const const_twa_graph_ptr& aut, bool pretty_print=false); + + // Old version of IAR + /// \ingroup twa_acc_transform + /// \brief Turn a Rabin-like or Streett-like automaton into a parity automaton + /// based on the index appearence record (IAR) + /// + /// If the input automaton has n states and k pairs, the output automaton has + /// at most k!*n states and 2k+1 colors. If the input automaton is + /// deterministic, the output automaton is deterministic as well, which is the + /// intended use case for this function. If the input automaton is + /// non-deterministic, the result is still correct, but way larger than an + /// equivalent Büchi automaton. + /// If the input automaton is Rabin-like (resp. Streett-like), the output + /// automaton has max odd (resp. min even) acceptance condition. + /// Details on the algorithm can be found in: + /// https://arxiv.org/pdf/1701.05738.pdf (published at TACAS 2017) + /// + /// Throws an std::runtime_error if the input is neither Rabin-like nor + /// Street-like. + SPOT_API + twa_graph_ptr + iar_old(const const_twa_graph_ptr& aut, bool pretty_print = false); + + /// \ingroup twa_acc_transform + /// \brief Turn a Rabin-like or Streett-like automaton into a parity automaton + /// based on the index appearence record (IAR) + /// + /// Returns nullptr if the input automaton is neither Rabin-like nor + /// Streett-like, and calls spot::iar() otherwise. + SPOT_API + twa_graph_ptr + iar_maybe_old(const const_twa_graph_ptr& aut, bool pretty_print = false); + +} // namespace spot \ No newline at end of file diff --git a/tests/Makefile.am b/tests/Makefile.am index d05a08035..58c140e41 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -373,7 +373,6 @@ TESTS_python = \ python/bdditer.py \ python/bddnqueen.py \ python/bugdet.py \ - python/car.py \ python/complement_semidet.py \ python/declenv.py \ python/decompose_scc.py \ diff --git a/tests/python/car.py b/tests/python/car.py deleted file mode 100644 index 376ee8a01..000000000 --- a/tests/python/car.py +++ /dev/null @@ -1,304 +0,0 @@ -#!/usr/bin/python3 -# -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2018, 2019 Laboratoire de Recherche et Développement de -# l'EPITA. -# -# This file is part of Spot, a model checking library. -# -# Spot is free software; you can redistribute it and/or modify it -# under the terms of the GNU General Public License as published by -# the Free Software Foundation; either version 3 of the License, or -# (at your option) any later version. -# -# Spot is distributed in the hope that it will be useful, but WITHOUT -# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -# License for more details. -# -# You should have received a copy of the GNU General Public License -# along with this program. If not, see . - -import spot - -no_option = spot.car_option() -no_option.search_ex = False -no_option.use_last = False -no_option.force_order = False -no_option.partial_degen = False -no_option.acc_clean = False -no_option.parity_equiv = False -no_option.parity_prefix = False -no_option.rabin_to_buchi = False -no_option.propagate_col = False - -acc_clean_search_opt = spot.car_option() -acc_clean_search_opt.force_order = False -acc_clean_search_opt.partial_degen = False -acc_clean_search_opt.parity_equiv = False -acc_clean_search_opt.parity_prefix = False -acc_clean_search_opt.rabin_to_buchi = False -acc_clean_search_opt.propagate_col = False - -partial_degen_opt = spot.car_option() -partial_degen_opt.search_ex = False -partial_degen_opt.force_order = False -partial_degen_opt.parity_equiv = False -partial_degen_opt.parity_prefix = False -partial_degen_opt.rabin_to_buchi = False -partial_degen_opt.propagate_col = False - -parity_equiv_opt = spot.car_option() -parity_equiv_opt.search_ex = False -parity_equiv_opt.use_last = False -parity_equiv_opt.force_order = False -parity_equiv_opt.partial_degen = False -parity_equiv_opt.parity_prefix = False -parity_equiv_opt.rabin_to_buchi = False -parity_equiv_opt.propagate_col = False - -rab_to_buchi_opt = spot.car_option() -rab_to_buchi_opt.use_last = False -rab_to_buchi_opt.force_order = False -rab_to_buchi_opt.partial_degen = False -rab_to_buchi_opt.parity_equiv = False -rab_to_buchi_opt.parity_prefix = False -rab_to_buchi_opt.propagate_col = False - -# Force to use CAR or IAR for each SCC -use_car_opt = spot.car_option() -use_car_opt.partial_degen = False -use_car_opt.parity_equiv = False -use_car_opt.parity_prefix = False -use_car_opt.rabin_to_buchi = False -use_car_opt.propagate_col = False - -all_opt = spot.car_option() -all_opt.pretty_print = True - - -options = [ - no_option, - acc_clean_search_opt, - partial_degen_opt, - parity_equiv_opt, - rab_to_buchi_opt, - use_car_opt, - spot.car_option(), -] - -i = 1 - -def test(aut): - global i - for opt in options: - try: - p = spot.to_parity(aut, opt) - assert(spot.are_equivalent(aut, p)) - except: - # Are equivalent can raise exception - assert(False) - - -test(spot.automaton("""HOA: v1 -name: "(FGp0 & ((XFp0 & F!p1) | F(Gp1 & XG!p0))) | G(F!p0 & (XFp0 | F!p1) & -F(Gp1 | G!p0))" -States: 14 -Start: 0 -AP: 2 "p1" "p0" -Acceptance: 6 (Fin(0) & Fin(1)) | ((Fin(4)|Fin(5)) & (Inf(2)&Inf(3))) -properties: trans-labels explicit-labels trans-acc complete -properties: deterministic ---BODY-- -State: 0 -[!0] 1 -[0] 2 -State: 1 -[!0&!1] 1 {0 1 2 3 5} -[0&!1] 3 -[!0&1] 4 -[0&1] 5 -State: 2 -[0&!1] 2 {1} -[!0&1] 4 -[!0&!1] 6 -[0&1] 7 -State: 3 -[0&!1] 3 {1 3} -[!0&1] 4 -[!0&!1] 6 {0 1 2 3 5} -[0&1] 8 -State: 4 -[!0&!1] 4 {1 2 3 5} -[!0&1] 4 {2 4 5} -[0&!1] 5 {1 3} -[0&1] 5 {4} -State: 5 -[!0&1] 4 {2 4 5} -[0&!1] 5 {1 3} -[0&1] 8 {2 4} -[!0&!1] 9 {1 2 3 5} -State: 6 -[0&!1] 3 {1 3} -[!0&1] 4 -[0&1] 5 -[!0&!1] 10 -State: 7 -[!0&1] 4 -[0&!1] 7 {1 3} -[!0&!1] 11 -[0&1] 12 {0 4} -State: 8 -[!0&1] 4 {2 4 5} -[0&1] 5 {4} -[0&!1] 8 {1 3} -[!0&!1] 11 {1 3 5} -State: 9 -[!0&1] 4 {2 4 5} -[0&!1] 5 {1 3} -[0&1] 5 {4} -[!0&!1] 11 {1 3 5} -State: 10 -[!0&1] 4 -[0&1] 8 -[!0&!1] 10 {0 1 2 3 5} -[0&!1] 13 {1 2 3} -State: 11 -[!0&1] 4 {2 4 5} -[0&!1] 8 {1 2 3} -[0&1] 8 {2 4} -[!0&!1] 11 {1 2 3 5} -State: 12 -[!0&1] 4 -[0&1] 7 {0 2 4} -[!0&!1] 9 -[0&!1] 12 {1 3} -State: 13 -[!0&1] 4 -[0&1] 5 -[!0&!1] 10 {0 1 3 5} -[0&!1] 13 {1 3} ---END--""")) - -test(spot.automaton(""" -HOA: v1 -States: 2 -Start: 0 -AP: 2 "p0" "p1" -Acceptance: 5 (Inf(0)&Inf(1)) | ((Fin(2)|Fin(3)) & Fin(4)) ---BODY-- -State: 0 -[!0 & 1] 0 {2 3} -[!0 & !1] 0 {3} -[0] 1 -State: 1 -[0&1] 1 {1 2 4} -[0&!1] 1 {4} -[!0&1] 1 {0 1 2 3} -[!0&!1] 1 {0 3} ---END--""")) - -test(spot.automaton(""" -HOA: v1 States: 6 Start: 0 AP: 2 "p0" "p1" Acceptance: 6 Inf(5) | -Fin(2) | Inf(1) | (Inf(0) & Fin(3)) | Inf(4) properties: trans-labels -explicit-labels trans-acc --BODY-- State: 0 [0&1] 2 {4 5} [0&1] 4 {0 4} -[!0&!1] 3 {3 5} State: 1 [0&!1] 3 {1 5} [!0&!1] 5 {0 1} State: 2 [!0&!1] -0 {0 3} [0&!1] 1 {0} State: 3 [!0&1] 4 {1 2 3} [0&1] 3 {3 4 5} State: -4 [!0&!1] 1 {2 4} State: 5 [!0&1] 4 --END-- -""")) - -for f in spot.randltl(15, 2000): - test(spot.translate(f, "det", "G")) - -for f in spot.randltl(5, 25000): - test(spot.translate(f)) - -test(spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det')) - -test(spot.automaton(""" -HOA: v1 -States: 4 -Start: 0 -AP: 2 "p0" "p1" -Acceptance: 6 -((Fin(1) | Inf(2)) & Inf(5)) | (Fin(0) & (Fin(1) | (Fin(3) & Inf(4)))) -properties: trans-labels explicit-labels trans-acc complete -properties: deterministic ---BODY-- -State: 0 -[!0&!1] 0 {2} -[0&1] 1 {0 5} -[0&!1] 1 {0 2 5} -[!0&1] 2 {1} -State: 1 -[0&1] 1 {0} -[!0&!1] 1 {2} -[0&!1] 1 {0 2} -[!0&1] 2 {1} -State: 2 -[!0&!1] 0 {2 3} -[0&!1] 0 {0 2 3 5} -[!0&1] 2 {1 4} -[0&1] 3 {0 5} -State: 3 -[!0&!1] 0 {2 3} -[0&!1] 0 {0 2 3 5} -[!0&1] 2 {1 4} -[0&1] 3 {0} ---END-- -""")) - -test(spot.automaton(""" -HOA: v1 -States: 5 -Start: 0 -AP: 2 "p1" "p0" -Acceptance: 5 (Fin(0) & Fin(1)) | (Fin(3) & (Inf(2)&Inf(4))) -properties: trans-labels explicit-labels trans-acc complete -properties: deterministic ---BODY-- -State: 0 -[!0] 1 -[0] 2 -State: 1 -[!0&!1] 1 {0 1} -[!0&1] 3 -[0] 4 -State: 2 -[!0&1] 1 -[0&!1] 2 -[0&1] 2 {0 1 2 4} -[!0&!1] 3 -State: 3 -[!0&1] 3 {1 2 3} -[!0&!1] 3 {4} -[0&!1] 4 {3} -[0&1] 4 {1 2 3} -State: 4 -[!0&!1] 3 {3} -[!0&1] 3 {1 2 3} -[0&!1] 4 -[0&1] 4 {1 2 4} ---END-- -""")) - -test(spot.automaton(""" -HOA: v1 -States: 2 -Start: 0 -AP: 2 "p1" "p0" -Acceptance: 5 (Fin(0) & (Fin(3)|Fin(4)) & (Inf(1)&Inf(2))) | Inf(3) -properties: trans-labels explicit-labels trans-acc complete -properties: deterministic stutter-invariant ---BODY-- -State: 0 -[0&!1] 0 {2 3} -[!0&!1] 0 {2 3 4} -[!0&1] 1 -[0&1] 1 {2 4} -State: 1 -[!0&!1] 0 {0 2 3 4} -[!0&1] 1 {1} -[0&!1] 1 {2 3} -[0&1] 1 {1 2 4} ---END-- -""")) diff --git a/tests/python/except.py b/tests/python/except.py index 926aa864d..fbcc1563e 100644 --- a/tests/python/except.py +++ b/tests/python/except.py @@ -33,7 +33,7 @@ def report_missing_exception(): aut = spot.translate('GFa & GFb & GFc') aut.set_acceptance(spot.acc_cond("parity min even 4")) try: - spot.iar(aut) + spot.iar_old(aut) except RuntimeError as e: assert 'iar() expects Rabin-like or Streett-like input' in str(e) else: diff --git a/tests/python/toparity.py b/tests/python/toparity.py index b0bffbe23..90cc533df 100644 --- a/tests/python/toparity.py +++ b/tests/python/toparity.py @@ -20,6 +20,304 @@ import spot +# Tests for the new version of to_parity + +no_option = spot.car_option() +no_option.search_ex = False +no_option.use_last = False +no_option.force_order = False +no_option.partial_degen = False +no_option.acc_clean = False +no_option.parity_equiv = False +no_option.parity_prefix = False +no_option.rabin_to_buchi = False +no_option.propagate_col = False + +acc_clean_search_opt = spot.car_option() +acc_clean_search_opt.force_order = False +acc_clean_search_opt.partial_degen = False +acc_clean_search_opt.parity_equiv = False +acc_clean_search_opt.parity_prefix = False +acc_clean_search_opt.rabin_to_buchi = False +acc_clean_search_opt.propagate_col = False + +partial_degen_opt = spot.car_option() +partial_degen_opt.search_ex = False +partial_degen_opt.force_order = False +partial_degen_opt.parity_equiv = False +partial_degen_opt.parity_prefix = False +partial_degen_opt.rabin_to_buchi = False +partial_degen_opt.propagate_col = False + +parity_equiv_opt = spot.car_option() +parity_equiv_opt.search_ex = False +parity_equiv_opt.use_last = False +parity_equiv_opt.force_order = False +parity_equiv_opt.partial_degen = False +parity_equiv_opt.parity_prefix = False +parity_equiv_opt.rabin_to_buchi = False +parity_equiv_opt.propagate_col = False + +rab_to_buchi_opt = spot.car_option() +rab_to_buchi_opt.use_last = False +rab_to_buchi_opt.force_order = False +rab_to_buchi_opt.partial_degen = False +rab_to_buchi_opt.parity_equiv = False +rab_to_buchi_opt.parity_prefix = False +rab_to_buchi_opt.propagate_col = False + +# Force to use CAR or IAR for each SCC +use_car_opt = spot.car_option() +use_car_opt.partial_degen = False +use_car_opt.parity_equiv = False +use_car_opt.parity_prefix = False +use_car_opt.rabin_to_buchi = False +use_car_opt.propagate_col = False + +all_opt = spot.car_option() +all_opt.pretty_print = True + + +options = [ + no_option, + acc_clean_search_opt, + partial_degen_opt, + parity_equiv_opt, + rab_to_buchi_opt, + use_car_opt, + all_opt, +] + + +def test(aut): + global i + for opt in options: + try: + p = spot.to_parity(aut, + search_ex = opt.search_ex, + use_last = opt.use_last, + force_order = opt.force_order, + partial_degen = opt.partial_degen, + acc_clean = opt.acc_clean, + parity_equiv = opt.parity_equiv, + parity_prefix = opt.parity_prefix, + rabin_to_buchi = opt.rabin_to_buchi, + reduce_col_deg = opt.reduce_col_deg, + propagate_col = opt.propagate_col, + pretty_print = opt.pretty_print, + ) + assert(spot.are_equivalent(aut, p)) + except: + # are_equivalent can raise exception + assert(False) + + +test(spot.automaton("""HOA: v1 +name: "(FGp0 & ((XFp0 & F!p1) | F(Gp1 & XG!p0))) | G(F!p0 & (XFp0 | F!p1) & +F(Gp1 | G!p0))" +States: 14 +Start: 0 +AP: 2 "p1" "p0" +Acceptance: 6 (Fin(0) & Fin(1)) | ((Fin(4)|Fin(5)) & (Inf(2)&Inf(3))) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[!0] 1 +[0] 2 +State: 1 +[!0&!1] 1 {0 1 2 3 5} +[0&!1] 3 +[!0&1] 4 +[0&1] 5 +State: 2 +[0&!1] 2 {1} +[!0&1] 4 +[!0&!1] 6 +[0&1] 7 +State: 3 +[0&!1] 3 {1 3} +[!0&1] 4 +[!0&!1] 6 {0 1 2 3 5} +[0&1] 8 +State: 4 +[!0&!1] 4 {1 2 3 5} +[!0&1] 4 {2 4 5} +[0&!1] 5 {1 3} +[0&1] 5 {4} +State: 5 +[!0&1] 4 {2 4 5} +[0&!1] 5 {1 3} +[0&1] 8 {2 4} +[!0&!1] 9 {1 2 3 5} +State: 6 +[0&!1] 3 {1 3} +[!0&1] 4 +[0&1] 5 +[!0&!1] 10 +State: 7 +[!0&1] 4 +[0&!1] 7 {1 3} +[!0&!1] 11 +[0&1] 12 {0 4} +State: 8 +[!0&1] 4 {2 4 5} +[0&1] 5 {4} +[0&!1] 8 {1 3} +[!0&!1] 11 {1 3 5} +State: 9 +[!0&1] 4 {2 4 5} +[0&!1] 5 {1 3} +[0&1] 5 {4} +[!0&!1] 11 {1 3 5} +State: 10 +[!0&1] 4 +[0&1] 8 +[!0&!1] 10 {0 1 2 3 5} +[0&!1] 13 {1 2 3} +State: 11 +[!0&1] 4 {2 4 5} +[0&!1] 8 {1 2 3} +[0&1] 8 {2 4} +[!0&!1] 11 {1 2 3 5} +State: 12 +[!0&1] 4 +[0&1] 7 {0 2 4} +[!0&!1] 9 +[0&!1] 12 {1 3} +State: 13 +[!0&1] 4 +[0&1] 5 +[!0&!1] 10 {0 1 3 5} +[0&!1] 13 {1 3} +--END--""")) + +test(spot.automaton(""" +HOA: v1 +States: 2 +Start: 0 +AP: 2 "p0" "p1" +Acceptance: 5 (Inf(0)&Inf(1)) | ((Fin(2)|Fin(3)) & Fin(4)) +--BODY-- +State: 0 +[!0 & 1] 0 {2 3} +[!0 & !1] 0 {3} +[0] 1 +State: 1 +[0&1] 1 {1 2 4} +[0&!1] 1 {4} +[!0&1] 1 {0 1 2 3} +[!0&!1] 1 {0 3} +--END--""")) + +test(spot.automaton(""" +HOA: v1 States: 6 Start: 0 AP: 2 "p0" "p1" Acceptance: 6 Inf(5) | +Fin(2) | Inf(1) | (Inf(0) & Fin(3)) | Inf(4) properties: trans-labels +explicit-labels trans-acc --BODY-- State: 0 [0&1] 2 {4 5} [0&1] 4 {0 4} +[!0&!1] 3 {3 5} State: 1 [0&!1] 3 {1 5} [!0&!1] 5 {0 1} State: 2 [!0&!1] +0 {0 3} [0&!1] 1 {0} State: 3 [!0&1] 4 {1 2 3} [0&1] 3 {3 4 5} State: +4 [!0&!1] 1 {2 4} State: 5 [!0&1] 4 --END-- +""")) + +for f in spot.randltl(15, 2000): + test(spot.translate(f, "det", "G")) + +for f in spot.randltl(5, 25000): + test(spot.translate(f)) + +test(spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det')) + +test(spot.automaton(""" +HOA: v1 +States: 4 +Start: 0 +AP: 2 "p0" "p1" +Acceptance: 6 +((Fin(1) | Inf(2)) & Inf(5)) | (Fin(0) & (Fin(1) | (Fin(3) & Inf(4)))) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[!0&!1] 0 {2} +[0&1] 1 {0 5} +[0&!1] 1 {0 2 5} +[!0&1] 2 {1} +State: 1 +[0&1] 1 {0} +[!0&!1] 1 {2} +[0&!1] 1 {0 2} +[!0&1] 2 {1} +State: 2 +[!0&!1] 0 {2 3} +[0&!1] 0 {0 2 3 5} +[!0&1] 2 {1 4} +[0&1] 3 {0 5} +State: 3 +[!0&!1] 0 {2 3} +[0&!1] 0 {0 2 3 5} +[!0&1] 2 {1 4} +[0&1] 3 {0} +--END-- +""")) + +test(spot.automaton(""" +HOA: v1 +States: 5 +Start: 0 +AP: 2 "p1" "p0" +Acceptance: 5 (Fin(0) & Fin(1)) | (Fin(3) & (Inf(2)&Inf(4))) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[!0] 1 +[0] 2 +State: 1 +[!0&!1] 1 {0 1} +[!0&1] 3 +[0] 4 +State: 2 +[!0&1] 1 +[0&!1] 2 +[0&1] 2 {0 1 2 4} +[!0&!1] 3 +State: 3 +[!0&1] 3 {1 2 3} +[!0&!1] 3 {4} +[0&!1] 4 {3} +[0&1] 4 {1 2 3} +State: 4 +[!0&!1] 3 {3} +[!0&1] 3 {1 2 3} +[0&!1] 4 +[0&1] 4 {1 2 4} +--END-- +""")) + +test(spot.automaton(""" +HOA: v1 +States: 2 +Start: 0 +AP: 2 "p1" "p0" +Acceptance: 5 (Fin(0) & (Fin(3)|Fin(4)) & (Inf(1)&Inf(2))) | Inf(3) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic stutter-invariant +--BODY-- +State: 0 +[0&!1] 0 {2 3} +[!0&!1] 0 {2 3 4} +[!0&1] 1 +[0&1] 1 {2 4} +State: 1 +[!0&!1] 0 {0 2 3 4} +[!0&1] 1 {1} +[0&!1] 1 {2 3} +[0&1] 1 {1 2 4} +--END-- +""")) + + +# Tests for the old version of to_parity (CAR) a = spot.automaton("""HOA: v1 States: 1 Start: 0 @@ -32,7 +330,7 @@ State: 0 [!0&1] 0 {1} [!0&!1] 0 --END--""") -p = spot.to_parity(a) +p = spot.to_parity_old(a, True) assert spot.are_equivalent(a, p) a = spot.automaton(""" @@ -43,21 +341,21 @@ explicit-labels trans-acc --BODY-- State: 0 [0&1] 2 {4 5} [0&1] 4 {0 4} 0 {0 3} [0&!1] 1 {0} State: 3 [!0&1] 4 {1 2 3} [0&1] 3 {3 4 5} State: 4 [!0&!1] 1 {2 4} State: 5 [!0&1] 4 --END-- """) -p = spot.to_parity(a) +p = spot.to_parity_old(a, True) assert p.num_states() == 22 assert spot.are_equivalent(a, p) for f in spot.randltl(4, 400): d = spot.translate(f, "det", "G") - p = spot.to_parity(d) + p = spot.to_parity_old(d, True) assert spot.are_equivalent(p, d) for f in spot.randltl(5, 2000): n = spot.translate(f) - p = spot.to_parity(n) + p = spot.to_parity_old(n, True) assert spot.are_equivalent(n, p) # Issue #390. a = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det') -b = spot.to_parity(a) +b = spot.to_parity_old(a, True) assert a.equivalent_to(b)