diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index 41aa736e2..6fb126ff8 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -1005,7 +1005,7 @@ namespace spot if (gi.s == algo::LAR) { dpa = to_parity(aut); - // reduce_parity is called by to_parity() + reduce_parity_here(dpa, false); } else if (gi.s == algo::LAR_OLD) { diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc index 3c3f03607..c936ef57b 100644 --- a/spot/twaalgos/toparity.cc +++ b/spot/twaalgos/toparity.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2018-2020 Laboratoire de Recherche et Développement +// Copyright (C) 2018-2020, 2022 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -18,28 +18,49 @@ // along with this program. If not, see . #include "config.h" -#include -#include -#include -#include -#include +#include #include #include #include -#include -#include -#include #include #include -#include +#include #include -#include +#include + +#include +#include +#include + +namespace std +{ + template + inline void hash_combine(size_t &seed, T const &v) + { + seed ^= std::hash()(v) + 0x9e3779b9 + (seed << 6) + (seed >> 2); + } + + template + struct hash> + { + typedef vector argument_type; + typedef std::size_t result_type; + result_type operator()(argument_type const &in) const + { + size_t size = in.size(); + size_t seed = 0; + for (size_t i = 0; i < size; i++) + // Combine the hash of the current vector with the hashes of the + // previous ones + hash_combine(seed, in[i]); + return seed; + } + }; +} -#include namespace spot { - inline void assign_color(acc_cond::mark_t &mark, unsigned col) { @@ -76,7 +97,7 @@ namespace spot std::vector &res_colors, acc_cond &new_cond, bool &was_able_to_color) { - auto &ev = aut->edge_vector(); + auto& ev = aut->edge_vector(); const auto ev_size = ev.size(); const auto aut_init = aut->get_init_state_number(); was_able_to_color = false; @@ -98,7 +119,7 @@ namespace spot { for (unsigned edge_number = 1; edge_number < ev_size; ++edge_number) { - auto &e = ev[edge_number]; + auto& e = ev[edge_number]; if (si.scc_of(e.src) != si.scc_of(e.dst)) { status[edge_number] = LINK_SCC; @@ -260,7 +281,7 @@ namespace spot std::vector status; acc_cond new_cond; if (cond_type_main_aux(aut, kind, true, status, res_colors, new_cond, - was_able_to_color)) + was_able_to_color)) { auto res = make_twa_graph(aut, twa::prop_set::all()); auto &res_vector = res->edge_vector(); @@ -315,10 +336,2285 @@ namespace spot return cond_type_main(aut, cond_kind::CO_BUCHI, useless); } - // Old version of IAR. +// New version for paritizing + +// data type used in a memory for CAR and IAR. +// TAR is a particular case +#if MAX_ACCSETS < UCHAR_MAX + using memory_type = unsigned char; + #define MAX_MEM_ELEM UCHAR_MAX +#elif MAX_ACCSETS < USHRT_MAX + using memory_type = unsigned short; + #define MAX_MEM_ELEM USHRT_MAX +#else + using memory_type = unsigned; + #define MAX_MEM_ELEM UINT_MAX +#endif + + template + using memory = std::vector; + + // Maps a state of the automaton to a parity_state + class state_2_lar + { + public: + // If to_parity wants to find the newest or the oldest or both, we + // adapt the algorithms + enum memory_order + { + ONLY_NEWEST, + ONLY_OLDEST, + BOTH + }; + + class node + { + public: + // Color that lead to this node + memory_type color_; + // For a state in states_, any child can be taken. While a unique state + // could be used when we search an existing state, here we have + // to consider opt_.search_ex = False, opt_.use_last_post_process = True. + // This configuration can lead to 2 states in the same node. For example + // if we add [0 1 | 2 3] and [0 1 | 3 2] where '|' says which part of the + // memory can be reordered (right). + std::vector states_; + std::vector children_; + // A timer used to detect which child is the oldest + unsigned timer_; + + node() : node(MAX_MEM_ELEM, -1U) + { + } + + node(memory_type val, unsigned timer) : color_(val), timer_(timer) + { + } + + ~node() + { + for (auto c : children_) + delete c; + } + }; + + std::vector nodes_; + memory_order order_; + unsigned timer_; + + state_2_lar() : timer_(0) + { + } + + void + init(unsigned nb_states, memory_order order) + { + order_ = order; + nodes_.reserve(nb_states); + for (unsigned i = 0; i < nb_states; ++i) + nodes_.push_back(new node()); + } + + ~state_2_lar() + { + for (auto x : nodes_) + delete x; + } + + void + add_new_path(unsigned state, const memory &vals, + unsigned res_state, unsigned nb_seen) + { + ++timer_; + node *current = nodes_[state]; + // Position in vals + int pos = vals.size() - 1; + while (true) + { + if (pos == (int)(nb_seen - 1)) + current->states_.push_back(res_state); + if (pos == -1) + break; + const unsigned current_val = vals[pos]; + auto child = std::find_if(current->children_.begin(), + current->children_.end(), + [&](const auto &child) constexpr + { return child->color_ == current_val; }); + // If we don't have a child with the corresponding color… + if (child == current->children_.end()) + { + auto nn = new node(current_val, timer_); + current->children_.push_back(nn); + current = nn; + } + else + { + // If get_compatible_state wants the most recent + // (opt_.use_last or opt_.use_last_post_process), we help this + // function by moving this node to the last position. + // Otherwise the oldest leaf will be reachable from the first child. + // If we have use_last = false and use_last_post_process = true, + // we need to access to the oldest and newest child. As the tree is + // smallest when we want to access to the oldest value, we continue + // to move the value to the last position and compute the oldest + // child in get_compatible_state. + if (order_ != memory_order::ONLY_OLDEST) + { + std::iter_swap(child, current->children_.end() - 1); + current = current->children_.back(); + } + else + current = *child; + } + --pos; + } + } + + unsigned + get_compatible_state(unsigned state, const memory &m, + unsigned seen_nb, + bool use_last) const + { + int pos = m.size() - 1; + unsigned res = -1U; + node *current = nodes_[state]; + while (true) + { + const auto ¤t_states = current->states_; + if (!current_states.empty()) + res = use_last ? current_states.back() : current_states.front(); + + const auto ¤t_children = current->children_; + if (current_children.empty()) + { + assert(current->color_ == MAX_MEM_ELEM || pos == -1); + return res; + } + // If we are in the part of the memory where the order does not matter, + // we just take the oldest/newest state. + if (pos < (int)seen_nb) + { + if (order_ == BOTH) + { + if (!use_last) + current = *std::min_element( + current_children.begin(), current_children.end(), + [](const auto &x, const auto &y) constexpr + { return x->timer_ < y->timer_; }); + else + current = current_children.back(); + } + else + { + // add_new_path constructed the tree such that the oldest/newest + // leaf is reachable from the first child. + current = use_last ? current_children.back() + : current_children.front(); + } + } + else + { + auto current_val = m[pos]; + auto ch = std::find_if( + current_children.begin(), current_children.end(), + [&](const auto &x) constexpr + { return x->color_ == current_val; }); + if (ch != current_children.end()) + current = *ch; + else + return -1U; + } + --pos; + } + } + }; + + class to_parity_generator + { + private: + class relation + { + public: + // Size of the matrix + unsigned size_; + // A line/column is indexed by a partial memory + const std::vector> labels_; + // Matrix such that vals_[x][y] = ⊤ ⇔ vals_[x] > vals_[y] + std::vector vals_; + + inline bool + at(unsigned i, unsigned j) const + { + return vals_.at(i * size_ + j); + } + + inline void + set(unsigned i, unsigned j, bool val) + { + vals_[i * size_ + j] = val; + } + + // Test if m1 ⊆ m2 + bool is_included(memory m1, memory m2) + { + if (m1.size() > m2.size()) + return false; + assert(std::is_sorted(m1.begin(), m1.end())); + assert(std::is_sorted(m2.begin(), m2.end())); + memory diff; + std::set_union(m1.begin(), m1.end(), m2.begin(), m2.end(), + std::inserter(diff, diff.begin())); + return diff.size() == m2.size(); + } + + // Supposes that there is no duplicates. + relation(std::vector> &labels) + : size_(labels.size()), labels_(labels) + { + unsigned long long size_vals; + if (__builtin_umulll_overflow(size_, size_, &size_vals)) + throw std::bad_alloc(); + vals_ = std::vector(size_vals); + for (unsigned i = 0; i < size_; ++i) + for (unsigned j = 0; j < size_; ++j) + // We cannot have vals_[i] > vals_[j] and vals_[j] > vals_[i] + if (!at(j, i)) + set(i, j, (i != j && is_included(labels_[j], labels_[i]))); + // Remove x > z if ∃y s.t. x > y > z + simplify_relation(); + } + + // Apply a transitive reduction + void + simplify_relation() + { + for (unsigned j = 0; j < size_; ++j) + for (unsigned i = 0; i < size_; ++i) + if (at(i, j)) + for (unsigned k = 0; k < size_; ++k) + if (at(j, k)) + set(i, k, false); + } + + template + void + add_to_res_(const memory ¤t, + const memory &other, + memory &result) + { + assert(std::is_sorted(current.begin(), current.end())); + assert(std::is_sorted(other.begin(), other.end())); + std::set_difference(current.begin(), current.end(), + other.begin(), other.end(), + std::inserter(result, result.end())); + } + + // Gives a compatible ordered partial memory for the partial memory + // partial_mem. + memory + find_order(const memory &partial_mem) + { + // Now if we want to find an order, we start from the line + // that contains partial_mem in the matrix, we find a more restrictive + // order and add the value that are used in partial_mem but not in this + // "child" value. + // The call to simplify_relation implies that we are sure we have + // used the longest possible path. + memory result; + auto elem = std::find(labels_.begin(), labels_.end(), partial_mem); + assert(elem != labels_.end()); + // Line that contains partial_mem + unsigned i = std::distance(labels_.begin(), elem); + while (true) + { + // The interval corresponding to the line i + auto vals_i_begin = vals_.begin() + (i * size_); + auto vals_i_end = vals_i_begin + size_; + // End of line i + auto child = std::find(vals_i_begin, vals_i_end, true); + // If there is a more restrictive memory, we use this "child" + if (child != vals_i_end) + { + unsigned child_pos = std::distance(vals_i_begin, child); + add_to_res_(labels_[i], labels_[child_pos], result); + i = child_pos; + } + // If there is no more restrictive memory, we just add the remaining + // memory. + else + { + add_to_res_(labels_[i], {}, result); + break; + } + } + // The order want that a value that is in the lowest value is a + // the head. + std::reverse(result.begin(), result.end()); + return result; + } + }; + + class scc_info_to_parity + { + private: + scc_info si_; + + public: + scc_info_to_parity(const const_twa_graph_ptr aut, + const acc_cond::mark_t removed = {}) + : si_(scc_and_mark_filter(aut, removed)) + { + } + + scc_info_to_parity(const scc_info lower_si, + const std::shared_ptr keep) + : si_(scc_and_mark_filter(lower_si, 0, acc_cond::mark_t{}, *keep), + scc_info_options::NONE) + { + } + + std::vector + split_aut(acc_cond::mark_t mark = {}) + { + auto aut = si_.get_aut(); + const auto num_scc = si_.scc_count(); + const unsigned aut_num_states = aut->num_states(); + std::vector res(num_scc); + std::vector aut_to_res; + aut_to_res.reserve(aut_num_states); + for (auto &g : res) + { + g = make_twa_graph(aut->get_dict()); + g->copy_ap_of(aut); + g->copy_acceptance_of(aut); + g->prop_copy(aut, {true, true, false, false, false, true}); + auto orig = new std::vector(); + g->set_named_prop("original-states", orig); + } + const auto tp_orig_aut = + aut->get_named_prop>("original-states"); + for (unsigned i = 0; i < aut_num_states; ++i) + { + unsigned scc_i = si_.scc_of(i); + auto &g = res[scc_i]; + unsigned ns = g->new_state(); + unsigned ori = tp_orig_aut ? (*tp_orig_aut)[i] : i; + auto pr = g->get_named_prop>("original-states"); + pr->push_back(ori); + aut_to_res.push_back(ns); + } + + for (auto &e : aut->edges()) + { + unsigned src_scc = si_.scc_of(e.src); + unsigned dst_scc = si_.scc_of(e.dst); + if (src_scc == dst_scc && !(e.acc & mark)) + res[src_scc]->new_edge(aut_to_res[e.src], aut_to_res[e.dst], + e.cond, e.acc); + } + return res; + } + + std::vector + split_aut(const std::shared_ptr &keep) + { + auto aut = si_.get_aut(); + const auto num_scc = si_.scc_count(); + const unsigned aut_num_states = aut->num_states(); + std::vector res(num_scc); + std::vector aut_to_res; + aut_to_res.reserve(aut_num_states); + for (auto &g : res) + { + g = make_twa_graph(aut->get_dict()); + g->copy_ap_of(aut); + g->copy_acceptance_of(aut); + g->prop_copy(aut, {true, true, false, false, false, true}); + auto orig = new std::vector(); + g->set_named_prop("original-states", orig); + } + const auto tp_orig_aut = + aut->get_named_prop>("original-states"); + for (unsigned i = 0; i < aut_num_states; ++i) + { + unsigned scc_i = si_.scc_of(i); + auto &g = res[scc_i]; + unsigned ns = g->new_state(); + unsigned ori = tp_orig_aut ? (*tp_orig_aut)[i] : i; + auto pr = g->get_named_prop>("original-states"); + pr->push_back(ori); + aut_to_res.push_back(ns); + } + + const auto &ev = si_.get_aut()->edge_vector(); + auto ev_size = ev.size(); + for (unsigned i = 0; i < ev_size; ++i) + if (keep->get(i)) + { + auto &e = ev[i]; + unsigned scc_src = si_.scc_of(e.src); + if (scc_src == si_.scc_of(e.dst)) + res[scc_src]->new_edge(aut_to_res[e.src], aut_to_res[e.dst], + e.cond, e.acc); + } + return res; + } + + unsigned scc_count() + { + return si_.scc_count(); + } + + unsigned scc_of(unsigned state) + { + return si_.scc_of(state); + } + }; + + // Original automaton + const const_twa_graph_ptr aut_; + // Resulting parity automaton + twa_graph_ptr res_; + // options + to_parity_options opt_; + // nullptr if opt_.pretty_print is false + std::vector *names_ = nullptr; + // original_states. Is propagated if the original automaton has + // this named property + std::vector *orig_ = nullptr; + scc_info_to_parity si_; + bool need_purge_ = false; + // Tells if we are constructing a parity max odd + bool is_odd_ = false; + // min_color used in the automaton + 1 (result of max_set). + std::optional min_color_used_; + std::optional max_color_scc_; + std::optional max_color_used_; + std::vector state_to_res_; + std::vector res_to_aut_; + // Map a state of aut_ to every copy of this state. Used by a recursive call + // to to_parity by parity_prefix for example + std::vector> *state_to_nums_ = nullptr; + unsigned algo_used_ = 0; + + enum algorithm + { + CAR = 1, + IAR_RABIN = 1 << 1, + IAR_STREETT = 1 << 2, + TAR = 1 << 3, + RABIN_TO_BUCHI = 1 << 4, + STREETT_TO_COBUCHI = 1 << 5, + PARITY_TYPE = 1 << 6, + BUCHI_TYPE = 1 << 7, + CO_BUCHI_TYPE = 1 << 8, + PARITY_EQUIV = 1 << 9, + PARITY_PREFIX = 1 << 10, + PARITY_PREFIX_GENERAL = 1 << 11, + GENERIC_EMPTINESS = 1 << 12, + PARTIAL_DEGEN = 1 << 13, + ACC_CLEAN = 1 << 14, + NONE = 1 << 15 + }; + + static std::string + algorithm_to_str(const algorithm &algo) + { + switch (algo) + { + case CAR: + return "CAR"; + case IAR_RABIN: + return "IAR (Rabin)"; + case IAR_STREETT: + return "IAR (Streett)"; + case TAR: + return "TAR"; + case NONE: + return "None"; + case BUCHI_TYPE: + return "Büchi-type"; + case CO_BUCHI_TYPE: + return "co-Büchi-type"; + case PARITY_TYPE: + return "Parity-type"; + case PARITY_EQUIV: + return "Parity equivalent"; + case GENERIC_EMPTINESS: + return "Generic emptiness"; + case STREETT_TO_COBUCHI: + return "Streett to co-Büchi"; + case RABIN_TO_BUCHI: + return "Rabin to Büchi"; + case PARITY_PREFIX: + return "Parity-prefix"; + case PARITY_PREFIX_GENERAL: + return "Parity-prefix general"; + case PARTIAL_DEGEN: + return "Partial degeneralization"; + case ACC_CLEAN: + return "acceptance cleanup"; + } + SPOT_UNREACHABLE(); + } + + template + struct to_parity_state + { + unsigned state; + unsigned state_scc; + memory mem; + + to_parity_state(unsigned st, unsigned st_scc, memory m) : + state(st), state_scc(st_scc), mem(m) + {} + + to_parity_state(const to_parity_state &) = default; + to_parity_state(to_parity_state &&) noexcept = default; + + ~to_parity_state() noexcept = default; + + bool + operator<(const to_parity_state &other) const + { + if (state < other.state) + return true; + if (state > other.state) + return false; + if (state_scc < other.state_scc) + return true; + if (state_scc > other.state_scc) + return false; + if (mem < other.mem) + return true; + return false; + } + + std::string + to_str(const algorithm &algo) const + { + std::stringstream s; + s << state; + // An empty memory does not mean that we don't use LAR. For example + // if the condition is true. We don't display a useless memory. + if (!mem.empty()) + { + s << ",["; + const char delim = ','; + s << ((unsigned)mem[0]); + auto mem_size = mem.size(); + for (unsigned i = 1; i < mem_size; ++i) + s << delim << ((unsigned)mem[i]); + s << ']'; + } + s << ',' << algorithm_to_str(algo); + return s.str(); + } + + bool operator==(const to_parity_state &other) const + { + return state == other.state && state_scc == other.state_scc + && mem == other.mem; + } + }; + + template + struct to_parity_hash + { + size_t operator()(to_parity_state const &tp) const + { + size_t result = std::hash>{}(tp.mem); + std::hash_combine(result, tp.state); + std::hash_combine(result, tp.state_scc); + return result; + } + }; + + template + unsigned + add_res_state(const algorithm &algo, const to_parity_state &ps) + { + if (names_) + names_->emplace_back(ps.to_str(algo)); + orig_->push_back(ps.state); + auto res = res_->new_state(); + if (opt_.datas) + { + algo_used_ |= algo; + ++opt_.datas->nb_states_created; + } + assert(ps.state < aut_->num_states()); + // state_to_res_ could be updated even if there is already a value. + // However it would lead to a result close to BSCC. + // So it is easier to show the influence of BSCC when the value is not + // changed when there is already a value. + if (state_to_res_[ps.state] == -1U) + state_to_res_[ps.state] = res; + if (state_to_nums_) + { + assert(ps.state < state_to_nums_->size()); + (*state_to_nums_)[ps.state].push_back(res); + } + res_to_aut_.push_back(ps.state); + return res; + } + + unsigned + add_res_edge(unsigned res_src, unsigned res_dst, + const acc_cond::mark_t &mark, const bdd &cond, + const bool can_merge_edge = true, + robin_hood::unordered_map* + edge_cache = nullptr) + { + // In a parity automaton we just need the maximal value + auto simax = mark.max_set(); + + const bool need_cache = edge_cache != nullptr && can_merge_edge; + long long key = 0; + if (need_cache) + { + constexpr auto unsignedsize = sizeof(unsigned) * 8; + key = (long long)simax << unsignedsize | res_dst; + auto cache_value = edge_cache->find(key); + if (cache_value != edge_cache->end()) + { + auto edge_index = cache_value->second; + auto &existing_edge = res_->edge_vector()[edge_index]; + existing_edge.cond |= cond; + return edge_index; + } + } + + auto simplified = mark ? acc_cond::mark_t{simax - 1} + : acc_cond::mark_t{}; + assert(res_src != -1U); + assert(res_dst != -1U); + + // No edge already done in the current scc. + if (!max_color_scc_.has_value()) + max_color_scc_.emplace(simax); + else + max_color_scc_.emplace(std::max(*max_color_scc_, simax)); + + // If it is the first edge of the result + if (!min_color_used_.has_value()) + { + assert(!max_color_used_.has_value()); + max_color_used_.emplace(simax); + min_color_used_.emplace(simax); + } + else + { + min_color_used_.emplace(std::min(*min_color_used_, simax)); + max_color_used_.emplace(std::max(*max_color_used_, simax)); + } + + auto new_edge_num = res_->new_edge(res_src, res_dst, cond, simplified); + if (need_cache) + edge_cache->emplace(std::make_pair(key, new_edge_num)); + + if (opt_.datas) + ++opt_.datas->nb_edges_created; + return new_edge_num; + } + + // copy + using coloring_function = + std::function; + + void + apply_copy_general(const const_twa_graph_ptr &sub_automaton, + const coloring_function &col_fun, + const algorithm &algo) + { + if (opt_.datas) + algo_used_ |= algo; + auto init_states = + sub_automaton->get_named_prop>("original-states"); + assert(init_states); + std::vector state_2_res_local; + auto sub_aut_ns = sub_automaton->num_states(); + state_2_res_local.reserve(sub_aut_ns); + for (unsigned state = 0; state < sub_aut_ns; ++state) + { + to_parity_state ps = {(*init_states)[state], state, {}}; + state_2_res_local.push_back(add_res_state(algo, ps)); + } + for (auto &e : sub_automaton->edges()) + { + auto new_mark = col_fun(e); + add_res_edge(state_2_res_local[e.src], state_2_res_local[e.dst], + new_mark, e.cond); + } + } + + // Case where one color is replaced by another. + // new_colors is a vector such that new_colors[i + 1] = j means that the + // color i is replaced by j. new_colors[0] is the value for an uncolored + // edge. + void + apply_copy(const const_twa_graph_ptr &sub_aut, + const std::vector &new_colors, + const algorithm &algo) + { + auto col_fun = [&](const twa_graph::edge_storage_t &edge) + { + acc_cond::mark_t res{}; + for (auto c : edge.acc.sets()) + { + auto new_col = new_colors[c + 1]; + if (new_col != -1U) + assign_color(res, new_col); + } + if (!edge.acc && new_colors[0] != -1U) + assign_color(res, new_colors[0]); + return res; + }; + apply_copy_general(sub_aut, col_fun, algo); + } + + // Case where new_color is a function such that edge_vector[i] should + // be colored by new_color[i]. + void + apply_copy_edge_index(const const_twa_graph_ptr &sub_aut, + const std::vector &new_color, + const algorithm &algo) + { + auto col_fun = [&](const twa_graph::edge_storage_t &edge) + { + auto res = new_color[sub_aut->edge_number(edge)]; + if (res == -1U) + return acc_cond::mark_t{}; + return acc_cond::mark_t{res}; + }; + apply_copy_general(sub_aut, col_fun, algo); + } + + // Create a memory for the first state created by apply_lar. + // If the algorithm is IAR, it also fills pairs_indices that + // contains the indices of the pairs that can be moved to the head of + // the memory. + template + memory + initial_memory_of(const const_twa_graph_ptr &sub_aut, + const std::vector &pairs, + std::vector, memory>> &relations) + { + unsigned init_state = sub_aut->get_init_state_number(); + if constexpr (algo == algorithm::CAR) + { + unsigned max_set = sub_aut->get_acceptance().used_sets().max_set(); + memory values(max_set); + std::iota(values.begin(), values.end(), 0); + if (opt_.force_order) + apply_move_heuristic(init_state, values, max_set, relations); + return values; + } + else if constexpr (algo == algorithm::TAR) + { + if (UINT_MAX < sub_aut->num_edges()) + { + throw std::runtime_error("Too many edges for TAR"); + } + const auto &ev = sub_aut->edge_vector(); + const auto ev_size = ev.size(); + memory values(ev_size - 1); + // 0 is not an edge number + std::iota(values.begin(), values.end(), 1); + if (opt_.force_order && sub_aut->num_states() > 1) + { + unsigned free_pos = 0; + // If a transition goes to state, it is at the head of the memory. + for (unsigned i = 1; i < ev_size; ++i) + if (ev[i].dst == init_state) + { + std::swap(values[i - 1], values[free_pos]); + ++free_pos; + } + } + return values; + } + else + { + static_assert(algo == IAR_RABIN || algo == IAR_STREETT); + memory values(pairs.size()); + std::iota(values.begin(), values.end(), 0); + if (opt_.force_order) + apply_move_heuristic(init_state, values, values.size(), relations); + return values; + } + } + + // LAR + algorithm + choose_lar(const acc_cond &scc_condition, + std::vector &pairs, + const unsigned num_edges) + { + std::vector pairs1, pairs2; + bool is_rabin_like = scc_condition.is_rabin_like(pairs1); + bool is_streett_like = scc_condition.is_streett_like(pairs2); + // If we cannot apply IAR and TAR and CAR are not used + if ((!(is_rabin_like || is_streett_like) || !opt_.iar) + && !(opt_.car || opt_.tar)) + throw std::runtime_error("to_parity needs CAR or TAR to process " + "a condition that is not a Rabin or Streett " + "condition or if IAR is not enabled"); + remove_duplicates(pairs1); + remove_duplicates(pairs2); + unsigned num_col = scc_condition.num_sets(); + + auto num_pairs1 = (opt_.iar && is_streett_like) ? pairs2.size() : -1UL; + auto num_pairs2 = (opt_.iar && is_rabin_like) ? pairs1.size() : -1UL; + + // In practice, if the number of pairs is bigger than the number of + // colors, it will create a color greater than SPOT_MAX_ACCSETS, so + // we don't consider that it is a Rabin condition. + // In this case, if CAR or TAR is not used, it will throw a Runtime + // Error. + + bool iar_overflow = false; + if ((num_pairs1 > MAX_MEM_ELEM) && (num_pairs2 > MAX_MEM_ELEM)) + { + num_pairs1 = num_pairs2 = -1U; + iar_overflow = true; + } + + const std::vector + number_elements = + { + (opt_.iar && is_streett_like) ? pairs2.size() : -1UL, + (opt_.iar && is_rabin_like) ? pairs1.size() : -1UL, + opt_.car ? num_col : -1UL, + opt_.tar ? num_edges : -1UL}; + constexpr std::array algos = {IAR_STREETT, IAR_RABIN, CAR, + TAR}; + int min_pos = std::distance(number_elements.begin(), + std::min_element(number_elements.begin(), + number_elements.end())); + + if (number_elements[min_pos] == -1U && iar_overflow) + throw std::runtime_error( + "Too many Rabin/Streett pairs, try to increase SPOT_MAX_ACCSETS"); + algorithm algo = algos[min_pos]; + if (algo == IAR_RABIN) + pairs = pairs1; + else if (algo == IAR_STREETT) + pairs = pairs2; + return algo; + } + + // Remove duplicates in pairs without changing the order. + static void + remove_duplicates(std::vector &pairs) + { + std::vector res; + res.reserve(pairs.size()); + for (auto &elem : pairs) + if (std::find(res.begin(), res.end(), elem) == res.end()) + res.emplace_back(elem); + pairs = res; + } + + template + acc_cond::mark_t + fin(const std::vector &pairs, unsigned k) + { + static_assert(algo == IAR_RABIN || algo == IAR_STREETT); + if constexpr (algo == IAR_RABIN) + return pairs[k].fin; + else + return pairs[k].inf; + } + + template + acc_cond::mark_t + inf(const std::vector &pairs, unsigned k) + { + static_assert(algo == IAR_RABIN || algo == IAR_STREETT); + if constexpr (algo == IAR_RABIN) + return pairs[k].inf; + else + return pairs[k].fin; + } + + template + std::vector, memory>> + find_relations(const const_twa_graph_ptr &sub_aut, + const std::vector &pairs, + const std::set &pairs_indices) + { + static_assert(algo == IAR_RABIN || algo == IAR_STREETT || algo == CAR); + const unsigned sub_aut_num_states = sub_aut->num_states(); + // Set of memory elements that can be at the head of the memory for + // a given state. + std::vector>> incomem(sub_aut_num_states); + // Add a mark with all colors/pairs to deal with the order of the + // original state + if constexpr (algo == algorithm::CAR) + { + auto ms = sub_aut->get_acceptance().used_sets().max_set(); + memory m(ms); + std::iota(m.begin(), m.end(), 0); + incomem[sub_aut->get_init_state_number()].insert(std::move(m)); + } + else if constexpr (algo == IAR_RABIN || algo == IAR_STREETT) + { + memory m(pairs_indices.begin(), pairs_indices.end()); + incomem[sub_aut->get_init_state_number()].insert(std::move(m)); + } + + for (auto &e : sub_aut->edges()) + { + auto e_sets = e.acc.sets(); + if constexpr (algo == algorithm::CAR) + incomem[e.dst].insert({e_sets.begin(), e_sets.end()}); + // IAR + else + { + memory parti; + for (unsigned k : pairs_indices) + if (e.acc & fin(pairs, k)) + parti.push_back(k); + incomem[e.dst].insert(parti); + } + } + std::vector, memory>> res; + res.reserve(sub_aut_num_states); + for (unsigned i = 0; i < sub_aut_num_states; ++i) + { + std::map, memory> ma; + // Memory incoming to state i. + std::vector> elem(incomem[i].begin(), + incomem[i].end()); + relation rel(elem); + for (auto &x : rel.labels_) + ma.insert({x, rel.find_order(x)}); + res.emplace_back(ma); + } + return res; + } + + void + apply_move_heuristic(unsigned state, memory &m, + unsigned nb_seen, + std::vector, + memory>> &relations) + { + // If we move 0 or 1 color we cannot change the order + if (nb_seen < 2) + return; + memory seen{m.begin(), m.begin() + nb_seen}; + const auto &new_prefix = relations[state][seen]; + + unsigned new_prefix_size = new_prefix.size(); + for (unsigned i = 0; i < new_prefix_size; ++i) + m[i] = new_prefix[i]; + } + + template + void + find_new_memory(unsigned state, memory &m, unsigned edge_number, + const acc_cond::mark_t &colors, + const std::vector &pairs, + const std::set &pairs_indices, + unsigned &nb_seen, + unsigned &h, + std::vector, memory>> &relations) + { + if constexpr (algo == TAR) + { + (void)state; + auto pos = std::find(m.begin(), m.end(), edge_number); + assert(pos != m.end()); + h = std::distance(m.begin(), pos); + std::rotate(m.begin(), pos, pos + 1); + } + else if constexpr (algo == CAR) + { + (void)edge_number; + for (auto k : colors.sets()) + { + auto it = std::find(m.begin(), m.end(), k); + // A color can exist in the automaton but not in the condition. + if (it != m.end()) + { + h = std::max(h, (unsigned)(it - m.begin()) + 1); + std::rotate(m.begin(), it, it + 1); + ++nb_seen; + } + } + if (opt_.force_order) + { + // apply_move_heuristic needs an increasing list of values + std::reverse(m.begin(), m.begin() + nb_seen); + apply_move_heuristic(state, m, nb_seen, relations); + } + } + else if constexpr (algo == IAR_RABIN || algo == IAR_STREETT) + { + (void)edge_number; + for (auto k = pairs_indices.rbegin(); k != pairs_indices.rend(); ++k) + if (colors & fin(pairs, *k)) + { + ++nb_seen; + auto it = std::find(m.begin(), m.end(), *k); + assert(it != m.end()); + // move the pair in front of the permutation + std::rotate(m.begin(), it, it + 1); + } + if (opt_.force_order) + { + // As with CAR, in relation the partial memory is sorted. That is + // why the previous loop use a reverse iterator. + assert(std::is_sorted(m.begin(), m.begin() + nb_seen)); + apply_move_heuristic(state, m, nb_seen, relations); + } + } + } + + template + void + compute_new_color_lar(const const_twa_graph_ptr &sub_aut, + const memory ¤t_mem, + const memory &new_perm, + unsigned &h, + const acc_cond::mark_t &edge_colors, + acc_cond::mark_t &acc, + const std::vector &pairs, + robin_hood::unordered_map& + acc_cache) + { + // This function should not be called with algo ∉ [CAR, IAR, TAR]. + static_assert(algo == CAR || algo == IAR_RABIN || algo == IAR_STREETT + || algo == TAR); + assert(!acc); + auto sub_aut_cond = sub_aut->acc(); + if constexpr (algo == CAR) + { + acc_cond::mark_t m(new_perm.begin(), new_perm.begin() + h); + auto cc = acc_cache.find(m); + bool rej; + if (cc != acc_cache.end()) + rej = cc->second; + else + { + rej = !sub_aut_cond.accepting(m); + acc_cache.insert({m, rej}); + } + unsigned value = 2 * h + rej - 1; + if (value != -1U) + assign_color(acc, value); + return; + } + else if constexpr (algo == TAR) + { + auto &edge_vector = sub_aut->edge_vector(); + acc_cond::mark_t acc_seen {}; + for (unsigned i = 0; i <= h; ++i) + acc_seen |= edge_vector[new_perm[i]].acc; + + auto cc = acc_cache.find(acc_seen); + bool rej; + if (cc != acc_cache.end()) + rej = cc->second; + else + { + rej = !sub_aut_cond.accepting(acc_seen); + acc_cache.insert({acc_seen, rej}); + } + + unsigned acc_col = 2 * h + rej - 1; + if (acc_col != -1U) + assign_color(acc, acc_col); + } + else + { + // IAR_RABIN produces a parity max even condition. If res_ + // is parity max odd, we add 1 to a transition to produce a parity max + // odd automaton. + unsigned delta_acc = ((algo == IAR_RABIN) && is_odd_) - 1; + + unsigned maxint = -1U; + for (int k = current_mem.size() - 1; k >= 0; --k) + { + unsigned pk = current_mem[k]; + + if (!inf(pairs, pk) || (edge_colors + & (pairs[pk].fin | pairs[pk].inf))) + { + maxint = k; + break; + } + } + + unsigned value; + if (maxint == -1U) + value = delta_acc; + else if (edge_colors & fin(pairs, current_mem[maxint])) + value = 2 * maxint + 2 + delta_acc; + else + value = 2 * maxint + 1 + delta_acc; + + if (value != -1U) + assign_color(acc, value); + } + } + + void + change_to_odd() + { + if (is_odd_) + return; + is_odd_ = true; + // We can reduce if we don't have an edge without color. + bool can_reduce = (min_color_used_.has_value() && *min_color_used_ != 0); + int shift; + + if (can_reduce) + shift = -1 * (*min_color_used_ - (*min_color_used_ % 2) + 1); + else + shift = 1; + + // If we cannot decrease and we already the the maximum color, we don't + // have to try. Constructs a mark_t to avoid to make report_too_many_sets + // public. + if (!can_reduce && max_color_used_.value_or(-1) + shift == MAX_ACCSETS) + acc_cond::mark_t {SPOT_MAX_ACCSETS}; + if (max_color_used_.has_value()) + *max_color_used_ += shift; + if (min_color_used_.has_value()) + *min_color_used_ += shift; + for (auto &e : res_->edges()) + { + auto new_val = e.acc.max_set() - 1 + shift; + if (new_val != -1U) + e.acc = { new_val }; + else + e.acc = {}; + } + } + + template + void + apply_lar(twa_graph_ptr &sub_aut, + const std::vector &pairs) + { + if constexpr (algo != IAR_RABIN) + change_to_odd(); + // avoids to call LAR if there is one color/pair/transition. + // LAR can work with this kind of condition but some optimizations + // like searching an existing state suppose that there is at least + // one element. + if ((algo == CAR && sub_aut->acc().num_sets() == 0) + || ((algo == IAR_RABIN || algo == IAR_STREETT) && pairs.empty()) + || (algo == TAR && sub_aut->num_edges() == 0)) + { + bool need_col = sub_aut->acc().is_t() != is_odd_; + auto col_fun = [&](const twa_graph::edge_storage_t &) + { + return need_col ? acc_cond::mark_t{0} : acc_cond::mark_t{}; + }; + apply_copy_general(sub_aut, col_fun, algo); + return; + } + // We sometimes need to have a list of the states + // of res_ constructed by this call to apply_lar. + const bool use_bscc = opt_.bscc; + const bool use_last_post_process = opt_.use_last_post_process; + constexpr bool is_tar = algo == TAR; + const bool need_tree = !is_tar + && (opt_.search_ex || use_last_post_process); + const bool need_state_list = use_last_post_process || use_bscc; + const bool is_dfs = opt_.lar_dfs; + // state_2_lar adapts add_new_state such that depending on the + // value of use_last in get_compatible_state, we will be able + // to find a compatible state faster. + state_2_lar::memory_order order; + if (!opt_.use_last) + { + if (opt_.use_last_post_process) + order = state_2_lar::memory_order::BOTH; + else + order = state_2_lar::memory_order::ONLY_OLDEST; + } + else + order = state_2_lar::memory_order::ONLY_NEWEST; + state_2_lar s2l; + if (need_tree) + s2l.init(sub_aut->num_states(), order); + std::vector states_scc_res; + if (need_state_list) + states_scc_res.reserve(sub_aut->num_states()); + auto init = + sub_aut->get_named_prop>("original-states"); + + if (opt_.propagate_col) + propagate_marks_here(sub_aut); + + auto init_state = sub_aut->get_init_state_number(); + robin_hood::unordered_map, + unsigned, to_parity_hash> ps_2_num; + unsigned lb_size; + if constexpr (algo == TAR) + lb_size = aut_->num_edges(); + else if constexpr (algo == CAR) + lb_size = aut_->num_states() * aut_->acc().num_sets(); + else + lb_size = aut_->num_states() * pairs.size(); + // num_2_ps maps a state of the result to a parity_state. As this function + // does not always create the first state, we need to add + // "- nb_states_before" to get a value. + const unsigned nb_states_before = res_->num_states(); + std::vector> num_2_ps; + // At least one copy of each state will be created. + num_2_ps.reserve(lb_size + num_2_ps.size()); + ps_2_num.reserve(lb_size + num_2_ps.size()); + + std::deque todo; + // return a pair new_state, is_new such that + // ps is associated to the state new_state in res_ + // and is_new is true if a new state was created by + // get_state + // We store 2 unsigned in a long long. + static_assert(sizeof(long long) >= 2 * sizeof(unsigned)); + robin_hood::unordered_map* edge_cache = nullptr; + if (!use_last_post_process) + { + edge_cache = new robin_hood::unordered_map(); + edge_cache->reserve(sub_aut->num_edges()); + } + auto get_state = [&](const to_parity_state &&ps) constexpr + { + auto it = ps_2_num.find(ps); + if (it == ps_2_num.end()) + { + unsigned nb = add_res_state(algo, ps); + ps_2_num[ps] = nb; + assert(nb == num_2_ps.size() + nb_states_before); + num_2_ps.emplace_back(ps); + todo.push_back(nb); + if (need_state_list) + states_scc_res.push_back(nb); + return std::pair{nb, true}; + } + return std::pair{it->second, false}; + }; + + std::set pairs_indices; + std::vector, memory>> relations; + if constexpr (algo == IAR_STREETT || algo == IAR_RABIN) + { + const auto num_pairs = pairs.size(); + for (unsigned k = 0; k < num_pairs; ++k) + if (fin(pairs, k)) + pairs_indices.insert(k); + } + + if constexpr (algo != TAR) + if (opt_.force_order) + relations = find_relations(sub_aut, pairs, pairs_indices); + + auto m = initial_memory_of(sub_aut, pairs, relations); + + assert(init); + auto init_res = get_state({(*init)[init_state], init_state, m}).first; + // A path is added when it is a destination. That is why we need to + // add the initial state. + unsigned nb_edges_before = res_->num_edges(); + std::vector edge_to_seen_nb; + if (use_last_post_process && algo != TAR) + edge_to_seen_nb.reserve(sub_aut->num_edges()); + if constexpr(!is_tar) + if (need_tree) + s2l.add_new_path(init_state, m, init_res, 0); + + robin_hood::unordered_map acc_cache; + // Main loop + while (!todo.empty()) + { + if (edge_cache) + edge_cache->clear(); + // If we want to process the most recent state of the result, we + // take the last value + unsigned res_current = is_dfs ? todo.back() : todo.front(); + unsigned res_index = res_current - nb_states_before; + const auto ¤t_ps = num_2_ps[res_index]; + const auto current_mem = current_ps.mem; + if (is_dfs) + todo.pop_back(); + else + todo.pop_front(); + + // For each edge leaving the state corresponding to res_state in sub_aut + for (auto &e : sub_aut->out(current_ps.state_scc)) + { + // We create a new memory and update it + memory mem(current_mem); + unsigned nb_seen = 0, + h = 0; + find_new_memory(e.dst, mem, sub_aut->edge_number(e), e.acc, + pairs, pairs_indices, nb_seen, h, relations); + // Now we try to find a way to move the elements and obtain an + // existing memory. + unsigned res_dst = -1U; + if constexpr (algo != TAR) + if (opt_.search_ex) + res_dst = s2l.get_compatible_state(e.dst, mem, nb_seen, + opt_.use_last); + // If it doesn't exist, we create a new state… + if (res_dst == -1U) + { + auto gs = get_state({(*init)[e.dst], e.dst, mem}); + res_dst = gs.first; + // And add it to the "tree" used to find a compatible state + if constexpr (!is_tar) + { + if (need_tree && gs.second) + s2l.add_new_path(e.dst, mem, res_dst, nb_seen); + } + } + + // We compute the color assigned to the new edge. + acc_cond::mark_t new_edge_color{}; + compute_new_color_lar(sub_aut, current_mem, mem, h, e.acc, + new_edge_color, pairs, acc_cache); + + // As we can assign a new destination later when + // use_last_post_process is true, we cannot try to find a compatible + // edge. + auto edge_res_num = add_res_edge(res_current, res_dst, + new_edge_color, e.cond, + !use_last_post_process, + edge_cache); + (void) edge_res_num; + // We have to remember how many colors were seen if we do a post + // processing + if constexpr (algo != TAR) + if (use_last_post_process) + { + assert(edge_res_num == + edge_to_seen_nb.size() + nb_edges_before + 1); + edge_to_seen_nb.push_back(nb_seen); + } + } + } + + // We used the most recent compatible state but perhaps that another + // state was created after. We do a new search. As TAR always moves one + // element we don't need it. + if constexpr (algo != TAR) + if (use_last_post_process) + { + for (auto &res_state : states_scc_res) + for (auto &e : res_->out(res_state)) + { + auto e_dst = e.dst; + if (e.src == e_dst) + continue; + auto edge_num = res_->edge_number(e); + const auto &ps = num_2_ps[e_dst - nb_states_before]; + unsigned seen_nb = + edge_to_seen_nb[edge_num - nb_edges_before - 1]; + assert(seen_nb < SPOT_MAX_ACCSETS); + auto new_dst = s2l.get_compatible_state(ps.state_scc, ps.mem, + seen_nb, true); + if (new_dst != e_dst) + { + assert(new_dst != -1U); + need_purge_ = true; + e.dst = new_dst; + } + } + } + if (use_bscc) + { + // Contrary to the (old) implementation of IAR, adding an edge between + // 2 SCCs of the result is the last thing done. It means that + // we don't need to use a filter when we compute the BSCC. + // A state s is in the BSCC if scc_of(s) is 0. + scc_info sub_scc(res_, init_res, nullptr, nullptr, + scc_info_options::NONE); + if (sub_scc.scc_count() > 1) + { + need_purge_ = true; + for (auto &state_produced : states_scc_res) + if (sub_scc.scc_of(state_produced) == 0) + state_to_res_[res_to_aut_[state_produced]] = state_produced; + } + } + delete edge_cache; + } + + void + link_sccs() + { + if (si_.scc_count() > 1) + { + const unsigned res_num_states = res_->num_states(); + for (unsigned i = 0; i < res_num_states; ++i) + { + auto aut_i = res_to_aut_[i]; + auto aut_i_scc = si_.scc_of(aut_i); + for (auto &e : aut_->out(aut_i)) + if (aut_i_scc != si_.scc_of(e.dst)) + { + auto e_dst_repr = state_to_res_[e.dst]; + add_res_edge(i, e_dst_repr, {}, e.cond); + } + } + } + } + + bool + try_parity_equivalence(const zielonka_tree &tree, + const twa_graph_ptr &sub_aut) + { + if (tree.has_parity_shape()) + { + bool first_is_accepting = tree.is_even(); + // A vector that stores the difference between 2 levels. + std::vector colors_diff; + auto &tree_nodes = tree.nodes_; + // Supposes that the index of the root is 0. + unsigned current_index = 0; + auto current_node = tree_nodes[current_index]; + // While the current node has a child + while (current_node.first_child != 0) + { + auto child_index = current_node.first_child; + auto child = tree_nodes[child_index]; + acc_cond::mark_t diff = current_node.colors - child.colors; + colors_diff.emplace_back(diff); + current_node = child; + } + // We have to deal with the edge between the last node and ∅. + bool is_empty_accepting = sub_aut->acc().accepting({}); + bool is_current_accepting = (current_node.level % 2) != tree.is_even(); + if (is_empty_accepting != is_current_accepting) + colors_diff.emplace_back(current_node.colors); + // + 1 as we need to know which value should be given to an uncolored + // edge. + std::vector new_colors( + sub_aut->get_acceptance().used_sets().max_set() + 1, -1U); + unsigned current_col = colors_diff.size() - 1; + for (auto &diff : colors_diff) + { + for (auto col : diff.sets()) + new_colors[col + 1] = current_col; + --current_col; + } + bool is_max_even = first_is_accepting == (colors_diff.size() % 2); + if (!is_max_even) + change_to_odd(); + + bool is_even_in_odd_world = is_odd_ && is_max_even; + if (is_even_in_odd_world) + for (auto &x : new_colors) + ++x; + apply_copy(sub_aut, new_colors, PARITY_EQUIV); + return true; + } + return false; + } + + bool + try_parity_prefix(const zielonka_tree &tree, const twa_graph_ptr &sub_aut) + { + unsigned index = 0; + auto current = tree.nodes_[index]; + std::vector prefixes; + bool first_is_accepting = tree.is_even(); + + acc_cond::mark_t removed_cols{}; + auto has_one_child = [&](const auto node) constexpr + { + auto fc = node.first_child; + return tree.nodes_[fc].next_sibling == fc; + }; + while (has_one_child(current)) + { + auto child = tree.nodes_[current.first_child]; + acc_cond::mark_t diff{}; + const bool is_leaf = current.first_child == 0; + if (is_leaf) + diff = current.colors; + else + diff = current.colors - child.colors; + prefixes.emplace_back(diff); + removed_cols |= diff; + if (is_leaf) + break; + current = child; + } + if (prefixes.empty()) + return false; + + if (opt_.datas) + algo_used_ |= algorithm::PARITY_PREFIX; + + // As we want to remove the prefix we need to remove it from the + // condition. As an unused color is not always removed (acc_clean false), + // we do it here. + auto used_cols = sub_aut->get_acceptance().used_sets() - removed_cols; + auto new_cond = sub_aut->acc().restrict_to(used_cols); + scc_info_to_parity sub(sub_aut, removed_cols); + // The recursive call will add some informations to help + // to add missing edges + state_to_nums_ = + new std::vector>(aut_->num_states()); + opt_.parity_prefix = false; + bool old_pp_gen = opt_.parity_prefix_general; + opt_.parity_prefix_general = false; + + auto max_scc_color_rec = max_color_scc_; + for (auto x : sub.split_aut({removed_cols})) + { + x->set_acceptance(new_cond); + process_scc(x, algorithm::PARITY_PREFIX); + if (max_color_scc_.has_value()) + { + if (!max_scc_color_rec.has_value()) + max_scc_color_rec.emplace(*max_color_scc_); + else + max_scc_color_rec.emplace( + std::max(*max_scc_color_rec, *max_color_scc_)); + } + } + opt_.parity_prefix = true; + opt_.parity_prefix_general = old_pp_gen; + + assert(max_scc_color_rec.has_value()); + auto max_used_is_accepting = ((*max_scc_color_rec - 1) % 2) == is_odd_; + bool last_prefix_acc = (prefixes.size() % 2) != first_is_accepting; + + unsigned m = prefixes.size() + (max_used_is_accepting != last_prefix_acc) + + *max_scc_color_rec - 1; + auto sub_aut_orig = + sub_aut->get_named_prop>("original-states"); + assert(sub_aut_orig); + for (auto &e : sub_aut->edges()) + if (e.acc & removed_cols) + { + auto el = std::find_if(prefixes.begin(), prefixes.end(), + [&](acc_cond::mark_t &x) + { return x & e.acc; }); + assert(el != prefixes.end()); + unsigned pos = std::distance(prefixes.begin(), el); + const unsigned col = m - pos; + // As it is a parity prefix we should never get a lower value than + // the color recursively produced. + assert(!max_scc_color_rec.has_value() || *max_scc_color_rec == 0 + || col + 1 > *max_scc_color_rec); + unsigned dst = state_to_res_[(*sub_aut_orig)[e.dst]]; + for (auto src : (*state_to_nums_)[(*sub_aut_orig)[e.src]]) + if (col != -1U) + add_res_edge(src, dst, {col}, e.cond); + else + add_res_edge(src, dst, {}, e.cond); + } + // As when we need to use link_scc, a set of edges that link 2 SCC + // need to be added and don't need to have a color. + else if (sub.scc_of(e.src) != sub.scc_of(e.dst)) + { + unsigned dst = state_to_res_[(*sub_aut_orig)[e.dst]]; + for (auto src : (*state_to_nums_)[(*sub_aut_orig)[e.src]]) + add_res_edge(src, dst, {}, e.cond); + } + delete state_to_nums_; + state_to_nums_ = nullptr; + + return true; + } + + bool + try_parity_prefix_general(twa_graph_ptr &sub_aut) + { + // This function should not be applied on an "empty" automaton as + // it must create an empty SCC with the algorithm NONE. + assert(sub_aut->num_edges() > 0); + static_assert((MAX_ACCSETS % 2) == 0, + "MAX_ACCSETS is supposed to be even"); + std::vector res_colors; + std::vector status; + acc_cond new_cond; + bool was_able_to_color; + // Is the maximal color accepting? + bool start_inf = true; + cond_type_main_aux(sub_aut, cond_kind::INF_PARITY, false, status, + res_colors, new_cond, was_able_to_color); + // Otherwise we can try to find a rejecting transition as first step + if (!was_able_to_color) + { + cond_type_main_aux(sub_aut, cond_kind::FIN_PARITY, false, status, + res_colors, new_cond, was_able_to_color); + if (!was_able_to_color) + return false; + start_inf = false; + } + + // If we have a parity-type automaton, it is just a copy. + if (std::find(status.begin(), status.end(), edge_status::IMPOSSIBLE) + == status.end()) + { + std::vector res_cols; + res_cols.reserve(res_colors.size()); + + auto min_set = + std::min_element(res_colors.begin() + 1, res_colors.end())->max_set(); + // Does the minimal color has the same parity than the maximal parity? + bool same_acceptance_min_max = (min_set % 2); + // Do we need to shift to match the parity of res_? + bool odd_shift = start_inf != is_odd_; + unsigned shift_col = min_set - (same_acceptance_min_max != odd_shift); + std::transform(res_colors.begin(), res_colors.end(), + std::back_inserter(res_cols), [&](auto &x) + { return x.max_set() - 1 - shift_col; }); + apply_copy_edge_index(sub_aut, res_cols, + algorithm::PARITY_PREFIX_GENERAL); + return true; + } + + // At this moment, a prefix exists + auto& ev = sub_aut->edge_vector(); + const auto ev_size = ev.size(); + auto keep = std::shared_ptr(make_bitvect(ev_size)); + const unsigned status_size = status.size(); + for (unsigned i = 1; i < status_size; ++i) + if (status[i] == edge_status::IMPOSSIBLE) + keep->set(i); + else + keep->clear(i); + + // Avoid recursive parity prefix + opt_.parity_prefix_general = false; + bool old_pp = opt_.parity_prefix; + opt_.parity_prefix = false; + + auto max_scc_color_rec = max_color_scc_; + scc_info lower_scc(sub_aut, scc_info_options::TRACK_STATES); + scc_info_to_parity sub(lower_scc, keep); + state_to_nums_ = + new std::vector>(aut_->num_states()); + for (auto x : sub.split_aut(keep)) + { + process_scc(x, algorithm::PARITY_PREFIX_GENERAL); + if (!max_scc_color_rec.has_value()) + max_scc_color_rec = max_color_scc_; + else if (max_color_scc_.has_value()) + max_scc_color_rec.emplace( + std::max(*max_scc_color_rec, *max_color_scc_)); + } + + // restore options + opt_.parity_prefix_general = true; + opt_.parity_prefix = old_pp; + + assert(sub_aut->num_edges() > 0); + + // Compute the minimal color used by parity prefix. + unsigned min_set_prefix = -2U; + for (unsigned i = 1; i < ev_size; ++i) + if (status[i] == edge_status::MARKED) + { + auto e_mark = res_colors[i].max_set(); + if (min_set_prefix == -2U) + min_set_prefix = e_mark - 1; + else + min_set_prefix = std::min(min_set_prefix + 1, e_mark) - 1; + } + + // At least one transition should be marked here. + assert(min_set_prefix != -2U); + + // Reduce the colors used by parity_prefix. + const bool min_prefix_accepting = (min_set_prefix % 2) == start_inf; + // max_scc_color_rec has a value as the automaton is not parity-type, + // so there was a recursive paritisation + assert(max_scc_color_rec.has_value()); + const bool max_rec_accepting = ((*max_scc_color_rec - 1) % 2) == is_odd_; + const bool same_prio = min_prefix_accepting == max_rec_accepting; + const unsigned delta = + min_set_prefix - (*max_scc_color_rec + 1) - !same_prio; + + auto sub_aut_orig = + sub_aut->get_named_prop>("original-states"); + assert(sub_aut_orig); + for (unsigned e_num = 1; e_num < ev_size; ++e_num) + { + auto& e = ev[e_num]; + if (status[e_num] == edge_status::MARKED) + { + unsigned dst = state_to_res_[(*sub_aut_orig)[e.dst]]; + for (auto src : (*state_to_nums_)[(*sub_aut_orig)[e.src]]) + { + auto col = res_colors[e_num].max_set() - delta - 1; + if (col == -1U) + add_res_edge(src, dst, {}, e.cond); + else + add_res_edge(src, dst, {col}, e.cond); + } + } + } + + delete state_to_nums_; + state_to_nums_ = nullptr; + + return true; + } + + bool + try_emptiness(const const_twa_graph_ptr &sub_aut, bool &tried) + { + tried = true; + if (generic_emptiness_check(sub_aut)) + { + auto col_fun = + [col = is_odd_ ? acc_cond::mark_t{0} : acc_cond::mark_t{}] + (const twa_graph::edge_storage_t &) noexcept + { + return col; + }; + apply_copy_general(sub_aut, col_fun, GENERIC_EMPTINESS); + return true; + } + return false; + } + + bool + try_rabin_to_buchi(twa_graph_ptr &sub_aut) + { + algorithm algo = RABIN_TO_BUCHI; + auto buch_aut = rabin_to_buchi_if_realizable(sub_aut); + if (buch_aut == nullptr) + { + algo = STREETT_TO_COBUCHI; + auto old_cond = sub_aut->get_acceptance(); + sub_aut->set_acceptance(acc_cond(old_cond.complement())); + buch_aut = rabin_to_buchi_if_realizable(sub_aut); + sub_aut->set_acceptance(acc_cond(old_cond)); + } + if (buch_aut != nullptr) + { + if (algo == STREETT_TO_COBUCHI) + change_to_odd(); + unsigned shift = (algo == RABIN_TO_BUCHI) && is_odd_; + + auto &buch_aut_ev = buch_aut->edge_vector(); + // 0 is not an edge, so we assign -1; + std::vector colors; + colors.reserve(buch_aut_ev.size()); + colors.push_back(-1U); + std::transform( + buch_aut_ev.begin() + 1, buch_aut_ev.end(), + std::back_inserter(colors), + [&](const twa_graph::edge_storage_t &e) { + return e.acc.max_set() - 1 + shift; + }); + apply_copy_edge_index(sub_aut, colors, algo); + return true; + } + return false; + } + + bool + try_buchi_type(const twa_graph_ptr &sub_aut) + { + std::vector status; + std::vector res_colors; + acc_cond new_cond; + bool is_co_bu = false; + bool was_able_to_color; + if (!cond_type_main_aux(sub_aut, cond_kind::BUCHI, true, status, + res_colors, new_cond, was_able_to_color)) + { + is_co_bu = true; + if (!cond_type_main_aux(sub_aut, cond_kind::CO_BUCHI, true, status, + res_colors, new_cond, was_able_to_color)) + return false; + change_to_odd(); + } + // Tests if all edges are colored or all edges are uncolored + auto [min, max] = + std::minmax_element(res_colors.begin() + 1, res_colors.end()); + const bool one_color = min->max_set() == max->max_set(); + const bool is_colored = min->max_set(); + auto col_fun = [&](const twa_graph::edge_storage_t &edge) + { + // If there one color in the automaton, we can simplify. + if (one_color) + { + bool z = (is_colored && !is_odd_) || (!is_colored && is_odd_); + // When we do co-buchi, we reverse + if (is_co_bu) + z = !z; + return z ? acc_cond::mark_t{0} : acc_cond::mark_t{}; + } + // Otherwise, copy the color + auto edge_number = sub_aut->edge_number(edge); + unsigned mc = res_colors[edge_number].max_set() - 1; + mc += (!is_co_bu && is_odd_); + if (mc == -1U) + return acc_cond::mark_t{}; + return acc_cond::mark_t{mc}; + }; + apply_copy_general(sub_aut, col_fun, is_co_bu ? algorithm::CO_BUCHI_TYPE + : algorithm::BUCHI_TYPE); + return true; + } + + bool + try_parity_type(const twa_graph_ptr &sub_aut) + { + std::vector status; + std::vector res_colors; + acc_cond new_cond; + bool was_able_to_color; + if (!cond_type_main_aux(sub_aut, cond_kind::INF_PARITY, true, status, + res_colors, new_cond, was_able_to_color)) + { + if (!cond_type_main_aux(sub_aut, cond_kind::FIN_PARITY, true, status, + res_colors, new_cond, was_able_to_color)) + return false; + } + bool is_max, is_odd; + new_cond.is_parity(is_max, is_odd); + auto [min, max] = + std::minmax_element(res_colors.begin() + 1, res_colors.end()); + // cond_type_main_aux returns a parity max condition + assert(is_max); + auto col_fun = + [shift = (is_odd != is_odd_) - (min->max_set() + (min->max_set() % 2)), + &res_colors, &sub_aut] + (const twa_graph::edge_storage_t &edge) + { + auto edge_number = sub_aut->edge_number(edge); + unsigned mc = res_colors[edge_number].max_set() - 1; + mc += shift; + if (mc == -1U) + return acc_cond::mark_t{}; + return acc_cond::mark_t{mc}; + }; + apply_copy_general(sub_aut, col_fun, PARITY_TYPE); + return true; + } + + // Keeps the result of the partial degeneralization if it reduces the number + // of colors or it allows to apply IAR. + bool + keep_deg(const const_twa_graph_ptr &sub_aut, const const_twa_graph_ptr °) + { + if (!opt_.reduce_col_deg) + return true; + unsigned nb_col_orig = sub_aut->get_acceptance().used_sets().count(); + + if (deg->get_acceptance().used_sets().count() < nb_col_orig) + return true; + std::vector pairs; + if (deg->acc().is_rabin_like(pairs)) + { + remove_duplicates(pairs); + if (pairs.size() < nb_col_orig) + return true; + } + if (deg->acc().is_streett_like(pairs)) + { + remove_duplicates(pairs); + if (pairs.size() < nb_col_orig) + return true; + } + return false; + } + + // Process a SCC. If there is no edge in the automaton, a new state is + // created and we say (if pretty_print is true) that none_algo created + // this state. + void + process_scc(twa_graph_ptr &sub_aut, + const algorithm none_algo = algorithm::NONE) + { + // Init the maximal color produced when processing this SCC. + max_color_scc_.reset(); + // If the sub_automaton is "empty", we don't need to apply an algorithm. + if (sub_aut->num_edges() == 0) + { + apply_copy(sub_aut, {}, none_algo); + return; + } + + bool tried_emptiness = false; + bool changed_structure = true; + while (true) + { + auto cond_before_simpl = sub_aut->acc(); + if (opt_.acc_clean) + simplify_acceptance_here(sub_aut); + if (opt_.propagate_col) + { + propagate_marks_here(sub_aut); + if (opt_.acc_clean) + simplify_acceptance_here(sub_aut); + } + if (opt_.datas && sub_aut->acc() != cond_before_simpl) + algo_used_ |= algorithm::ACC_CLEAN; + + if (opt_.parity_equiv || opt_.parity_prefix) + { + // If we don't try to find a parity prefix, we can stop + // to construct the tree when it has not parity shape. + zielonka_tree_options zopt = zielonka_tree_options::MERGE_SUBTREES + | zielonka_tree_options::CHECK_PARITY; + if (!opt_.parity_prefix) + zopt = zopt | zielonka_tree_options::ABORT_WRONG_SHAPE; + auto tree = zielonka_tree(sub_aut->acc(), zopt); + // If it is not parity shape, tree.nodes_ will be empty + if (tree.num_branches() != 0 && opt_.parity_equiv + && try_parity_equivalence(tree, sub_aut)) + return; + if (opt_.parity_prefix && try_parity_prefix(tree, sub_aut)) + return; + } + + if (changed_structure && opt_.parity_prefix_general + && try_parity_prefix_general(sub_aut)) + return; + + if (opt_.generic_emptiness && !tried_emptiness + && try_emptiness(sub_aut, tried_emptiness)) + return; + + // Buchi_type_to_buchi is more general that Rabin_to_buchi so + // we just call rabin_to_buchi if buchi_type_to_buchi is false. + if (!opt_.buchi_type_to_buchi && !opt_.parity_type_to_parity + && opt_.rabin_to_buchi + && try_rabin_to_buchi(sub_aut)) + return; + + // As parity_type_to_parity is stronger, we don't + // try if this option is used. + if (opt_.buchi_type_to_buchi && !opt_.parity_type_to_parity + && try_buchi_type(sub_aut)) + return; + + // We don't do it if parity_prefix_general is true as on a parity-type + // automaton parity_prefix_general removes all the transitions and + // we also get a parity-type automaton. + if (!opt_.parity_prefix_general && opt_.parity_type_to_parity + && try_parity_type(sub_aut)) + return; + + if (opt_.partial_degen + && is_partially_degeneralizable(sub_aut, true, true)) + { + auto deg = sub_aut; + std::vector forbid; + auto m = is_partially_degeneralizable(sub_aut, true, true, forbid); + bool changed = false; + while (m) + { + auto tmp = partial_degeneralize(deg, m); + simplify_acceptance_here(tmp); + if (keep_deg(deg, tmp)) + { + algo_used_ |= algorithm::PARTIAL_DEGEN; + deg = tmp; + changed = true; + changed_structure = true; + } + else + forbid.emplace_back(m); + m = is_partially_degeneralizable(deg, true, true, forbid); + } + + if (changed) + { + sub_aut = deg; + continue; + } + } + break; + } + if (opt_.use_generalized_rabin) + { + auto gen_rab = to_generalized_rabin(sub_aut); + // to_generalized_rabin does not propagate original-states. + auto sub_aut_orig = + sub_aut->get_named_prop>("original-states"); + assert(sub_aut_orig); + auto orig = new std::vector(); + const auto sub_aut_num_states = sub_aut->num_states(); + orig->reserve(sub_aut_num_states); + gen_rab->set_named_prop("original-states", orig); + for (unsigned i = 0; i < sub_aut_num_states; ++i) + orig->push_back((*sub_aut_orig)[i]); + sub_aut = partial_degeneralize(gen_rab); + } + std::vector pairs; + algorithm algo = choose_lar(sub_aut->acc(), pairs, sub_aut->num_edges()); + if (opt_.datas) + algo_used_ |= algo; + if (algo == CAR) + apply_lar(sub_aut, pairs); + else if (algo == IAR_STREETT) + apply_lar(sub_aut, pairs); + else if (algo == IAR_RABIN) + apply_lar(sub_aut, pairs); + else if (algo == TAR) + apply_lar(sub_aut, pairs); + else + SPOT_UNREACHABLE(); + } + + public: + twa_graph_ptr + run() + { + res_ = make_twa_graph(aut_->get_dict()); + res_->copy_ap_of(aut_); + const unsigned num_scc = si_.scc_count(); + auto orig_aut = + aut_->get_named_prop>("original-states"); + std::optional> orig_st; + if (orig_aut) + { + orig_st.emplace(std::vector{*orig_aut}); + std::const_pointer_cast(aut_) + ->set_named_prop("original-states", nullptr); + } + auto sccs = si_.split_aut(); + for (unsigned scc = 0; scc < num_scc; ++scc) + { + auto sub_automaton = sccs[scc]; + process_scc(sub_automaton); + } + + link_sccs(); + // During the execution, to_parity works on its own + // original-states and we must combine it with the property original + // states of aut_ to propagate the information. + if (orig_st) + for (unsigned i = 0; i < orig_->size(); ++i) + (*orig_)[i] = (*orig_aut)[(*orig_)[i]]; + res_->set_named_prop("original-states", orig_); + if (opt_.pretty_print) + res_->set_named_prop("state-names", names_); + if (res_->num_states() == 0) + add_res_state(NONE, {0, 0, {}}); + res_->set_init_state(state_to_res_[aut_->get_init_state_number()]); + // There is only a subset of algorithm that can create an unreachable + // state + if (need_purge_) + res_->purge_unreachable_states(); + // A special case is an automaton without edge. It implies + // max_color_used_ has not value so we need to test it. + if (!max_color_used_.has_value()) + { + assert(aut_->num_edges() == 0); + res_->set_acceptance(acc_cond(acc_cond::acc_code::f())); + } + else + { + res_->set_acceptance(acc_cond( + acc_cond::acc_code::parity(true, is_odd_, *max_color_used_))); + } + if (opt_.datas) + { + constexpr std::array + algos = {BUCHI_TYPE, CAR, CO_BUCHI_TYPE, GENERIC_EMPTINESS, IAR_RABIN, + IAR_STREETT, NONE, PARITY_EQUIV, PARITY_PREFIX, + PARITY_PREFIX_GENERAL, PARITY_TYPE, RABIN_TO_BUCHI, + STREETT_TO_COBUCHI, TAR}; + for (auto al : algos) + if (algo_used_ & al) + opt_.datas->algorithms_used.emplace_back(algorithm_to_str(al)); + } + return res_; + } + + to_parity_generator(const const_twa_graph_ptr &aut, + const to_parity_options opt) + : aut_(aut), + opt_(opt), + si_(aut), + state_to_res_(aut->num_states(), -1U) + { + auto aut_num = aut->num_states(); + res_to_aut_.reserve(aut_num); + orig_ = new std::vector(); + orig_->reserve(aut_num); + if (opt.pretty_print) + { + names_ = new std::vector(); + names_->reserve(aut_num); + } + } + }; + + twa_graph_ptr + to_parity(const const_twa_graph_ptr &aut, + const to_parity_options options) + { + bool is_max, is_odd; + if (aut->acc().is_parity(is_max, is_odd, false)) + { + if (!is_max) + return change_parity(aut, parity_kind::parity_kind_max, + parity_style::parity_style_any); + else + { + auto res = make_twa_graph(aut, twa::prop_set::all()); + res->copy_acceptance_of(aut); + return res; + } + } + to_parity_generator gen(aut, options); + return gen.run(); + } + + // Old version of CAR + namespace { + struct lar_state + { + unsigned state; + std::vector perm; + bool operator<(const lar_state &s) const + { + return state == s.state ? perm < s.perm : state < s.state; + } + + std::string to_string() const + { + std::ostringstream s; + s << state << " ["; + unsigned ps = perm.size(); + for (unsigned i = 0; i < ps; ++i) + { + if (i > 0) + s << ','; + s << perm[i]; + } + s << ']'; + return s.str(); + } + }; + + class lar_generator + { + const const_twa_graph_ptr &aut_; + twa_graph_ptr res_; + const bool pretty_print; + + std::map lar2num; + + public: + explicit lar_generator(const const_twa_graph_ptr &a, bool pretty_print) + : aut_(a), res_(nullptr), pretty_print(pretty_print) + { + } + + twa_graph_ptr run() + { + res_ = make_twa_graph(aut_->get_dict()); + res_->copy_ap_of(aut_); + + std::deque todo; + auto get_state = [this, &todo](const lar_state &s) + { + auto it = lar2num.emplace(s, -1U); + if (it.second) // insertion took place + { + unsigned nb = res_->new_state(); + it.first->second = nb; + todo.push_back(s); + } + return it.first->second; + }; + + std::vector initial_perm(aut_->num_sets()); + std::iota(initial_perm.begin(), initial_perm.end(), 0); + { + lar_state s0{aut_->get_init_state_number(), initial_perm}; + res_->set_init_state(get_state(s0)); + } + + scc_info si(aut_, scc_info_options::NONE); + // main loop + while (!todo.empty()) + { + lar_state current = todo.front(); + todo.pop_front(); + + // TODO: todo could store this number to avoid one lookup + unsigned src_num = get_state(current); + + unsigned source_scc = si.scc_of(current.state); + for (const auto &e : aut_->out(current.state)) + { + // find the new permutation + std::vector new_perm = current.perm; + unsigned h = 0; + for (unsigned k : e.acc.sets()) + { + auto it = std::find(new_perm.begin(), new_perm.end(), k); + h = std::max(h, unsigned(new_perm.end() - it)); + std::rotate(it, it + 1, new_perm.end()); + } + + if (source_scc != si.scc_of(e.dst)) + { + new_perm = initial_perm; + h = 0; + } + + lar_state dst{e.dst, new_perm}; + unsigned dst_num = get_state(dst); + + // Do the h last elements satisfy the acceptance condition? + // If they do, emit 2h, if they don't emit 2h+1. + acc_cond::mark_t m(new_perm.end() - h, new_perm.end()); + bool rej = !aut_->acc().accepting(m); + res_->new_edge(src_num, dst_num, e.cond, {2 * h + rej}); + } + } + + // parity max even + unsigned sets = 2 * aut_->num_sets() + 2; + res_->set_acceptance(sets, acc_cond::acc_code::parity_max_even(sets)); + + if (pretty_print) + { + auto names = new std::vector(res_->num_states()); + for (const auto &p : lar2num) + (*names)[p.second] = p.first.to_string(); + res_->set_named_prop("state-names", names); + } + + return res_; + } + }; + } + + twa_graph_ptr + 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"); + // if aut is already parity return it as is + if (aut->acc().is_parity()) + return std::const_pointer_cast(aut); + + lar_generator gen(aut, pretty_print); + return gen.run(); + } + + // Old version of IAR + + namespace + { using perm_t = std::vector; struct iar_state { @@ -326,18 +2622,18 @@ namespace spot perm_t perm; bool - operator<(const iar_state& other) const + operator<(const iar_state &other) const { return state == other.state ? perm < other.perm : state < other.state; } }; - template + 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& + const acc_cond::mark_t & fin(unsigned k) const { if (is_rabin) @@ -353,16 +2649,15 @@ namespace spot else return pairs_[k].fin; } + public: - explicit iar_generator(const const_twa_graph_ptr& a, - const std::vector& p, + 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) - {} + : aut_(a), pairs_(p), scc_(scc_info(a)), pretty_print_(pretty_print), + state2pos_iar_states(aut_->num_states(), -1U) + { + } twa_graph_ptr run() @@ -386,9 +2681,6 @@ namespace spot 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(); @@ -396,13 +2688,13 @@ namespace spot for (auto e : res_->edges()) { unsigned s = e.src; - iar_state iar = num2iar.at(s); + iar_state iar = num2iar[s]; std::ostringstream st; st << iar.state << ' '; if (iar.perm.empty()) st << '['; char sep = '['; - for (unsigned h: iar.perm) + for (unsigned h : iar.perm) { st << sep << h; sep = ','; @@ -413,6 +2705,8 @@ namespace spot res_->set_named_prop("state-names", names); } + // there could be quite a number of unreachable states, prune them + res_->purge_unreachable_states(); return res_; } @@ -423,44 +2717,44 @@ namespace spot unsigned init = scc_.one_state_of(scc_num); std::deque todo; - auto get_state = [&](const iar_state& s) + auto get_state = [&](const iar_state &s) + { + auto it = iar2num.find(s); + if (it == iar2num.end()) { - 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({s, old_newest_pos}); - todo.push_back(s); - return nb; - } - return it->second; - }; + 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({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)); - }; + { + 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; - } + { + 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); @@ -478,109 +2772,110 @@ namespace spot // 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)) { - iar_state current = todo.front(); - todo.pop_front(); + // 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); + } - unsigned src_num = get_state(current); + iar_state dst; + unsigned dst_num = -1U; - for (const auto& e : aut_->out(current.state)) + // 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) { - // 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); - } + 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.set(0); + else if (e.acc & fin(current.perm[maxint])) + assign_color(acc, 2 * maxint + 2); + else + assign_color(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&, + auto leaving_edge = [&](unsigned d) constexpr + { + 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); + void *filter_data) constexpr + { + 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; - }; + 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. + // 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( @@ -590,23 +2885,23 @@ namespace spot if (sub_scc.succ(s).empty()) return false; return true; - } ()); + }()); assert(sub_scc.states_of(bscc).size() - >= scc_.states_of(scc_num).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; - } + { + 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 const_twa_graph_ptr &aut_; + const std::vector &pairs_; const scc_info scc_; twa_graph_ptr res_; bool pretty_print_; @@ -625,1520 +2920,36 @@ namespace spot // Make this a function different from iar_maybe(), so that // iar() does not have to call a deprecated function. static twa_graph_ptr - iar_maybe_(const const_twa_graph_ptr& aut, bool pretty_print) + 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); + 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_maybe(const const_twa_graph_ptr& aut, bool pretty_print) - { - return iar_maybe_(aut, pretty_print); - } - - twa_graph_ptr - iar(const const_twa_graph_ptr& aut, bool pretty_print) + 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"); } -// 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); - } - } - - node* - get_sub_tree(const std::vector& elements, int pos) - { - if (pos < 0) - return this; - unsigned lab = elements[pos]; - auto child = std::find_if(children.begin(), children.end(), - [lab](node* n){ - return n->label == lab; - }); - assert(child != children.end()); - return (*child)->get_sub_tree(elements, pos - 1); - } - - // 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()){ -} - -// Try to find a state compatible with the permu when seen_nb colors are -// moved. If use_last is true, it return the last created compatible state. -// If it is false, it returns the oldest. -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); -} - -node* -get_sub_tree(const std::vector& elements, unsigned state) -{ - return nodes[state].get_sub_tree(elements, elements.size() - 1); -} -}; - -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; -} - -// Gives for each state a set of marks incoming to this state. -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.has_many()) - inputs[e.dst].insert(elements); - } - return inputs; -} - -// Gives for each state a set of pairs incoming to this state. -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; -} -// Give an order from the set of marks -std::vector -group_to_vector(const std::set& group) -{ - // In this function, we have for example the marks {1, 2}, {1, 2, 3}, {2} - // A compatible order is [2, 1, 3] - std::vector group_vect(group.begin(), group.end()); - - // We sort the elements by inclusion. This function is called on a - // set of marks such that each mark is included or includes the others. - std::sort(group_vect.begin(), group_vect.end(), - [](const acc_cond::mark_t left, const acc_cond::mark_t right) - { - return (left != right) && ((left & right) == left); - }); - // At this moment, we have the vector [{2}, {1, 2}, {1, 2, 3}]. - // In order to create the order, we add the elements of the first element. - // Then we add the elements of the second mark (without duplication), etc. - 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; -} - -// Give an order from the set of indices of pairs -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 (right != left) - && 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; -} - -// Give a correspondance between a mark and an order for CAR -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({mark, new_vector}); - } - return result; -} - -// Give a correspondance between a mark and an order for IAR -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({vect, new_vector}); - } - return result; -} - -// Give for each state the correspondance between a mark and an order (CAR) -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) - result.push_back(get_groups(inputs[state])); - return result; -} - -// Give for each state the correspondance between a mark and an order (IAR) -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) - result.push_back(get_groups_iar(inputs[state])); - return result; -} - -public: -explicit car_generator(const const_twa_graph_ptr &a, to_parity_options options) - : aut_(a) - , scc_(scc_info(a)) - , is_odd(false) - , options(options) -{ - if (options.pretty_print) - names = new std::vector(); - else - names = nullptr; -} - -// During the creation of the states, we had to choose between a set of -// compatible states. But it is possible to create another compatible state -// after. This function checks if a compatible state was created after and -// use it. -void -change_transitions_destination(twa_graph_ptr& aut, -const std::vector& states, -std::map>& partial_history, -state_2_car_scc& state_2_car) -{ - for (auto s : states) - for (auto& edge : aut->out(s)) - { - unsigned - src = edge.src, - dst = edge.dst; - // We don't change loops - if (src == dst) - continue; - unsigned dst_scc = num2car[dst].state_scc; - auto cant_change = partial_history[aut->edge_number(edge)]; - edge.dst = state_2_car.get_sub_tree(cant_change, dst_scc) - ->get_end(true); - } -} - -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) - { - 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)) - { - auto col = is_true ^ !is_odd; - if (((unsigned)col) > max_free_color) - throw std::runtime_error("CAR needs more sets"); - 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(); -} - -// Create a permutation for the first state of a SCC (IAR) -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); - // For each edge e of res_, we store the elements of the permutation - // that are not moved, and we respect the order. - std::map> edge_to_colors; - 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); - } - - std::vector not_moved(new_perm.begin() + seen_nb, - new_perm.end()); - - 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; - } - } - auto new_e = res_->new_edge(src_num, dst_num, e.cond, { acc_col }); - edge_to_colors.insert({new_e, not_moved}); - } - } - if (options.search_ex && options.use_last) - { - std::vector added_states; - std::transform(car2num_local.begin(), car2num_local.end(), - std::back_inserter(added_states), - [](std::pair pair) { - return pair.second; - }); - change_transitions_destination( - res_, added_states, edge_to_colors, state_2_car); - } - 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, - - SPOT_MAX_ACCSETS - 2); - 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); - if (deg != 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; - // We try with and without degeneralization and we keep the best. - 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; - } - if (!options.force_degen || !has_degeneralized) - 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_ptr = state2car.find(initial_state); - car_state initial_car; - // If we take an automaton with one state and without transition, - // the SCC was useless so state2car doesn't have initial_state - if (initial_car_ptr == state2car.end()) - { - assert(res_->num_states() == 0); - auto new_state = res_->new_state(); - car_state new_car = {initial_state, 0, perm_t()}; - state2car[initial_state] = new_car; - if (options.pretty_print) - names->push_back(new_car.to_string(None)); - num2car.insert(num2car.begin() + new_state, new_car); - car2num[new_car] = new_state; - initial_car = new_car; - } - else - initial_car = initial_car_ptr->second; - auto initial_state_res = car2num.find(initial_car); - if (initial_state_res != car2num.end()) - res_->set_init_state(initial_state_res->second); - else - res_->new_state(); - if (options.pretty_print) - res_->set_named_prop("state-names", names); - - res_->purge_unreachable_states(); - // If parity_prefix is used, we use all available colors by - // default: The IAR/CAR are using lower indices, and the prefix is - // using the upper indices. So we use reduce_parity() to clear - // the mess. If parity_prefix is not used, - unsigned max_color = SPOT_MAX_ACCSETS; - if (!options.parity_prefix) - { - acc_cond::mark_t all = {}; - for (auto& e: res_->edges()) - all |= e.acc; - max_color = all.max_set(); - } - res_->set_acceptance(acc_cond::acc_code::parity_max(is_odd, max_color)); - if (options.parity_prefix) - reduce_parity_here(res_); - return res_; -} - -private: -const const_twa_graph_ptr &aut_; -const scc_info scc_; -twa_graph_ptr res_; -// Says if we constructing an odd or even max -bool is_odd; - -std::vector num2car; -std::map state2car; -std::map car2num; - -to_parity_options options; - -std::vector* names; -}; // car_generator - -}// namespace - - -twa_graph_ptr -to_parity(const const_twa_graph_ptr &aut, const to_parity_options options) -{ - return car_generator(aut, options).run(); -} - - // Old version of CAR. - namespace - { - struct lar_state - { - unsigned state; - std::vector perm; - - bool operator<(const lar_state& s) const - { - return state == s.state ? perm < s.perm : state < s.state; - } - - std::string to_string() const - { - std::stringstream s; - s << state << " ["; - unsigned ps = perm.size(); - for (unsigned i = 0; i != ps; ++i) - { - if (i > 0) - s << ','; - s << perm[i]; - } - s << ']'; - return s.str(); - } - }; - - class lar_generator - { - const const_twa_graph_ptr& aut_; - twa_graph_ptr res_; - const bool pretty_print; - - std::map lar2num; - public: - explicit lar_generator(const const_twa_graph_ptr& a, bool pretty_print) - : aut_(a) - , res_(nullptr) - , pretty_print(pretty_print) - {} - - twa_graph_ptr run() - { - res_ = make_twa_graph(aut_->get_dict()); - res_->copy_ap_of(aut_); - - std::deque todo; - auto get_state = [this, &todo](const lar_state& s) - { - auto it = lar2num.emplace(s, -1U); - if (it.second) // insertion took place - { - unsigned nb = res_->new_state(); - it.first->second = nb; - todo.push_back(s); - } - return it.first->second; - }; - - std::vector initial_perm(aut_->num_sets()); - std::iota(initial_perm.begin(), initial_perm.end(), 0); - { - lar_state s0{aut_->get_init_state_number(), initial_perm}; - res_->set_init_state(get_state(s0)); - } - - scc_info si(aut_, scc_info_options::NONE); - // main loop - while (!todo.empty()) - { - lar_state current = todo.front(); - todo.pop_front(); - - // TODO: todo could store this number to avoid one lookup - unsigned src_num = get_state(current); - - unsigned source_scc = si.scc_of(current.state); - for (const auto& e : aut_->out(current.state)) - { - // find the new permutation - std::vector new_perm = current.perm; - unsigned h = 0; - for (unsigned k : e.acc.sets()) - { - auto it = std::find(new_perm.begin(), new_perm.end(), k); - h = std::max(h, unsigned(new_perm.end() - it)); - std::rotate(it, it+1, new_perm.end()); - } - - if (source_scc != si.scc_of(e.dst)) - { - new_perm = initial_perm; - h = 0; - } - - lar_state dst{e.dst, new_perm}; - unsigned dst_num = get_state(dst); - - // Do the h last elements satisfy the acceptance condition? - // If they do, emit 2h, if they don't emit 2h+1. - acc_cond::mark_t m(new_perm.end() - h, new_perm.end()); - bool rej = !aut_->acc().accepting(m); - res_->new_edge(src_num, dst_num, e.cond, {2*h + rej}); - } - } - - // parity max even - unsigned sets = 2*aut_->num_sets() + 2; - res_->set_acceptance(sets, acc_cond::acc_code::parity_max_even(sets)); - - if (pretty_print) - { - auto names = new std::vector(res_->num_states()); - for (const auto& p : lar2num) - (*names)[p.second] = p.first.to_string(); - res_->set_named_prop("state-names", names); - } - - return res_; - } - }; - } - twa_graph_ptr - to_parity_old(const const_twa_graph_ptr& aut, bool pretty_print) + iar_maybe(const const_twa_graph_ptr &aut, bool pretty_print) { - if (!aut->is_existential()) - throw std::runtime_error("LAR does not handle alternation"); - // if aut is already parity return it as is - if (aut->acc().is_parity()) - return std::const_pointer_cast(aut); - - lar_generator gen(aut, pretty_print); - return gen.run(); + return iar_maybe_(aut, pretty_print); } - } diff --git a/spot/twaalgos/toparity.hh b/spot/twaalgos/toparity.hh index 6aecf7659..d82403aa5 100644 --- a/spot/twaalgos/toparity.hh +++ b/spot/twaalgos/toparity.hh @@ -19,10 +19,24 @@ #pragma once -#include +#include +#include +#include namespace spot { + /// Structure used by to_parity to store some information about the + /// construction + struct to_parity_data + { + /// Total number of states created + unsigned nb_states_created = 0; + /// Total number of edges created + unsigned nb_edges_created = 0; + /// Name of algorithms used + std::vector algorithms_used; + }; + /// \ingroup twa_acc_transform /// \brief Options to control various optimizations of to_parity(). struct to_parity_options @@ -35,6 +49,9 @@ namespace spot /// most recent state when we find multiple existing state /// compatible with the current move. bool use_last = true; + /// If \c use_last_post_process is true, then when LAR ends, it tries to + /// replace the destination of an edge by the newest compatible state. + bool use_last_post_process = false; /// If \c force_order is true, we force to use an order when CAR or IAR is /// applied. Given a state s and a set E ({0}, {0 1}, {2} for example) we /// construct an order on colors. With the given example, we ask to have @@ -45,16 +62,26 @@ namespace spot /// degeneralization to remove occurrences of acceptance /// subformulas such as `Fin(x) | Fin(y)` or `Inf(x) & Inf(y)`. bool partial_degen = true; - /// If \c force_degen is false, to_parity will checks if we can - /// get a better result if we don't apply partial_degeneralize. - bool force_degen = true; /// If \c scc_acc_clean is true, to_parity() will ignore colors /// not occurring in an SCC while processing this SCC. bool acc_clean = true; /// If \c parity_equiv is true, to_parity() will check if there - /// exists a permutations of colors such that the acceptance - /// condition is a parity condition. + /// exists a way to see the acceptance condition as a parity max one. bool parity_equiv = true; + /// If \c Car is true, to_parity will try to apply CAR. It is a version of + /// LAR that tracks colors. + bool car = true; + /// If \c tar is true, to_parity will try to apply TAR. It is a version of + /// LAR that tracks transitions instead of colors. + bool tar = false; + /// If \c iar is true, to_parity will try to apply IAR. + bool iar = true; + /// if \c lar_dfs is true, then when LAR is used the next state of the + /// result that will be processed is the last created state. + bool lar_dfs = true; + /// If \c bscc is true, to_parity() will only keep the bottommost automaton + /// when it applies LAR. + bool bscc = true; /// If \c parity_prefix is true, to_parity() will use a special /// handling for acceptance conditions of the form `Inf(m0) | /// (Fin(m1) & (Inf(m2) | (… β)))` that start as a parity @@ -62,30 +89,42 @@ namespace spot /// `β` can be an arbitrary formula. In this case, the paritization /// algorithm is really applied only to `β`, and the marks of the /// prefix are appended after a suitable renumbering. - /// - /// For technical reasons, activating this option (and this is the - /// default) causes reduce_parity() to be called at the end to - /// minimize the number of colors used. It is therefore - /// recommended to disable this option when one wants to follow - /// the output CAR/IAR constructions. bool parity_prefix = true; + /// If \c parity_prefix_general is true, to_parity() will rewrite the + /// acceptance condition as `Inf(m0) | (Fin(m1) & (Inf(m2) | (… β)))` before + /// applying the same construction as with the option \c parity_prefix. + bool parity_prefix_general = false; + /// If \c generic_emptiness is true, to_parity() will check if the automaton + /// does not accept any word with an emptiness check algorithm. + bool generic_emptiness = false; /// If \c rabin_to_buchi is true, to_parity() tries to convert a Rabin or /// Streett condition to Büchi or co-Büchi with /// rabin_to_buchi_if_realizable(). bool rabin_to_buchi = true; - /// Only allow degeneralization if it reduces the number of colors in the - /// acceptance condition. + /// If \c buchi_type_to_buchi is true, to_parity converts a + /// (co-)Büchi type automaton to a (co-)Büchi automaton. + bool buchi_type_to_buchi = false; + /// If \c parity_type_to_parity is true, to_parity converts a + /// parity type automaton to a parity automaton. + bool parity_type_to_parity = false; + /// Only allow partial degeneralization if it reduces the number of colors + /// in the acceptance condition or if it implies to apply IAR instead of + /// CAR. bool reduce_col_deg = false; /// Use propagate_marks_here to increase the number of marks on transition /// in order to move more colors (and increase the number of /// compatible states) when we apply LAR. bool propagate_col = true; + /// If \c use_generalized_buchi is true, each SCC will use a generalized + /// Rabin acceptance in order to avoid CAR. + bool use_generalized_rabin = false; /// If \c pretty_print is true, states of the output automaton are /// named to help debugging. bool pretty_print = false; + /// Structure used to store some information about the construction. + to_parity_data* datas = nullptr; }; - /// \ingroup twa_acc_transform /// \brief Take an automaton with any acceptance condition and return an /// equivalent parity automaton. diff --git a/spot/twaalgos/zlktree.hh b/spot/twaalgos/zlktree.hh index b8e47bc2a..d210033e3 100644 --- a/spot/twaalgos/zlktree.hh +++ b/spot/twaalgos/zlktree.hh @@ -181,7 +181,6 @@ namespace spot /// \brief Render the tree as in GraphViz format. void dot(std::ostream&) const; - private: struct zielonka_node { unsigned parent; @@ -191,6 +190,7 @@ namespace spot acc_cond::mark_t colors; }; std::vector nodes_; + private: unsigned one_branch_ = 0; unsigned num_branches_ = 0; bool is_even_; diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 6cb449012..95e0bf4d7 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -58,11 +58,11 @@ parity 13; 13 1 1 6,10; 1 1 1 6,3; parity 5; -1 1 0 4,5 "INIT"; +0 1 0 2,3 "INIT"; +3 3 1 1; +1 1 0 4,5; 5 2 1 1,1; 4 3 1 0,1; -0 1 0 2,3; -3 3 1 1; 2 1 1 0,0; EOF @@ -414,13 +414,13 @@ grep 'DPA has 29 states' err ltlsynt --verbose -x wdba-minimize=1 --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err grep 'DPA has 12 states' err -ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=no | grep 'States: 5' -ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bisim | grep 'States: 5' -ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bwoa | grep 'States: 4' -ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" | grep 'States: 4' -ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=sat | grep 'States: 2' -ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bisim-sat | grep 'States: 2' -ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bwoa-sat | grep 'States: 4' +ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=no | grep 'States: 7' +ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bisim | grep 'States: 7' +ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bwoa | grep 'States: 6' +ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" | grep 'States: 6' +ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=sat | grep 'States: 3' +ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bisim-sat | grep 'States: 3' +ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bwoa-sat | grep 'States: 6' # The following used to raise an exception because of a bug in # split_2step_fast_here(). @@ -707,7 +707,7 @@ automaton has 4 states and 1 colors LAR construction done in X seconds DPA has 4 states, 1 colors split inputs and outputs done in X seconds -automaton has 9 states +automaton has 10 states solving game with acceptance: Büchi game solved in X seconds simplification took X seconds diff --git a/tests/python/games.ipynb b/tests/python/games.ipynb index 891ebcd94..f3ffd7502 100644 --- a/tests/python/games.ipynb +++ b/tests/python/games.ipynb @@ -47,153 +47,153 @@ "\n", "\n", - "\n", "\n", "\n", "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "2->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "6->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "7->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -285,153 +285,153 @@ "\n", "\n", - "\n", "\n", "\n", "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "2->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "6->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "7->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -501,153 +501,153 @@ "\n", "\n", - "\n", "\n", "\n", "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", "\n", - "0\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", "\n", - "1\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", "\n", - "3\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", "\n", - "2\n", + "2\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", "\n", - "4\n", + "4\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", "\n", - "6\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", "\n", - "5\n", + "5\n", "\n", "\n", "\n", "2->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7\n", "\n", - "7\n", + "7\n", "\n", "\n", "\n", "6->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", "\n", - "8\n", + "8\n", "\n", "\n", "\n", "7->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -686,233 +686,218 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "⓿\n", - ")\n", - "[co-Büchi]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-Büchi]\n", "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "I->4\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "10\n", - "\n", - "10\n", - "\n", - "\n", - "\n", - "4->10\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "11\n", - "\n", - "11\n", - "\n", - "\n", - "\n", - "4->11\n", - "\n", - "\n", - "a\n", - "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "0->5\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "\n", + "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "0->6\n", - "\n", - "\n", - "a\n", - "⓿\n", - "\n", - "\n", - "\n", - "5->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "a\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", - "\n", + "\n", + "\n", + "5->1\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", "\n", - "6->1\n", - "\n", - "\n", - "1\n", - "⓿\n", - "\n", - "\n", - "\n", - "1->6\n", - "\n", - "\n", - "a\n", - "⓿\n", - "\n", - "\n", - "\n", - "7\n", - "\n", - "7\n", - "\n", - "\n", - "\n", - "1->7\n", - "\n", - "\n", - "!a\n", - "⓿\n", - "\n", - "\n", - "\n", - "7->0\n", - "\n", - "\n", - "1\n", - "⓿\n", + "5->3\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "6->2\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "1->7\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "\n", + "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", - "\n", - "\n", - "2->8\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1->8\n", + "\n", + "\n", + "a\n", + "⓿\n", + "\n", + "\n", + "\n", + "7->1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "8->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", + "⓿\n", "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", + "\n", + "\n", + "2->7\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "2->8\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", - "\n", + "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", - "\n", + "\n", "3->9\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "9->2\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n", - "9->3\n", - "\n", - "\n", - "b\n", - "⓿\n", - "\n", - "\n", "\n", - "10->0\n", - "\n", - "\n", - "!b\n", + "9->3\n", + "\n", + "\n", + "b\n", + "⓿\n", "\n", - "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", "\n", - "10->3\n", - "\n", - "\n", - "b\n", + "9->4\n", + "\n", + "\n", + "!b\n", "\n", - "\n", + "\n", + "\n", + "10\n", + "\n", + "10\n", + "\n", + "\n", + "\n", + "4->10\n", + "\n", + "\n", + "1\n", + "\n", + "\n", "\n", - "11->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "11->3\n", - "\n", - "\n", - "b\n", + "10->4\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f657c403180> >" + " *' at 0x7f6be431fbd0> >" ] }, "execution_count": 8, @@ -944,46 +929,44 @@ "output_type": "stream", "text": [ "HOA: v1\n", - "States: 12\n", - "Start: 4\n", + "States: 11\n", + "Start: 0\n", "AP: 2 \"b\" \"a\"\n", "acc-name: co-Buchi\n", "Acceptance: 1 Fin(0)\n", "properties: trans-labels explicit-labels trans-acc complete\n", "properties: deterministic\n", - "spot-state-player: 0 0 0 0 0 1 1 1 1 1 1 1\n", + "spot-state-player: 0 0 0 0 0 1 1 1 1 1 1\n", "controllable-AP: 0\n", "--BODY--\n", "State: 0\n", "[!1] 5\n", - "[1] 6 {0}\n", + "[1] 6\n", "State: 1\n", - "[1] 6 {0}\n", - "[!1] 7 {0}\n", + "[!1] 7\n", + "[1] 8 {0}\n", "State: 2\n", - "[t] 8\n", + "[!1] 7\n", + "[1] 8 {0}\n", "State: 3\n", "[t] 9\n", "State: 4\n", - "[!1] 10\n", - "[1] 11\n", + "[t] 10\n", "State: 5\n", - "[t] 0\n", - "State: 6\n", - "[t] 1 {0}\n", - "State: 7\n", - "[t] 0 {0}\n", - "State: 8\n", - "[t] 2\n", - "State: 9\n", - "[!0] 2\n", - "[0] 3 {0}\n", - "State: 10\n", - "[!0] 0\n", - "[0] 3\n", - "State: 11\n", "[!0] 1\n", "[0] 3\n", + "State: 6\n", + "[!0] 2\n", + "[0] 3\n", + "State: 7\n", + "[t] 1\n", + "State: 8\n", + "[t] 2 {0}\n", + "State: 9\n", + "[0] 3 {0}\n", + "[!0] 4\n", + "State: 10\n", + "[t] 4\n", "--END--\n" ] } @@ -1030,233 +1013,218 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "⓿\n", - ")\n", - "[co-Büchi]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-Büchi]\n", "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "I->4\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "10\n", - "\n", - "10\n", - "\n", - "\n", - "\n", - "4->10\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "11\n", - "\n", - "11\n", - "\n", - "\n", - "\n", - "4->11\n", - "\n", - "\n", - "a\n", - "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "0->5\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "\n", + "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "0->6\n", - "\n", - "\n", - "a\n", - "⓿\n", - "\n", - "\n", - "\n", - "5->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "a\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", - "\n", + "\n", + "\n", + "5->1\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", "\n", - "6->1\n", - "\n", - "\n", - "1\n", - "⓿\n", - "\n", - "\n", - "\n", - "1->6\n", - "\n", - "\n", - "a\n", - "⓿\n", - "\n", - "\n", - "\n", - "7\n", - "\n", - "7\n", - "\n", - "\n", - "\n", - "1->7\n", - "\n", - "\n", - "!a\n", - "⓿\n", - "\n", - "\n", - "\n", - "7->0\n", - "\n", - "\n", - "1\n", - "⓿\n", + "5->3\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "6->2\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "1->7\n", + "\n", + "\n", + "!a\n", "\n", "\n", - "\n", + "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", - "\n", - "\n", - "2->8\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1->8\n", + "\n", + "\n", + "a\n", + "⓿\n", + "\n", + "\n", + "\n", + "7->1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "8->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", + "⓿\n", "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", + "\n", + "\n", + "2->7\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "2->8\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", - "\n", + "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", - "\n", + "\n", "3->9\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "9->2\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n", - "9->3\n", - "\n", - "\n", - "b\n", - "⓿\n", - "\n", - "\n", "\n", - "10->0\n", - "\n", - "\n", - "!b\n", + "9->3\n", + "\n", + "\n", + "b\n", + "⓿\n", "\n", - "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", "\n", - "10->3\n", - "\n", - "\n", - "b\n", + "9->4\n", + "\n", + "\n", + "!b\n", "\n", - "\n", + "\n", + "\n", + "10\n", + "\n", + "10\n", + "\n", + "\n", + "\n", + "4->10\n", + "\n", + "\n", + "1\n", + "\n", + "\n", "\n", - "11->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "11->3\n", - "\n", - "\n", - "b\n", + "10->4\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f658c612f30> >" + " *' at 0x7f6be431fcf0> >" ] }, "execution_count": 11, @@ -1267,18 +1235,11 @@ "source": [ "spot.highlight_strategy(game)" ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": { "kernelspec": { - "display_name": "Python 3 (ipykernel)", + "display_name": "Python 3", "language": "python", "name": "python3" }, @@ -1292,7 +1253,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.10" + "version": "3.7.3" } }, "nbformat": 4, diff --git a/tests/python/synthesis.ipynb b/tests/python/synthesis.ipynb index 3e8b4f5ea..654d22873 100644 --- a/tests/python/synthesis.ipynb +++ b/tests/python/synthesis.ipynb @@ -3,7 +3,6 @@ { "cell_type": "code", "execution_count": 1, - "id": "7a864ea1", "metadata": {}, "outputs": [], "source": [ @@ -14,7 +13,6 @@ }, { "cell_type": "markdown", - "id": "9a294cae", "metadata": {}, "source": [ "This notebook presents functions that can be used to solve the Reactive Synthesis problem using games.\n", @@ -39,7 +37,6 @@ { "cell_type": "code", "execution_count": 2, - "id": "70429a41", "metadata": {}, "outputs": [ { @@ -56,590 +53,590 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "⓿\n", - ")\n", - "[co-Büchi]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-Büchi]\n", "\n", - "\n", - "\n", - "9\n", - "\n", - "9\n", - "\n", - "\n", - "\n", - "I->9\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "25\n", - "\n", - "25\n", - "\n", - "\n", - "\n", - "9->25\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", - "\n", - "\n", - "26\n", - "\n", - "26\n", - "\n", - "\n", - "\n", - "9->26\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", - "\n", - "\n", - "27\n", - "\n", - "27\n", - "\n", - "\n", - "\n", - "9->27\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", - "\n", - "\n", - "28\n", - "\n", - "28\n", - "\n", - "\n", - "\n", - "9->28\n", - "\n", - "\n", - "i0 & i1\n", - "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "0->10\n", - "\n", - "\n", - "!i1\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", - "\n", + "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "0->11\n", - "\n", - "\n", - "i1\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "10->1\n", - "\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "11->0\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", - "\n", + "\n", "12\n", - "\n", - "12\n", + "\n", + "12\n", "\n", - "\n", + "\n", "\n", - "1->12\n", - "\n", - "\n", - "!i1\n", + "0->12\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", - "\n", + "\n", "13\n", - "\n", - "13\n", + "\n", + "13\n", "\n", - "\n", + "\n", "\n", - "1->13\n", - "\n", - "\n", - "i1\n", + "0->13\n", + "\n", + "\n", + "i0 & i1\n", "\n", - "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "10->8\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "11->7\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "9\n", + "\n", + "\n", "\n", - "12->1\n", - "\n", - "\n", - "!o0\n", + "12->9\n", + "\n", + "\n", + "1\n", "\n", - "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", "\n", - "13->0\n", - "\n", - "\n", - "!o0\n", + "13->5\n", + "\n", + "\n", + "1\n", "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "14\n", - "\n", - "14\n", + "\n", + "14\n", "\n", - "\n", + "\n", "\n", - "2->14\n", - "\n", - "\n", - "i1\n", + "1->14\n", + "\n", + "\n", + "i0\n", "\n", "\n", - "\n", + "\n", "16\n", - "\n", - "16\n", + "\n", + "16\n", "\n", - "\n", + "\n", "\n", - "2->16\n", - "\n", - "\n", - "!i1\n", + "1->16\n", + "\n", + "\n", + "!i0\n", "\n", "\n", "\n", "15\n", - "\n", - "15\n", + "\n", + "15\n", "\n", "\n", "\n", "14->15\n", - "\n", - "\n", - "1\n", - "⓿\n", + "\n", + "\n", + "1\n", + "⓿\n", "\n", - "\n", + "\n", "\n", - "16->2\n", - "\n", - "\n", - "1\n", + "16->1\n", + "\n", + "\n", + "1\n", "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", "\n", - "\n", + "\n", "\n", - "3->13\n", - "\n", - "\n", - "i1\n", + "2->14\n", + "\n", + "\n", + "i1\n", "\n", "\n", - "\n", + "\n", "17\n", - "\n", - "17\n", + "\n", + "17\n", "\n", - "\n", + "\n", "\n", - "3->17\n", - "\n", - "\n", - "!i1\n", + "2->17\n", + "\n", + "\n", + "!i1\n", "\n", "\n", "\n", "17->2\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "1\n", "\n", - "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "3->14\n", + "\n", + "\n", + "i0 & i1\n", + "\n", + "\n", + "\n", + "3->16\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", + "\n", + "\n", + "3->17\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", + "\n", + "\n", + "18\n", + "\n", + "18\n", + "\n", + "\n", + "\n", + "3->18\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", + "\n", "\n", - "17->3\n", - "\n", - "\n", - "!o0\n", + "18->3\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "4->14\n", - "\n", - "\n", - "i0\n", - "\n", - "\n", - "\n", - "18\n", - "\n", - "18\n", - "\n", - "\n", - "\n", - "4->18\n", - "\n", - "\n", - "!i0\n", - "\n", - "\n", - "\n", - "18->4\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "5\n", - "\n", - "5\n", - "\n", - "\n", - "\n", - "5->14\n", - "\n", - "\n", - "i0 & i1\n", - "\n", - "\n", - "\n", - "5->16\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", - "\n", - "\n", - "5->18\n", - "\n", - "\n", - "!i0 & i1\n", + "\n", + "4\n", "\n", "\n", - "\n", + "\n", "19\n", - "\n", - "19\n", + "\n", + "19\n", "\n", - "\n", - "\n", - "5->19\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", - "\n", - "\n", - "19->5\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "6\n", - "\n", - "6\n", - "\n", - "\n", - "\n", - "6->10\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", - "\n", - "\n", - "6->11\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "4->19\n", + "\n", + "\n", + "!i1\n", "\n", "\n", - "\n", + "\n", "20\n", - "\n", - "20\n", + "\n", + "20\n", "\n", - "\n", - "\n", - "6->20\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "4->20\n", + "\n", + "\n", + "i1\n", + "\n", + "\n", + "\n", + "19->4\n", + "\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "20->5\n", + "\n", + "\n", + "!o0\n", "\n", "\n", - "\n", + "\n", "21\n", - "\n", - "21\n", + "\n", + "21\n", "\n", - "\n", - "\n", - "6->21\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", - "\n", - "\n", - "20->4\n", - "\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "7\n", - "\n", - "7\n", - "\n", - "\n", - "\n", - "20->7\n", - "\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "21->4\n", - "\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "21->6\n", - "\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "7->12\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", - "\n", - "\n", - "7->13\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "5->21\n", + "\n", + "\n", + "!i1\n", "\n", "\n", - "\n", + "\n", "22\n", - "\n", - "22\n", + "\n", + "22\n", "\n", - "\n", - "\n", - "7->22\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "5->22\n", + "\n", + "\n", + "i1\n", + "\n", + "\n", + "\n", + "21->4\n", + "\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "22->5\n", + "\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "6->19\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", + "\n", + "\n", + "6->20\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", - "\n", + "\n", "23\n", - "\n", - "23\n", + "\n", + "23\n", "\n", - "\n", - "\n", - "7->23\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", - "\n", - "\n", - "22->4\n", - "\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "22->7\n", - "\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "23->4\n", - "\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "23->6\n", - "\n", - "\n", - "!o0\n", - "\n", - "\n", - "\n", - "8\n", - "\n", - "8\n", - "\n", - "\n", - "\n", - "8->13\n", - "\n", - "\n", - "i0 & i1\n", - "\n", - "\n", - "\n", - "8->17\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", - "\n", - "\n", - "8->23\n", - "\n", - "\n", - "!i0 & i1\n", + "\n", + "\n", + "6->23\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", - "\n", + "\n", "24\n", - "\n", - "24\n", + "\n", + "24\n", + "\n", + "\n", + "\n", + "6->24\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", + "\n", + "\n", + "23->1\n", + "\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "23->6\n", + "\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "24->1\n", + "\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "24->9\n", + "\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "7->20\n", + "\n", + "\n", + "i1\n", + "\n", + "\n", + "\n", + "25\n", + "\n", + "25\n", + "\n", + "\n", + "\n", + "7->25\n", + "\n", + "\n", + "!i1\n", + "\n", + "\n", + "\n", + "25->2\n", + "\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "25->7\n", + "\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "8->20\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", - "\n", + "\n", "8->24\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "!i0 & i1\n", "\n", - "\n", - "\n", - "24->5\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "8->25\n", + "\n", + "\n", + "i0 & !i1\n", "\n", - "\n", - "\n", - "24->8\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "26\n", + "\n", + "26\n", "\n", - "\n", - "\n", - "25->8\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "8->26\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", - "\n", + "\n", "26->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "26->8\n", + "\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "9->21\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", + "\n", + "\n", + "9->22\n", + "\n", + "\n", + "i0 & i1\n", + "\n", + "\n", + "\n", + "27\n", + "\n", + "27\n", + "\n", + "\n", + "\n", + "9->27\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", + "\n", + "\n", + "28\n", + "\n", + "28\n", + "\n", + "\n", + "\n", + "9->28\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", + "\n", + "\n", + "27->1\n", + "\n", + "\n", + "!o0\n", "\n", "\n", - "\n", + "\n", "27->6\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "o0\n", "\n", - "\n", + "\n", + "\n", + "28->1\n", + "\n", + "\n", + "!o0\n", + "\n", + "\n", "\n", - "28->0\n", - "\n", - "\n", - "1\n", + "28->9\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "15->14\n", - "\n", - "\n", - "1\n", - "⓿\n", + "\n", + "\n", + "1\n", + "⓿\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fc9680c32d0> >" + " *' at 0x7f0e584de570> >" ] }, "metadata": {}, @@ -658,7 +655,6 @@ }, { "cell_type": "markdown", - "id": "c02b2d8f", "metadata": {}, "source": [ "Solving the game, is done with `solve_game()` as with any game. There is also a version that takes a `synthesis_info` as second argument in case the time it takes has to be recorded. Here passing `si` or not makes no difference." @@ -667,7 +663,6 @@ { "cell_type": "code", "execution_count": 3, - "id": "d08e7b9f", "metadata": {}, "outputs": [ { @@ -683,529 +678,529 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "⓿\n", - ")\n", - "[co-Büchi]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-Büchi]\n", "\n", - "\n", - "\n", - "9\n", - "\n", - "9\n", - "\n", - "\n", - "\n", - "I->9\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "25\n", - "\n", - "25\n", - "\n", - "\n", - "\n", - "9->25\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "26\n", - "\n", - "26\n", - "\n", - "\n", - "\n", - "9->26\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "27\n", - "\n", - "27\n", - "\n", - "\n", - "\n", - "9->27\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "28\n", - "\n", - "28\n", - "\n", - "\n", - "\n", - "9->28\n", - "\n", - "\n", - "\n", "\n", - "\n", + "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "0->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "0->11\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "10->1\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "11->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "12\n", - "\n", - "12\n", + "\n", + "12\n", "\n", - "\n", + "\n", "\n", - "1->12\n", - "\n", - "\n", + "0->12\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "13\n", - "\n", - "13\n", + "\n", + "13\n", "\n", - "\n", + "\n", "\n", - "1->13\n", - "\n", - "\n", + "0->13\n", + "\n", + "\n", "\n", - "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "10->8\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "11->7\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "9\n", + "\n", + "\n", "\n", - "12->1\n", - "\n", - "\n", + "12->9\n", + "\n", + "\n", "\n", - "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", "\n", - "13->0\n", - "\n", - "\n", + "13->5\n", + "\n", + "\n", "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "14\n", - "\n", - "14\n", + "\n", + "14\n", "\n", - "\n", + "\n", "\n", - "2->14\n", - "\n", - "\n", + "1->14\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "16\n", - "\n", - "16\n", + "\n", + "16\n", "\n", - "\n", + "\n", "\n", - "2->16\n", - "\n", - "\n", + "1->16\n", + "\n", + "\n", "\n", "\n", "\n", "15\n", - "\n", - "15\n", + "\n", + "15\n", "\n", "\n", "\n", "14->15\n", - "\n", - "\n", - "⓿\n", + "\n", + "\n", + "⓿\n", "\n", - "\n", + "\n", "\n", - "16->2\n", - "\n", - "\n", + "16->1\n", + "\n", + "\n", "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", "\n", - "\n", + "\n", "\n", - "3->13\n", - "\n", - "\n", + "2->14\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "17\n", - "\n", - "17\n", + "\n", + "17\n", "\n", - "\n", + "\n", "\n", - "3->17\n", - "\n", - "\n", + "2->17\n", + "\n", + "\n", "\n", "\n", "\n", "17->2\n", - "\n", - "\n", + "\n", + "\n", "\n", - "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "3->14\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->16\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->17\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "18\n", + "\n", + "18\n", + "\n", + "\n", + "\n", + "3->18\n", + "\n", + "\n", + "\n", + "\n", "\n", - "17->3\n", - "\n", - "\n", + "18->3\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "4->14\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "18\n", - "\n", - "18\n", - "\n", - "\n", - "\n", - "4->18\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "18->4\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "5\n", - "\n", - "5\n", - "\n", - "\n", - "\n", - "5->14\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "5->16\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "5->18\n", - "\n", - "\n", + "\n", + "4\n", "\n", "\n", - "\n", + "\n", "19\n", - "\n", - "19\n", + "\n", + "19\n", "\n", - "\n", - "\n", - "5->19\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "19->5\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "6\n", - "\n", - "6\n", - "\n", - "\n", - "\n", - "6->10\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "6->11\n", - "\n", - "\n", + "\n", + "\n", + "4->19\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "20\n", - "\n", - "20\n", + "\n", + "20\n", "\n", - "\n", - "\n", - "6->20\n", - "\n", - "\n", + "\n", + "\n", + "4->20\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "19->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "20->5\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "21\n", - "\n", - "21\n", + "\n", + "21\n", "\n", - "\n", - "\n", - "6->21\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "20->4\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "7\n", - "\n", - "7\n", - "\n", - "\n", - "\n", - "20->7\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "21->4\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "21->6\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "7->12\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "7->13\n", - "\n", - "\n", + "\n", + "\n", + "5->21\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "22\n", - "\n", - "22\n", + "\n", + "22\n", "\n", - "\n", - "\n", - "7->22\n", - "\n", - "\n", + "\n", + "\n", + "5->22\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "21->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "22->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "6->19\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "6->20\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "23\n", - "\n", - "23\n", + "\n", + "23\n", "\n", - "\n", - "\n", - "7->23\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "22->4\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "22->7\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "23->4\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "23->6\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "8\n", - "\n", - "8\n", - "\n", - "\n", - "\n", - "8->13\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "8->17\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "8->23\n", - "\n", - "\n", + "\n", + "\n", + "6->23\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "24\n", - "\n", - "24\n", + "\n", + "24\n", + "\n", + "\n", + "\n", + "6->24\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "23->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "23->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "24->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "24->9\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7->20\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "25\n", + "\n", + "25\n", + "\n", + "\n", + "\n", + "7->25\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "25->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "25->7\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "8->20\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "8->24\n", - "\n", - "\n", + "\n", + "\n", "\n", - "\n", - "\n", - "24->5\n", - "\n", - "\n", + "\n", + "\n", + "8->25\n", + "\n", + "\n", "\n", - "\n", - "\n", - "24->8\n", - "\n", - "\n", + "\n", + "\n", + "26\n", + "\n", + "26\n", "\n", - "\n", - "\n", - "25->8\n", - "\n", - "\n", + "\n", + "\n", + "8->26\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "26->3\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "26->8\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "9->21\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "9->22\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "27\n", + "\n", + "27\n", + "\n", + "\n", + "\n", + "9->27\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "28\n", + "\n", + "28\n", + "\n", + "\n", + "\n", + "9->28\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "27->1\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "27->6\n", - "\n", - "\n", + "\n", + "\n", "\n", - "\n", + "\n", + "\n", + "28->1\n", + "\n", + "\n", + "\n", + "\n", "\n", - "28->0\n", - "\n", - "\n", + "28->9\n", + "\n", + "\n", "\n", "\n", "\n", "15->14\n", - "\n", - "\n", - "⓿\n", + "\n", + "\n", + "⓿\n", "\n", "\n", "\n" @@ -1227,7 +1222,6 @@ }, { "cell_type": "markdown", - "id": "9590cf55", "metadata": {}, "source": [ "Once a strategy has been found, it can be extracted as an automaton and simplified using 6 different levels (the default is 2). The output should be interpreted as a Mealy automaton, where transition have the form `(ins)&(outs)` where `ins` and `outs` are Boolean formulas representing possible inputs and outputs (they could be more than just conjunctions of atomic proposition). Mealy machines with this type of labels are called \"separated\" in Spot." @@ -1236,7 +1230,6 @@ { "cell_type": "code", "execution_count": 4, - "id": "d6cb467d", "metadata": {}, "outputs": [ { @@ -1252,309 +1245,309 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "2->4\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "3->5\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "4->5\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "5->4\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "6->3\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "6->4\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fc9682230f0> >" + " *' at 0x7f0e5855c9f0> >" ] }, "metadata": {}, @@ -1573,175 +1566,175 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "1\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fc968069180> >" + " *' at 0x7f0e5855cb10> >" ] }, "metadata": {}, @@ -1760,125 +1753,125 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "I->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fc968069210> >" + " *' at 0x7f0e5855ccf0> >" ] }, "metadata": {}, @@ -1897,81 +1890,81 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fc968069180> >" + " *' at 0x7f0e5855cd80> >" ] }, "metadata": {}, @@ -1990,81 +1983,81 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "!i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fc968069210> >" + " *' at 0x7f0e584defc0> >" ] }, "metadata": {}, @@ -2083,125 +2076,125 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fc968069060> >" + " *' at 0x7f0e5855ca20> >" ] }, "metadata": {}, @@ -2235,7 +2228,6 @@ }, { "cell_type": "markdown", - "id": "7ee86443", "metadata": {}, "source": [ "If needed, a separated Mealy machine can be turned into game shape using `split_sepearated_mealy()`, which is more efficient than `split_2step()`." @@ -2244,7 +2236,6 @@ { "cell_type": "code", "execution_count": 5, - "id": "80510b01", "metadata": {}, "outputs": [ { @@ -2253,260 +2244,260 @@ "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "\n", - "!i0 & i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "\n", - "!i0 & !i1\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "!i0 & !i1\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "i0 & !i1\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "!i0 & i1\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "3->0\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "!i0 & i1\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "1->5\n", - "\n", - "\n", - "i0 & !i1\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "1->5\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "4->0\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "5->1\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", @@ -2526,7 +2517,6 @@ }, { "cell_type": "markdown", - "id": "8f97aa04", "metadata": {}, "source": [ "# Converting the separated Mealy machine to AIG\n", @@ -2539,7 +2529,6 @@ { "cell_type": "code", "execution_count": 6, - "id": "9c6d9e8b", "metadata": {}, "outputs": [ { @@ -2548,60 +2537,60 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", "6\n", - "\n", - "L0_out\n", + "\n", + "L0_out\n", "\n", "\n", "\n", "o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "6->o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "L0\n", - "\n", - "L0_in\n", + "\n", + "L0_in\n", "\n", "\n", "\n", "2\n", - "\n", - "i1\n", + "\n", + "i1\n", "\n", "\n", "\n", "2->L0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2615,7 +2604,6 @@ }, { "cell_type": "markdown", - "id": "d67f8bce", "metadata": {}, "source": [ "While we are at it, let us mention that you can render those circuits horizontally as follows:" @@ -2624,7 +2612,6 @@ { "cell_type": "code", "execution_count": 7, - "id": "3a363374", "metadata": {}, "outputs": [ { @@ -2633,54 +2620,54 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", "6\n", - "\n", - "L0_out\n", + "\n", + "L0_out\n", "\n", "\n", "\n", "o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "6->o0:w\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "L0\n", - "\n", - "L0_in\n", + "\n", + "L0_in\n", "\n", "\n", "\n", "2\n", - "\n", - "i1\n", + "\n", + "i1\n", "\n", "\n", "\n", "2->L0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n" @@ -2700,7 +2687,6 @@ }, { "cell_type": "markdown", - "id": "e4f607c3", "metadata": {}, "source": [ "To encode the circuit in the AIGER format (ASCII version) use:" @@ -2709,7 +2695,6 @@ { "cell_type": "code", "execution_count": 8, - "id": "564f7d0b", "metadata": {}, "outputs": [ { @@ -2733,7 +2718,6 @@ }, { "cell_type": "markdown", - "id": "cf2d4831", "metadata": {}, "source": [ "# Adding more inputs and outputs by force" @@ -2741,7 +2725,6 @@ }, { "cell_type": "markdown", - "id": "874a108e", "metadata": {}, "source": [ "It can happen that propositions declared as output are ommited in the aig circuit (either because they are not part of the specification, or because they do not appear in the winning strategy). In that case those \n", @@ -2753,7 +2736,6 @@ { "cell_type": "code", "execution_count": 9, - "id": "1fc4c566", "metadata": {}, "outputs": [ { @@ -2762,151 +2744,151 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "I->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", - "i0\n", + "\n", + "\n", + "i0\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "3->7\n", - "\n", - "\n", - "!i0\n", + "\n", + "\n", + "!i0\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "1\n", - "⓿\n", + "\n", + "\n", + "1\n", + "⓿\n", "\n", "\n", "\n", "4->0\n", - "\n", - "\n", - "1\n", - "⓿\n", + "\n", + "\n", + "1\n", + "⓿\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "1->5\n", - "\n", - "\n", - "1\n", - "⓿\n", + "\n", + "\n", + "1\n", + "⓿\n", "\n", "\n", "\n", "5->1\n", - "\n", - "\n", - "!o0\n", - "⓿\n", + "\n", + "\n", + "!o0\n", + "⓿\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "6->0\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "6->2\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "7->1\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fc968143d80> >" + " *' at 0x7f0e5855cb70> >" ] }, "metadata": {}, @@ -2918,112 +2900,112 @@ "\n", "\n", - "\n", "\n", "\n", "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "i0\n", + "\n", + "\n", + "i0\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!i0\n", + "\n", + "\n", + "!i0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "1->5\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "5->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fc9680c3330> >" + " *' at 0x7f0e5855cc60> >" ] }, "metadata": {}, @@ -3035,144 +3017,144 @@ "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "t\n", - "[all]\n", + " viewBox=\"0.00 0.00 282.00 148.79\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "i0\n", + "\n", + "\n", + "i0\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "!i0\n", + "\n", + "\n", + "!i0\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", "\n", "\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "i0\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "i0\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", - "!i0\n", - "/\n", + "!i0\n", + "/\n", "\n", - "!o0\n", + "!o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", + "\n", + "\n", "\n", - "1\n", - "/\n", + "1\n", + "/\n", "\n", - "!o0\n", + "!o0\n", "\n", "\n", "\n", @@ -3191,72 +3173,72 @@ "\n", "\n", - "\n", "\n", "\n", + " viewBox=\"0.00 0.00 143.20 352.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", "\n", - "\n", + "\n", "\n", "\n", "4\n", - "\n", - "L0_out\n", + "\n", + "L0_out\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "4->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "L0\n", - "\n", - "L0_in\n", + "\n", + "L0_in\n", "\n", "\n", "\n", "6->L0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "6->o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -3278,7 +3260,6 @@ }, { "cell_type": "markdown", - "id": "f8dab019", "metadata": {}, "source": [ "To force the presence of extra variables in the circuit, they can be passed to `mealy_machine_to_aig()`." @@ -3287,7 +3268,6 @@ { "cell_type": "code", "execution_count": 10, - "id": "091d7c97", "metadata": {}, "outputs": [ { @@ -3296,96 +3276,96 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", "6\n", - "\n", - "L0_out\n", + "\n", + "L0_out\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "6->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "L0\n", - "\n", - "L0_in\n", + "\n", + "L0_in\n", "\n", "\n", "\n", "8->L0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "8->o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o1\n", - "\n", - "o1\n", + "\n", + "o1\n", "\n", "\n", "\n", "2\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "i1\n", + "\n", + "i1\n", "\n", "\n", "\n", "0\n", - "\n", - "False\n", + "\n", + "False\n", "\n", "\n", "\n", "0->o1:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -3398,7 +3378,6 @@ }, { "cell_type": "markdown", - "id": "364c8d76", "metadata": {}, "source": [ "# Combining Mealy machines\n", @@ -3418,7 +3397,6 @@ { "cell_type": "code", "execution_count": 11, - "id": "57b3b51d", "metadata": {}, "outputs": [ { @@ -3434,134 +3412,134 @@ "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "(!i0 & !i1) | (i0 & i1)\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "(!i0 & i1) | (i0 & !i1)\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "(!i0 & !i1) | (i0 & i1)\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "(!i0 & i1) | (i0 & !i1)\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "o1\n", + "\n", + "\n", + "o1\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "!o1\n", + "\n", + "\n", + "!o1\n", "\n", "\n", "\n", @@ -3587,94 +3565,94 @@ "
\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "(!i0 & !i1) | (i0 & i1)\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "(!i0 & i1) | (i0 & !i1)\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "(!i0 & !i1) | (i0 & i1)\n", - "/\n", - "\n", - "o1\n", + "\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", + "/\n", + "\n", + "o1\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "(!i0 & i1) | (i0 & !i1)\n", - "/\n", - "\n", - "!o1\n", + "\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", + "/\n", + "\n", + "!o1\n", "\n", "\n", "\n", @@ -3700,108 +3678,108 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "10->o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o1\n", - "\n", - "o1\n", + "\n", + "o1\n", "\n", "\n", "\n", "10->o1:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "i1\n", + "\n", + "i1\n", "\n", "\n", "\n", "4->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -3820,53 +3798,53 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "(!i0 & !i1) | (i0 & i1)\n", - "/\n", - "\n", - "!o0 & o1\n", + "\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", + "/\n", + "\n", + "!o0 & o1\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "(!i0 & i1) | (i0 & !i1)\n", - "/\n", - "\n", - "o0 & !o1\n", + "\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", + "/\n", + "\n", + "o0 & !o1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fc968143bd0> >" + " *' at 0x7f0e5855cd20> >" ] }, "metadata": {}, @@ -3878,108 +3856,108 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "10->o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o1\n", - "\n", - "o1\n", + "\n", + "o1\n", "\n", "\n", "\n", "10->o1:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "i1\n", + "\n", + "i1\n", "\n", "\n", "\n", "4->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -4013,7 +3991,6 @@ }, { "cell_type": "markdown", - "id": "7d5a8a32", "metadata": {}, "source": [ "# Reading an AIGER-file\n", @@ -4028,7 +4005,6 @@ { "cell_type": "code", "execution_count": 12, - "id": "9da1f39e", "metadata": {}, "outputs": [], "source": [ @@ -4049,7 +4025,6 @@ { "cell_type": "code", "execution_count": 13, - "id": "7295f20a", "metadata": {}, "outputs": [ { @@ -4058,108 +4033,108 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o1\n", - "\n", - "d\n", + "\n", + "d\n", "\n", "\n", "\n", "6->o1:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o0\n", - "\n", - "c\n", + "\n", + "c\n", "\n", "\n", "\n", "10->o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "a\n", + "\n", + "a\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "b\n", + "\n", + "b\n", "\n", "\n", "\n", "4->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -4174,7 +4149,6 @@ { "cell_type": "code", "execution_count": 14, - "id": "730952f7", "metadata": {}, "outputs": [ { @@ -4203,7 +4177,6 @@ { "cell_type": "code", "execution_count": 15, - "id": "38b5b8a1", "metadata": {}, "outputs": [ { @@ -4220,7 +4193,6 @@ }, { "cell_type": "markdown", - "id": "6bde5eac", "metadata": {}, "source": [ "An AIG circuit can be transformed into a monitor/Mealy machine. This can be used for instance to check that it does not intersect the negation of the specification." @@ -4229,7 +4201,6 @@ { "cell_type": "code", "execution_count": 16, - "id": "14f89c9b", "metadata": {}, "outputs": [ { @@ -4238,52 +4209,52 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "!a & !b\n", - "/\n", - "\n", - "!c & !d\n", - "\n", - "a & b\n", - "/\n", - "\n", - "!c & d\n", - "\n", - "(!a & b) | (a & !b)\n", - "/\n", - "\n", - "c & !d\n", + "\n", + "\n", + "\n", + "!a & !b\n", + "/\n", + "\n", + "!c & !d\n", + "\n", + "a & b\n", + "/\n", + "\n", + "!c & d\n", + "\n", + "(!a & b) | (a & !b)\n", + "/\n", + "\n", + "c & !d\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fc968069ed0> >" + " *' at 0x7f0e584ee4e0> >" ] }, "execution_count": 16, @@ -4297,7 +4268,6 @@ }, { "cell_type": "markdown", - "id": "e1f01aa0", "metadata": {}, "source": [ "Note that the generation of aiger circuits from Mealy machines is flexible and accepts separated Mealy machines\n", @@ -4307,7 +4277,6 @@ { "cell_type": "code", "execution_count": 17, - "id": "93e1fc70", "metadata": {}, "outputs": [ { @@ -4316,114 +4285,114 @@ "
\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "(!i0 & !i1) | (i0 & i1)\n", - "/\n", - "\n", - "!o0\n", + "\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", + "/\n", + "\n", + "!o0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "\n", - "(!i0 & i1) | (i0 & !i1)\n", - "/\n", - "\n", - "o0\n", + "\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", + "/\n", + "\n", + "o0\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "(!i0 & !i1) | (i0 & i1)\n", + "\n", + "\n", + "(!i0 & !i1) | (i0 & i1)\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "(!i0 & i1) | (i0 & !i1)\n", + "\n", + "\n", + "(!i0 & i1) | (i0 & !i1)\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", @@ -4455,7 +4424,6 @@ { "cell_type": "code", "execution_count": 18, - "id": "6cb96c81", "metadata": {}, "outputs": [ { @@ -4464,180 +4432,180 @@ "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "10->o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "i1\n", + "\n", + "i1\n", "\n", "\n", "\n", "4->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "10->o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "i1\n", + "\n", + "i1\n", "\n", "\n", "\n", "4->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", @@ -4658,7 +4626,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3 (ipykernel)", + "display_name": "Python 3", "language": "python", "name": "python3" }, @@ -4672,7 +4640,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.10" + "version": "3.7.3" } }, "nbformat": 4, diff --git a/tests/python/toparity.py b/tests/python/toparity.py index 37e111f9b..ad9bc6e0b 100644 --- a/tests/python/toparity.py +++ b/tests/python/toparity.py @@ -26,57 +26,135 @@ tc = TestCase() # Tests for the new version of to_parity +# It is no more a no_option as we now have more options (like iar, bscc, …) no_option = spot.to_parity_options() no_option.search_ex = False no_option.use_last = False -no_option.force_order = False +no_option.use_last_post_process = False no_option.partial_degen = False no_option.acc_clean = False no_option.parity_equiv = False +no_option.tar = False +no_option.iar = True +no_option.lar_dfs = True +no_option.bscc = True no_option.parity_prefix = False +no_option.parity_prefix_general = False +no_option.generic_emptiness = False no_option.rabin_to_buchi = False +no_option.buchi_type_to_buchi = False +no_option.parity_type_to_parity = False +no_option.reduce_col_deg = False no_option.propagate_col = False +no_option.use_generalized_rabin = False acc_clean_search_opt = spot.to_parity_options() -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 +no_option.search_ex = False +no_option.use_last = False +no_option.use_last_post_process = False +no_option.force_order = False +no_option.partial_degen = False +no_option.acc_clean = True +no_option.parity_equiv = False +no_option.tar = False +no_option.iar = True +no_option.lar_dfs = True +no_option.bscc = True +no_option.parity_prefix = False +no_option.parity_prefix_general = False +no_option.generic_emptiness = False +no_option.rabin_to_buchi = False +no_option.buchi_type_to_buchi = False +no_option.parity_type_to_parity = False +no_option.reduce_col_deg = False +no_option.propagate_col = False +no_option.use_generalized_rabin = False partial_degen_opt = spot.to_parity_options() partial_degen_opt.search_ex = False +partial_degen_opt.use_last = False +partial_degen_opt.use_last_post_process = False partial_degen_opt.force_order = False +partial_degen_opt.partial_degen = True +partial_degen_opt.acc_clean = False partial_degen_opt.parity_equiv = False +partial_degen_opt.tar = False +partial_degen_opt.iar = True +partial_degen_opt.lar_dfs = True +partial_degen_opt.bscc = True partial_degen_opt.parity_prefix = False +partial_degen_opt.parity_prefix_general = False +partial_degen_opt.generic_emptiness = False partial_degen_opt.rabin_to_buchi = False +partial_degen_opt.buchi_type_to_buchi = False +partial_degen_opt.parity_type_to_parity = False +partial_degen_opt.reduce_col_deg = False partial_degen_opt.propagate_col = False +partial_degen_opt.use_generalized_rabin = False parity_equiv_opt = spot.to_parity_options() parity_equiv_opt.search_ex = False parity_equiv_opt.use_last = False -parity_equiv_opt.force_order = False +parity_equiv_opt.use_last_post_process = False parity_equiv_opt.partial_degen = False +parity_equiv_opt.acc_clean = False +parity_equiv_opt.parity_equiv = True +parity_equiv_opt.tar = False +parity_equiv_opt.iar = True +parity_equiv_opt.lar_dfs = True +parity_equiv_opt.bscc = True parity_equiv_opt.parity_prefix = False +parity_equiv_opt.parity_prefix_general = False +parity_equiv_opt.generic_emptiness = False parity_equiv_opt.rabin_to_buchi = False +parity_equiv_opt.buchi_type_to_buchi = False +parity_equiv_opt.parity_type_to_parity = False +parity_equiv_opt.reduce_col_deg = False parity_equiv_opt.propagate_col = False +parity_equiv_opt.use_generalized_rabin = False rab_to_buchi_opt = spot.to_parity_options() +rab_to_buchi_opt.search_ex = False rab_to_buchi_opt.use_last = False -rab_to_buchi_opt.force_order = False +rab_to_buchi_opt.use_last_post_process = False rab_to_buchi_opt.partial_degen = False -rab_to_buchi_opt.parity_equiv = False +rab_to_buchi_opt.acc_clean = False +rab_to_buchi_opt.parity_equiv = True +rab_to_buchi_opt.tar = False +rab_to_buchi_opt.iar = True +rab_to_buchi_opt.lar_dfs = False +rab_to_buchi_opt.bscc = False rab_to_buchi_opt.parity_prefix = False +rab_to_buchi_opt.parity_prefix_general = False +rab_to_buchi_opt.generic_emptiness = False +rab_to_buchi_opt.rabin_to_buchi = True +rab_to_buchi_opt.buchi_type_to_buchi = False +rab_to_buchi_opt.parity_type_to_parity = False +rab_to_buchi_opt.reduce_col_deg = False rab_to_buchi_opt.propagate_col = False +rab_to_buchi_opt.use_generalized_rabin = False -# Force to use CAR or IAR for each SCC +# Force to use CAR, IAR or TAR for each SCC use_car_opt = spot.to_parity_options() +use_car_opt.search_ex = True +use_car_opt.use_last = True +use_car_opt.use_last_post_process = True use_car_opt.partial_degen = False +use_car_opt.acc_clean = False use_car_opt.parity_equiv = False +use_car_opt.tar = True +use_car_opt.iar = True +use_car_opt.lar_dfs = True +use_car_opt.bscc = True use_car_opt.parity_prefix = False +use_car_opt.parity_prefix_general = False +use_car_opt.generic_emptiness = False use_car_opt.rabin_to_buchi = False +use_car_opt.buchi_type_to_buchi = False +use_car_opt.parity_type_to_parity = False +use_car_opt.reduce_col_deg = False use_car_opt.propagate_col = False +use_car_opt.use_generalized_rabin = False all_opt = spot.to_parity_options() all_opt.pretty_print = True @@ -100,15 +178,28 @@ def test(aut, expected_num_states=[], full=True): p1 = spot.to_parity(aut, search_ex = opt.search_ex, use_last = opt.use_last, + use_last_post_process = \ + opt.use_last_post_process, force_order = opt.force_order, partial_degen = opt.partial_degen, acc_clean = opt.acc_clean, parity_equiv = opt.parity_equiv, + tar = opt.tar, + iar = opt.iar, + lar_dfs = opt.lar_dfs, + bscc = opt.bscc, parity_prefix = opt.parity_prefix, + parity_prefix_general = \ + opt.parity_prefix_general, + generic_emptiness = opt.generic_emptiness, rabin_to_buchi = opt.rabin_to_buchi, + buchi_type_to_buchi = opt.buchi_type_to_buchi, + parity_type_to_parity = \ + opt.parity_type_to_parity, reduce_col_deg = opt.reduce_col_deg, propagate_col = opt.propagate_col, - pretty_print = opt.pretty_print, + use_generalized_rabin = \ + opt.use_generalized_rabin ) else: p1 = spot.acd_transform(aut) @@ -205,7 +296,7 @@ State: 13 [0&1] 5 [!0&!1] 10 {0 1 3 5} [0&!1] 13 {1 3} ---END--"""), [35, 30, 23, 32, 31, 28, 22, 21]) +--END--"""), [32, 22, 23, 30, 33, 45, 22, 21]) test(spot.automaton(""" HOA: v1 @@ -223,7 +314,7 @@ State: 1 [0&!1] 1 {4} [!0&1] 1 {0 1 2 3} [!0&!1] 1 {0 3} ---END--"""), [7, 5, 3, 6, 5, 5, 3, 3]) +--END--"""), [6, 3, 3, 5, 5, 26, 3, 3]) test(spot.automaton("""HOA: v1 States: 2 @@ -239,7 +330,7 @@ State: 0 State: 1 [0&1] 1 {2 3 4} [!0&!1] 0 {1 2} ---END--"""), [9, 3, 2, 3, 3, 3, 2, 2]) +--END--"""), [3, 2, 2, 9, 9, 10, 2, 2]) for i,f in enumerate(spot.randltl(10, 200)): test(spot.translate(f, "det", "G"), full=(i<50)) @@ -279,7 +370,7 @@ State: 3 [!0&1] 2 {1 4} [0&1] 3 {0} --END-- -"""), [80, 47, 104, 104, 102, 29, 6, 5]) +"""), [104, 6, 80, 23, 27, 17, 6, 5]) test(spot.automaton(""" HOA: v1 @@ -313,7 +404,7 @@ State: 4 [0&!1] 4 [0&1] 4 {1 2 4} --END-- -"""), [9, 6, 7, 7, 6, 6, 6, 6]) +"""), [6, 6, 7, 9, 9, 10, 6, 6]) test(spot.automaton(""" HOA: v1 @@ -335,7 +426,7 @@ State: 1 [0&!1] 1 {2 3} [0&1] 1 {1 2 4} --END-- -"""), [11, 3, 2, 3, 3, 3, 2, 2]) +"""), [3, 2, 2, 6, 6, 6, 2, 2]) # Tests both the old and new version of to_parity @@ -366,7 +457,7 @@ explicit-labels trans-acc --BODY-- State: 0 [0&1] 2 {4 5} [0&1] 4 {0 4} p = spot.to_parity_old(a, True) tc.assertEqual(p.num_states(), 22) tc.assertTrue(spot.are_equivalent(a, p)) -test(a, [8, 6, 6, 6, 6, 6, 6, 6]) +test(a, [6, 6, 7, 8, 6, 7, 6, 6]) # Force a few edges to false, to make sure to_parity() is OK with that. for e in a.out(2): @@ -380,7 +471,7 @@ for e in a.out(3): p = spot.to_parity_old(a, True) tc.assertEqual(p.num_states(), 22) tc.assertTrue(spot.are_equivalent(a, p)) -test(a, [7, 6, 6, 6, 6, 6, 6, 6]) +test(a, [6, 6, 7, 8, 6, 7, 6, 6]) for f in spot.randltl(4, 400): d = spot.translate(f, "det", "G") @@ -396,4 +487,4 @@ for f in spot.randltl(5, 2000): a = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det') b = spot.to_parity_old(a, True) tc.assertTrue(a.equivalent_to(b)) -test(a, [7, 7, 3, 7, 7, 7, 3, 3]) +test(a, [7, 3, 3, 8, 8, 7, 3, 3])