diff --git a/NEWS b/NEWS index b6341365412dfb5e8d5fb0187117f7268399843a..c48bbd88734105ccd33087904fc0609d5f8918c0 100644 --- a/NEWS +++ b/NEWS @@ -64,15 +64,25 @@ New in spot 1.99.6a (not yet released) when calling for instance the Python version of twa_graph::new_edge(). See https://spot.lrde.epita.fr/tut22.html for a demonstration. + * Automaton states can be named via the set_state_names() method. + See https://spot.lrde.epita.fr/ipynb/product.html for an example. + Documentation: * There is a new page explaining how to compile example programs and and link them with Spot. https://spot.lrde.epita.fr/compile.html + * Python bindings for manipulating acceptance conditions are + demonstrated by https://spot.lrde.epita.fr/ipynb/acc_cond.html, + and a Python implementation of the product of two automata is + illustrated by https://spot.lrde.epita.fr/ipynb/product.html + Bug fixes: * twa::ap() would contain duplicates when an atomic proposition was registered several times. + * product() would incorrectly mark the product of two + sttuter-sensitive automata as stutter-sensitive as well. New in spot 1.99.6 (2015-12-04) diff --git a/doc/org/hoa.org b/doc/org/hoa.org index cd01deebdc3c1a3b4db3d9df5a3bbdd5773535ff..95e2c5005006e5e188e493547969ce71240ed8d5 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -584,6 +584,9 @@ labels whenever that is possible. The option is named =k= (i.e., use is used to describe a Kripke structure. ** Property bits + :PROPERTIES: + :CUSTOM_ID: property-bits + :END: The =HOA= format supports a number of optional =property:= tokens. These properties can be useful to speedup certain algorithms: for diff --git a/doc/org/tut.org b/doc/org/tut.org index 73db395fe0103534432477f159ca31c87118da66..241e816c283bb9193636b20b8d7ca1493faf1794 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -52,6 +52,8 @@ real notebooks instead. - [[https://spot.lrde.epita.fr/ipynb/accparse.html][accparse.ipynb]] exercises the acceptance condition parser - [[https://spot.lrde.epita.fr/ipynb/acc_cond.html][acc_cond.ipynb]] documents the interface for manipulating acceptance conditions +- [[https://spot.lrde.epita.fr/ipynb/product.html][product.ipynb]] shows how to re-implement the product of two automata + in Python - [[https://spot.lrde.epita.fr/ipynb/randltl.html][randltl.ipynb]] demonstrates a Python-version of [[file:randltl.org][=randltl=]] - [[https://spot.lrde.epita.fr/ipynb/decompose.html][decompose.ipynb]] illustrates the =decompose_strength()= function - [[https://spot.lrde.epita.fr/ipynb/testingaut.html][testingaut.ipynb]] shows the step necessary to build a testing diff --git a/spot/twaalgos/product.cc b/spot/twaalgos/product.cc index b0a37bc4679164fa5e6dd5a86e3fac8a3fa62fd3..7be9f588bbe4554e652c8a45da4ea55eb7e731b6 100644 --- a/spot/twaalgos/product.cc +++ b/spot/twaalgos/product.cc @@ -105,10 +105,18 @@ namespace spot && right->prop_deterministic()); res->prop_stutter_invariant(left->prop_stutter_invariant() && right->prop_stutter_invariant()); - res->prop_stutter_sensitive(left->prop_stutter_sensitive() - && right->prop_stutter_sensitive()); + // The product of X!a and Xa, two stutter-sentive formulas, + // is stutter-invariant. + //res->prop_stutter_sensitive(left->prop_stutter_sensitive() + // && right->prop_stutter_sensitive()); + res->prop_inherently_weak(left->prop_inherently_weak() + && right->prop_inherently_weak()); + res->prop_weak(left->prop_weak() + && right->prop_weak()); + res->prop_terminal(left->prop_terminal() + && right->prop_terminal()); res->prop_state_acc(left->prop_state_acc() - && right->prop_state_acc()); + && right->prop_state_acc()); return res; } } diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index a7fbe43c51cab6f9948c6da534ee9e2d83d41158..9d2e0107f90ca6ebcc080705a776ea1170ff7a6b 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -339,6 +339,7 @@ namespace std { %template(liststr) list; %template(vectorformula) vector; %template(vectorunsigned) vector; + %template(vectorstring) vector; %template(atomic_prop_set) set; %template(relabeling_map) map; } @@ -465,6 +466,18 @@ namespace std { std::string __str__() { return spot::str_psl(*self); } } +%extend spot::bdd_dict { + bool operator==(const spot::bdd_dict& b) const + { + return self == &b; + } + + bool operator!=(const spot::bdd_dict& b) const + { + return self != &b; + } +} + %extend spot::twa { void set_name(std::string name) { @@ -475,6 +488,17 @@ namespace std { { return self->get_named_prop("automaton-name"); } + + void set_state_names(std::vector names) + { + self->set_named_prop("state-names", + new std::vector(std::move(names))); + } + + std::vector* get_state_names() + { + return self->get_named_prop>("state-names"); + } } diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am index 1c3c45d8c03d69e97e59b35d9225eec8e96ca59d..327c2f2b5f9344e771105c8f95710fa7baeec419 100644 --- a/wrap/python/tests/Makefile.am +++ b/wrap/python/tests/Makefile.am @@ -49,6 +49,7 @@ TESTS = \ optionmap.py \ parsetgba.py \ piperead.ipynb \ + product.ipynb \ randaut.ipynb \ randgen.py \ randltl.ipynb \ diff --git a/wrap/python/tests/ipnbdoctest.py b/wrap/python/tests/ipnbdoctest.py index d4e828d909f296e1b50b47824e5565b0b0c226c4..2f65785fa7bf7f51f0b8dadbd7e8168363bc1b80 100755 --- a/wrap/python/tests/ipnbdoctest.py +++ b/wrap/python/tests/ipnbdoctest.py @@ -70,6 +70,9 @@ def sanitize(s): # normalize graphviz version s = re.sub(r'Generated by graphviz version.*', 'VERSION', s) + # ignore %timeit results + s = re.sub(r'^[0-9]+ loops, best of 3:.*per loop', '', s) + # SVG generated by graphviz may put note at different positions # depending on the graphviz build. Let's just strip anything that # look like a position. diff --git a/wrap/python/tests/product.ipynb b/wrap/python/tests/product.ipynb new file mode 100644 index 0000000000000000000000000000000000000000..31cdb4550463aa4ef6a596928105454301730cfc --- /dev/null +++ b/wrap/python/tests/product.ipynb @@ -0,0 +1,2001 @@ +{ + "metadata": { + "name": "", + "signature": "sha256:50d5adbd44f5981c700cec9133b926c8edb75b3ff80a4cf28e7c26cf918fe04a" + }, + "nbformat": 3, + "nbformat_minor": 0, + "worksheets": [ + { + "cells": [ + { + "cell_type": "code", + "collapsed": false, + "input": [ + "from IPython.display import display, HTML\n", + "import spot\n", + "import buddy\n", + "spot.setup(show_default='.tavb')\n", + "\n", + "def horiz(*args):\n", + " s = ''\n", + " for arg in args:\n", + " s += ''\n", + " return HTML(s + '
' + arg.data + '
')" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 1 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Anatomy of a product\n", + "\n", + "In this notebook, we write a Python function that constructs the product of two automata.\n", + "\n", + "This is obviously not a new feature: Spot can already make a product of two automata using its `product()` function. \n", + "For instance:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "a1 = spot.translate('X(a W b)')\n", + "a2 = spot.translate('G(Fc U b)')\n", + "prod = spot.product(a1, a2)\n", + "horiz(a1.show(), a2.show(), prod.show())" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "html": [ + "
\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2776\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\u24ff\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\u24ff\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\u2776\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2776\n", + ")&Inf(\n", + "\u2777\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & c\n", + "\u2776\n", + "\n", + "\n", + "2\n", + "\n", + "0,1\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\u24ff\n", + "\n", + "\n", + "3\n", + "\n", + "2,0\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & c\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\u24ff\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "b & c\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "4\n", + "\n", + "2,1\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "b & !c\n", + "\u24ff\n", + "\u2777\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b & c\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!b & !c\n", + "\u24ff\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "b & c\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!b & c\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b & !c\n", + "\u24ff\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "b & !c\n", + "\u24ff\n", + "\u2777\n", + "\n", + "\n", + "
" + ], + "metadata": {}, + "output_type": "pyout", + "prompt_number": 2, + "text": [ + "" + ] + } + ], + "prompt_number": 2 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The builtin `spot.product()` function produces an automaton whose language is the intersection of the two input languages. It does so by building an automaton that keeps track of the runs in the two input automata. The states are labeled by pairs of input states so that we can more easily follow what is going on, but those labels are purely cosmetic. The acceptance condition is the conjunction of the two acceptance condition, but the acceptance sets of one input automaton have been shifted to not conflict with the other automaton.\n", + "\n", + "In fact, that automaton printer has an option to shift those sets in its output, and this is perfect for illustrating products. For instance `a.show('+3')` will display `a1` with all its acceptance sets shifted by 3. \n", + "\n", + "Let's define a function for displaying the three automata involved in a product, using this shift option so we can follow what is going on with the acceptance sets." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "def show_prod(a1, a2, res):\n", + " s1 = a1.num_sets()\n", + " display(horiz(a1.show(), a2.show('.tavb+{}'.format(s1)), res.show()))\n", + "\n", + "show_prod(a1, a2, prod)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "html": [ + "
\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u2776\n", + ")&Inf(\n", + "\u2777\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\u2776\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\u2776\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\u2777\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2776\n", + ")&Inf(\n", + "\u2777\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & c\n", + "\u2776\n", + "\n", + "\n", + "2\n", + "\n", + "0,1\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\u24ff\n", + "\n", + "\n", + "3\n", + "\n", + "2,0\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & c\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\u24ff\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "b & c\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "4\n", + "\n", + "2,1\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "b & !c\n", + "\u24ff\n", + "\u2777\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b & c\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!b & !c\n", + "\u24ff\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "b & c\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!b & c\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b & !c\n", + "\u24ff\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "b & !c\n", + "\u24ff\n", + "\u2777\n", + "\n", + "\n", + "
" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "" + ] + } + ], + "prompt_number": 3 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Building a product\n", + "\n", + "Let's now rewrite `product()` in Python. We will do that in three steps.\n", + "\n", + "\n", + "## First attempt\n", + "\n", + "First, we build a product without taking care of the acceptance sets. We just want to get the general shape of the algorithm.\n", + "\n", + "We will build an automaton of type `twa_graph`, i.e., an automaton represented explicitely using a graph. In those automata, states are numbered by integers, starting from `0`. (Those states can also be given a different name, which is why the the `product()` shows us something that appears to be labeled by pairs, but the real identifier of each state is an integer.)\n", + "\n", + "We will use a dictionnary to keep track of the association between a pair `(ls,rs)` of input states, and its number in the output." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "def product1(left, right):\n", + " # A bdd_dict object associates BDD variables (that are \n", + " # used in BDDs labeleing the edges) to atomic propositions.\n", + " bdict = left.get_dict()\n", + " # If the two automata do not have the same BDD dict, then\n", + " # we cannot easily detect compatible transitions.\n", + " if right.get_dict() != bdict:\n", + " raise RuntimeError(\"automata should share their dictionary\")\n", + " \n", + " result = spot.make_twa_graph(bdict)\n", + " # This will be our state dictionary\n", + " sdict = {}\n", + " # The list of output states for which we have not yet\n", + " # computed the successors. Items on this list are triplets\n", + " # of the form (ls, rs, p) where ls,rs are the state number in\n", + " # the left and right automata, and p is the state number if\n", + " # the output automaton.\n", + " todo = []\n", + " # Transform a pair of state number (ls, rs) into a state number in\n", + " # the output automaton, creating a new state if needed. Whenever\n", + " # a new state is created, we can add it to todo.\n", + " def dst(ls, rs):\n", + " pair = (ls, rs)\n", + " p = sdict.get(pair)\n", + " if p is None:\n", + " p = result.new_state()\n", + " sdict[pair] = p\n", + " todo.append((ls, rs, p))\n", + " return p\n", + " \n", + " # Setup the initial state. It always exists.\n", + " result.set_init_state(dst(left.get_init_state_number(), \n", + " right.get_init_state_number()))\n", + "\n", + " # Build all states and edges in the product\n", + " while todo:\n", + " lsrc, rsrc, osrc = todo.pop()\n", + " for lt in left.out(lsrc):\n", + " for rt in right.out(rsrc):\n", + " cond = lt.cond & rt.cond\n", + " if cond != buddy.bddfalse:\n", + " result.new_edge(osrc, dst(lt.dst, rt.dst), cond)\n", + " return result\n", + "\n", + "p1 = product1(a1, a2)\n", + "show_prod(a1, a2, p1)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "html": [ + "
\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u2776\n", + ")&Inf(\n", + "\u2777\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\u2776\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\u2776\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\u2777\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "t\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & c\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "b & c\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!b & c\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "b & !c\n", + "\n", + "\n", + "
" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "" + ] + } + ], + "prompt_number": 4 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Besides the obvious lack of acceptance condition (which defaults to `t`) and acceptance sets, there is a less obvious problem: we never declared the set of atomic proposition used by the result automaton. This as two consequences:\n", + "- calling `p1.ap()` will return an empty set of atomic propositions" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "print(a1.ap())\n", + "print(a2.ap())\n", + "print(p1.ap())" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "(a, b)\n", + "(c, b)\n", + "()\n" + ] + } + ], + "prompt_number": 5 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "- the `bdd_dict` instance that is shared by the three automata knows that the atomic propositions `a` and `b` are used by automata `a1` and that `b` and `c` are used by `a2`. But it is unaware of `p1`. That means that if we delete automata `a1` and `a2`, then the `bdd_dict` will release the associated BDD variables, and attempting to print automaton `p1` will either crash (because it uses bdd variables that are not associated to any atomic proposition) or display different atomic propositions (in case the BDD variables have been associated to different propositions in the meantime).\n", + "\n", + "These two issues are fixed by either calling `p1.register_ap(...)` for each atomic proposition, or in our case `p1.copy_ap_of(...)` to copy the atomic propositions of each input automaton. " + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Second attempt: a working product\n", + "\n", + "This fixes the list of atomtic propositions, as discussed above, and also sets the correct acceptance condition.\n", + "The `set_acceptance` method takes two arguments: a number of sets, and an acceptance function. In our case, both of these arguments are readily computed from the number of states and acceptance functions of the input automata." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "def product2(left, right):\n", + " bdict = left.get_dict()\n", + " if right.get_dict() != bdict:\n", + " raise RuntimeError(\"automata should share their dictionary\")\n", + " \n", + " result = spot.make_twa_graph(bdict)\n", + " # Copy the atomic propositions of the two input automata\n", + " result.copy_ap_of(left)\n", + " result.copy_ap_of(right)\n", + " \n", + " sdict = {}\n", + " todo = []\n", + " def dst(ls, rs):\n", + " pair = (ls, rs)\n", + " p = sdict.get(pair)\n", + " if p is None:\n", + " p = result.new_state()\n", + " sdict[pair] = p\n", + " todo.append((ls, rs, p))\n", + " return p\n", + " \n", + " result.set_init_state(dst(left.get_init_state_number(), \n", + " right.get_init_state_number()))\n", + "\n", + " # The acceptance sets of the right automaton will be shifted by this amount\n", + " shift = left.num_sets()\n", + " result.set_acceptance(shift + right.num_sets(),\n", + " left.get_acceptance() & (right.get_acceptance() << shift))\n", + " \n", + " while todo:\n", + " lsrc, rsrc, osrc = todo.pop()\n", + " for lt in left.out(lsrc):\n", + " for rt in right.out(rsrc):\n", + " cond = lt.cond & rt.cond\n", + " if cond != buddy.bddfalse:\n", + " # membership of this transitions to the new acceptance sets\n", + " acc = lt.acc | (rt.acc << shift)\n", + " result.new_edge(osrc, dst(lt.dst, rt.dst), cond, acc)\n", + " return result\n", + "\n", + "p2 = product2(a1, a2)\n", + "show_prod(a1, a2, p2)\n", + "print(p2.ap())" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "html": [ + "
\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u2776\n", + ")&Inf(\n", + "\u2777\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\u2776\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\u2776\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\u2777\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2776\n", + ")&Inf(\n", + "\u2777\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & c\n", + "\u2776\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\u24ff\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & c\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\u24ff\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "b & c\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "b & !c\n", + "\u24ff\n", + "\u2777\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b & c\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!b & !c\n", + "\u24ff\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "b & c\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!b & c\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b & !c\n", + "\u24ff\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "b & !c\n", + "\u24ff\n", + "\u2777\n", + "\n", + "\n", + "
" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "" + ] + }, + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "(a, b, c)\n" + ] + } + ], + "prompt_number": 6 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Third attempt: a more usable product\n", + "\n", + "We could stop with the previous function: the result is a correct product from a theoretical point of view. However our function is still inferior to `spot.product()` in a couple of points:\n", + "- states are not presented as pairs\n", + "- the properties of the resulting automaton are not sets\n", + "\n", + "The former point can be addressed by calling `set_state_names()` and passing an array of strings: if a state number is smaller than the size of that array, then the string at that position will be displayed instead of the state number in the dot output. \n", + "\n", + "(Note: the original `spot.product()` is in fact *not* naming states. The `spot.product()` function actually attaches a vector of pairs of integers to the automaton because some algorithms need to project a state of the product onto the original automaton. The `dot` printer knows how to display those pairs for states that are not named. Here we shall name states because (1) that is more flexible, and (2) there is a Python interface for this.)\n", + "\n", + "Regarding the latter point, consider for instance the deterministic nature of these automata:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "print(a1.prop_deterministic())\n", + "print(a2.prop_deterministic())\n", + "print(prod.prop_deterministic())\n", + "print(p1.prop_deterministic())" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "True\n", + "True\n", + "True\n", + "False\n" + ] + } + ], + "prompt_number": 7 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Because `a1` and `a2` are deterministic, their product is necessarily deterministic. This is a property that the `spot.product()` algorithm will preserve, but that our version does not yet preserve. We can fix that by adding\n", + "\n", + " result.prop_deterministic(left.prop_deterministic() and right.prop_deterministic())\n", + " \n", + "at the end of our function. However the question is in fact more general than just determinism: the product of two weak automata is weak, the product of two stutter-invariant automata is stutter-invariant, etc. So when writing an algorithm one should consider which of the [property bits](https://spot.lrde.epita.fr/hoa.html#property-bits) are naturally preserved by the algorithm, and set the relevant bits: this can save time later if the resulting automaton is used as input for another algorithm." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "def product3(left, right):\n", + " bdict = left.get_dict()\n", + " if right.get_dict() != bdict:\n", + " raise RuntimeError(\"automata should share their dictionary\")\n", + " \n", + " result = spot.make_twa_graph(bdict)\n", + " result.copy_ap_of(left)\n", + " result.copy_ap_of(right)\n", + " \n", + " names = [] # our array of state names\n", + " sdict = {}\n", + " todo = []\n", + " def dst(ls, rs):\n", + " pair = (ls, rs)\n", + " p = sdict.get(pair)\n", + " if p is None:\n", + " p = result.new_state()\n", + " sdict[pair] = p\n", + " todo.append((ls, rs, p))\n", + " names.append(\"{},{}\".format(ls, rs)) # name each state\n", + " return p\n", + " \n", + " result.set_init_state(dst(left.get_init_state_number(), \n", + " right.get_init_state_number()))\n", + "\n", + " shift = left.num_sets()\n", + " result.set_acceptance(shift + right.num_sets(),\n", + " left.get_acceptance() & (right.get_acceptance() << shift))\n", + " \n", + " while todo:\n", + " lsrc, rsrc, osrc = todo.pop()\n", + " for lt in left.out(lsrc):\n", + " for rt in right.out(rsrc):\n", + " cond = lt.cond & rt.cond\n", + " if cond != buddy.bddfalse:\n", + " acc = lt.acc | (rt.acc << shift)\n", + " result.new_edge(osrc, dst(lt.dst, rt.dst), cond, acc)\n", + "\n", + " # Remember the names of our states\n", + " result.set_state_names(names)\n", + " \n", + " # Loop over all the properties we want to preserve if they are in both automata\n", + " for p in ('prop_deterministic', 'prop_weak', 'prop_inherently_weak', \n", + " 'prop_terminal', 'prop_stutter_invariant', 'prop_state_acc'):\n", + " getattr(result, p)(getattr(left, p)() and getattr(right, p)())\n", + " return result\n", + "\n", + "p3 = product3(a1, a2)\n", + "show_prod(a1, a2, p3)\n", + "print(p3.prop_deterministic())" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "html": [ + "
\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u2776\n", + ")&Inf(\n", + "\u2777\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!b & c\n", + "\u2776\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b & c\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!b & c\n", + "\u2776\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b & !c\n", + "\u2777\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2776\n", + ")&Inf(\n", + "\u2777\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "1,0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "0,0\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!b & c\n", + "\u2776\n", + "\n", + "\n", + "2\n", + "\n", + "0,1\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!b & !c\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b & c\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\u24ff\n", + "\n", + "\n", + "3\n", + "\n", + "2,0\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b & c\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & !b & !c\n", + "\u24ff\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "b & c\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "4\n", + "\n", + "2,1\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "b & !c\n", + "\u24ff\n", + "\u2777\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!b & c\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!b & !c\n", + "\u24ff\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "b & c\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "!b & c\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "!b & !c\n", + "\u24ff\n", + "\n", + "\n", + "4->4\n", + "\n", + "\n", + "b & !c\n", + "\u24ff\n", + "\u2777\n", + "\n", + "\n", + "
" + ], + "metadata": {}, + "output_type": "display_data", + "text": [ + "" + ] + }, + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "True\n" + ] + } + ], + "prompt_number": 8 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Timings\n", + "\n", + "As an indication of how slow it is to implement such an algorithm using the Python bindings of Spot, consider the following comparison:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "%timeit product3(a1, a2)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "1000 loops, best of 3: 353 \u00b5s per loop\n" + ] + } + ], + "prompt_number": 9 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "%timeit spot.product(a1, a2)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "100000 loops, best of 3: 6.39 \u00b5s per loop\n" + ] + } + ], + "prompt_number": 10 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Depending on the machine where this notebook has been run, using the C++ version of the product can be 1 to 2 order of magnitude faster. This is due to all the type conversions (converting Python types to C++ types) that occurs everytime a function/method of Spot is called from Python. When calling high-level C++ functions (such as `spot.product()`) from Python, the overhead is negligible because most of the time is spent on the C++ side, actually executing the function. However when calling low-level functions (such as `new_edge()`, `new_state()`, `out()`) most of the time is spent converting the arguments from Python to C++ and the results from C++ to Python.\n", + "\n", + "Despite that speed difference, Python can be useful to prototype an algorithm before implementing it in C++." + ] + } + ], + "metadata": {} + } + ] +} \ No newline at end of file