From 3bcffa2fcdb1578d96d78a45cd9329b649159d20 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 18 Mar 2024 16:31:07 +0100 Subject: [PATCH] split: add separate_edges() and a edge_separator class This generalizes (and replaces) the two-argument split that was introduced in c2832cabfc. * spot/twaalgos/split.cc, spot/twaalgos/split.hh (edge_separator): New class. (separate_edges): New function. (split_edges): Remove the two argument version. * spot/twaalgos/forq_contains.cc: Adjust to use the edge_separator class. * tests/python/splitedge.py: Adjust test case. * tests/python/split.ipynb: New file. * tests/Makefile.am, doc/org/tut.org: Add it. * NEWS: Mention it. --- NEWS | 3 + doc/org/tut.org | 1 + spot/twaalgos/forq_contains.cc | 17 +- spot/twaalgos/split.cc | 230 +--- spot/twaalgos/split.hh | 197 ++- tests/Makefile.am | 1 + tests/python/split.ipynb | 2139 ++++++++++++++++++++++++++++++++ tests/python/splitedge.py | 7 +- 8 files changed, 2395 insertions(+), 200 deletions(-) create mode 100644 tests/python/split.ipynb diff --git a/NEWS b/NEWS index 9da91b234..832e0fd61 100644 --- a/NEWS +++ b/NEWS @@ -135,6 +135,9 @@ New in spot 2.11.6.dev (not yet released) Büchi automaton will always return a Büchi automaton. For those, a "keep_one_color" option has been added to scc_filter. + - spot::separate_edges() and spot::edge_separator offers more ways + to split labels. See https://spot.lrde.epita.fr/ipynb/split.html + - ltsmin's interface will now point to README.ltsmin in case an error is found while running divine or spins. diff --git a/doc/org/tut.org b/doc/org/tut.org index 8ae701bc5..c3833ff5d 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -71,6 +71,7 @@ real notebooks instead. conditions - [[https://spot.lrde.epita.fr/ipynb/contains.html][=contains.ipynb=]] demonstrates containment checks between formulas or automata +- [[https://spot.lrde.epita.fr/ipynb/split.html][=split.ipynb=]] illustrates various ways to split labels - [[https://spot.lrde.epita.fr/ipynb/parity.html][=parity.ipynb=]] documents algorithms for manipulating parity automata in Python - [[https://spot.lrde.epita.fr/ipynb/games.html][=games.ipynb=]] illustrates support for games diff --git a/spot/twaalgos/forq_contains.cc b/spot/twaalgos/forq_contains.cc index 4d4264ae2..bc76146bd 100644 --- a/spot/twaalgos/forq_contains.cc +++ b/spot/twaalgos/forq_contains.cc @@ -695,19 +695,6 @@ namespace spot::forq::util return all_states; } - // Create a list of bdds, where each corresponds to an edge in B - static std::vector create_edge_splitting_basis(const_graph const& B) - { - auto edges = B->edges(); - std::unordered_set out; - std::transform(edges.begin(), edges.end(), std::inserter(out, out.begin()), - [](auto& edge) - { - return edge.cond; - }); - return std::vector(out.begin(), out.end()); - } - forq_context create_forq_context(const_graph const& A, const_graph const& B) { forq_context retval; @@ -715,7 +702,9 @@ namespace spot::forq::util retval.B.outgoing = util::generate_outgoing_states(B); retval.B.final_edges = get_final_edges(B); - retval.A.aut = split_edges(A, create_edge_splitting_basis(B)); + edge_separator es; + es.add_to_basis(B); + retval.A.aut = es.separate_compat(A); retval.A.outgoing = util::generate_outgoing_states(retval.A.aut); retval.A.final_edges = get_final_edges(retval.A.aut); retval.cache.precomputed_ipost.resize(B->num_states()); diff --git a/spot/twaalgos/split.cc b/spot/twaalgos/split.cc index 8e40f79a5..a4d973d58 100644 --- a/spot/twaalgos/split.cc +++ b/spot/twaalgos/split.cc @@ -22,180 +22,10 @@ #include #include -namespace std -{ - template<> - struct hash<::bdd> - { - size_t operator()(::bdd const& instance) const noexcept - { - return ::spot::bdd_hash{}(instance); - } - }; - - template<> - struct hash> - { - size_t operator()(pair const& x) const noexcept - { - size_t first_hash = std::hash()(x.first); - size_t second_hash = std::hash()(x.second); - size_t sum = second_hash - + 0x9e3779b9 - + (first_hash << 6) - + (first_hash >> 2); - return first_hash ^ sum; - } - }; -} - namespace spot { namespace { - // We attempt to add a potentially new set of symbols defined as "value" to - // our current set of edge partitions, "current_set". We also specify a set - // of valid symbols considered - static void - add_to_lower_bound_set_helper(std::unordered_set& current_set, - bdd valid_symbol_set, bdd value) - { - // This function's correctness is defined by the invariant, that - // we never add a bdd to our current set unless the bdd is - // disjoint from every other element in the current_set. In - // other words, we will only reach the final set.insert(value), - // if we can iterate over the whole of current_set without - // finding some set intersections - if (value == bddfalse) // Don't add empty sets, as they subsume everything - { - return; - } - for (auto sym : current_set) - { - // If a sym is a subset of value, recursively add the set of symbols - // defined in value, but not in sym. This ensures the two elements - // are disjoint. - if (bdd_implies(sym, value)) - { - add_to_lower_bound_set_helper(current_set, - valid_symbol_set, - (value - sym) & valid_symbol_set); - return; - } - // If a sym is a subset of the value we're trying to add, then we - // remove the symbol and add the two symbols created by partitioning - // the sym with value. - else if (bdd_implies(value, sym)) - { - current_set.erase(sym); - add_to_lower_bound_set_helper(current_set, - valid_symbol_set, - sym & value); - add_to_lower_bound_set_helper(current_set, - valid_symbol_set, - sym - value); - return; - } - } - // This line is only reachable if value is not a subset and doesn't - // subsume any element currently in our set - current_set.insert(value); - } - - using bdd_set = std::unordered_set; - using bdd_pair_set = std::unordered_set>; - - // Transforms each element of the basis into a complement pair, - // with a valid symbol set specified - static bdd_pair_set create_complement_pairs(std::vector const& basis, - bdd valid_symbol_set) - { - bdd_pair_set intersections; - for (bdd sym: basis) - { - bdd intersection = sym & valid_symbol_set; - if (intersection != bddfalse) - { - bdd negation = valid_symbol_set - intersection; - intersections.insert(std::make_pair(intersection, negation)); - } - } - return intersections; - } - - template - void iterate_possible_intersections(bdd_pair_set const& complement_pairs, - bdd valid_symbol_set, - Callable callable) - { - for (auto it = complement_pairs.begin(); - it != complement_pairs.end(); ++it) - for (auto it2 = std::next(it); it2 != complement_pairs.end(); ++it2) - { - auto intermediate = it2->first & valid_symbol_set; - auto intermediate2 = it2->second & valid_symbol_set; - callable(it->first & intermediate); - callable(it->second & intermediate); - callable(it->first & intermediate2); - callable(it->second & intermediate2); - } - } - - // Compute the lower set bound of a set. A valid symbol set is also - // provided to make sure that no symbol exists in the output if it is - // not also included in the valid symbol set - static bdd_set lower_set_bound(std::vector const& basis, - bdd valid_symbol_set) - { - auto complement_pairs = create_complement_pairs(basis, valid_symbol_set); - if (complement_pairs.size() == 1) - { - bdd_set lower_bound; - auto& pair = *complement_pairs.begin(); - if (pair.first != bddfalse - && bdd_implies(pair.first, valid_symbol_set)) - lower_bound.insert(pair.first); - if (pair.second != bddfalse - && bdd_implies(pair.second, valid_symbol_set)) - lower_bound.insert(pair.second); - return lower_bound; - } - else - { - bdd_set lower_bound; - iterate_possible_intersections(complement_pairs, valid_symbol_set, - [&](auto intersection) - { - add_to_lower_bound_set_helper(lower_bound, - valid_symbol_set, - intersection); - }); - return lower_bound; - } - } - - // Partitions a symbol based on a list of other bdds called the - // basis. The resulting partition will have the property that for - // any partitioned element and any element element in the basis, - // the partitioned element will either by completely contained by - // that element of the basis, or completely disjoint. - static bdd_set - generate_contained_or_disjoint_symbols(bdd sym, - std::vector const& basis) - { - auto lower_bound = lower_set_bound(basis, sym); - // If the sym was disjoint from everything in the basis, we'll - // be left with an empty lower_bound. To fix this, we will - // simply return a singleton, with sym as the only - // element. Notice, this singleton will satisfy the requirements - // of a return value from this function. Additionally, if the - // sym is false, that means nothing can traverse it, so we - // simply are left with no edges. - if (lower_bound.empty() && sym != bddfalse) - lower_bound.insert(sym); - return lower_bound; - } - template twa_graph_ptr split_edges_aux(const const_twa_graph_ptr& aut, genlabels gen) @@ -217,7 +47,7 @@ namespace spot // robin_hood::unordered_map with GCC 9.4. Use robin_hood::pair // instead. typedef robin_hood::pair cached_t; - robin_hood::unordered_map split_cond; + robin_hood::unordered_map split_cond; internal::univ_dest_mapper uniq(out->get_graph()); @@ -260,12 +90,60 @@ namespace spot }); } - twa_graph_ptr split_edges(const const_twa_graph_ptr& aut, - std::vector const& basis) + void edge_separator::add_to_basis(bdd label) { - bdd all = aut->ap_vars(); - return split_edges_aux(aut, [&](bdd cond) { - return generate_contained_or_disjoint_symbols(cond, basis); + if (label == bddfalse) + return; + // Split our current set of labels using this new one. + // + // Do not use a range-based or iterator-based for loop here, + // as push_back invalidates the end iterator. + for (unsigned cur = 0, sz = basis_.size(); cur < sz; ++cur) + if (bdd common = basis_[cur] & label; + common != bddfalse && common != basis_[cur]) + { + basis_[cur] -= label; + basis_.push_back(common); + } + } + + void edge_separator::add_to_basis(const const_twa_graph_ptr& aut) + { + for (formula f: aut->ap()) + aps_.insert(f); + + robin_hood::unordered_set seen{bddtrue.id()}; + for (auto& e: aut->edges()) + if (bdd lab = e.cond; seen.insert(lab.id()).second) + add_to_basis(lab); + } + + twa_graph_ptr + edge_separator::separate_implying(const const_twa_graph_ptr& aut) + { + auto res = split_edges_aux(aut, [this](bdd cond) { + return this->separate_implying(cond); }); + for (formula f: aps_) + res->register_ap(f); + return res; + } + + twa_graph_ptr + edge_separator::separate_compat(const const_twa_graph_ptr& aut) + { + auto res = split_edges_aux(aut, [this](bdd cond) { + return this->separate_compat(cond); + }); + for (formula f: aps_) + res->register_ap(f); + return res; + } + + twa_graph_ptr separate_edges(const const_twa_graph_ptr& aut) + { + edge_separator es; + es.add_to_basis(aut); + return es.separate_implying(aut); } } diff --git a/spot/twaalgos/split.hh b/spot/twaalgos/split.hh index 63304db1e..a30d8645e 100644 --- a/spot/twaalgos/split.hh +++ b/spot/twaalgos/split.hh @@ -28,17 +28,198 @@ namespace spot /// /// Create a new version of the automaton where all edges are split /// so that they are all labeled by a conjunction of all atomic - /// propositions. After this we can consider that each edge of the - /// automate is a transition labeled by one letter. + /// propositions. + /// + /// So if an edge is labeled by "true", it will be split into + /// $2^{AP}$ distinct edges. + /// + /// After this we can consider that each edge of the automaton is a + /// transition labeled by one of $2^{AP}$ letters. + /// + /// \see separate_edges SPOT_API twa_graph_ptr split_edges(const const_twa_graph_ptr& aut); +#ifndef SWIG + // pseudo container that we use to iterate over + // the items of LABELS that are compatible with COND. + template + struct SPOT_API edge_separator_filter + { + edge_separator_filter(const std::vector& labels, bdd cond) + : labels_(labels), cond_(cond) + { + } + + class iterator + { + std::vector::const_iterator pos_; + std::vector const& labels_; + bdd cond_; + + public: + iterator(const std::vector& labels, bdd cond) + : labels_(labels), cond_(cond) + { + pos_ = labels_.begin(); + next(); + } + + iterator& operator++() + { + ++pos_; + next(); + return *this; + } + + void next() + { + // If subsumed is true, we want to match the labels + // that imply the current condition. Otherwise we + // want to match the labels that are compatible. + while (pos_ != labels_.end() && + ((subsumed && !bdd_implies(*pos_, cond_)) + || (!subsumed && (*pos_ & cond_) == bddfalse))) + ++pos_; + } + + bdd operator*() const + { + if (subsumed) + return *pos_; + else + return *pos_ & cond_; + } + + bool operator==(const iterator& other) const + { + return pos_ == other.pos_; + } + + bool operator!=(const iterator& other) const + { + return pos_ != other.pos_; + } + + bool operator==(std::vector::const_iterator pos) const + { + return pos_ == pos; + } + + bool operator!=(std::vector::const_iterator pos) const + { + return pos_ != pos; + } + }; + + iterator begin() const + { + return iterator(labels_, cond_); + } + + std::vector::const_iterator end() const + { + return labels_.end(); + } + + private: + const std::vector& labels_; + bdd cond_; + }; +#endif + + /// \ingroup twa_misc - /// \brief transform edges into transitions based on set of bdds + /// \brief separate edges so that their labels are disjoint + /// + /// To use this class, first call add_to_basis() for each label that + /// you want to separate. Then call separate() to get a new + /// automaton. + /// + /// Note that all labels seen by separate() should have been + /// previously declared using add_to_basis(), but more can be + /// declared. + /// + /// For instance an automaton has labels in {a,b,!a&!b&c} and those + /// are used as basis, the separated automaton should have its + /// labels among {a&!b,a&b,!a&b,!a&!b&c}. + class SPOT_API edge_separator + { + public: + /// \brief add label(s) to a basis + /// + /// Add a single label, or all the labels of an automaton. + /// + /// The version that takes an automaton will also record the + /// atomic propositions used by the automaton. Those atomic + /// propositions will be registered by separate_implying() or + /// separate_compat(). If you call the BDD version of + /// add_to_basis() and add a new atomic proposition, you should + /// remember to register it in the result of separate_implying() + /// or separate_compat() yourself. + /// @{ + void add_to_basis(bdd label); + void add_to_basis(const const_twa_graph_ptr& aut); + /// @} + /// \brief Separate an automaton + /// + /// This variant replaces each edge labeled by L by an edge + /// for each label of the basis that is implies L. This + /// faster than separate_compat when all edges of aut have + /// been declared in the basis. + twa_graph_ptr separate_implying(const const_twa_graph_ptr& aut); + /// \brief Separate an automaton + /// + /// This variant replaces each edge labeled by L by an edge for + /// each label of the basis that compatible implies L. This + /// faster than separate_compat when all edges of aut have been + /// declared in the basis. + twa_graph_ptr separate_compat(const const_twa_graph_ptr& aut); +#ifndef SWIG + /// \brief Separate a label + /// + /// This returns a pseudo-container that can be used to iterate + /// over the elements of the basis that imply the current label. + /// + /// For instance if the basis was created from {a,b} (i.e., the + /// basis is actually {!a&!b,a&!b,!a&b,a&b}), and the label is + /// {a}, the result will be {a&!b,a&b}. + edge_separator_filter separate_implying(bdd label) + { + return {basis_, label}; + } + /// \brief Separate a label + /// + /// This returns a pseudo-container that can be used to iterate + /// over the elements of the basis compatible with the current labal. + /// + /// For instance if the basis was created from {a,b} (i.e., the + /// basis is actually {!a&!b,a&!b,!a&b,a&b}), and the label is + /// {c&a}, the result will be {a&!b&c,a&b&c}. + edge_separator_filter separate_compat(bdd label) + { + return {basis_, label}; + } +#endif + unsigned basis_size() const + { + return basis_.size(); + } + private: + std::vector basis_{bddtrue}; + std::set aps_; + }; + + /// \ingroup twa_misc + /// \brief Make edge labels disjoints /// /// Create a new version of the automaton where all edges are split - /// such that, for any transformed edge and any set of symbols in - /// the basis, the transformed edge is either completely disjoint - /// from the set of symbols, or it is a subset of them. - SPOT_API twa_graph_ptr split_edges( - const const_twa_graph_ptr& aut, std::vector const& basis); + /// in such a way that two labels are either equal or disjoint. + /// + /// For instance if the automaton uses only {a,b,!a&!b&c} as labels, + /// the result should have label among {a&!b,a&b,!a&b,!a&!b&c}. + /// + /// Using split_edges() also creates an automaton with separated labels, + /// but the separation will be much finer since it will result in a much + /// involves all atomtic proposition. + SPOT_API twa_graph_ptr separate_edges(const const_twa_graph_ptr& aut); } diff --git a/tests/Makefile.am b/tests/Makefile.am index 4a36a725b..c6430b2ac 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -378,6 +378,7 @@ TESTS_ipython = \ python/randaut.ipynb \ python/randltl.ipynb \ python/satmin.ipynb \ + python/split.ipynb \ python/stutter-inv.ipynb \ python/synthesis.ipynb \ python/testingaut.ipynb \ diff --git a/tests/python/split.ipynb b/tests/python/split.ipynb new file mode 100644 index 000000000..3ef8bc9a5 --- /dev/null +++ b/tests/python/split.ipynb @@ -0,0 +1,2139 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "edc9ac7a", + "metadata": {}, + "source": [ + "In Spot, automata edges are labeled by Boolean functions over atomic propositions.\n", + "As a consequence, it is sometimes difficult to adapt algorithms that expect automata labeled by letters. This notebook presents methods that can be used to split those edge labels to make it easier to consider them as letters." + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "id": "f9791763", + "metadata": {}, + "outputs": [], + "source": [ + "import spot\n", + "from spot.jupyter import display_inline\n", + "spot.setup(show_default=\".A\")" + ] + }, + { + "cell_type": "markdown", + "id": "81867c56", + "metadata": {}, + "source": [ + "Consider the labels appearing in the following automaton:" + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "id": "28ab6c77", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a | b\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n" + ], + "text/html": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a | b\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f31fe0369d0> >" + ] + }, + "execution_count": 11, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut = spot.translate(\"a & X(a->b) & XX(!a&!b&c)\")\n", + "aut" + ] + }, + { + "cell_type": "markdown", + "id": "dcd554c8", + "metadata": {}, + "source": [ + "We try to use the word \"edge\" to refer to an edge of the automaton, labeled by a Boolean formula over AP. These edges can be seen as representing several \"transitions\", each labeled by a valuation of all atomic propositions. So the above automaton uses 4 edges to represent 19 transitions" + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "id": "3679412a", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "4 19\n" + ] + } + ], + "source": [ + "s = spot.sub_stats_reachable(aut)\n", + "print(s.edges, s.transitions)" + ] + }, + { + "cell_type": "markdown", + "id": "0804e219", + "metadata": {}, + "source": [ + "We can split the edges into the corresponding transitions using `split_edges()`." + ] + }, + { + "cell_type": "code", + "execution_count": 13, + "id": "6f373fde", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b & !c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & b & !c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & b & c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b & !c\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & b & !c\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & b & c\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n" + ], + "text/html": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b & !c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & b & !c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & b & c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b & !c\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & b & !c\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & b & c\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b & !c\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b & c\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f31fd7cfd20> >" + ] + }, + "execution_count": 13, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut_split = spot.split_edges(aut)\n", + "aut_split" + ] + }, + { + "cell_type": "markdown", + "id": "101a7100", + "metadata": {}, + "source": [ + "The opposite operation is `merge_edges()`, but it works in place:" + ] + }, + { + "cell_type": "code", + "execution_count": 14, + "id": "cf014f95", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a | b\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n" + ], + "text/html": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a | b\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f31fd7cfd20> >" + ] + }, + "execution_count": 14, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut_split.merge_edges()\n", + "aut_split" + ] + }, + { + "cell_type": "markdown", + "id": "2bc773cf", + "metadata": {}, + "source": [ + "Another way to split edges is `separate_edges()` this tweaks the labels so that any two labels can only be equal or disjoint. Note how this creates fewer edges." + ] + }, + { + "cell_type": "code", + "execution_count": 15, + "id": "3a130b23", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & b) | (!a & !c)\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "(!a & b) | (!a & !c)\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n" + ], + "text/html": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & b) | (!a & !c)\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "(!a & b) | (!a & !c)\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f31fd7cff90> >" + ] + }, + "execution_count": 15, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.separate_edges(aut)" + ] + }, + { + "cell_type": "markdown", + "id": "3f523aba", + "metadata": {}, + "source": [ + "A slightly lower-level interface is the `edge_separator` class. This makes it possible to declare a \"basis\" (a set of labels) that will be used to separate the edge of an automaton.\n", + "\n", + "`separate_edges()` is actually implemented as follows:" + ] + }, + { + "cell_type": "code", + "execution_count": 16, + "id": "2716cc20", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & b) | (!a & !c)\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "(!a & b) | (!a & !c)\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n" + ], + "text/html": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & b) | (!a & !c)\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "(!a & b) | (!a & !c)\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !b & c\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f31fd7dcf00> >" + ] + }, + "execution_count": 16, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "es = spot.edge_separator()\n", + "es.add_to_basis(aut) # create a basis from the labels of aut\n", + "es.separate_implying(aut) # replace labels by all labels of the basis that imply them" + ] + }, + { + "cell_type": "markdown", + "id": "9a46e347", + "metadata": {}, + "source": [ + "The `edge_separator` can also be used to separate the edges of *another* automaton:" + ] + }, + { + "cell_type": "code", + "execution_count": 19, + "id": "25d779a9", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "d\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "(!a & b & d) | (!a & !c & d)\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & !b & c & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & b & d) | (!a & !c & d)\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b & c & d\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "aut2 = spot.translate('a W Gd')\n", + "# replace labels based on \"compatibility\" with those from the basis\n", + "aut2sep = es.separate_compat(aut2)\n", + "display_inline(aut2, aut2sep)" + ] + }, + { + "cell_type": "markdown", + "id": "d448df40", + "metadata": {}, + "source": [ + "Now, if we take any label A in `aut2sep` and any label B in `aut`, we necessarily \n", + "have A∧B ∈ {A,0}. I.e., either A implies B, or A and B are incompatible. This is useful in certain algorithm that want to check that the inclusion of on automaton in another one, because they can arange to onlu check the inclusion (with `bdd_implies`) of the labels from the small automaton into the labels of the larger automaton." + ] + }, + { + "cell_type": "markdown", + "id": "db0b203b", + "metadata": {}, + "source": [ + "We could also use `edge_separator` to create a combined basis for two automata:" + ] + }, + { + "cell_type": "code", + "execution_count": 20, + "id": "2de45a46", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !d\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & !d\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & d\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & d\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & b & !d) | (!a & !c & !d)\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b & !d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b & !d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b & c & !d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & b & d) | (!a & !c & d)\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b & c & d\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "(!a & b & !d) | (!a & !c & !d)\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b & !d\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b & c & !d\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "(!a & b & d) | (!a & !c & d)\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b & d\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b & c & d\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !b & c & !d\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !b & c & d\n", + "\n", + "\n", + "\n" + ], + "text/html": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !d\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & !d\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & d\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & b & d\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & b & !d) | (!a & !c & !d)\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b & !d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b & !d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b & c & !d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & b & d) | (!a & !c & d)\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b & c & d\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "(!a & b & !d) | (!a & !c & !d)\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b & !d\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b & c & !d\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "(!a & b & d) | (!a & !c & d)\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a & b & d\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!a & !b & c & d\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !b & c & !d\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!a & !b & c & d\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f31fe037180> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & !d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b & !d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b & d\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "(!a & b & d) | (!a & !c & d)\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & !b & c & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & b & d) | (!a & !c & d)\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b & c & d\n", + "\n", + "\n", + "\n" + ], + "text/html": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & !d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b & !d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & d\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b & d\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "(!a & b & d) | (!a & !c & d)\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & !b & c & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "(!a & b & d) | (!a & !c & d)\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b & d\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b & c & d\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f31fd7dd2c0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "es2 = spot.edge_separator()\n", + "es2.add_to_basis(aut)\n", + "es2.add_to_basis(aut2)\n", + "display(es2.separate_implying(aut), es2.separate_implying(aut2))" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "9f5035f7", + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3 (ipykernel)", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.11.8" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} diff --git a/tests/python/splitedge.py b/tests/python/splitedge.py index 4911b10c2..af5d9f1a1 100644 --- a/tests/python/splitedge.py +++ b/tests/python/splitedge.py @@ -27,8 +27,11 @@ def create_aps(aut): def do_edge_test(aut, aps, edges_before, edges_after): tc.assertEqual(aut.num_edges(), edges_before) - aut = spot.split_edges(aut, aps) - tc.assertEqual(aut.num_edges(), edges_after) + es = spot.edge_separator() + for ap in aps: + es.add_to_basis(ap) + res = es.separate_compat(aut) + tc.assertEqual(res.num_edges(), edges_after) aut = spot.automaton(""" HOA: v1