From 9669806cd08efbb89f2621ce88d4fb85e2d603ae Mon Sep 17 00:00:00 2001 From: Florian Renkin Date: Sun, 11 Jul 2021 00:11:04 +0200 Subject: [PATCH] Adding signature based minimization of mealy machines * spot/twaalgos/mealy_machine.cc: Here * tests/python/mealy.py: Adding tests --- spot/twaalgos/mealy_machine.cc | 565 ++++++++++++++++++++++++++++++++- tests/python/mealy.py | 205 ++++++++++++ 2 files changed, 753 insertions(+), 17 deletions(-) diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index 5b2a5aa09..fa105ef7c 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/spot/twaalgos/mealy_machine.cc @@ -20,6 +20,7 @@ #include "config.h" #include +#include #include #include #include @@ -51,6 +52,553 @@ # define dotimeprint while (0) std::cerr #endif + + +namespace +{ + // Anonymous for minimize_mealy_fast + using namespace spot; + + // Used to get the signature of the state. + typedef std::vector vector_state_bdd; + + // Get the list of state for each class. + // Note: Use map as iter. are not invalidated by inserting new elements + typedef std::map, + bdd_less_than> map_bdd_lstate; + + // This part is just a copy of a part of simulation.cc only suitable for + // deterministic monitors. + class sig_calculator final + { + protected: + typedef std::unordered_map map_bdd_bdd; + int acc_vars; + acc_cond::mark_t all_inf_; + + public: + sig_calculator(twa_graph_ptr aut, bool implications) : a_(aut), + po_size_(0), + want_implications_(implications) + { + size_a_ = a_->num_states(); + // Now, we have to get the bdd which will represent the + // class. We register one bdd by state, because in the worst + // case, |Class| == |State|. + unsigned set_num = a_->get_dict() + ->register_anonymous_variables(size_a_, this); + + bdd init = bdd_ithvar(set_num++); + + used_var_.emplace_back(init); + + // Initialize all classes to init. + previous_class_.resize(size_a_); + for (unsigned s = 0; s < size_a_; ++s) + previous_class_[s] = init; + for (unsigned i = set_num; i < set_num + size_a_ - 1; ++i) + free_var_.push(i); + + relation_.reserve(size_a_); + relation_[init] = init; + } + + // Reverse all the acceptance condition at the destruction of + // this object, because it occurs after the return of the + // function simulation. + virtual ~sig_calculator() + { + a_->get_dict()->unregister_all_my_variables(this); + } + + // Update the name of the classes. + void update_previous_class() + { + auto it_bdd = used_var_.begin(); + + // We run through the map bdd/list, and we update + // the previous_class_ with the new data. + for (auto& p : sorted_classes_) + { + // If the signature of a state is bddfalse (no + // edges) the class of this state is bddfalse + // instead of an anonymous variable. It allows + // simplifications in the signature by removing a + // edge which has as a destination a state with + // no outgoing edge. + if (p->first == bddfalse) + for (unsigned s : p->second) + previous_class_[s] = bddfalse; + else + for (unsigned s : p->second) + previous_class_[s] = *it_bdd; + ++it_bdd; + } + } + + void main_loop() + { + unsigned int nb_partition_before = 0; + unsigned int nb_po_before = po_size_ - 1; + + while (nb_partition_before != bdd_lstate_.size() + || nb_po_before != po_size_) + { + update_previous_class(); + nb_partition_before = bdd_lstate_.size(); + nb_po_before = po_size_; + po_size_ = 0; + update_sig(); + go_to_next_it(); + } + update_previous_class(); + } + + // Take a state and compute its signature. + bdd compute_sig(unsigned src) + { + bdd res = bddfalse; + + for (auto& t : a_->out(src)) + { + // to_add is a conjunction of the acceptance condition, + // the label of the edge and the class of the + // destination and all the class it implies. + bdd to_add = t.cond & relation_[previous_class_[t.dst]]; + + res |= to_add; + } + return res; + } + + void update_sig() + { + bdd_lstate_.clear(); + sorted_classes_.clear(); + for (unsigned s = 0; s < size_a_; ++s) + { + bdd sig = compute_sig(s); + auto p = bdd_lstate_.emplace(std::piecewise_construct, + std::forward_as_tuple(sig), + std::forward_as_tuple(1, s)); + if (p.second) + sorted_classes_.emplace_back(p.first); + else + p.first->second.emplace_back(s); + } + } + + // This method renames the color set, updates the partial order. + void go_to_next_it() + { + int nb_new_color = bdd_lstate_.size() - used_var_.size(); + + // If we have created more partitions, we need to use more + // variables. + for (int i = 0; i < nb_new_color; ++i) + { + assert(!free_var_.empty()); + used_var_.emplace_back(bdd_ithvar(free_var_.front())); + free_var_.pop(); + } + + // If we have reduced the number of partition, we 'free' them + // in the free_var_ list. + for (int i = 0; i > nb_new_color; --i) + { + assert(!used_var_.empty()); + free_var_.push(bdd_var(used_var_.front())); + used_var_.pop_front(); + } + + assert((bdd_lstate_.size() == used_var_.size()) + || (bdd_lstate_.find(bddfalse) != bdd_lstate_.end() + && bdd_lstate_.size() == used_var_.size() + 1)); + + // This vector links the tuple "C^(i-1), N^(i-1)" to the + // new class coloring for the next iteration. + std::vector> now_to_next; + unsigned sz = bdd_lstate_.size(); + now_to_next.reserve(sz); + + auto it_bdd = used_var_.begin(); + + for (auto& p : sorted_classes_) + { + // If the signature of a state is bddfalse (no edges) the + // class of this state is bddfalse instead of an anonymous + // variable. It allows simplifications in the signature by + // removing an edge which has as a destination a state + // with no outgoing edge. + bdd acc = bddfalse; + if (p->first != bddfalse) + acc = *it_bdd; + now_to_next.emplace_back(p->first, acc); + ++it_bdd; + } + + // Update the partial order. + + // This loop follows the pattern given by the paper. + // foreach class do + // | foreach class do + // | | update po if needed + // | od + // od + + for (unsigned n = 0; n < sz; ++n) + { + bdd n_sig = now_to_next[n].first; + bdd n_class = now_to_next[n].second; + if (want_implications_) + for (unsigned m = 0; m < sz; ++m) + { + if (n == m) + continue; + if (bdd_implies(n_sig, now_to_next[m].first)) + { + n_class &= now_to_next[m].second; + ++po_size_; + } + } + relation_[now_to_next[n].second] = n_class; + } + } + + // The list of states for each class at the current_iteration. + // Computed in `update_sig'. + map_bdd_lstate bdd_lstate_; + + protected: + // The automaton which is reduced. + twa_graph_ptr a_; + + // Implications between classes. + map_bdd_bdd relation_; + + // Represent the class of each state at the previous iteration. + vector_state_bdd previous_class_; + + // The above map, sorted by states number instead of BDD + // identifier to avoid non-determinism while iterating over all + // states. + std::vector sorted_classes_; + + // The queue of free bdd. They will be used as the identifier + // for the class. + std::queue free_var_; + + // The list of used bdd. They are in used as identifier for class. + std::deque used_var_; + + // Size of the automaton. + unsigned int size_a_; + + // Used to know when there is no evolution in the partial order. + unsigned int po_size_; + + // Whether to compute implications between classes. This is costly + // and useless when we want to recognize the same language. + bool want_implications_; + }; + + // An acyclic digraph such that there is an edge q1 -> q2 if + // q1.label_ ⇒ q2.label_ + class bdd_digraph + { + private: + bdd label_; + unsigned state_; + std::vector> children_; + + public: + bdd_digraph() : label_(bddtrue), state_(-1U) {} + + bdd_digraph(bdd label, unsigned state) : label_(label), state_(state) {} + + void + all_children_aux_(std::set>& res) + { + for (auto c : children_) + if (res.insert(c).second) + c->all_children_aux_(res); + } + + std::set> + all_children() + { + std::set> res; + all_children_aux_(res); + return res; + } + + void + add_aux_(std::shared_ptr& new_node, std::vector& done) + { + // Avoid doing twice the same state + if (state_ != -1U) + done[state_] = true; + for (auto& ch : children_) + { + if (done[ch->state_]) + continue; + if (bdd_implies(new_node->label_, ch->label_)) + ch->add_aux_(new_node, done); + else if (bdd_implies(ch->label_, new_node->label_)) + { + auto ch_nodes = ch->all_children(); + new_node->children_.push_back(ch); + for (auto& x : ch_nodes) + new_node->children_.push_back(x); + } + } + assert(bdd_implies(new_node->label_, label_)); + children_.push_back(new_node); + } + + void + add(std::shared_ptr& new_node, bool rec, + unsigned max_state) + { + if (new_node->label_ == bddtrue) + { + assert(label_ == bddtrue); + state_ = new_node->state_; + return; + } + if (rec) + { + std::vector done(max_state, false); + add_aux_(new_node, done); + } + else + children_.push_back(new_node); + } + + unsigned + flatten_aux(std::unordered_map& res) + { + if (children_.empty()) + { + res.insert({label_, state_}); + return state_; + } + auto ch_size = children_.size(); + unsigned pos = ch_size - 1; + auto my_repr = children_[pos]->flatten_aux(res); + res.insert({label_, my_repr}); + for (unsigned i = 0; i < ch_size; ++i) + { + if (i == pos) + continue; + children_[i]->flatten_aux(res); + } + return my_repr; + } + + std::unordered_map + flatten() + { + std::unordered_map res; + flatten_aux(res); + return res; + } + + // Transforms children_ such that the child with the higher use_count() is + // at the end. + void + sort_nodes() + { + if (!children_.empty()) + { + auto max_pos = std::max_element(children_.begin(), children_.end(), + [](const std::shared_ptr& n1, + const std::shared_ptr& n2) + { + return n1.use_count() < n2.use_count(); + }); + std::iter_swap(max_pos, children_.end() - 1); + } + } + }; + + + // Associate to a state a representative. The first value of the result + // is -1U if ∀i repr[i] = i + std::vector + get_repres(twa_graph_ptr& a, bool rec) + { + const auto a_num_states = a->num_states(); + + std::vector repr(a_num_states); + bdd_digraph graph; + std::vector signatures(a_num_states); + sig_calculator red(a, rec); + red.main_loop(); + if (!rec && red.bdd_lstate_.size() == a_num_states) + { + repr[0] = -1U; + return repr; + } + for (auto& [sig, states] : red.bdd_lstate_) + { + assert(!states.empty()); + bool in_tree = false; + for (auto state : states) + { + signatures[state] = sig; + // If it is not the first iteration, le BDD is already in the graph. + if (!in_tree) + { + in_tree = true; + auto new_node = + std::make_shared(bdd_digraph(sig, state)); + graph.add(new_node, rec, a_num_states); + } + } + } + graph.sort_nodes(); + auto repr_map = graph.flatten(); + + bool is_useless_map = true; + for (unsigned i = 0; i < a_num_states; ++i) + { + repr[i] = repr_map[signatures[i]]; + is_useless_map &= (repr[i] == i); + } + + if (is_useless_map) + { + repr[0] = -1U; + return repr; + } + return repr; + } +} + +namespace spot +{ + twa_graph_ptr minimize_mealy_fast(const const_twa_graph_ptr& mm, + bool use_inclusion) + { + bool orig_is_split = true; + bdd* outsptr = nullptr; + bdd outs = bddfalse; + + twa_graph_ptr mmc; + if (mm->get_named_prop>("state-player") != nullptr) + { + outsptr = mm->get_named_prop("synthesis-outputs"); + assert(outsptr && "If the original strat is split, " + "we need \"synthesis-outputs\"."); + outs = *outsptr; + mmc = unsplit_2step(mm); + } + else + { + mmc = make_twa_graph(mm, twa::prop_set::all()); + mmc->copy_ap_of(mm); + mmc->copy_acceptance_of(mm); + orig_is_split = false; + } + + minimize_mealy_fast_here(mmc, use_inclusion); + + // Split if the initial aut was split + if (orig_is_split) + { + bdd ins = bddtrue; + for (const auto& ap : mmc->ap()) + if (!bdd_implies(outs, + bdd_ithvar(mmc->register_ap(ap)))) + ins &= bdd_ithvar(mmc->register_ap(ap)); + mmc = split_2step(mmc, ins, outs, false, false); + bool orig_init_player = + mm->get_named_prop>("state-player") + ->at(mm->get_init_state_number()); + alternate_players(mmc, orig_init_player, false); + } + // Try to set outputs + if (outsptr) + mmc->set_named_prop("synthesis-outputs", new bdd(outs)); + + return mmc; + } + + void minimize_mealy_fast_here(twa_graph_ptr& mm, bool use_inclusion) + { + + bool orig_is_split = false; + bdd* outsptr = nullptr; + bdd outs = bddfalse; + + auto sp_ptr = mm->get_named_prop>("state-player"); + + bool init_player = sp_ptr ? sp_ptr->at(mm->get_init_state_number()) + : false; + + // Only consider infinite runs + mm->purge_dead_states(); + + if (mm->get_named_prop>("state-player") != nullptr) + { + // Check if done + if (std::count(sp_ptr->begin(), sp_ptr->end(), false) == 1) + return; + outsptr = mm->get_named_prop("synthesis-outputs"); + assert(outsptr && "If the original strat is split, " + "we need \"synthesis-outputs\"."); + outs = *outsptr; + init_player = + mm->get_named_prop>("state-player")->at( + mm->get_init_state_number()); + mm = unsplit_2step(mm); + orig_is_split = true; + } + else + // Check if done + if (mm->num_states() == 1) + return; + + auto repr = get_repres(mm, use_inclusion); + if (repr[0] == -1U) + return; + + // Change the destination of transitions using a DFT to avoid useless + // modifications. + auto init = repr[mm->get_init_state_number()]; + mm->set_init_state(init); + std::stack todo; + std::vector done(mm->num_states(), false); + todo.emplace(init); + while (!todo.empty()) + { + auto current = todo.top(); + todo.pop(); + done[current] = true; + for (auto& e : mm->out(current)) + { + auto repr_dst = repr[e.dst]; + e.dst = repr_dst; + if (!done[repr_dst]) + todo.emplace(repr_dst); + } + } + mm->purge_unreachable_states(); + if (orig_is_split) + { + bdd ins = bddtrue; + for (const auto& ap : mm->ap()) + if (!bdd_implies(outs, + bdd_ithvar(mm->register_ap(ap)))) + ins &= bdd_ithvar(mm->register_ap(ap)); + mm = split_2step(mm, ins, outs, false, false); + alternate_players(mm, init_player, false); + mm->set_named_prop("synthesis-outputs", new bdd(outs)); + } + } +} + // Anonymous for mealy_min namespace { @@ -3058,23 +3606,6 @@ namespace spot namespace spot { - - void minimize_mealy_fast_here(twa_graph_ptr& mm, - bool use_inclusion) - { - (void) mm; - (void) use_inclusion; - } - - twa_graph_ptr minimize_mealy_fast(const const_twa_graph_ptr& mm, - bool use_inclusion) - { - // Dummy for now - (void) use_inclusion; - return make_twa_graph(mm, twa::prop_set::all()); - } - - bool is_mealy_specialization(const_twa_graph_ptr left, const_twa_graph_ptr right, bool verbose) diff --git a/tests/python/mealy.py b/tests/python/mealy.py index 8f6fdac75..382bfc786 100644 --- a/tests/python/mealy.py +++ b/tests/python/mealy.py @@ -20,6 +20,8 @@ import spot, buddy +# Testing Sat-based approach + # Empty bdd intersection bug test # See issue #472 true = buddy.bddtrue @@ -380,7 +382,210 @@ for (mealy_str, nenv_min) in test_auts: assert(spot.is_mealy_specialization(mealy, mealy_min_us_s, True)) +# Testing bisimulation (with output assignment) +# Syntcomp: Alarm_2d1010f8.tlsf +aut = spot.automaton("""HOA: v1 +States: 17 +Start: 0 +AP: 6 "u02alarm29control02alarm29control" +"u02alarm29control0f1d2alarm29turn2off1b" +"u02alarm29control0f1d2alarm29turn2on1b" "p0p0off02alarm29intent" +"p0p0on02alarm29intent" "p0b02alarm29alarm" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 +[!0&!1&2&!3&!4 | !0&!1&2&3&4 | !0&1&!2&!3&!4 | !0&1&!2&3&4 | 0&!1&!2&!3&!4 + | 0&!1&!2&3&4] 1 +[!0&!1&2&!3&4&!5 | !0&!1&2&3&!4&5] 2 +[!0&!1&2&!3&4&5 | !0&!1&2&3&!4&!5] 3 +State: 1 +[!0&!1&2 | !0&1&!2 | 0&!1&!2] 1 +State: 2 +[!0&!1&2&!3&!4 | !0&!1&2&3&4 | !0&1&!2&!3&!4 | !0&1&!2&3&4 | 0&!1&!2&!3&!4 + | 0&!1&!2&3&4] 4 +[!0&!1&2&!3&4&!5] 5 +[!0&!1&2&3&!4&!5] 6 +[!0&!1&2&!3&4&5] 7 +[!0&1&!2&3&!4&5] 8 +State: 3 +[!0&!1&2&3&!4&5] 2 +[!0&!1&2&!3&!4 | !0&!1&2&3&4 | !0&1&!2&!3&!4 | !0&1&!2&3&4 | 0&!1&!2&!3&!4 + | 0&!1&!2&3&4] 4 +[!0&!1&2&!3&4&!5] 5 +[!0&!1&2&3&!4&!5] 6 +[!0&!1&2&!3&4&5] 7 +State: 4 +[!0&!1&2&!3&!4 | !0&!1&2&3&4 | !0&!1&2&!4&5 | !0&1&!2&!3&!4 | !0&1&!2&3&4 + | !0&1&!2&!4&5 | 0&!1&!2&!3&!4 | 0&!1&!2&3&4 | 0&!1&!2&!4&5] 4 +[!0&!1&2&!3&4 | !0&1&!2&!3&4 | 0&!1&!2&!3&4] 9 +[!0&!1&2&3&!4&!5 | !0&1&!2&3&!4&!5 | 0&!1&!2&3&!4&!5] 10 +State: 5 +[!0&!1&2&!3&!4 | !0&1&!2&!3&!4 | 0&!1&!2&!3&!4] 4 +[!0&!1&2&!3&4] 5 +[!0&!1&2&3&4 | !0&1&!2&3&4 | 0&!1&!2&3&4] 9 +[!0&!1&2&3&!4] 11 +State: 6 +[!0&!1&2&!3&!4 | !0&!1&2&3&4&5 | !0&1&!2&!3&!4 | !0&1&!2&3&4&5 | 0&!1&!2&!3&!4 + | 0&!1&!2&3&4&5] 4 +[!0&!1&2&!3&4] 5 +[!0&!1&2&3&!4&!5] 6 +[!0&!1&2&3&!4&5] 11 +[!0&!1&2&3&4&!5 | !0&1&!2&3&4&!5 | 0&!1&!2&3&4&!5] 10 +State: 7 +[!0&!1&2&3&!4&5] 2 +[!0&!1&2&!3&!4 | !0&1&!2&!3&!4 | 0&!1&!2&!3&!4] 4 +[!0&!1&2&!3&4&!5] 5 +[!0&!1&2&!3&4&5] 7 +[!0&!1&2&3&4&!5 | !0&1&!2&3&4&!5 | 0&!1&!2&3&4&!5] 9 +[!0&!1&2&3&!4&!5] 11 +[!0&!1&2&3&4&5 | !0&1&!2&3&4&5 | 0&!1&!2&3&4&5] 12 +State: 8 +[!0&!1&2&!3&!4 | !0&!1&2&3&4 | !0&1&!2&!3&!4 | !0&1&!2&3&4 | 0&!1&!2&!3&!4 + | 0&!1&!2&3&4] 4 +[!0&!1&2&3&!4&5] 11 +[!0&!1&2&!3&4&5] 13 +[!0&!1&2&!3&4&!5] 14 +[!0&1&!2&3&!4&!5] 15 +State: 9 +[!0&!1&2&!4 | !0&1&!2&!4 | 0&!1&!2&!4] 4 +[!0&!1&2&4 | !0&1&!2&4 | 0&!1&!2&4] 9 +State: 10 +[!0&!1&2&!3&!4 | !0&!1&2&3&5 | !0&1&!2&!3&!4 | !0&1&!2&3&5 | 0&!1&!2&!3&!4 + | 0&!1&!2&3&5] 4 +[!0&!1&2&!3&4 | !0&1&!2&!3&4 | 0&!1&!2&!3&4] 9 +[!0&!1&2&3&!5 | !0&1&!2&3&!5 | 0&!1&!2&3&!5] 10 +State: 11 +[!0&!1&2&!3&!4 | !0&!1&2&3&4 | !0&1&!2&!3&!4 | !0&1&!2&3&4 | 0&!1&!2&!3&!4 + | 0&!1&!2&3&4] 4 +[!0&!1&2&!3&4] 5 +[!0&!1&2&3&!4&!5] 6 +[!0&!1&2&3&!4&5] 11 +State: 12 +[!0&!1&2&!4 | !0&1&!2&!4 | 0&!1&!2&!4] 4 +[!0&!1&2&4&!5 | !0&1&!2&4&!5 | 0&!1&!2&4&!5] 9 +[!0&!1&2&4&5 | !0&1&!2&4&5 | 0&!1&!2&4&5] 12 +State: 13 +[!0&!1&2&!3&!4 | !0&1&!2&!3&!4 | 0&!1&!2&!3&!4] 4 +[!0&!1&2&!3&4&!5] 5 +[!0&!1&2&3&4&!5 | !0&1&!2&3&4&!5 | 0&!1&!2&3&4&!5] 9 +[!0&!1&2&3&!4] 11 +[!0&!1&2&3&4&5 | !0&1&!2&3&4&5 | 0&!1&!2&3&4&5] 12 +[!0&!1&2&!3&4&5] 13 +State: 14 +[!0&!1&2&3&!4&5] 2 +[!0&!1&2&!3&!4 | !0&1&!2&!3&!4 | 0&!1&!2&!3&!4] 4 +[!0&!1&2&!3&4&!5] 5 +[!0&!1&2&!3&4&5] 7 +[!0&!1&2&3&4 | !0&1&!2&3&4 | 0&!1&!2&3&4] 9 +[!0&!1&2&3&!4&!5] 11 +State: 15 +[!0&!1&2&!3&!4 | !0&!1&2&3&4&5 | !0&1&!2&!3&!4 | !0&1&!2&3&4&5 | 0&!1&!2&!3&!4 + | 0&!1&!2&3&4&5] 4 +[!0&!1&2&!3&4&5] 5 +[!0&!1&2&3&!4&5] 11 +[!0&!1&2&!3&4&!5] 14 +[!0&1&!2&3&!4&!5] 15 +[!0&!1&2&3&4&!5 | !0&1&!2&3&4&!5 | 0&!1&!2&3&4&!5] 16 +State: 16 +[!0&!1&2&!3&!4 | !0&!1&2&3&5 | !0&1&!2&!3&!4 | !0&1&!2&3&5 | 0&!1&!2&!3&!4 + | 0&!1&!2&3&5] 4 +[!0&!1&2&!3&4 | !0&1&!2&!3&4 | 0&!1&!2&!3&4] 9 +[!0&!1&2&3&!5 | !0&1&!2&3&!5 | 0&!1&!2&3&!5] 16 +--END--""") + +# Build an equivalent deterministic monitor +min_equiv = spot.minimize_mealy_fast(aut, False) +assert min_equiv.num_states() == 6 +assert spot.are_equivalent(min_equiv, aut) + +# Build an automaton that recognizes a subset of the language of the original +# automaton +min_sub = spot.minimize_mealy_fast(aut, True) +assert min_sub.num_states() == 5 +prod = spot.product(spot.complement(aut), min_sub) +assert spot.generic_emptiness_check(prod) + +aut = spot.automaton(""" +HOA: v1 +States: 4 +Start: 0 +AP: 2 "a" "b" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 +[!0&!1] 1 +[!0&1] 2 +[0] 3 +State: 1 +[0] 1 +State: 2 +[1] 2 +State: 3 +[0&1] 3 +--END-- +""") + +exp = """HOA: v1 +States: 1 +Start: 0 +AP: 2 "a" "b" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 +[0&1] 0 +--END--""" + +# An example that shows that we should not build a tree when we use inclusion. +res = spot.minimize_mealy_fast(aut, True) +assert res.to_str() == exp + +aut = spot.automaton(""" +HOA: v1 +States: 4 +Start: 0 +AP: 2 "a" "b" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[!0&!1] 1 +[!0&1] 2 +[0&!1] 3 +State: 1 +[0] 1 +State: 2 +[1] 2 +State: 3 +[0&1] 3 +--END-- +""") + +exp = """HOA: v1 +States: 2 +Start: 0 +AP: 2 "a" "b" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 +[!0&!1] 1 +[!0&1] 1 +[0&!1] 1 +State: 1 +[0&1] 1 +--END--""" + +res = spot.minimize_mealy_fast(aut, True) +assert res.to_str() == exp