From 46590af6934676854b0232a41092571e1e42cac2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 10 Jul 2018 17:17:59 +0200 Subject: [PATCH] more documentation for twa_graph internals * spot/graph/graph.hh, spot/twa/twagraph.hh, spot/twa/twagraph.cc: Implement a dump_storage_as_dot() method. * python/spot/__init__.py (twa_graph.show_storage): New method, above dump_storage_as_dot(). * tests/python/twagraph-internals.ipynb: New file, with documentation about the twa_graph internals, using show_storage() to illustrate everything. * tests/Makefile.am, doc/org/tut.org: Add it. * python/spot/impl.i: Add bindings for out_iterasor, demonstrated in the Python notebook. * spot/twa/twa.hh: Add prop_reset(). Used in the notebook. * NEWS: Mention the new notebook and function. * doc/org/tut50.org: Link to the notebook. * tests/python/ipnbdoctest.py: Adjust for twa_graph_ptr being redefined in the spot namespace. --- NEWS | 5 + doc/org/tut.org | 1 + doc/org/tut50.org | 7 +- python/spot/__init__.py | 8 + python/spot/impl.i | 19 + spot/graph/graph.hh | 150 + spot/twa/twa.hh | 5 + spot/twa/twagraph.cc | 137 + spot/twa/twagraph.hh | 27 +- tests/Makefile.am | 1 + tests/python/ipnbdoctest.py | 7 + tests/python/twagraph-internals.ipynb | 5519 +++++++++++++++++++++++++ 12 files changed, 5880 insertions(+), 6 deletions(-) create mode 100644 tests/python/twagraph-internals.ipynb diff --git a/NEWS b/NEWS index e7425e479..4119127cd 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,11 @@ New in spot 2.6.0.dev (not yet released) formula::F(unsigned, unsigned, formula) formula::G(unsigned, unsigned, formula) + - The twa_graph class has a new dump_storage_as_dot() method + to show its data structure. This is more conveniently used + as aut.show_storage() in a Jupyter notebook. See + https://spot.lrde.epita.fr/ipynb/twagraph-internals.html + New in spot 2.6 (2018-07-04) Command-line tools: diff --git a/doc/org/tut.org b/doc/org/tut.org index 9e7e1bb7e..a68751a92 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -85,3 +85,4 @@ real notebooks instead. - [[https://spot.lrde.epita.fr/ipynb/alternation.html][=alternation.ipynb=]] examples of alternating automata. - [[https://spot.lrde.epita.fr/ipynb/stutter-inv.html][=stutter-inv.ipynb=]] working with stutter-invariant formulas properties. - [[https://spot.lrde.epita.fr/ipynb/satmin.html][=satmin.ipynb=]] Python interface for [[file:satmin.org][SAT-based minimization of deterministic ω-automata]]. +- [[https://spot.lrde.epita.fr/ipynb/twagraph-internals.html][=twagraph-internals.ipynb=]] Inner workings of the =twa_graph= class. diff --git a/doc/org/tut50.org b/doc/org/tut50.org index df925625f..ef5af56d8 100644 --- a/doc/org/tut50.org +++ b/doc/org/tut50.org @@ -21,9 +21,10 @@ from the initial state of an automaton. The explicit interface can only be used on =twa_graph= objects. In this interface, states and edges are referred to by numbers that are -indices into state and edge vectors. This interface is lightweight, -and is the preferred interface for writing most automata algorithms in -Spot. +indices into state and edge vectors (the [[https://spot.lrde.epita.fr/ipynb/satmin.html][=twagraph-internals.ipynb=]] +notebook shows these vectors graphically). This interface is +lightweight, and is the preferred interface for writing most automata +algorithms in Spot. ** How this interface works diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 74131f8e5..b01c21cc8 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -175,6 +175,13 @@ class twa: f.write('\n') return a +@_extend(twa_graph) +class twa_graph: + def show_storage(self, opt=None): + ostr = ostringstream() + self.dump_storage_as_dot(ostr, opt) + from IPython.display import SVG + return SVG(_ostream_to_svg(ostr)) @_extend(formula) class formula: @@ -761,6 +768,7 @@ def postprocess(automaton, *args, formula=None): twa.postprocess = postprocess + # Wrap C++-functions into lambdas so that they get converted into # instance methods (i.e., self passed as first argument # automatically), because only user-defined functions are converted as diff --git a/python/spot/impl.i b/python/spot/impl.i index 1050c7568..397cf7b0b 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -509,6 +509,7 @@ namespace std { %include %nodefaultctor spot::digraph; %nodefaultctor spot::internal::state_out; +%nodefaultctor spot::internal::killer_edge_iterator; %nodefaultctor spot::internal::all_trans; %nodefaultctor spot::internal::universal_dests; %traits_swigtype(spot::internal::edge_storage >); @@ -556,6 +557,7 @@ def state_is_accepting(self, src) -> "bool": %include %template(twa_graph_state_out) spot::internal::state_out>; +%template(twa_graph_killer_edge_iterator) spot::internal::killer_edge_iterator>; %template(twa_graph_all_trans) spot::internal::all_trans>; %template(twa_graph_edge_boxed_data) spot::internal::boxed_label; %template(twa_graph_edge_storage) spot::internal::edge_storage >; @@ -799,6 +801,23 @@ def state_is_accepting(self, src) -> "bool": } } +%extend spot::internal::killer_edge_iterator> { + + spot::internal::edge_storage >& current() + { + return **self; + } + + void advance() + { + ++*self; + } + bool __bool__() + { + return *self; + } +} + %extend spot::internal::all_trans> { swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF) { diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh index b1d235123..7833aae68 100644 --- a/spot/graph/graph.hh +++ b/spot/graph/graph.hh @@ -1059,6 +1059,156 @@ namespace spot } } + enum dump_storage_items { + DSI_GraphHeader = 1, + DSI_GraphFooter = 2, + DSI_StatesHeader = 4, + DSI_StatesBody = 8, + DSI_StatesFooter = 16, + DSI_States = DSI_StatesHeader | DSI_StatesBody | DSI_StatesFooter, + DSI_EdgesHeader = 32, + DSI_EdgesBody = 64, + DSI_EdgesFooter = 128, + DSI_Edges = DSI_EdgesHeader | DSI_EdgesBody | DSI_EdgesFooter, + DSI_DestsHeader = 256, + DSI_DestsBody = 512, + DSI_DestsFooter = 1024, + DSI_Dests = DSI_DestsHeader | DSI_DestsBody | DSI_DestsFooter, + DSI_All = + DSI_GraphHeader | DSI_States | DSI_Edges | DSI_Dests | DSI_GraphFooter, + }; + + /// Dump the state and edge storage for debugging + void dump_storage_as_dot(std::ostream& o, int dsi = DSI_All) const + { + if (dsi & DSI_GraphHeader) + o << "digraph g { \nnode [shape=plaintext]\n"; + unsigned send = states_.size(); + if (dsi & DSI_StatesHeader) + { + o << ("states [label=<\n" + "\n" + "\n"); + for (unsigned s = 0; s < send; ++s) + o << "\n"; + o << "\n"; + } + if (dsi & DSI_StatesBody) + { + o << "\n"; + for (unsigned s = 0; s < send; ++s) + { + o << "\n"; + } + o << "\n"; + for (unsigned s = 0; s < send; ++s) + { + o << "\n"; + } + o << "\n"; + } + if (dsi & DSI_StatesFooter) + o << "
states" + << s << "
succ" << states_[s].succ << "
succ_tail" << states_[s].succ_tail << "
>]\n"; + unsigned eend = edges_.size(); + if (dsi & DSI_EdgesHeader) + { + o << ("edges [label=<\n" + "\n" + "\n"); + for (unsigned e = 1; e < eend; ++e) + { + o << "\n"; + } + o << ""; + } + if (dsi & DSI_EdgesBody) + { + o << "\n"; + for (unsigned e = 1; e < eend; ++e) + { + o << "\n"; + } + o << "\n"; + for (unsigned e = 1; e < eend; ++e) + { + o << "\n"; + } + o << "\n"; + for (unsigned e = 1; e < eend; ++e) + o << "\n"; + o << "\n"; + } + if (dsi & DSI_EdgesFooter) + o << "
edges" << e << "
dst~" << ~d; + else + o << "' bgcolor='yellow'>" << d; + o << "
next_succ" << edges_[e].next_succ << "
src" + << edges_[e].src << "
>]\n"; + if (!dests_.empty()) + { + unsigned dend = dests_.size(); + if (dsi & DSI_DestsHeader) + { + o << ("dests [label=<\n" + "\n" + "\n"); + unsigned d = 0; + while (d < dend) + { + o << "\n"; + unsigned cnt = dests_[d]; + d += cnt + 1; + while (cnt--) + o << "\n"; + } + o << "\n"; + } + if (dsi & DSI_DestsBody) + { + o << "\n"; + unsigned d = 0; + while (d < dend) + { + unsigned cnt = dests_[d]; + o << "\n"; + ++d; + while (cnt--) + { + o << "\n"; + ++d; + } + } + o << "\n"; + } + if (dsi & DSI_DestsFooter) + o << "
dests~" << d << "
#cnt/dst#" << cnt << "" << dests_[d] << "
>]\n"; + } + if (dsi & DSI_GraphFooter) + o << "}\n"; + } + /// \brief Remove all dead edges. /// /// The edges_ vector is left in a state that is incorrect and diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index f6d00d7e8..84e3cbf68 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -1071,6 +1071,7 @@ namespace spot bprop is; }; + protected: #ifndef SWIG // Dynamic properties, are given with a name and a destructor function. std::unordered_map #include #include +#include +#include #include #include @@ -764,6 +766,141 @@ namespace spot set_named_prop("state-names", names.release()); } + void twa_graph::dump_storage_as_dot(std::ostream& out, + const char* opt) const + { + bool want_vectors = false; + bool want_data = false; + bool want_properties = false; + if (!opt || !*opt) + { + want_vectors = want_data = want_properties = true; + } + else + { + while (*opt) + switch (*opt++) + { + case 'v': + want_vectors = true; + break; + case 'd': + want_data = true; + break; + case 'p': + want_properties = true; + break; + default: + throw std::runtime_error(std::string("dump_storage_as_dow(): " + "unsupported option '") + + opt[-1] +"'"); + } + } + + const graph_t& g = get_graph(); + + g.dump_storage_as_dot(out, graph_t::DSI_GraphHeader); + out << "rankdir=BT\n"; + + if (want_vectors) + { + out << "{rank=same;\n"; + + g.dump_storage_as_dot(out, graph_t::DSI_States | + graph_t::DSI_EdgesHeader); + + auto edges = g.edge_vector(); + unsigned eend = edges.size(); + out << "cond\n"; + for (unsigned e = 1; e < eend; ++e) + { + out << ""; + std::string f = bdd_format_formula(get_dict(), edges[e].cond); + escape_html(out, f); + out << "\n"; + } + out << "\nacc\n"; + for (unsigned e = 1; e < eend; ++e) + out << "" << edges[e].acc << "\n"; + out << "\n"; + + g.dump_storage_as_dot(out, graph_t::DSI_EdgesBody + | graph_t::DSI_EdgesFooter + | graph_t::DSI_Dests); + out << "}\n"; + } + if (want_data || want_properties) + { + out << "{rank=same;\n"; + + if (want_data) + { + out << ("meta [label=<\n" + "\n"); + unsigned d = get_init_state_number(); + out << ("" + "" + "" + "" + "
init_state:~" << ~d; + else + out << "yellow'>" << d; + out << ("
num_sets:") + << num_sets() + << ("
acceptance:"); + get_acceptance().to_html(out); + out << ("
ap_vars:"); + escape_html(out, bdd_format_sat(get_dict(), ap_vars())); + out << "
>]\n"; + } + if (want_properties) + { + out << ("props [label=<\n" + "\n"); +#define print_prop(name) \ + out << ("" \ + "\n"; + print_prop(prop_state_acc); + print_prop(prop_inherently_weak); + print_prop(prop_terminal); + print_prop(prop_weak); + print_prop(prop_very_weak); + print_prop(prop_complete); + print_prop(prop_universal); + print_prop(prop_unambiguous); + print_prop(prop_semi_deterministic); + print_prop(prop_stutter_invariant); +#undef print_prop + out << "
" #name ":") << name() << "
>]\n"; + + if (!named_prop_.empty()) + { + out << "namedprops [label=\"named properties:\n"; + for (auto p: named_prop_) + escape_html(out, p.first) << '\n'; + out << "\"]\n"; + } + } + out << "}\n"; + } + + if (want_data && want_vectors) + out << "meta -> states [style=invis]\n"; + if (want_properties && want_vectors) + { + out << "props -> edges [style=invis]\n"; + if (!named_prop_.empty()) + { + out << "namedprops -> edges [style=invis]\n"; + if (!is_existential()) + out << "namedprops -> dests [style=invis]\n"; + } + } + g.dump_storage_as_dot(out, graph_t::DSI_GraphFooter); + } + namespace { twa_graph_ptr diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index b2020721f..14da195aa 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -471,6 +471,12 @@ namespace spot return g_.out(src); } + internal::killer_edge_iterator + out_iteraser(unsigned src) + { + return g_.out_iteraser(src); + } + internal::const_universal_dests univ_dests(unsigned d) const noexcept { @@ -525,11 +531,18 @@ namespace spot SPOT_RETURN(g_.edge_vector()); auto edge_vector() SPOT_RETURN(g_.edge_vector()); - - auto is_dead_edge(const graph_t::edge_storage_t& t) const - SPOT_RETURN(g_.is_dead_edge(t)); #endif + bool is_dead_edge(unsigned t) const + { + return g_.is_dead_edge(t); + } + + bool is_dead_edge(const graph_t::edge_storage_t& t) const + { + return g_.is_dead_edge(t); + } + /// \brief Merge edges that can be merged. /// /// This makes two passes over the automaton to reduce the number @@ -682,6 +695,14 @@ namespace spot /// Use -1U to erase a state. /// \param used_states the number of states used (after renumbering) void defrag_states(std::vector&& newst, unsigned used_states); + + /// \brief Print the data structures used to represent the + /// automaton in dot's format. + /// + /// \a opt should be a substring of "vdp" if you want to print + /// only the vectors, data, or properties. + void dump_storage_as_dot(std::ostream& out, + const char* opt = nullptr) const; }; /// \ingroup twa_representation diff --git a/tests/Makefile.am b/tests/Makefile.am index 9749312a9..6b2b0501e 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -351,6 +351,7 @@ TESTS_ipython = \ python/satmin.ipynb \ python/stutter-inv.ipynb \ python/testingaut.ipynb \ + python/twagraph-internals.ipynb \ python/word.ipynb # TESTS_python contains all tests. It may includes notebooks we diff --git a/tests/python/ipnbdoctest.py b/tests/python/ipnbdoctest.py index dc05fce22..6a3005370 100755 --- a/tests/python/ipnbdoctest.py +++ b/tests/python/ipnbdoctest.py @@ -81,6 +81,9 @@ def canonicalize(s, type, ignores): # normalize UUIDs: s = re.sub(r'[a-f0-9]{8}(\-[a-f0-9]{4}){3}\-[a-f0-9]{12}', 'U-U-I-D', s) + # class from spot.impl. may be redefined in spot. without notice. + s = re.sub(r'', '>\n<title>', s) diff --git a/tests/python/twagraph-internals.ipynb b/tests/python/twagraph-internals.ipynb new file mode 100644 index 000000000..815d35006 --- /dev/null +++ b/tests/python/twagraph-internals.ipynb @@ -0,0 +1,5519 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "This notebook discusses how explicit automata (the `spot::twa_graph_ptr` objects in C++) are stored by Spot. The Python bindings do not expose all of the internals available in C++, however they have some graphical representation that are convenient to present those inner workings." + ] + }, + { + "cell_type": "code", + "execution_count": 1, + "metadata": {}, + "outputs": [], + "source": [ + "import buddy\n", + "import spot\n", + "spot.setup(show_default='.n')\n", + "from IPython.display import display" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# The two-vector representation" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Let's consider a small automaton, generated from an LTL formula." + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "metadata": {}, + "outputs": [], + "source": [ + "aut = spot.translate('GF(a <-> Xa) & FGb', 'det', 'gen')" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n", + "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n", + " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n", + "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n", + " -->\n", + "<!-- Pages: 1 -->\n", + "<svg width=\"198pt\" height=\"220pt\"\n", + " viewBox=\"0.00 0.00 197.50 219.60\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", + "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 215.597)\">\n", + "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-215.597 193.5,-215.597 193.5,4 -4,4\"/>\n", + "<text text-anchor=\"start\" x=\"42.75\" y=\"-197.397\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">Fin(</text>\n", + "<text text-anchor=\"start\" x=\"67.75\" y=\"-197.397\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n", + "<text text-anchor=\"start\" x=\"83.75\" y=\"-197.397\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">) & Inf(</text>\n", + "<text text-anchor=\"start\" x=\"126.75\" y=\"-197.397\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n", + "<text text-anchor=\"start\" x=\"142.75\" y=\"-197.397\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">)</text>\n", + "<text text-anchor=\"start\" x=\"65.75\" y=\"-183.397\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[Rabin 1]</text>\n", + "<!-- I -->\n", + "<!-- 0 -->\n", + "<g id=\"node2\" class=\"node\">\n", + "<title>0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b\n", + "❶\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "❶\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f616c1788a0> >" + ] + }, + "execution_count": 3, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The graphical representation above is just a convenient representation of that automaton and hides some details. Internally, this automaton is stored as two vectors plus some additional data. All of those can be displayed using the `show_storage()` method. The two vectors are the `states` and `edges` vectors. The additional data gives the initial state, number of acceptance sets, acceptance condition, list of atomic propositions, as well as a bunch of [property flags](https://spot.lrde.epita.fr/concepts.html#property-flags) on the automaton. All those properties default to `maybe`, but some algorithms will turn them to `yes` or `no` whenever that property can be decided at very low cost (usually a side effect of the algorithm). In this example we asked for a deterministic automaton, so the output of the construction is necessarily `universal` (this means no existantial branching, hence deterministic for our purpose), and this property implies `unambiguous` and `semi_deterministic`." + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "5\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "cond\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "acc\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "dst\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "next_succ\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "0\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "meta\n", + "init_state:\n", + "\n", + "0\n", + "num_sets:\n", + "2\n", + "acceptance:\n", + "Fin(0) & Inf(1)\n", + "ap_vars:\n", + "b a\n", + "\n", + "\n", + "\n", + "\n", + "props\n", + "prop_state_acc:\n", + "maybe\n", + "prop_inherently_weak:\n", + "maybe\n", + "prop_terminal:\n", + "no\n", + "prop_weak:\n", + "maybe\n", + "prop_very_weak:\n", + "maybe\n", + "prop_complete:\n", + "maybe\n", + "prop_universal:\n", + "yes\n", + "prop_unambiguous:\n", + "yes\n", + "prop_semi_deterministic:\n", + "yes\n", + "prop_stutter_invariant:\n", + "maybe\n", + "\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 4, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut.show_storage()" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Each state is represented by an integer that is a 0-based index into the `states` array. Each edge is also represented by an integer that is a 1-based index into the `edges` array. In the above picture, yellow and cyan denote state and edge indices respectively.\n", + "\n", + "Adding a new edge, for instance, will augment the size of the `edges` array and return the index of the newly added edge:" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "9" + ] + }, + "execution_count": 5, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "s = aut.new_state()\n", + "aut.set_init_state(s)\n", + "aut.new_edge(s, 0, buddy.bddtrue)" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "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", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "I->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b\n", + "❶\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "❶\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f616c1788a0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "9\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "cond\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "dst\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "next_succ\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "0\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "display(aut, aut.show_storage(\"v\")) # \"v\" displays only the states and edges Vectors" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "For each state, the `states` vector stores two edge indices: `succ` is the index of the first outgoing edge, and `succ_tail` is the index of the last outgoing edge. Since there is no edge at index `0`, that value is used to indicate that there is no outgoing edge.\n", + "\n", + "In the `edges` vector, the field `next_succ` is used to organize the outgoing edges of a state as a linked list. For instance to iterate over all successors of state `0`, we would start at the edge `e = states[0].succ` (if it's not `0`),\n", + "then move to the next successor with `e = edges[e].next_succ`, and repeat until `e` becomes `0`. This code cannot be executed in Python because the automaton class won't let us access the `states` vector. However this iteration mechanism is what is used into the `out()` method: `out()` simply provides an iterator over some columns of the `edges` vector, following the `next_succ` links. When we have a reference to a column of `edges` as returned by `out()`, we can convert it into an edge index with the `edge_number()` method." + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "edges[1].src=0, edges[1].dst=0\n", + "edges[2].src=0, edges[2].dst=0\n", + "edges[3].src=0, edges[3].dst=1\n", + "edges[4].src=0, edges[4].dst=1\n" + ] + } + ], + "source": [ + "for ed in aut.out(0):\n", + " print(\"edges[{e}].src={src}, edges[{e}].dst={dst}\".format(e=aut.edge_number(ed), src=ed.src, dst=ed.dst))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The other fields of the `edges` vector probably speak for themselves. `cond` is a BDD representing the boolean combination of atomic propositions expected by the edge, `acc` is an instance of `spot::acc_cond::mark_t`, i.e., a bit set representing the set of acceptance sets the edge belongs to, `src` and `dst` are the source and destination of the transition. Of course when iterating over the successors of a state with `aut.out(src)`, the source is well known, but there are other situations where it is convenient to retrieve the source from the edge (e.g., when iterating over all edges of an automaton, or when storing edges indices for later processing).\n", + "\n", + "You can access one column of the `edges` vector using the `edge_storage()` method. For instance let's modify edge 3:" + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "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", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "I->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & b\n", + "❶\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & b\n", + "❶\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "❶\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f616c1788a0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "9\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "cond\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "dst\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "next_succ\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "0\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 8, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut.edge_storage(3).acc.set(1)\n", + "aut.edge_storage(3).dst = 0\n", + "display(aut)\n", + "aut.show_storage(\"v\")" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Having the source into the `edges` vector also allows us to easily sort that vector to put all sibling transitions (i.e., transition leaving the same state) together to improve data locality. The `merge_edges()` method will do that and a bit more: edges are first sorted by (`src`, `dst`, `acc`) making possible to merge the `cond` field of edges with identical (`src`, `dst`, `acc`). On Fin-less automata (not our example), the a second pass is perform to sort the edge (`src`, `dst`, `cond`) and then merge the `acc` fields of edges that share the other fields.\n", + "\n", + "In our example, `merge_edges()` will merge edges 1 and 3." + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "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", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "I->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "❶\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "❶\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f616c1788a0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "8\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "cond\n", + "\n", + "b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "dst\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "next_succ\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "0\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "aut.merge_edges()\n", + "display(aut, aut.show_storage(\"v\"))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Note that the `succ_tail` field of the `states` vector is seldom used when reading automata as the linked list of edges ends when `next_succ` (or `succ`) equals `0`. Its main use is during calls to `new_edge()`: new edges are always created at the end of the list (otherwise it would be hard to preserve the order of edges when parsing and automaton and printing it)." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# The property-update issue\n", + "\n", + "Properties like `prop_complete()`, `prop_universal()`, and the like are normally updated by algorithms that modify the automaton in place. They are not updated when we modify the automaton using low-level methods like `new_state()` or `new_edges()` as we have done so far.\n", + "\n", + "For instance we could add a new edge to the automaton to introduce some non-determinism, and the automaton would still pretend it is universal." + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "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", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "I->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "❶\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "❶\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f616c1788a0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "8\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "cond\n", + "\n", + "b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "{0,1}\n", + "\n", + "dst\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "next_succ\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "0\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "9\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "meta\n", + "init_state:\n", + "\n", + "2\n", + "num_sets:\n", + "2\n", + "acceptance:\n", + "Fin(0) & Inf(1)\n", + "ap_vars:\n", + "b a\n", + "\n", + "\n", + "\n", + "\n", + "props\n", + "prop_state_acc:\n", + "maybe\n", + "prop_inherently_weak:\n", + "maybe\n", + "prop_terminal:\n", + "no\n", + "prop_weak:\n", + "maybe\n", + "prop_very_weak:\n", + "maybe\n", + "prop_complete:\n", + "maybe\n", + "prop_universal:\n", + "yes\n", + "prop_unambiguous:\n", + "yes\n", + "prop_semi_deterministic:\n", + "yes\n", + "prop_stutter_invariant:\n", + "maybe\n", + "\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "aut.new_edge(1, 1, buddy.bddtrue, [1, 0])\n", + "display(aut, aut.show_storage())" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Such an inconsistency will cause many issues when the automaton is passed to algorithm with specialized handling of universal automata. When writing an algorithm that modify the automaton, it is your responsibility to update the property bits as well. In this case it could be fixed by calling `aut.prop_universal(False); aut.prop_unambiguous(spot.trival_maybe()); ...` for each property, or by reseting all properties to `maybe` with `prop_reset()`:" + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "props\n", + "prop_state_acc:\n", + "maybe\n", + "prop_inherently_weak:\n", + "maybe\n", + "prop_terminal:\n", + "maybe\n", + "prop_weak:\n", + "maybe\n", + "prop_very_weak:\n", + "maybe\n", + "prop_complete:\n", + "maybe\n", + "prop_universal:\n", + "maybe\n", + "prop_unambiguous:\n", + "maybe\n", + "prop_semi_deterministic:\n", + "maybe\n", + "prop_stutter_invariant:\n", + "maybe\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 11, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut.prop_reset()\n", + "aut.show_storage(\"p\") # \"p\" displays only the properties" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Erasing edges\n", + "\n", + "Erasing a single edge, denoted by its edge index `i`, is not convenient because of the linked structure of the edges: the `next_succ` of the previous (but unknown given `i`) edge would have to be updated (or maybe the `succ` or `succ_tail` fields of `states` vector have to be updated).\n", + "\n", + "The `out_iteraser(s)` method provides a way to iterate over the outgoing edges of state `s` that allows erasing edges. The iteration does not follow the usual Python pattern because once you have looked at the current edge using `current()`, you have two choices: `advance()` to the next one, or `erase()` the current one (and advance to the next). Note that `it.current()` and `it.advance()` are written `*it` and `++it` in C++.\n", + "\n", + "The following example erases all the outgoing transitions of state `0` that belong to acceptance set `1`." + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "pos=1, acc={1}, toerase=True\n", + "pos=2, acc={0,1}, toerase=True\n", + "pos=3, acc={0}, toerase=False\n" + ] + } + ], + "source": [ + "it = aut.out_iteraser(0)\n", + "while it:\n", + " e = it.current()\n", + " toerase = e.acc.has(1)\n", + " print(\"pos={}, acc={}, toerase={}\".format(aut.edge_number(e), e.acc, toerase))\n", + " if toerase:\n", + " it.erase()\n", + " else:\n", + " it.advance()" + ] + }, + { + "cell_type": "code", + "execution_count": 13, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "succ\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "8\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "cond\n", + "\n", + "b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "{0,1}\n", + "\n", + "dst\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "next_succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "0\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "9\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 13, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut.show_storage(\"v\")" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Notice that the edges vector hasn't been resized, as doing so would renumber edges. Instead, erased edges have removed from the linked list of outgoing edges of `0`, and their `next_succ` field has been changed to point to themselves. \n", + "\n", + "You can test whether an edges has been erased with `is_dead_edge()`:" + ] + }, + { + "cell_type": "code", + "execution_count": 14, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "True" + ] + }, + "execution_count": 14, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut.is_dead_edge(2)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "However you usually do not have to care, because iterator methods will skip such dead edges. For instance:" + ] + }, + { + "cell_type": "code", + "execution_count": 15, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "edges[3].src=0, edges[3].dst=1\n", + "edges[4].src=1, edges[4].dst=0\n", + "edges[5].src=1, edges[5].dst=0\n", + "edges[6].src=1, edges[6].dst=1\n", + "edges[7].src=1, edges[7].dst=1\n", + "edges[8].src=2, edges[8].dst=0\n", + "edges[9].src=1, edges[9].dst=1\n" + ] + } + ], + "source": [ + "for e in aut.edges(): # iterate over all non-erased edges\n", + " print(\"edges[{e}].src={src}, edges[{e}].dst={dst}\".format(e=aut.edge_number(e), src=e.src, dst=e.dst))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Similarly, `num_edges()` returns the count of non-erased edges." + ] + }, + { + "cell_type": "code", + "execution_count": 16, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "7" + ] + }, + "execution_count": 16, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut.num_edges()" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Erased edges are actually removed by `merge_edges()`:" + ] + }, + { + "cell_type": "code", + "execution_count": 17, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "6\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "cond\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "dst\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "next_succ\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 17, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut.merge_edges()\n", + "aut.show_storage(\"v\")" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Another way to erase an edge, is to set its `cond` field to `bddfalse`. Strictly speaking, this does not really erase the edge, and it will still be iterated upon. However a subsequent call to `merge_edges()` will perform the removal of that edge." + ] + }, + { + "cell_type": "code", + "execution_count": 18, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "6\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "cond\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "0\n", + "\n", + "!a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "dst\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "next_succ\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 18, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut.edge_storage(3).cond = buddy.bddfalse\n", + "aut.show_storage(\"v\")" + ] + }, + { + "cell_type": "code", + "execution_count": 19, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "edges[1].src=0, edges[1].dst=1\n", + "edges[2].src=1, edges[2].dst=0\n", + "edges[3].src=1, edges[3].dst=0\n", + "edges[4].src=1, edges[4].dst=1\n", + "edges[5].src=1, edges[5].dst=1\n", + "edges[6].src=2, edges[6].dst=0\n" + ] + } + ], + "source": [ + "for e in aut.edges(): # iterate over all non-erased edges\n", + " print(\"edges[{e}].src={src}, edges[{e}].dst={dst}\".format(e=aut.edge_number(e), src=e.src, dst=e.dst))" + ] + }, + { + "cell_type": "code", + "execution_count": 20, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "False" + ] + }, + "execution_count": 20, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut.is_dead_edge(3)" + ] + }, + { + "cell_type": "code", + "execution_count": 21, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "5\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "cond\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "!a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "dst\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "next_succ\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 21, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut.merge_edges()\n", + "aut.show_storage(\"v\")" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Alternation\n", + "\n", + "The data structures seen so far only support a single destination per edge. Support for universal branching therefore calls for something new.\n", + "\n", + "Let's add some universal branching in our example automaton." + ] + }, + { + "cell_type": "code", + "execution_count": 22, + "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", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "I->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "0->-1\n", + "\n", + "\n", + "a\n", + "❶\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "❶\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "-1->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4\n", + "\n", + "\n", + "\n", + "\n", + "3->-4\n", + "\n", + "\n", + "!a\n", + "⓿\n", + "\n", + "\n", + "\n", + "-4->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4->1\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f616c1788a0> >" + ] + }, + "execution_count": 22, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "a = buddy.bdd_ithvar(aut.register_ap('a'))\n", + "s = aut.new_state()\n", + "aut.new_univ_edge(0, [0, s], a, [1])\n", + "aut.new_univ_edge(s, [0, 1], -a, [0])\n", + "aut" + ] + }, + { + "cell_type": "code", + "execution_count": 23, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "7\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "cond\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "!a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "a\n", + "\n", + "!a\n", + "\n", + "acc\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", + "\n", + "dst\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "~3\n", + "\n", + "next_succ\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "dests\n", + "\n", + "\n", + "dests\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "\n", + "\n", + "~3\n", + "\n", + "\n", + "\n", + "#cnt/dst\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "meta\n", + "init_state:\n", + "\n", + "2\n", + "num_sets:\n", + "2\n", + "acceptance:\n", + "Fin(0) & Inf(1)\n", + "ap_vars:\n", + "b a\n", + "\n", + "\n", + "\n", + "\n", + "props\n", + "prop_state_acc:\n", + "maybe\n", + "prop_inherently_weak:\n", + "maybe\n", + "prop_terminal:\n", + "maybe\n", + "prop_weak:\n", + "maybe\n", + "prop_very_weak:\n", + "maybe\n", + "prop_complete:\n", + "maybe\n", + "prop_universal:\n", + "maybe\n", + "prop_unambiguous:\n", + "maybe\n", + "prop_semi_deterministic:\n", + "maybe\n", + "prop_stutter_invariant:\n", + "maybe\n", + "\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 23, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut.show_storage()" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Here we have created two universal transitions: `0->[0,2]` and `2->[0,1]`. The destination groups `[0,2]` and `[0,1]` are stored in a integer vector called `dests`. Each group is encoded by its size immediately followed by the state numbers of the destinations. So group `[0,2]` get encoded as `2,0,2` at position `0` of `dests`, and group `[0,1]` is encoded as `2,0,1` at position `3`. Each group is denoted by the index of its size in the `dests` vector. When an edge targets a destination group, the complement of that destination index is written in the `dst` field of the `edges` entry, hence that `~0` and `~3` that appear here. Using a complement like this allows us to quickly detect universal edges by looking at the sign bit if their `dst` entry.\n", + "\n", + "To work on alternating automata, one can no longuer just blindingly use the `dst` field of outgoing iterations:" + ] + }, + { + "cell_type": "code", + "execution_count": 24, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "1\n", + "0\n", + "1\n", + "1\n", + "0\n", + "4294967295\n", + "4294967292\n" + ] + } + ], + "source": [ + "for e in aut.edges():\n", + " print(e.dst)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Using such a large `e.dst` value as an index in `states` would likely crash the program. Instead we should iterate over all the successor of an edge using the `univ_dests()` method. Note that `univ_dests()` can be applied to regular edges as well." + ] + }, + { + "cell_type": "code", + "execution_count": 25, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[1]\n", + "[0]\n", + "[1]\n", + "[1]\n", + "[0]\n", + "[0, 3]\n", + "[0, 1]\n" + ] + } + ], + "source": [ + "for e in aut.edges():\n", + " print([d for d in aut.univ_dests(e.dst)])" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Note that `univ_dests()` can be applied to `e.dst` or `e`." + ] + }, + { + "cell_type": "code", + "execution_count": 26, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[1]\n", + "[0]\n", + "[1]\n", + "[1]\n", + "[0]\n", + "[0, 3]\n", + "[0, 1]\n" + ] + } + ], + "source": [ + "for e in aut.edges():\n", + " print([d for d in aut.univ_dests(e)])" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Note that the initial state get also use universal branching:" + ] + }, + { + "cell_type": "code", + "execution_count": 27, + "metadata": {}, + "outputs": [], + "source": [ + "aut.set_univ_init_state([0, 1, 2])" + ] + }, + { + "cell_type": "code", + "execution_count": 28, + "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", + "-7\n", + "\n", + "\n", + "\n", + "\n", + "I->-7\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "-7->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "-7->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "-7->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "0->-1\n", + "\n", + "\n", + "a\n", + "❶\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "❶\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "-1->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4\n", + "\n", + "\n", + "\n", + "\n", + "3->-4\n", + "\n", + "\n", + "!a\n", + "⓿\n", + "\n", + "\n", + "\n", + "-4->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4->1\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f616c1788a0> >" + ] + }, + "execution_count": 28, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut" + ] + }, + { + "cell_type": "code", + "execution_count": 29, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[0, 1, 2]\n" + ] + } + ], + "source": [ + "print([d for d in aut.univ_dests(aut.get_init_state_number())])" + ] + }, + { + "cell_type": "code", + "execution_count": 30, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "7\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "cond\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "!a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "a\n", + "\n", + "!a\n", + "\n", + "acc\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", + "\n", + "dst\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "~3\n", + "\n", + "next_succ\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "dests\n", + "\n", + "\n", + "dests\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "\n", + "\n", + "~3\n", + "\n", + "\n", + "\n", + "\n", + "~6\n", + "\n", + "\n", + "\n", + "\n", + "#cnt/dst\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "#3\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "meta\n", + "init_state:\n", + "\n", + "~6\n", + "num_sets:\n", + "2\n", + "acceptance:\n", + "Fin(0) & Inf(1)\n", + "ap_vars:\n", + "b a\n", + "\n", + "\n", + "\n", + "\n", + "props\n", + "prop_state_acc:\n", + "maybe\n", + "prop_inherently_weak:\n", + "maybe\n", + "prop_terminal:\n", + "maybe\n", + "prop_weak:\n", + "maybe\n", + "prop_very_weak:\n", + "maybe\n", + "prop_complete:\n", + "maybe\n", + "prop_universal:\n", + "maybe\n", + "prop_unambiguous:\n", + "maybe\n", + "prop_semi_deterministic:\n", + "maybe\n", + "prop_stutter_invariant:\n", + "maybe\n", + "\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 30, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut.show_storage()" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Adding several transitions with the same destination groups may result in duplicates in the `dests` vector. Those groups get merged during `merge_edges()`." + ] + }, + { + "cell_type": "code", + "execution_count": 31, + "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", + "-7\n", + "\n", + "\n", + "\n", + "\n", + "I->-7\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "-7->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "-7->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "-7->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "0->-1\n", + "\n", + "\n", + "a\n", + "❶\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "❶\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "-1->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4\n", + "\n", + "\n", + "\n", + "\n", + "3->-4\n", + "\n", + "\n", + "!a\n", + "⓿\n", + "\n", + "\n", + "\n", + "-11\n", + "\n", + "\n", + "\n", + "\n", + "3->-11\n", + "\n", + "\n", + "1\n", + "⓿\n", + "\n", + "\n", + "\n", + "-4->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-11->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-11->3\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f616c1788a0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "7\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "cond\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "!a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "a\n", + "\n", + "!a\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "dst\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "~3\n", + "\n", + "\n", + "~10\n", + "\n", + "next_succ\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "8\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "dests\n", + "\n", + "\n", + "dests\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "\n", + "\n", + "~3\n", + "\n", + "\n", + "\n", + "\n", + "~6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "~10\n", + "\n", + "\n", + "\n", + "#cnt/dst\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "#3\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "meta\n", + "init_state:\n", + "\n", + "~6\n", + "num_sets:\n", + "2\n", + "acceptance:\n", + "Fin(0) & Inf(1)\n", + "ap_vars:\n", + "b a\n", + "\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "⓿\n", + ") & Inf(\n", + "❶\n", + ")\n", + "[Rabin 1]\n", + "\n", + "\n", + "\n", + "-7\n", + "\n", + "\n", + "\n", + "\n", + "I->-7\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "-7->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "-7->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "-7->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "\n", + "\n", + "\n", + "-1\n", + "\n", + "\n", + "\n", + "\n", + "0->-1\n", + "\n", + "\n", + "a\n", + "❶\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "❶\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "⓿\n", + "❶\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "-1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "-1->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->-1\n", + "\n", + "\n", + "1\n", + "⓿\n", + "\n", + "\n", + "\n", + "-4\n", + "\n", + "\n", + "\n", + "\n", + "3->-4\n", + "\n", + "\n", + "!a\n", + "⓿\n", + "\n", + "\n", + "\n", + "-4->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "-4->1\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f616c1788a0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "cond\n", + "\n", + "!a & !b\n", + "\n", + "a\n", + "\n", + "a & b\n", + "\n", + "!a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "!a\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "dst\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "~3\n", + "\n", + "\n", + "~0\n", + "\n", + "next_succ\n", + "\n", + "\n", + "2\n", + "\n", + "0\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "8\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "dests\n", + "\n", + "\n", + "dests\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "\n", + "\n", + "~3\n", + "\n", + "\n", + "\n", + "\n", + "~6\n", + "\n", + "\n", + "\n", + "\n", + "#cnt/dst\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "#3\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "meta\n", + "init_state:\n", + "\n", + "~6\n", + "num_sets:\n", + "2\n", + "acceptance:\n", + "Fin(0) & Inf(1)\n", + "ap_vars:\n", + "b a\n", + "\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "aut.new_univ_edge(3, [0,3], buddy.bddtrue, [0])\n", + "display(aut, aut.show_storage(\"vd\"))\n", + "aut.merge_edges()\n", + "display(aut, aut.show_storage(\"vd\"))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Above group `~0` and `~10` have been merged." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Named properties\n", + "\n", + "Finally automata can also been attached [arbitrarily named properties](https://spot.lrde.epita.fr/concepts.html#named-properties). The `show_storage()` method will only display the name of these properties, not their contents. Properties like `automaton-name` are used to store a name for the automaton, `product-states` is filled by `product()` and holds a vector of pairs representing the source states in the product's operands, etc." + ] + }, + { + "cell_type": "code", + "execution_count": 32, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "aub * gfa\n", + "\n", + "aub * gfa\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "⓿\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f616c0b3bd0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "cond\n", + "\n", + "!a & b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a\n", + "\n", + "a\n", + "\n", + "acc\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "dst\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "next_succ\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "0\n", + "\n", + "\n", + "5\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "meta\n", + "init_state:\n", + "\n", + "0\n", + "num_sets:\n", + "1\n", + "acceptance:\n", + "Inf(0)\n", + "ap_vars:\n", + "b a\n", + "\n", + "\n", + "\n", + "\n", + "props\n", + "prop_state_acc:\n", + "maybe\n", + "prop_inherently_weak:\n", + "maybe\n", + "prop_terminal:\n", + "maybe\n", + "prop_weak:\n", + "maybe\n", + "prop_very_weak:\n", + "maybe\n", + "prop_complete:\n", + "maybe\n", + "prop_universal:\n", + "yes\n", + "prop_unambiguous:\n", + "yes\n", + "prop_semi_deterministic:\n", + "yes\n", + "prop_stutter_invariant:\n", + "yes\n", + "\n", + "\n", + "\n", + "\n", + "namedprops\n", + "named properties:\n", + "automaton-name\n", + "product-states\n", + "\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "aub = spot.translate('a U b')\n", + "gfa = spot.translate('GFa')\n", + "prod = spot.product(aub, gfa)\n", + "prod.set_name(\"aub * gfa\")\n", + "display(prod, prod.show_storage())" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "This properties also need to be updated by algorithms. They can be reset with:" + ] + }, + { + "cell_type": "code", + "execution_count": 33, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\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", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "⓿\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f616c0b3bd0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "g\n", + "\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "cond\n", + "\n", + "!a & b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a\n", + "\n", + "a\n", + "\n", + "acc\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "dst\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "next_succ\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "0\n", + "\n", + "\n", + "5\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "meta\n", + "init_state:\n", + "\n", + "0\n", + "num_sets:\n", + "1\n", + "acceptance:\n", + "Inf(0)\n", + "ap_vars:\n", + "b a\n", + "\n", + "\n", + "\n", + "\n", + "props\n", + "prop_state_acc:\n", + "maybe\n", + "prop_inherently_weak:\n", + "maybe\n", + "prop_terminal:\n", + "maybe\n", + "prop_weak:\n", + "maybe\n", + "prop_very_weak:\n", + "maybe\n", + "prop_complete:\n", + "maybe\n", + "prop_universal:\n", + "yes\n", + "prop_unambiguous:\n", + "yes\n", + "prop_semi_deterministic:\n", + "yes\n", + "prop_stutter_invariant:\n", + "yes\n", + "\n", + "\n", + "\n", + "" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "prod.release_named_properties()\n", + "display(prod, prod.show_storage())" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "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.6.6" + } + }, + "nbformat": 4, + "nbformat_minor": 2 +}