From 70ede35702fd7335de846e08a3fcb8a8fee43883 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 24 Sep 2021 13:37:16 +0200 Subject: [PATCH] acd: add support for state-based output * spot/twaalgos/zlktree.hh, spot/twaalgos/zlktree.cc (acd::node_level, acd::state_step, acd_transform_sbacc): New public functions. * tests/python/zlktree.ipynb, tests/python/zlktree.py: More tests. * NEWS: Typo. --- NEWS | 20 +- spot/twaalgos/zlktree.cc | 130 +- spot/twaalgos/zlktree.hh | 21 + tests/python/zlktree.ipynb | 2572 ++++++++++++++++++++++++++++++++++-- tests/python/zlktree.py | 7 + 5 files changed, 2621 insertions(+), 129 deletions(-) diff --git a/NEWS b/NEWS index 2a0bca2e9..b51db0cf1 100644 --- a/NEWS +++ b/NEWS @@ -15,19 +15,19 @@ New in spot 2.9.8.dev (not yet released) - ltlsynt --aiger option now takes an optional argument indicating how the bdd and states are to be encoded in the aiger output. - The option has to be given in the form - ite|isop|both[+ud][+dc][+sub0|sub1|sub2] where the first + The option has to be given in the form + ite|isop|both[+ud][+dc][+sub0|sub1|sub2] where the first only obligatory argument decides whether "if-then-else" ("ite") or irreducible-sum-of-products ("isop") is to be used. "both" executes both strategies and retains the smaller circuits. - The additional options are for fine-tuning. "ud" also encodes the + The additional options are for fine-tuning. "ud" also encodes the dual of the conditions and retains the smaller circuits. "dc" computes if for some inputs we do not care whether the output is high or low and try to use this information to compute a smaller circuit. "subX" indicates different strategies to find common subexpressions, with "sub0" indicating no extra computations. - - ltlsynt --verify checks the computed strategy or aiger circuit + - ltlsynt --verify checks the computed strategy or aiger circuit against the specification. - ltlsynt -x "specification-decomposition" determines whether or not @@ -36,8 +36,8 @@ New in spot 2.9.8.dev (not yet released) into a circuit. - ltlsynt -x "minimization-level=[0-5]" determines how to minimize - the strategy (a monitor). 0, no minimization; 1, regular DFA - minimization; 2, signature based minimization with + the strategy (a monitor). 0, no minimization; 1, regular DFA + minimization; 2, signature based minimization with output assignement; 3, SAT based minimization; 4, 1 then 3; 5, 2 then 3. @@ -58,11 +58,11 @@ New in spot 2.9.8.dev (not yet released) Library: - Spot now provides convenient function to create and solve game. - The functions are located in twaalgos/game.hh and - twaalgos/synthesis.hh. Moreover a new structure holding + The functions are located in twaalgos/game.hh and + twaalgos/synthesis.hh. Moreover a new structure holding all the necessary options called game_info is now available. - - A new class called aig is introduced to represent + - A new class called aig is introduced to represent and-inverter-graphs, which is useful for synthesis. - Historically, Spot labels automata by Boolean formulas over @@ -275,7 +275,7 @@ New in spot 2.9.8.dev (not yet released) Additionally, this function now returns the number of states that have been merged (and therefore removed from the automaton). - - spot::zielonka_tree and spot::acd are new class that implement the + - spot::zielonka_tree and spot::acd are new classes that implement the Zielonka Tree and Alternatic Cycle Decomposition, based on a paper by Casares et al. (ICALP'21). Those structures can be used to paritize any automaton, and more. The graphical rendering of ACD diff --git a/spot/twaalgos/zlktree.cc b/spot/twaalgos/zlktree.cc index 1fa0573f6..0273e2c2c 100644 --- a/spot/twaalgos/zlktree.cc +++ b/spot/twaalgos/zlktree.cc @@ -646,25 +646,69 @@ namespace spot branch = parent; } unsigned lvl = nodes_[branch].level; - if (child != 0) + if (child == 0) // came here without climbing up + return { leftmost_branch_(branch, dst), lvl }; + + unsigned start_child = child; + // find the next children that contains dst. + do { - unsigned start_child = child; - // find the next children that contains dst. - do - { - child = nodes_[child].next_sibling; - if (nodes_[child].states.get(dst)) - return {leftmost_branch_(child, dst), lvl}; - } - while (child != start_child); - return { branch, lvl }; - } - else - { - return { leftmost_branch_(branch, dst), lvl }; + child = nodes_[child].next_sibling; + if (nodes_[child].states.get(dst)) + return {leftmost_branch_(child, dst), lvl}; } + while (child != start_child); + return { branch, lvl }; } + unsigned acd::state_step(unsigned node, unsigned edge) const + { + // The rule is almost similar to step(), except we do note + // go down to the leftmost leave after we have seen a round + // of all children. + if (SPOT_UNLIKELY(nodes_.size() <= node)) + throw std::runtime_error("acd::step(): incorrect node number"); + if (SPOT_UNLIKELY(nodes_[node].edges.size() < edge)) + throw std::runtime_error("acd::step(): incorrect edge number"); + + unsigned child = 0; + auto& es = aut_->edge_storage(edge); + unsigned dst = es.dst; + unsigned src = es.src; + // If we are not on a leaf of the subtree of src, go there before + // continuing. + node = leftmost_branch_(node, src); + while (!nodes_[node].edges.get(edge)) + { + unsigned parent = nodes_[node].parent; + if (SPOT_UNLIKELY(node == parent)) + { + // Changing SCc + return first_branch(dst); + } + child = node; + node = parent; + } + if (child == 0) // came here without climbing up + return leftmost_branch_(node, dst); + unsigned start_child = child; + // find the next children that contains dst. + do + { + child = nodes_[child].next_sibling; + if (nodes_[child].states.get(dst)) + { + if (child <= start_child) + return node; // full loop of children done + else + return child; + } + } + while (child != start_child); + return node; + } + + void acd::dot(std::ostream& os, const char* id) const { unsigned ns = nodes_.size(); @@ -786,6 +830,14 @@ namespace spot return (nodes_[n].level & 1) ^ is_even_; } + /// Return the level of a node. + unsigned acd::node_level(unsigned n) + { + if (SPOT_UNLIKELY(nodes_.size() <= n)) + throw std::runtime_error("acd::node_level(): unknown node"); + return nodes_[n].level; + } + std::vector acd::edges_of_node(unsigned n) const { if (SPOT_UNLIKELY(nodes_.size() <= n)) @@ -821,8 +873,11 @@ namespace spot return has_streett_shape_ && has_rabin_shape_; } + // This handle both the transition-based and state-based version of + // ACD, to + template twa_graph_ptr - acd_transform(const const_twa_graph_ptr& a, bool colored) + acd_transform_(const const_twa_graph_ptr& a, bool colored) { auto res = make_twa_graph(a->get_dict()); res->copy_ap_of(a); @@ -844,6 +899,8 @@ namespace spot // state-based acceptance is lost, // inherently-weak automata become weak. res->prop_copy(a, { false, false, true, true, true, true }); + if constexpr (sbacc) + res->prop_state_acc(true); auto orig_states = new std::vector(); auto branches = new std::vector(); @@ -889,24 +946,42 @@ namespace spot unsigned src_scc = si.scc_of(s.first); unsigned scc_max_lvl = theacd.scc_max_level(src_scc); bool scc_max_lvl_can_be_omitted = (scc_max_lvl & 1) == max_level_is_odd; + unsigned src_prio; + if constexpr (!sbacc) + { + (void)src_prio; // this is only used for sbacc + } + else + { + src_prio = si.is_trivial(src_scc) ? + scc_max_lvl : theacd.node_level(branch); + if (!scc_max_lvl_can_be_omitted || src_prio != scc_max_lvl) + max_color = std::max(max_color, src_prio); + } for (auto& i: a->out(s.first)) { unsigned newbranch; unsigned prio; + if constexpr (sbacc) // All successor have the same colors. + prio = src_prio; unsigned dst_scc = si.scc_of(i.dst); if (dst_scc != src_scc) { newbranch = theacd.first_branch(i.dst); - prio = 0; + if constexpr (!sbacc) + prio = 0; } else { - std::tie(newbranch, prio) = - theacd.step(branch, a->edge_number(i)); + if constexpr (!sbacc) + std::tie(newbranch, prio) = + theacd.step(branch, a->edge_number(i)); + else + newbranch = theacd.state_step(branch, a->edge_number(i)); } zlk_state d(i.dst, newbranch); unsigned dst = new_state(d); - if (!colored && ((dst_scc != src_scc) + if (!colored && ((!sbacc && dst_scc != src_scc) || (scc_max_lvl_can_be_omitted && scc_max_lvl == prio))) { @@ -914,7 +989,8 @@ namespace spot } else { - max_color = std::max(max_color, prio); + if (!sbacc) + max_color = std::max(max_color, prio); res->new_edge(src, dst, i.cond, {prio}); } } @@ -939,4 +1015,16 @@ namespace spot return res; } + twa_graph_ptr + acd_transform(const const_twa_graph_ptr& a, bool colored) + { + return acd_transform_(a, colored); + } + + twa_graph_ptr + acd_transform_sbacc(const const_twa_graph_ptr& a, bool colored) + { + return acd_transform_(a, colored); + } + } diff --git a/spot/twaalgos/zlktree.hh b/spot/twaalgos/zlktree.hh index 7501aa5df..17c142521 100644 --- a/spot/twaalgos/zlktree.hh +++ b/spot/twaalgos/zlktree.hh @@ -222,6 +222,13 @@ namespace spot std::pair step(unsigned branch, unsigned edge) const; + /// \brief Step through the ACD, with rules for state-based output. + /// + /// Given a \a node number, and an edge, this returns + /// the new node to associate to the destination state. This + /// node is not necessarily a leave, and its level should be + /// the level for the output state. + unsigned state_step(unsigned node, unsigned edge) const; /// \brief Return the list of edges covered by node n of the ACD. /// @@ -239,6 +246,9 @@ namespace spot /// This is mostly used for interactive display. bool node_acceptance(unsigned n) const; + /// Return the level of a node. + unsigned node_level(unsigned n); + /// \brief Whether the ACD corresponds to a min even or min odd /// parity acceptance in SCC \a scc. bool is_even(unsigned scc) const @@ -392,7 +402,18 @@ namespace spot /// if the input has n colors. If \colored is unsed (the default), /// output transitions will use at most one color, and output /// automaton will use at most n colors. + /// + /// The acd_tranform() is the original function producing + /// optimal transition-based output (optimal in the sense of least + /// number of duplicated states), while the acd_tansform_sbacc() variant + /// produces state-based output from transition-based input and without + /// any optimality claim. + /// @{ SPOT_API twa_graph_ptr acd_transform(const const_twa_graph_ptr& aut, bool colored = false); + SPOT_API + twa_graph_ptr acd_transform_sbacc(const const_twa_graph_ptr& aut, + bool colored = false); + /// @} } diff --git a/tests/python/zlktree.ipynb b/tests/python/zlktree.ipynb index f3ab8c860..f4c822e9a 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 0x7f5a81a71c00> >" + " *' at 0x7f296c3d8210> >" ] }, "execution_count": 10, @@ -1063,7 +1063,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a81a71690> >" + " *' at 0x7f296c3d8fc0> >" ] }, "execution_count": 11, @@ -1256,7 +1256,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a81a785d0> >" + " *' at 0x7f296c3d8c90> >" ] }, "execution_count": 13, @@ -1701,7 +1701,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a81a787b0> >" + " *' at 0x7f296c3e1210> >" ] }, "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 0x7f5a90499e70> >" + " *' at 0x7f296c3d81e0> >" ] }, "execution_count": 27, @@ -5376,7 +5376,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a903c2810> >" + " *' at 0x7f296cd16c30> >" ] }, "execution_count": 29, @@ -5443,7 +5443,7 @@ }, { "cell_type": "markdown", - "id": "3782b244", + "id": "ce62b966", "metadata": {}, "source": [ "## Typeness checks" @@ -5462,7 +5462,7 @@ { "cell_type": "code", "execution_count": 32, - "id": "c72d6e41", + "id": "7727735d", "metadata": {}, "outputs": [], "source": [ @@ -5489,7 +5489,7 @@ }, { "cell_type": "markdown", - "id": "73342d2c", + "id": "09ec9887", "metadata": {}, "source": [ "Calling the above methods withtout passing the relevant option will raise an exception." @@ -5497,7 +5497,7 @@ }, { "cell_type": "markdown", - "id": "2d982b74", + "id": "816ee0eb", "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." @@ -5506,7 +5506,7 @@ { "cell_type": "code", "execution_count": 34, - "id": "ccadeeaf", + "id": "78643aae", "metadata": {}, "outputs": [ { @@ -5524,7 +5524,7 @@ { "cell_type": "code", "execution_count": 35, - "id": "6161a3e6", + "id": "13a7796b", "metadata": {}, "outputs": [], "source": [ @@ -5534,7 +5534,7 @@ { "cell_type": "code", "execution_count": 36, - "id": "7170615f", + "id": "3ee900b7", "metadata": {}, "outputs": [ { @@ -5549,6 +5549,2083 @@ "print(theacd.has_streett_shape(), theacd.node_count())" ] }, + { + "cell_type": "markdown", + "id": "f380ca5f", + "metadata": {}, + "source": [ + "## State-based transformation\n", + "\n", + "The ACD usage can be modified slightly in order to produce a state-based automaton. The rules for stepping through the ACD are similar, except that when we detect that a cycle through all children of a node has been done, we return the current node without going to the leftmost leave of the next children. When stepping a transition from a node a child, we should act as if we were in the leftmost child of that node containing the source of tha transition. Stepping through a transition this way do not emit any color, instead the color of a state will be the level of its associated node.\n", + "(This modified transformation do not claim to be optimal, unlike the transition-based version.)" + ] + }, + { + "cell_type": "code", + "execution_count": 37, + "id": "e12bb020", + "metadata": {}, + "outputs": [], + "source": [ + "theacd = spot.acd(a3)" + ] + }, + { + "cell_type": "code", + "execution_count": 38, + "id": "813d15ed", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "acd\n", + "\n", + "min odd\n", + "\n", + "\n", + "0\n", + "\n", + "SCC #0\n", + "T: 9-16,21-28,33-36\n", + "{1,2,3,4,5}\n", + "Q: 2,3,5,6,8\n", + "lvl: 0\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "T: 10,12,13,15,21,22\n", + "{2,4,5}\n", + "Q: 2,3,5\n", + "lvl: 1\n", + "<4>\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "T: 23,24,34,36\n", + "{1,2,3,5}\n", + "Q: 5,8\n", + "lvl: 1\n", + "\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "T: 14,15,22,23\n", + "{1,2,3,4}\n", + "Q: 3,5\n", + "lvl: 1\n", + "\n", + "\n", + "\n", + "0->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "T: 14,16,26\n", + "{1,2,3,5}\n", + "Q: 3,6\n", + "lvl: 1\n", + "\n", + "\n", + "\n", + "0->7\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "T: 9\n", + "{1,2,3,5}\n", + "Q: 2\n", + "lvl: 1\n", + "<8>\n", + "\n", + "\n", + "\n", + "0->8\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "11\n", + "\n", + "T: 23\n", + "{1,3}\n", + "Q: 5\n", + "lvl: 2\n", + "<11>\n", + "\n", + "\n", + "\n", + "5->11\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "12\n", + "\n", + "T: 14\n", + "{1,3}\n", + "Q: 3\n", + "lvl: 2\n", + "<12>\n", + "\n", + "\n", + "\n", + "6->12\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "13\n", + "\n", + "T: 23\n", + "{1,3}\n", + "Q: 5\n", + "lvl: 2\n", + "<13>\n", + "\n", + "\n", + "\n", + "6->13\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "14\n", + "\n", + "T: 14\n", + "{1,3}\n", + "Q: 3\n", + "lvl: 2\n", + "<14>\n", + "\n", + "\n", + "\n", + "7->14\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "SCC #1\n", + "T: 31,32,39,40\n", + "{0,1,2,3,5}\n", + "Q: 7,9\n", + "lvl: 1\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "T: 40\n", + "{1,3}\n", + "Q: 9\n", + "lvl: 2\n", + "<9>\n", + "\n", + "\n", + "\n", + "1->9\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "SCC #2\n", + "T: 5,7,17\n", + "{0,1,2,3,5}\n", + "Q: 1,4\n", + "lvl: 1\n", + "\n", + "\n", + "\n", + "10\n", + "\n", + "T: 5\n", + "{1,3}\n", + "Q: 1\n", + "lvl: 2\n", + "<10>\n", + "\n", + "\n", + "\n", + "2->10\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "SCC #3\n", + "T: 1\n", + "{0,1,2,3,5}\n", + "Q: 0\n", + "lvl: 1\n", + "<3>\n", + "\n", + "\n", + "\n" + ], + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "(FGp0 & ((XFp0 & F!p1) | F(Gp1 &\\nXG!p0))) | G(F!p0 &\\n(XFp0 | F!p1) & F(Gp1 | G!p0))\n", + "\n", + "(Fin(\n", + "⓿\n", + ") & Fin(\n", + "❶\n", + ")) | ((Fin(\n", + "❹\n", + ")|Fin(\n", + "❺\n", + ")) & (Inf(\n", + "❷\n", + ")&Inf(\n", + "❸\n", + ")))\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", + "❶\n", + "❷\n", + "❸\n", + "❺\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", + "❸\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", + "❶\n", + "❷\n", + "❸\n", + "❺\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "1->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", + "❷\n", + "❸\n", + "❺\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & !p1\n", + "❷\n", + "❹\n", + "❺\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", + "❸\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & p1\n", + "❹\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & !p1\n", + "❷\n", + "❹\n", + "❺\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", + "❸\n", + "\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & p1\n", + "❷\n", + "❹\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", + "❷\n", + "❸\n", + "❺\n", + "\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", + "❸\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "4->7\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & !p1\n", + "❷\n", + "❹\n", + "❺\n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & p1\n", + "❹\n", + "\n", + "\n", + "\n", + "5->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", + "❸\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "5->8\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", + "❸\n", + "❺\n", + "\n", + "\n", + "\n", + "6->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & !p1\n", + "❷\n", + "❹\n", + "❺\n", + "\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", + "❸\n", + "\n", + "\n", + "\n", + "6->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & p1\n", + "❹\n", + "\n", + "\n", + "\n", + "6->8\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", + "❸\n", + "❺\n", + "\n", + "\n", + "\n", + "7->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "7->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "7->7\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", + "❶\n", + "❷\n", + "❸\n", + "❺\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "9\n", + "\n", + "\n", + "\n", + "7->9\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", + "❷\n", + "❸\n", + "\n", + "\n", + "\n", + "8->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & !p1\n", + "❷\n", + "❹\n", + "❺\n", + "\n", + "\n", + "\n", + "8->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", + "❷\n", + "❸\n", + "\n", + "\n", + "\n", + "8->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & p1\n", + "❷\n", + "❹\n", + "\n", + "\n", + "\n", + "8->8\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", + "❷\n", + "❸\n", + "❺\n", + "\n", + "\n", + "\n", + "9->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "9->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "9->7\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", + "❶\n", + "❸\n", + "❺\n", + "\n", + "\n", + "\n", + "9->9\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", + "❸\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "acd\n", + "\n", + "min odd\n", + "\n", + "\n", + "0\n", + "\n", + "SCC #0\n", + "T: 9-16,21-28,33-36\n", + "{1,2,3,4,5}\n", + "Q: 2,3,5,6,8\n", + "lvl: 0\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "T: 10,12,13,15,21,22\n", + "{2,4,5}\n", + "Q: 2,3,5\n", + "lvl: 1\n", + "<4>\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "T: 23,24,34,36\n", + "{1,2,3,5}\n", + "Q: 5,8\n", + "lvl: 1\n", + "\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "T: 14,15,22,23\n", + "{1,2,3,4}\n", + "Q: 3,5\n", + "lvl: 1\n", + "\n", + "\n", + "\n", + "0->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "T: 14,16,26\n", + "{1,2,3,5}\n", + "Q: 3,6\n", + "lvl: 1\n", + "\n", + "\n", + "\n", + "0->7\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "T: 9\n", + "{1,2,3,5}\n", + "Q: 2\n", + "lvl: 1\n", + "<8>\n", + "\n", + "\n", + "\n", + "0->8\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "11\n", + "\n", + "T: 23\n", + "{1,3}\n", + "Q: 5\n", + "lvl: 2\n", + "<11>\n", + "\n", + "\n", + "\n", + "5->11\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "12\n", + "\n", + "T: 14\n", + "{1,3}\n", + "Q: 3\n", + "lvl: 2\n", + "<12>\n", + "\n", + "\n", + "\n", + "6->12\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "13\n", + "\n", + "T: 23\n", + "{1,3}\n", + "Q: 5\n", + "lvl: 2\n", + "<13>\n", + "\n", + "\n", + "\n", + "6->13\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "14\n", + "\n", + "T: 14\n", + "{1,3}\n", + "Q: 3\n", + "lvl: 2\n", + "<14>\n", + "\n", + "\n", + "\n", + "7->14\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "SCC #1\n", + "T: 31,32,39,40\n", + "{0,1,2,3,5}\n", + "Q: 7,9\n", + "lvl: 1\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "T: 40\n", + "{1,3}\n", + "Q: 9\n", + "lvl: 2\n", + "<9>\n", + "\n", + "\n", + "\n", + "1->9\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "SCC #2\n", + "T: 5,7,17\n", + "{0,1,2,3,5}\n", + "Q: 1,4\n", + "lvl: 1\n", + "\n", + "\n", + "\n", + "10\n", + "\n", + "T: 5\n", + "{1,3}\n", + "Q: 1\n", + "lvl: 2\n", + "<10>\n", + "\n", + "\n", + "\n", + "2->10\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "SCC #3\n", + "T: 1\n", + "{0,1,2,3,5}\n", + "Q: 0\n", + "lvl: 1\n", + "<3>\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + " >" + ] + }, + "execution_count": 38, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "theacd" + ] + }, + { + "cell_type": "markdown", + "id": "98a1474c", + "metadata": {}, + "source": [ + "Let set what happens when we step through the two self-loops of state 2 (edges 9 and 10)." + ] + }, + { + "cell_type": "code", + "execution_count": 39, + "id": "00acde97", + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "4" + ] + }, + "execution_count": 39, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "theacd.first_branch(2)" + ] + }, + { + "cell_type": "code", + "execution_count": 40, + "id": "23c5f4df", + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "8" + ] + }, + "execution_count": 40, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "theacd.state_step(4, 9)" + ] + }, + { + "cell_type": "code", + "execution_count": 41, + "id": "da0bbcbe", + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "0" + ] + }, + "execution_count": 41, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "theacd.state_step(8, 10)" + ] + }, + { + "cell_type": "code", + "execution_count": 42, + "id": "da0dc5bc", + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "8" + ] + }, + "execution_count": 42, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "# since 0 is not a leaf of the tree associated to state 2, the following acts like state_step(first_branch(2), 9)\n", + "theacd.state_step(0, 9) " + ] + }, + { + "cell_type": "markdown", + "id": "c9725681", + "metadata": {}, + "source": [ + "The state-based version of the ACD transformation is `acd_transform_sbacc()`. In the output, the cycle between `2#8` and `2#0` corresponds to the repeatitions of edges 9 and 10 we stepped through above." + ] + }, + { + "cell_type": "code", + "execution_count": 43, + "id": "94999c2e", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "⓿\n", + ") & Inf(\n", + "❶\n", + ")\n", + "[Rabin 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0#3\n", + "❶\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1#10\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2#4\n", + "❶\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3#4\n", + "❶\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4#2\n", + "❶\n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5#4\n", + "❶\n", + "\n", + "\n", + "\n", + "1->5\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "2#8\n", + "❶\n", + "\n", + "\n", + "\n", + "2->6\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "3#6\n", + "❶\n", + "\n", + "\n", + "\n", + "2->7\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "3->7\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "6#7\n", + "❶\n", + "\n", + "\n", + "\n", + "3->8\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "4->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "7#1\n", + "❶\n", + "\n", + "\n", + "\n", + "4->9\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "5->3\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "10\n", + "\n", + "5#5\n", + "❶\n", + "\n", + "\n", + "\n", + "5->10\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "11\n", + "\n", + "8#5\n", + "❶\n", + "\n", + "\n", + "\n", + "5->11\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "6->6\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "12\n", + "\n", + "2#0\n", + "⓿\n", + "\n", + "\n", + "\n", + "6->12\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "13\n", + "\n", + "3#0\n", + "⓿\n", + "\n", + "\n", + "\n", + "6->13\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "6->13\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "7->6\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "7->8\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "14\n", + "\n", + "3#12\n", + "\n", + "\n", + "\n", + "7->14\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "15\n", + "\n", + "5#13\n", + "\n", + "\n", + "\n", + "7->15\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "8->6\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "8->13\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "16\n", + "\n", + "3#14\n", + "\n", + "\n", + "\n", + "8->16\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "17\n", + "\n", + "8#0\n", + "⓿\n", + "\n", + "\n", + "\n", + "8->17\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "9->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "9->5\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "9->9\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "18\n", + "\n", + "9#9\n", + "\n", + "\n", + "\n", + "9->18\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "10->6\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "10->7\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "10->11\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "19\n", + "\n", + "5#11\n", + "\n", + "\n", + "\n", + "10->19\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "11->6\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "11->11\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "11->19\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "20\n", + "\n", + "5#6\n", + "❶\n", + "\n", + "\n", + "\n", + "11->20\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "12->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "12->3\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "12->6\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "12->7\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "13->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "13->5\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "13->7\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "13->8\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "14->6\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "14->8\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "14->14\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "14->15\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "15->6\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "15->7\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "15->15\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "15->17\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "16->6\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "16->8\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "16->16\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "21\n", + "\n", + "5#0\n", + "⓿\n", + "\n", + "\n", + "\n", + "16->21\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "17->6\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "17->11\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "17->19\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "17->20\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "18->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "18->3\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "18->9\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "18->18\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "19->6\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "19->7\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "19->11\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "19->19\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "20->6\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "20->7\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "20->15\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "20->17\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "21->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "21->3\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "21->10\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "21->11\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f296c3f3810> >" + ] + }, + "execution_count": 43, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "s3 = spot.acd_transform_sbacc(a3);\n", + "assert s3.equivalent_to(a3)\n", + "s3.copy_state_names_from(a3)\n", + "s3" + ] + }, + { + "cell_type": "markdown", + "id": "5b770f23", + "metadata": {}, + "source": [ + "In this case, the number of states we obtain with `acd_transform_sbacc()` is smaller than what we would obtain by calling `sbacc()` on the result of `acd_transform()`." + ] + }, + { + "cell_type": "code", + "execution_count": 44, + "id": "b57476cf", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "22 28\n" + ] + } + ], + "source": [ + "print(s3.num_states(), \n", + " spot.sbacc(spot.acd_transform(a3)).num_states())" + ] + }, { "cell_type": "markdown", "id": "15f094c0", @@ -5561,7 +7638,7 @@ }, { "cell_type": "code", - "execution_count": 37, + "execution_count": 45, "id": "criminal-northwest", "metadata": {}, "outputs": [ @@ -5687,10 +7764,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a81a8b840> >" + " *' at 0x7f296c18e210> >" ] }, - "execution_count": 37, + "execution_count": 45, "metadata": {}, "output_type": "execute_result" } @@ -5721,7 +7798,7 @@ }, { "cell_type": "code", - "execution_count": 38, + "execution_count": 46, "id": "63c7c062", "metadata": {}, "outputs": [ @@ -5799,10 +7876,10 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, - "execution_count": 38, + "execution_count": 46, "metadata": {}, "output_type": "execute_result" } @@ -5813,7 +7890,7 @@ }, { "cell_type": "code", - "execution_count": 39, + "execution_count": 47, "id": "balanced-investing", "metadata": {}, "outputs": [ @@ -5965,10 +8042,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a81a8b0f0> >" + " *' at 0x7f296c18e030> >" ] }, - "execution_count": 39, + "execution_count": 47, "metadata": {}, "output_type": "execute_result" } @@ -5979,7 +8056,7 @@ }, { "cell_type": "code", - "execution_count": 40, + "execution_count": 48, "id": "nutritional-rugby", "metadata": {}, "outputs": [], @@ -5989,7 +8066,7 @@ }, { "cell_type": "code", - "execution_count": 41, + "execution_count": 49, "id": "criminal-marking", "metadata": {}, "outputs": [ @@ -6052,7 +8129,7 @@ "\n", "\n", - "\n", + "\n", "\n", "(Fin(\n", "⓿\n", @@ -6075,7 +8152,7 @@ "0\n", "\n", "\n", - "\n", + "\n", "I->0\n", "\n", "\n", @@ -6193,7 +8270,7 @@ "\n", "\n", - "\n", + "\n", "acd\n", "\n", "min even\n", @@ -6221,7 +8298,7 @@ "<1>\n", "\n", "\n", - "\n", + "\n", "0->1\n", "\n", "\n", @@ -6229,50 +8306,71 @@ "\n", "\n", "" + " $(\"#acd2 #N\" + node).addClass(\"acdbold acdhigh\");\n", + "};$(\"#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 #E8\").addClass(\"acdN0\");$(\"#acdaut2 #E6\").addClass(\"acdN1\");$(\"#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 #E8\").click(function(){acd2_edge(8);});$(\"#acdaut2 #S0\").click(function(){acd2_state(0);});$(\"#acdaut2 #S1\").click(function(){acd2_state(1);});$(\"#acd2 #N0\").click(function(){acd2_node(0, 1);});$(\"#acd2 #N1\").click(function(){acd2_node(1, 0);});" ], "text/plain": [ - " >" + " >" ] }, - "execution_count": 41, + "execution_count": 49, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "spot.acd(c)" + "cacd = spot.acd(c); cacd" ] }, { "cell_type": "code", - "execution_count": 42, + "execution_count": 50, + "id": "e7760d51", + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "0" + ] + }, + "execution_count": 50, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "cacd.state_step(1, 7)" + ] + }, + { + "cell_type": "code", + "execution_count": 51, "id": "unusual-dependence", "metadata": { "scrolled": true @@ -6381,10 +8479,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a81a8b180> >" + " *' at 0x7f296c193240> >" ] }, - "execution_count": 42, + "execution_count": 51, "metadata": {}, "output_type": "execute_result" } @@ -6395,12 +8493,160 @@ }, { "cell_type": "code", - "execution_count": 43, + "execution_count": 52, + "id": "d5440de1", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "p0 & p1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f296c1934b0> >" + ] + }, + "execution_count": 52, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "e = spot.acd_transform_sbacc(c); e" + ] + }, + { + "cell_type": "code", + "execution_count": 53, "id": "9ed0bc59", "metadata": {}, "outputs": [], "source": [ - "assert c.equivalent_to(d)" + "assert c.equivalent_to(d)\n", + "assert c.equivalent_to(e)" ] }, { @@ -6414,7 +8660,7 @@ }, { "cell_type": "code", - "execution_count": 44, + "execution_count": 54, "id": "deb92971", "metadata": {}, "outputs": [ @@ -6493,7 +8739,7 @@ "\n", "\n", - "\n", + "\n", "\n", "Inf(\n", "⓿\n", @@ -6513,7 +8759,7 @@ "0\n", "\n", "\n", - "\n", + "\n", "I->0\n", "\n", "\n", @@ -6633,7 +8879,7 @@ "\n", "\n", - "\n", + "\n", "acd\n", "\n", "min even\n", @@ -6665,7 +8911,7 @@ "<1>\n", "\n", "\n", - "\n", + "\n", "0->1\n", "\n", "\n", @@ -6682,7 +8928,7 @@ "<2>\n", "\n", "\n", - "\n", + "\n", "0->2\n", "\n", "\n", @@ -6690,39 +8936,39 @@ "\n", "\n", "" + " $(\"#acd3 #N\" + node).addClass(\"acdbold acdhigh\");\n", + "};$(\"#acdaut3 #E1\").addClass(\"acdN0\");$(\"#acdaut3 #E2\").addClass(\"acdN0\");$(\"#acdaut3 #E3\").addClass(\"acdN0\");$(\"#acdaut3 #E4\").addClass(\"acdN0\");$(\"#acdaut3 #E5\").addClass(\"acdN0\");$(\"#acdaut3 #E6\").addClass(\"acdN0\");$(\"#acdaut3 #E7\").addClass(\"acdN0\");$(\"#acdaut3 #E1\").addClass(\"acdN1\");$(\"#acdaut3 #E3\").addClass(\"acdN1\");$(\"#acdaut3 #E4\").addClass(\"acdN1\");$(\"#acdaut3 #E5\").addClass(\"acdN1\");$(\"#acdaut3 #E7\").addClass(\"acdN2\");$(\"#acdaut3 #E1\").click(function(){acd3_edge(1);});$(\"#acdaut3 #E2\").click(function(){acd3_edge(2);});$(\"#acdaut3 #E3\").click(function(){acd3_edge(3);});$(\"#acdaut3 #E4\").click(function(){acd3_edge(4);});$(\"#acdaut3 #E5\").click(function(){acd3_edge(5);});$(\"#acdaut3 #E6\").click(function(){acd3_edge(6);});$(\"#acdaut3 #E7\").click(function(){acd3_edge(7);});$(\"#acdaut3 #S0\").click(function(){acd3_state(0);});$(\"#acdaut3 #S1\").click(function(){acd3_state(1);});$(\"#acdaut3 #S2\").click(function(){acd3_state(2);});$(\"#acdaut3 #S3\").click(function(){acd3_state(3);});$(\"#acd3 #N0\").click(function(){acd3_node(0, 1);});$(\"#acd3 #N1\").click(function(){acd3_node(1, 0);});$(\"#acd3 #N2\").click(function(){acd3_node(2, 0);});" ], "text/plain": [ - " >" + " >" ] }, - "execution_count": 44, + "execution_count": 54, "metadata": {}, "output_type": "execute_result" } @@ -6740,7 +8986,7 @@ }, { "cell_type": "code", - "execution_count": 45, + "execution_count": 55, "id": "94a02201", "metadata": {}, "outputs": [ @@ -6847,10 +9093,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a8001f3c0> >" + " *' at 0x7f296c193b70> >" ] }, - "execution_count": 45, + "execution_count": 55, "metadata": {}, "output_type": "execute_result" } @@ -6861,7 +9107,137 @@ }, { "cell_type": "code", - "execution_count": 46, + "execution_count": 56, + "id": "d484ba8f", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f296c198330> >" + ] + }, + "execution_count": 56, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.acd_transform_sbacc(g)" + ] + }, + { + "cell_type": "code", + "execution_count": 57, "id": "3332e850", "metadata": {}, "outputs": [ @@ -7127,10 +9503,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a8001f7b0> >" + " *' at 0x7f296c1984e0> >" ] }, - "execution_count": 46, + "execution_count": 57, "metadata": {}, "output_type": "execute_result" } @@ -7151,7 +9527,7 @@ }, { "cell_type": "code", - "execution_count": 47, + "execution_count": 58, "id": "german-vienna", "metadata": {}, "outputs": [ @@ -7221,10 +9597,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a8001ff60> >" + " *' at 0x7f296c198cf0> >" ] }, - "execution_count": 47, + "execution_count": 58, "metadata": {}, "output_type": "execute_result" } @@ -7248,7 +9624,7 @@ }, { "cell_type": "code", - "execution_count": 48, + "execution_count": 59, "id": "chemical-primary", "metadata": {}, "outputs": [ @@ -7258,7 +9634,7 @@ "(spot.trival_maybe(), spot.trival(True))" ] }, - "execution_count": 48, + "execution_count": 59, "metadata": {}, "output_type": "execute_result" } @@ -7269,7 +9645,7 @@ }, { "cell_type": "code", - "execution_count": 49, + "execution_count": 60, "id": "hispanic-floor", "metadata": {}, "outputs": [ @@ -7332,10 +9708,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a80026240> >" + " *' at 0x7f296c19e120> >" ] }, - "execution_count": 49, + "execution_count": 60, "metadata": {}, "output_type": "execute_result" } @@ -7346,7 +9722,7 @@ }, { "cell_type": "code", - "execution_count": 50, + "execution_count": 61, "id": "central-london", "metadata": {}, "outputs": [ @@ -7356,7 +9732,7 @@ "(spot.trival(True), spot.trival(True))" ] }, - "execution_count": 50, + "execution_count": 61, "metadata": {}, "output_type": "execute_result" } diff --git a/tests/python/zlktree.py b/tests/python/zlktree.py index be565342c..89571e520 100644 --- a/tests/python/zlktree.py +++ b/tests/python/zlktree.py @@ -117,3 +117,10 @@ except RuntimeError as e: assert 'unknown node' in str(e) else: report_missing_exception() + +try: + aa.node_level(0) +except RuntimeError as e: + assert 'unknown node' in str(e) +else: + report_missing_exception()