From 19348c893819563d0598bc28b82a7d81bf5a1a1e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 22 Dec 2017 17:23:56 +0100 Subject: [PATCH] python: give access to the "product-states" property * python/spot/impl.i (get_product_states, set_product_states): New. * tests/python/product.ipynb: Use it. * NEWS: Mention it. --- NEWS | 5 + python/spot/impl.i | 30 +++++ tests/python/product.ipynb | 237 +++++++++++++++++++++++++++++++++++-- 3 files changed, 259 insertions(+), 13 deletions(-) diff --git a/NEWS b/NEWS index b06f5f224..18998208e 100644 --- a/NEWS +++ b/NEWS @@ -212,6 +212,11 @@ New in spot 2.4.3.dev (not yet released) - The new function spot::check_determinism() sets both prop_semi_deterministic() and prop_universal() appropriately. + Python: + + - The "product-states" property of automata is now accessible via + spot.twa.get_product_states() and spot.set.get_product_states(). + Deprecation notices: (These functions still work but compilers emit warnings.) diff --git a/python/spot/impl.i b/python/spot/impl.i index 76df4800d..2bd09ef03 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -428,8 +428,10 @@ namespace swig namespace std { %template(liststr) list; + %template(pairunsigned) pair; %template(vectorformula) vector; %template(vectorunsigned) vector; + %template(vectorpairunsigned) vector>; %template(vectorbool) vector; %template(vectorbdd) vector; %template(vectorstring) vector; @@ -465,6 +467,19 @@ namespace std { DeprecationWarning) %} +// Must occur before the twa declaration +%typemap(out) SWIGTYPE* spot::twa::get_product_states %{ + if (!$1) + $result = SWIG_Py_Void(); + else + { + unsigned sz = $1->size(); + $result = PyList_New(sz); + for (unsigned i = 0; i < sz; ++i) + PyList_SetItem($result, i, swig::from((*$1)[i])); + } +%} + %include %include @@ -769,6 +784,21 @@ def state_is_accepting(self, src) -> "bool": return self->get_named_prop>("state-names"); } + + void set_product_states(std::vector> pairs) + { + self->set_named_prop("product-states", new + std::vector>(std::move(pairs))); + } + + std::vector>* get_product_states() + { + return self->get_named_prop + >>("product-states"); + } + + twa* highlight_state(unsigned state, unsigned color) { auto hs = diff --git a/tests/python/product.ipynb b/tests/python/product.ipynb index 947bd17e4..774439a00 100644 --- a/tests/python/product.ipynb +++ b/tests/python/product.ipynb @@ -15,7 +15,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.5.4" + "version": "3.6.4" }, "name": "" }, @@ -34,6 +34,7 @@ "spot.setup(show_default='.tavb')\n", "\n", "def horiz(*args):\n", + " \"\"\"Display multiple arguments side by side in a table.\"\"\"\n", " s = ''\n", " for arg in args:\n", " s += ''\n", @@ -1538,9 +1539,7 @@ "- states are not presented as pairs\n", "- the properties of the resulting automaton are not set\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", + "The former point could 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. However we can do even better by using `set_product_states()` and passing an array of pairs of states. Besides the output routines, some algorithms actually retrieve this vector of pair of states to work on the product.\n", "\n", "Regarding the latter point, consider for instance the deterministic nature of these automata. In Spot an automaton is deterministic if it is both existential (no universal branching) and universal (no non-deterministic branching). In our case we will restrict the algorithm to existantial input (by asserting `is_existential()` on both operands), so we can consider that the `prop_universal()` property is an indication of determinism:" ] @@ -1662,7 +1661,7 @@ " result.copy_ap_of(left)\n", " result.copy_ap_of(right)\n", " \n", - " names = [] # our array of state names\n", + " pairs = [] # our array of state pairs\n", " sdict = {}\n", " todo = []\n", " def dst(ls, rs):\n", @@ -1672,7 +1671,7 @@ " p = result.new_state()\n", " sdict[pair] = p\n", " todo.append((ls, rs, p))\n", - " names.append(\"{},{}\".format(ls, rs)) # name each state\n", + " pairs.append((ls, rs)) # name each state\n", " return p\n", " \n", " result.set_init_state(dst(left.get_init_state_number(), \n", @@ -1691,8 +1690,8 @@ " 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", + " # Remember the origin of our states\n", + " result.set_product_states(pairs)\n", " \n", " # Loop over all the properties we want to preserve if they hold in both automata\n", " for p in ('prop_universal', 'prop_complete', 'prop_weak', 'prop_inherently_weak', \n", @@ -2038,6 +2037,218 @@ ], "prompt_number": 9 }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "For development, it is useful to know that we can force the automaton printer to show the real state numbers (not the pairs) by passing option `1`, and that we can retrieve the associated pairs ourselves." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "display(p3.show('.1'))\n", + "pairs = p3.get_product_states()\n", + "for s in range(p3.num_states()):\n", + " print(\"{}: {}\".format(s, pairs[s]))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "G\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 & c\n", + "\u2776\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\u2777\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 & c\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\u2776\n", + "\u2777\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", + "\n", + "\n", + "4->3\n", + "\n", + "\n", + "b & c\n", + "\u24ff\n", + "\u2776\n", + "\u2777\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", + "" + ], + "text": [ + "" + ] + }, + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "0: (1, 0)\n", + "1: (0, 0)\n", + "2: (0, 1)\n", + "3: (2, 0)\n", + "4: (2, 1)\n" + ] + } + ], + "prompt_number": 10 + }, { "cell_type": "markdown", "metadata": {}, @@ -2060,11 +2271,11 @@ "output_type": "stream", "stream": "stdout", "text": [ - "1000 loops, best of 3: 216 \u00b5s per loop\n" + "1000 loops, best of 3: 231 \u00b5s per loop\n" ] } ], - "prompt_number": 10 + "prompt_number": 11 }, { "cell_type": "code", @@ -2079,12 +2290,12 @@ "output_type": "stream", "stream": "stdout", "text": [ - "The slowest run took 4.86 times longer than the fastest. This could mean that an intermediate result is being cached.\n", - "100000 loops, best of 3: 10.3 \u00b5s per loop\n" + "The slowest run took 5.96 times longer than the fastest. This could mean that an intermediate result is being cached.\n", + "100000 loops, best of 3: 4.6 \u00b5s per loop\n" ] } ], - "prompt_number": 11 + "prompt_number": 12 }, { "cell_type": "markdown",
' + arg.data + '