diff --git a/spot/twaalgos/zlktree.cc b/spot/twaalgos/zlktree.cc index fba8e2039..1fa0573f6 100644 --- a/spot/twaalgos/zlktree.cc +++ b/spot/twaalgos/zlktree.cc @@ -23,6 +23,7 @@ #include #include #include +using namespace std::string_literals; namespace spot { @@ -188,7 +189,7 @@ namespace spot std::pair zielonka_tree::step(unsigned branch, acc_cond::mark_t colors) const { - if (SPOT_UNLIKELY(nodes_.size() < branch || nodes_[branch].first_child)) + if (SPOT_UNLIKELY(nodes_.size() <= branch || nodes_[branch].first_child)) throw std::runtime_error ("zielonka_tree::step(): incorrect branch number"); @@ -345,14 +346,26 @@ namespace spot + " is too large"); } - acd::acd(const const_twa_graph_ptr& aut) - : si_(new scc_info(aut)), own_si_(true), trees_(si_->scc_count()) + void acd::report_need_opt(const char* opt) + { + throw std::runtime_error("ACD should be built with option "s + opt); + } + + void acd::report_empty_acd(const char* fn) + { + throw + std::runtime_error(std::string(fn) + + "(): ACD is empty, did you use ABORT_WRONG_SHAPE?"); + } + + acd::acd(const const_twa_graph_ptr& aut, acd_options opt) + : si_(new scc_info(aut)), own_si_(true), opt_(opt), trees_(si_->scc_count()) { build_(); } - acd::acd(const scc_info& si) - : si_(&si), own_si_(false), trees_(si_->scc_count()) + acd::acd(const scc_info& si, acd_options opt) + : si_(&si), own_si_(false), opt_(opt), trees_(si_->scc_count()) { build_(); } @@ -507,10 +520,39 @@ namespace spot } else if (children > 1) { - if (accepting_node) - has_rabin_shape_ = false; - else - has_streett_shape_ = false; + // Check the shape if requested. + if ((has_rabin_shape_ + && !!(opt_ & acd_options::CHECK_RABIN) + && accepting_node) + || (has_streett_shape_ + && !!(opt_ & acd_options::CHECK_STREETT) + && !accepting_node)) + { + std::unique_ptr seen(make_bitvect(nstates)); + std::unique_ptr cur(make_bitvect(nstates)); + for (const auto& [sz, bv]: out) + { + cur->clear_all(); + bv->foreach_set_index([&aut, &cur](unsigned e) + { + cur->set(aut->edge_storage(e).src); + }); + if (cur->intersects(*seen)) + { + if (accepting_node) + has_rabin_shape_ = false; + else + has_streett_shape_ = false; + if (!!(opt_ & acd_options::ABORT_WRONG_SHAPE)) + { + nodes_.clear(); + return; + } + break; + } + *seen |= *cur; + } + } } } // Now we decide if the ACD corresponds to a "min even" or "max @@ -565,11 +607,14 @@ namespace spot unsigned acd::first_branch(unsigned s) const { if (SPOT_UNLIKELY(aut_->num_states() < s)) - throw std::runtime_error("first_branch(): unknown state " + + throw std::runtime_error("acd::first_branch(): unknown state " + std::to_string(s)); unsigned scc = si_->scc_of(s); if (trees_[scc].trivial) // the branch is irrelevant for transiant SCCs return 0; + if (SPOT_UNLIKELY(nodes_.empty())) + // make sure we do not complain about this if all SCCs are trivial. + report_empty_acd("acd::first_branch"); unsigned n = trees_[scc].root; assert(nodes_[n].states.get(s)); return leftmost_branch_(n, s); @@ -579,7 +624,7 @@ namespace spot std::pair acd::step(unsigned branch, unsigned edge) const { - if (SPOT_UNLIKELY(nodes_.size() < branch)) + if (SPOT_UNLIKELY(nodes_.size() <= branch)) throw std::runtime_error("acd::step(): incorrect branch number"); if (SPOT_UNLIKELY(nodes_[branch].edges.size() < edge)) throw std::runtime_error("acd::step(): incorrect edge number"); @@ -622,13 +667,13 @@ namespace spot void acd::dot(std::ostream& os, const char* id) const { + unsigned ns = nodes_.size(); os << "digraph acd {\n labelloc=\"t\"\n label=\"\n" - << (is_even_ ? "min even\"" : "min odd\"\n"); + << (ns ? (is_even_ ? "min even\"" : "min odd\"") : "empty ACD\""); if (id) escape_str(os << " id=\"", id) // fill the node so that the entire node is clickable << "\"\n node [id=\"N\\N\", style=filled, fillcolor=white]\n"; - unsigned ns = nodes_.size(); for (unsigned n = 0; n < ns; ++n) { acc_cond::mark_t m = {}; @@ -736,14 +781,14 @@ namespace spot bool acd::node_acceptance(unsigned n) const { - if (SPOT_UNLIKELY(nodes_.size() < n)) + if (SPOT_UNLIKELY(nodes_.size() <= n)) throw std::runtime_error("acd::node_acceptance(): unknown node"); return (nodes_[n].level & 1) ^ is_even_; } std::vector acd::edges_of_node(unsigned n) const { - if (SPOT_UNLIKELY(nodes_.size() < n)) + if (SPOT_UNLIKELY(nodes_.size() <= n)) throw std::runtime_error("acd::edges_of_node(): unknown node"); std::vector res; unsigned scc = nodes_[n].scc; @@ -755,6 +800,27 @@ namespace spot return res; } + bool acd::has_rabin_shape() const + { + if (!(opt_ & acd_options::CHECK_RABIN)) + report_need_opt("CHECK_RABIN"); + return has_rabin_shape_; + } + + bool acd::has_streett_shape() const + { + if (!(opt_ & acd_options::CHECK_STREETT)) + report_need_opt("CHECK_STREETT"); + return has_streett_shape_; + } + + bool acd::has_parity_shape() const + { + if ((opt_ & acd_options::CHECK_PARITY) != acd_options::CHECK_PARITY) + report_need_opt("CHECK_PARITY"); + return has_streett_shape_ && has_rabin_shape_; + } + twa_graph_ptr acd_transform(const const_twa_graph_ptr& a, bool colored) { diff --git a/spot/twaalgos/zlktree.hh b/spot/twaalgos/zlktree.hh index c4d3563b4..7501aa5df 100644 --- a/spot/twaalgos/zlktree.hh +++ b/spot/twaalgos/zlktree.hh @@ -151,6 +151,48 @@ namespace spot twa_graph_ptr zielonka_tree_transform(const const_twa_graph_ptr& aut); + /// \ingroup twa_acc_transform + /// \brief Options to alter the behavior of acd + enum class acd_options + { + /// Build the ACD, without checking its shape. + NONE = 0, + /// Check if the ACD has Rabin shape. + CHECK_RABIN = 1, + /// Check if the ACD has Streett shape. + CHECK_STREETT = 2, + /// Check if the ACD has Parity shape + CHECK_PARITY = CHECK_RABIN | CHECK_STREETT, + /// Abort the construction of the ACD if it does not have the + /// shape that is tested. When that happens, node_count() is set + /// to 0. + ABORT_WRONG_SHAPE = 4, + }; + +#ifndef SWIG + inline + bool operator!(acd_options me) + { + return me == acd_options::NONE; + } + + inline + acd_options operator&(acd_options left, acd_options right) + { + typedef std::underlying_type_t ut; + return static_cast(static_cast(left) + & static_cast(right)); + } + + inline + acd_options operator|(acd_options left, acd_options right) + { + typedef std::underlying_type_t ut; + return static_cast(static_cast(left) + | static_cast(right)); + } +#endif + /// \ingroup twa_acc_transform /// \brief Alternating Cycle Decomposition implementation /// @@ -164,8 +206,8 @@ namespace spot { public: /// \brief Build a Alternating Cycle Decomposition an SCC decomposition - acd(const scc_info& si); - acd(const const_twa_graph_ptr& aut); + acd(const scc_info& si, acd_options opt = acd_options::NONE); + acd(const const_twa_graph_ptr& aut, acd_options opt = acd_options::NONE); ~acd(); @@ -229,29 +271,24 @@ namespace spot /// \brief Whether the ACD has Rabin shape. /// - /// The ACD has Rabin shape of all accepting (round) nodes have - /// at most one child. - bool has_rabin_shape() const - { - return has_rabin_shape_; - } + /// The ACD has Rabin shape if all accepting (round) nodes have no + /// children with a state in common. The acd should be built with + /// option CHECK_RABIN or CHECK_PARITY for this function to work. + bool has_rabin_shape() const; /// \brief Whether the ACD has Streett shape. /// - /// The ACD has Streett shape of all rejecting (square) nodes have - /// at most one child. - bool has_streett_shape() const - { - return has_streett_shape_; - } + /// The ACD has Streett shape if all rejecting (square) nodes have no + /// children with a state in common. The acd should be built with + /// option CHECK_STREETT or CHECK_PARITY for this function to work. + bool has_streett_shape() const; - /// \brief Whether the ACD has parity shape. + /// \brief Whether the ACD has Streett shape. /// - /// The ACD has parity shape of all nodes have at most one child. - bool has_parity_shape() const - { - return has_streett_shape() && has_rabin_shape(); - } + /// The ACD has Streett shape if all nodes have no + /// children with a state in common. The acd should be built with + /// option CHECK_PARITY for this function to work. + bool has_parity_shape() const; /// \brief Return the automaton on which the ACD is defined. const const_twa_graph_ptr get_aut() const @@ -268,6 +305,7 @@ namespace spot private: const scc_info* si_; bool own_si_ = false; + acd_options opt_; // This structure is used to represent one node in the ACD forest. // The tree use a left-child / right-sibling representation @@ -335,6 +373,8 @@ namespace spot #ifndef SWIG [[noreturn]] static void report_invalid_scc_number(unsigned num, const char* fn); + [[noreturn]] static void report_need_opt(const char* opt); + [[noreturn]] static void report_empty_acd(const char* fn); #endif }; diff --git a/tests/python/zlktree.ipynb b/tests/python/zlktree.ipynb index b7675ccdf..f3ab8c860 100644 --- a/tests/python/zlktree.ipynb +++ b/tests/python/zlktree.ipynb @@ -216,7 +216,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 2, @@ -640,7 +640,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fced599cfc0> >" + " *' at 0x7f5a81a71c00> >" ] }, "execution_count": 10, @@ -1063,7 +1063,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fced599c600> >" + " *' at 0x7f5a81a71690> >" ] }, "execution_count": 11, @@ -1256,7 +1256,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fced599c0c0> >" + " *' at 0x7f5a81a785d0> >" ] }, "execution_count": 13, @@ -1701,7 +1701,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fced599c450> >" + " *' at 0x7f5a81a787b0> >" ] }, "execution_count": 14, @@ -2096,7 +2096,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2427,7 +2427,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2513,7 +2513,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2624,7 +2624,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2662,7 +2662,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -2700,7 +2700,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -3862,7 +3862,7 @@ "};$(\"#acdaut0 #E9\").addClass(\"acdN0\");$(\"#acdaut0 #E10\").addClass(\"acdN0\");$(\"#acdaut0 #E11\").addClass(\"acdN0\");$(\"#acdaut0 #E12\").addClass(\"acdN0\");$(\"#acdaut0 #E13\").addClass(\"acdN0\");$(\"#acdaut0 #E14\").addClass(\"acdN0\");$(\"#acdaut0 #E15\").addClass(\"acdN0\");$(\"#acdaut0 #E16\").addClass(\"acdN0\");$(\"#acdaut0 #E21\").addClass(\"acdN0\");$(\"#acdaut0 #E22\").addClass(\"acdN0\");$(\"#acdaut0 #E23\").addClass(\"acdN0\");$(\"#acdaut0 #E24\").addClass(\"acdN0\");$(\"#acdaut0 #E25\").addClass(\"acdN0\");$(\"#acdaut0 #E26\").addClass(\"acdN0\");$(\"#acdaut0 #E27\").addClass(\"acdN0\");$(\"#acdaut0 #E28\").addClass(\"acdN0\");$(\"#acdaut0 #E33\").addClass(\"acdN0\");$(\"#acdaut0 #E34\").addClass(\"acdN0\");$(\"#acdaut0 #E35\").addClass(\"acdN0\");$(\"#acdaut0 #E36\").addClass(\"acdN0\");$(\"#acdaut0 #E31\").addClass(\"acdN1\");$(\"#acdaut0 #E32\").addClass(\"acdN1\");$(\"#acdaut0 #E39\").addClass(\"acdN1\");$(\"#acdaut0 #E40\").addClass(\"acdN1\");$(\"#acdaut0 #E5\").addClass(\"acdN2\");$(\"#acdaut0 #E7\").addClass(\"acdN2\");$(\"#acdaut0 #E17\").addClass(\"acdN2\");$(\"#acdaut0 #E1\").addClass(\"acdN3\");$(\"#acdaut0 #E10\").addClass(\"acdN4\");$(\"#acdaut0 #E12\").addClass(\"acdN4\");$(\"#acdaut0 #E13\").addClass(\"acdN4\");$(\"#acdaut0 #E15\").addClass(\"acdN4\");$(\"#acdaut0 #E21\").addClass(\"acdN4\");$(\"#acdaut0 #E22\").addClass(\"acdN4\");$(\"#acdaut0 #E23\").addClass(\"acdN5\");$(\"#acdaut0 #E24\").addClass(\"acdN5\");$(\"#acdaut0 #E34\").addClass(\"acdN5\");$(\"#acdaut0 #E36\").addClass(\"acdN5\");$(\"#acdaut0 #E14\").addClass(\"acdN6\");$(\"#acdaut0 #E15\").addClass(\"acdN6\");$(\"#acdaut0 #E22\").addClass(\"acdN6\");$(\"#acdaut0 #E23\").addClass(\"acdN6\");$(\"#acdaut0 #E14\").addClass(\"acdN7\");$(\"#acdaut0 #E16\").addClass(\"acdN7\");$(\"#acdaut0 #E26\").addClass(\"acdN7\");$(\"#acdaut0 #E9\").addClass(\"acdN8\");$(\"#acdaut0 #E40\").addClass(\"acdN9\");$(\"#acdaut0 #E5\").addClass(\"acdN10\");$(\"#acdaut0 #E23\").addClass(\"acdN11\");$(\"#acdaut0 #E14\").addClass(\"acdN12\");$(\"#acdaut0 #E23\").addClass(\"acdN13\");$(\"#acdaut0 #E14\").addClass(\"acdN14\");$(\"#acdaut0 #E1\").click(function(){acd0_edge(1);});$(\"#acdaut0 #E2\").click(function(){acd0_edge(2);});$(\"#acdaut0 #E3\").click(function(){acd0_edge(3);});$(\"#acdaut0 #E4\").click(function(){acd0_edge(4);});$(\"#acdaut0 #E5\").click(function(){acd0_edge(5);});$(\"#acdaut0 #E6\").click(function(){acd0_edge(6);});$(\"#acdaut0 #E7\").click(function(){acd0_edge(7);});$(\"#acdaut0 #E8\").click(function(){acd0_edge(8);});$(\"#acdaut0 #E9\").click(function(){acd0_edge(9);});$(\"#acdaut0 #E10\").click(function(){acd0_edge(10);});$(\"#acdaut0 #E11\").click(function(){acd0_edge(11);});$(\"#acdaut0 #E12\").click(function(){acd0_edge(12);});$(\"#acdaut0 #E13\").click(function(){acd0_edge(13);});$(\"#acdaut0 #E14\").click(function(){acd0_edge(14);});$(\"#acdaut0 #E15\").click(function(){acd0_edge(15);});$(\"#acdaut0 #E16\").click(function(){acd0_edge(16);});$(\"#acdaut0 #E17\").click(function(){acd0_edge(17);});$(\"#acdaut0 #E18\").click(function(){acd0_edge(18);});$(\"#acdaut0 #E19\").click(function(){acd0_edge(19);});$(\"#acdaut0 #E20\").click(function(){acd0_edge(20);});$(\"#acdaut0 #E21\").click(function(){acd0_edge(21);});$(\"#acdaut0 #E22\").click(function(){acd0_edge(22);});$(\"#acdaut0 #E23\").click(function(){acd0_edge(23);});$(\"#acdaut0 #E24\").click(function(){acd0_edge(24);});$(\"#acdaut0 #E25\").click(function(){acd0_edge(25);});$(\"#acdaut0 #E26\").click(function(){acd0_edge(26);});$(\"#acdaut0 #E27\").click(function(){acd0_edge(27);});$(\"#acdaut0 #E28\").click(function(){acd0_edge(28);});$(\"#acdaut0 #E29\").click(function(){acd0_edge(29);});$(\"#acdaut0 #E30\").click(function(){acd0_edge(30);});$(\"#acdaut0 #E31\").click(function(){acd0_edge(31);});$(\"#acdaut0 #E32\").click(function(){acd0_edge(32);});$(\"#acdaut0 #E33\").click(function(){acd0_edge(33);});$(\"#acdaut0 #E34\").click(function(){acd0_edge(34);});$(\"#acdaut0 #E35\").click(function(){acd0_edge(35);});$(\"#acdaut0 #E36\").click(function(){acd0_edge(36);});$(\"#acdaut0 #E37\").click(function(){acd0_edge(37);});$(\"#acdaut0 #E38\").click(function(){acd0_edge(38);});$(\"#acdaut0 #E39\").click(function(){acd0_edge(39);});$(\"#acdaut0 #E40\").click(function(){acd0_edge(40);});$(\"#acdaut0 #S0\").click(function(){acd0_state(0);});$(\"#acdaut0 #S1\").click(function(){acd0_state(1);});$(\"#acdaut0 #S2\").click(function(){acd0_state(2);});$(\"#acdaut0 #S3\").click(function(){acd0_state(3);});$(\"#acdaut0 #S4\").click(function(){acd0_state(4);});$(\"#acdaut0 #S5\").click(function(){acd0_state(5);});$(\"#acdaut0 #S6\").click(function(){acd0_state(6);});$(\"#acdaut0 #S7\").click(function(){acd0_state(7);});$(\"#acdaut0 #S8\").click(function(){acd0_state(8);});$(\"#acdaut0 #S9\").click(function(){acd0_state(9);});$(\"#acd0 #N0\").click(function(){acd0_node(0, 0);});$(\"#acd0 #N1\").click(function(){acd0_node(1, 1);});$(\"#acd0 #N2\").click(function(){acd0_node(2, 1);});$(\"#acd0 #N3\").click(function(){acd0_node(3, 1);});$(\"#acd0 #N4\").click(function(){acd0_node(4, 1);});$(\"#acd0 #N5\").click(function(){acd0_node(5, 1);});$(\"#acd0 #N6\").click(function(){acd0_node(6, 1);});$(\"#acd0 #N7\").click(function(){acd0_node(7, 1);});$(\"#acd0 #N8\").click(function(){acd0_node(8, 1);});$(\"#acd0 #N9\").click(function(){acd0_node(9, 0);});$(\"#acd0 #N10\").click(function(){acd0_node(10, 0);});$(\"#acd0 #N11\").click(function(){acd0_node(11, 0);});$(\"#acd0 #N12\").click(function(){acd0_node(12, 0);});$(\"#acd0 #N13\").click(function(){acd0_node(13, 0);});$(\"#acd0 #N14\").click(function(){acd0_node(14, 0);});" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 18, @@ -4737,7 +4737,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fced599c210> >" + " *' at 0x7f5a90499e70> >" ] }, "execution_count": 27, @@ -5376,7 +5376,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fced599c720> >" + " *' at 0x7f5a903c2810> >" ] }, "execution_count": 29, @@ -5441,17 +5441,37 @@ "spot.zielonka_tree_transform(a3).num_states()" ] }, + { + "cell_type": "markdown", + "id": "3782b244", + "metadata": {}, + "source": [ + "## Typeness checks" + ] + }, { "cell_type": "markdown", "id": "e3d0ff64", "metadata": {}, "source": [ - "We can decide Rabin, Streett, and parity-typeness with the following methods. However building the entire ACD to decide that is a bit overkill, especially in case of a negative answer." + "The ACD can be used to decide Rabin, Streett, and parity-typeness. Testing Rabin-typeness requires making sure that round nodes have no children sharing a common state, and testing Streett-typeness needs a similar test for square node. These additional tests have a cost, so they need to be enabled by passing `spot.acd_options_CHECK_RABIN`, `spot.acd_options_CHECK_STREETT`, or `spot.acd_options_CHECK_PARTIY` to the ACD constructor. The latter option implies the former two.\n", + "\n", + "As an example, automaton `a3` is Rabin-type because nodes 12 and 13, which are the children of the only round node with more than one child, do not share any state. It it not Street-type, because for instance state 2 appears in both nodes 4 and 8, two children of a square node." ] }, { "cell_type": "code", "execution_count": 32, + "id": "c72d6e41", + "metadata": {}, + "outputs": [], + "source": [ + "theacd = spot.acd(a3, spot.acd_options_CHECK_PARITY)" + ] + }, + { + "cell_type": "code", + "execution_count": 33, "id": "2d0bbc0b", "metadata": {}, "outputs": [ @@ -5459,7 +5479,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "False False False\n" + "True False False\n" ] } ], @@ -5467,6 +5487,68 @@ "print(theacd.has_rabin_shape(), theacd.has_streett_shape(), theacd.has_parity_shape())" ] }, + { + "cell_type": "markdown", + "id": "73342d2c", + "metadata": {}, + "source": [ + "Calling the above methods withtout passing the relevant option will raise an exception." + ] + }, + { + "cell_type": "markdown", + "id": "2d982b74", + "metadata": {}, + "source": [ + "Additonally, when the goal is only to check some typeness, the construction of the ACD can be aborted as soon as the typeness is found to be wrong. This can be enabled by passing the additional option `spot.acd_options_ABORT_WRONG_SHAPE`. In case the construction is aborted the ACD forest will be erased (to make sure it is not used), and `node_count()` will return 0." + ] + }, + { + "cell_type": "code", + "execution_count": 34, + "id": "ccadeeaf", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "15\n" + ] + } + ], + "source": [ + "print(theacd.node_count())" + ] + }, + { + "cell_type": "code", + "execution_count": 35, + "id": "6161a3e6", + "metadata": {}, + "outputs": [], + "source": [ + "theacd = spot.acd(a3, spot.acd_options_CHECK_STREETT | spot.acd_options_ABORT_WRONG_SHAPE)" + ] + }, + { + "cell_type": "code", + "execution_count": 36, + "id": "7170615f", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "False 0\n" + ] + } + ], + "source": [ + "print(theacd.has_streett_shape(), theacd.node_count())" + ] + }, { "cell_type": "markdown", "id": "15f094c0", @@ -5479,7 +5561,7 @@ }, { "cell_type": "code", - "execution_count": 33, + "execution_count": 37, "id": "criminal-northwest", "metadata": {}, "outputs": [ @@ -5605,10 +5687,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fced59b53c0> >" + " *' at 0x7f5a81a8b840> >" ] }, - "execution_count": 33, + "execution_count": 37, "metadata": {}, "output_type": "execute_result" } @@ -5639,7 +5721,7 @@ }, { "cell_type": "code", - "execution_count": 34, + "execution_count": 38, "id": "63c7c062", "metadata": {}, "outputs": [ @@ -5717,10 +5799,10 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, - "execution_count": 34, + "execution_count": 38, "metadata": {}, "output_type": "execute_result" } @@ -5731,7 +5813,7 @@ }, { "cell_type": "code", - "execution_count": 35, + "execution_count": 39, "id": "balanced-investing", "metadata": {}, "outputs": [ @@ -5883,10 +5965,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fced59b5660> >" + " *' at 0x7f5a81a8b0f0> >" ] }, - "execution_count": 35, + "execution_count": 39, "metadata": {}, "output_type": "execute_result" } @@ -5897,7 +5979,7 @@ }, { "cell_type": "code", - "execution_count": 36, + "execution_count": 40, "id": "nutritional-rugby", "metadata": {}, "outputs": [], @@ -5907,7 +5989,7 @@ }, { "cell_type": "code", - "execution_count": 37, + "execution_count": 41, "id": "criminal-marking", "metadata": {}, "outputs": [ @@ -6176,10 +6258,10 @@ "};$(\"#acdaut1 #E1\").addClass(\"acdN0\");$(\"#acdaut1 #E2\").addClass(\"acdN0\");$(\"#acdaut1 #E3\").addClass(\"acdN0\");$(\"#acdaut1 #E4\").addClass(\"acdN0\");$(\"#acdaut1 #E5\").addClass(\"acdN0\");$(\"#acdaut1 #E6\").addClass(\"acdN0\");$(\"#acdaut1 #E7\").addClass(\"acdN0\");$(\"#acdaut1 #E8\").addClass(\"acdN0\");$(\"#acdaut1 #E6\").addClass(\"acdN1\");$(\"#acdaut1 #E1\").click(function(){acd1_edge(1);});$(\"#acdaut1 #E2\").click(function(){acd1_edge(2);});$(\"#acdaut1 #E3\").click(function(){acd1_edge(3);});$(\"#acdaut1 #E4\").click(function(){acd1_edge(4);});$(\"#acdaut1 #E5\").click(function(){acd1_edge(5);});$(\"#acdaut1 #E6\").click(function(){acd1_edge(6);});$(\"#acdaut1 #E7\").click(function(){acd1_edge(7);});$(\"#acdaut1 #E8\").click(function(){acd1_edge(8);});$(\"#acdaut1 #S0\").click(function(){acd1_state(0);});$(\"#acdaut1 #S1\").click(function(){acd1_state(1);});$(\"#acd1 #N0\").click(function(){acd1_node(0, 1);});$(\"#acd1 #N1\").click(function(){acd1_node(1, 0);});" ], "text/plain": [ - " >" + " >" ] }, - "execution_count": 37, + "execution_count": 41, "metadata": {}, "output_type": "execute_result" } @@ -6190,7 +6272,7 @@ }, { "cell_type": "code", - "execution_count": 38, + "execution_count": 42, "id": "unusual-dependence", "metadata": { "scrolled": true @@ -6299,10 +6381,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fced59bb060> >" + " *' at 0x7f5a81a8b180> >" ] }, - "execution_count": 38, + "execution_count": 42, "metadata": {}, "output_type": "execute_result" } @@ -6313,7 +6395,7 @@ }, { "cell_type": "code", - "execution_count": 39, + "execution_count": 43, "id": "9ed0bc59", "metadata": {}, "outputs": [], @@ -6332,7 +6414,7 @@ }, { "cell_type": "code", - "execution_count": 40, + "execution_count": 44, "id": "deb92971", "metadata": {}, "outputs": [ @@ -6637,10 +6719,10 @@ "};$(\"#acdaut2 #E1\").addClass(\"acdN0\");$(\"#acdaut2 #E2\").addClass(\"acdN0\");$(\"#acdaut2 #E3\").addClass(\"acdN0\");$(\"#acdaut2 #E4\").addClass(\"acdN0\");$(\"#acdaut2 #E5\").addClass(\"acdN0\");$(\"#acdaut2 #E6\").addClass(\"acdN0\");$(\"#acdaut2 #E7\").addClass(\"acdN0\");$(\"#acdaut2 #E1\").addClass(\"acdN1\");$(\"#acdaut2 #E3\").addClass(\"acdN1\");$(\"#acdaut2 #E4\").addClass(\"acdN1\");$(\"#acdaut2 #E5\").addClass(\"acdN1\");$(\"#acdaut2 #E7\").addClass(\"acdN2\");$(\"#acdaut2 #E1\").click(function(){acd2_edge(1);});$(\"#acdaut2 #E2\").click(function(){acd2_edge(2);});$(\"#acdaut2 #E3\").click(function(){acd2_edge(3);});$(\"#acdaut2 #E4\").click(function(){acd2_edge(4);});$(\"#acdaut2 #E5\").click(function(){acd2_edge(5);});$(\"#acdaut2 #E6\").click(function(){acd2_edge(6);});$(\"#acdaut2 #E7\").click(function(){acd2_edge(7);});$(\"#acdaut2 #S0\").click(function(){acd2_state(0);});$(\"#acdaut2 #S1\").click(function(){acd2_state(1);});$(\"#acdaut2 #S2\").click(function(){acd2_state(2);});$(\"#acdaut2 #S3\").click(function(){acd2_state(3);});$(\"#acd2 #N0\").click(function(){acd2_node(0, 1);});$(\"#acd2 #N1\").click(function(){acd2_node(1, 0);});$(\"#acd2 #N2\").click(function(){acd2_node(2, 0);});" ], "text/plain": [ - " >" + " >" ] }, - "execution_count": 40, + "execution_count": 44, "metadata": {}, "output_type": "execute_result" } @@ -6658,7 +6740,7 @@ }, { "cell_type": "code", - "execution_count": 41, + "execution_count": 45, "id": "94a02201", "metadata": {}, "outputs": [ @@ -6765,10 +6847,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fced59bba50> >" + " *' at 0x7f5a8001f3c0> >" ] }, - "execution_count": 41, + "execution_count": 45, "metadata": {}, "output_type": "execute_result" } @@ -6779,7 +6861,7 @@ }, { "cell_type": "code", - "execution_count": 42, + "execution_count": 46, "id": "3332e850", "metadata": {}, "outputs": [ @@ -7045,10 +7127,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fced59bb360> >" + " *' at 0x7f5a8001f7b0> >" ] }, - "execution_count": 42, + "execution_count": 46, "metadata": {}, "output_type": "execute_result" } @@ -7069,7 +7151,7 @@ }, { "cell_type": "code", - "execution_count": 43, + "execution_count": 47, "id": "german-vienna", "metadata": {}, "outputs": [ @@ -7139,10 +7221,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fced59bbf30> >" + " *' at 0x7f5a8001ff60> >" ] }, - "execution_count": 43, + "execution_count": 47, "metadata": {}, "output_type": "execute_result" } @@ -7166,7 +7248,7 @@ }, { "cell_type": "code", - "execution_count": 44, + "execution_count": 48, "id": "chemical-primary", "metadata": {}, "outputs": [ @@ -7176,7 +7258,7 @@ "(spot.trival_maybe(), spot.trival(True))" ] }, - "execution_count": 44, + "execution_count": 48, "metadata": {}, "output_type": "execute_result" } @@ -7187,7 +7269,7 @@ }, { "cell_type": "code", - "execution_count": 45, + "execution_count": 49, "id": "hispanic-floor", "metadata": {}, "outputs": [ @@ -7250,10 +7332,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fced474f300> >" + " *' at 0x7f5a80026240> >" ] }, - "execution_count": 45, + "execution_count": 49, "metadata": {}, "output_type": "execute_result" } @@ -7264,7 +7346,7 @@ }, { "cell_type": "code", - "execution_count": 46, + "execution_count": 50, "id": "central-london", "metadata": {}, "outputs": [ @@ -7274,7 +7356,7 @@ "(spot.trival(True), spot.trival(True))" ] }, - "execution_count": 46, + "execution_count": 50, "metadata": {}, "output_type": "execute_result" } diff --git a/tests/python/zlktree.py b/tests/python/zlktree.py index 92df881fb..be565342c 100644 --- a/tests/python/zlktree.py +++ b/tests/python/zlktree.py @@ -27,3 +27,93 @@ trans-acc --BODY-- State: 0 [!0&!1] 3 [!0&!1] 4 State: 1 [!0&!1] 4 {3} b = spot.zielonka_tree_transform(a) assert spot.are_equivalent(a, b) assert b.acc().is_buchi() + +def report_missing_exception(): + raise RuntimeError("missing exception") + +a = spot.automaton(""" +HOA: v1 States: 10 Start: 0 AP: 2 "p0" "p1" acc-name: Rabin 3 +Acceptance: 6 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) & +Inf(5)) properties: trans-labels explicit-labels trans-acc --BODY-- +State: 0 [0&!1] 0 {1 2 3} [!0&!1] 8 [0&1] 4 State: 1 [0&1] 1 {2} +State: 2 [0&1] 8 {3} [0&1] 2 {1} [!0&1] 4 {3 4} [!0&!1] 3 {2 5} State: +3 [!0&!1] 5 [0&1] 8 {1 2} [!0&!1] 9 {1} State: 4 [0&!1] 3 {0 2} [!0&1] +5 {1} State: 5 [!0&!1] 6 [!0&!1] 7 {2} [0&!1] 3 {1} [!0&1] 5 State: 6 +[!0&!1] 1 [!0&!1] 2 {4} [0&!1] 0 {1 3 4} [0&1] 5 [!0&!1] 3 State: 7 +[0&1] 4 {0} [0&1] 5 [0&1] 0 {3} [0&1] 1 {2 4} State: 8 [0&!1] 6 {0 4 +5} [!0&!1] 7 {4} [0&!1] 2 {1 3} [0&1] 0 {0 1 4} State: 9 [!0&1] 6 {4} +[!0&!1] 2 {5} [!0&!1] 0 {3} [!0&!1] 5 --END--""") +aa = spot.acd(a) +try: + assert aa.has_rabin_shape() +except RuntimeError as e: + assert 'CHECK_RABIN' in str(e) +else: + report_missing_exception() + +try: + assert not aa.has_streett_shape() +except RuntimeError as e: + assert 'CHECK_STREETT' in str(e) +else: + report_missing_exception() + +try: + assert not aa.has_parity_shape() +except RuntimeError as e: + assert 'CHECK_PARITY' in str(e) +else: + report_missing_exception() + + +aa = spot.acd(a, spot.acd_options_CHECK_RABIN) +assert aa.has_rabin_shape() +assert aa.node_count() == 13 + +try: + assert not aa.has_streett_shape() +except RuntimeError as e: + assert 'CHECK_STREETT' in str(e) +else: + report_missing_exception() + +try: + assert aa.has_parity_shape() +except RuntimeError as e: + assert 'CHECK_PARITY' in str(e) +else: + report_missing_exception() + +aa = spot.acd(a, (spot.acd_options_CHECK_PARITY | + spot.acd_options_ABORT_WRONG_SHAPE)) +assert aa.has_rabin_shape() +assert not aa.has_streett_shape() +assert not aa.has_parity_shape() +assert aa.node_count() == 0 +try: + aa.first_branch(0) +except RuntimeError as e: + assert 'ABORT_WRONG_SHAPE' in str(e) +else: + report_missing_exception() + +try: + aa.step(0, 0) +except RuntimeError as e: + assert 'incorrect branch number' in str(e) +else: + report_missing_exception() + +try: + aa.node_acceptance(0) +except RuntimeError as e: + assert 'unknown node' in str(e) +else: + report_missing_exception() + +try: + aa.edges_of_node(0) +except RuntimeError as e: + assert 'unknown node' in str(e) +else: + report_missing_exception()