From 15131e74f2aad5b6b049e70fb2859782a9cebc13 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 17 Dec 2015 11:46:46 +0100 Subject: [PATCH] python: better binding for is_parity() * wrap/python/spot_impl.i: Here. * wrap/python/tests/acc_cond.ipynb: Document it. * spot/twa/acc.cc (is_parity): Always initialize max. --- spot/twa/acc.cc | 5 +- wrap/python/spot_impl.i | 26 +++++++- wrap/python/tests/acc_cond.ipynb | 102 +++++++++++++++++++++++++++++-- 3 files changed, 124 insertions(+), 9 deletions(-) diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 9a42cf572..02abc56ca 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -685,7 +685,10 @@ namespace spot odd = !u_inf.has(0); for (auto s: u_inf.sets()) if ((s & 1) != odd) - return false; + { + max = false; // just so the value is not uninitialized + return false; + } auto max_code = acc_code::parity(true, odd, sets); if (max_code == code_) diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index ce6583496..8157c839b 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -221,8 +221,9 @@ namespace swig // For spot::emptiness_check_instantiator::construct and any other // function that return errors via a "char **err" argument. -%typemap(in, numinputs=0) char** OUTPUT (char* temp) - "$1 = &temp;"; +%typemap(in, numinputs=0) char** OUTPUT (char* temp) { + $1 = &temp; +} %typemap(argout) char** OUTPUT { PyObject *obj = SWIG_FromCharPtr(*$1); if (!$result) { @@ -239,13 +240,32 @@ namespace swig $result = PyList_New(1); PyList_SetItem($result, 0, o2); } - PyList_Append($result,obj); + PyList_Append($result, obj); Py_DECREF(obj); } }; %apply char** OUTPUT { char** err }; +// This is mainly for acc_cond::is_parity() +%typemap(in, numinputs=0) bool& (bool temp) { + $1 = &temp; + }; +%typemap(argout) bool& { + PyObject *obj = SWIG_From_bool(*$1); + if (!$result) { + $result = obj; + } else { + if (!PyList_Check($result)) { + PyObject *o2 = $result; + $result = PyList_New(1); + PyList_SetItem($result, 0, o2); + } + PyList_Append($result, obj); + Py_DECREF(obj); + } + }; + // Allow None to be passed for formula. Some functions like // postprocessor::run() take an optional formula that defaults to // nullptr. So it make sense to have function that take formulas that diff --git a/wrap/python/tests/acc_cond.ipynb b/wrap/python/tests/acc_cond.ipynb index d7e98d354..facbfd754 100644 --- a/wrap/python/tests/acc_cond.ipynb +++ b/wrap/python/tests/acc_cond.ipynb @@ -17,7 +17,8 @@ "pygments_lexer": "ipython3", "version": "3.4.3+" }, - "name": "" + "name": "", + "signature": "sha256:bcc334639d07643d72b406a76d5aa91c5accb4e05a55128c0f909ad73b4b2491" }, "nbformat": 3, "nbformat_minor": 0, @@ -1085,7 +1086,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "The `acc_cond` class has several methods for detecting acceptance conditions that match the named acceptance conditions of the HOA format. Note that in the HOA format, `Inf(0)&Inf(1)&Inf(2)&Inf(3)` is only called generalized B\u00fcchi if exactly for acceptance sets are used. So the following behavior should not be a surprise:" + "The `acc_cond` class has several methods for detecting acceptance conditions that match the named acceptance conditions of the HOA format. Note that in the HOA format, `Inf(0)&Inf(1)&Inf(2)&Inf(3)` is only called generalized B\u00fcchi if exactly 4 acceptance sets are used. So the following behavior should not be surprising:" ] }, { @@ -1148,17 +1149,108 @@ ], "prompt_number": 42 }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The check for parity acceptance returns three Boolean in a list of the form `[matched, max?, odd?]`. If `matched` is `False`, the other values should be ignored." + ] + }, { "cell_type": "code", - "collapsed": true, + "collapsed": false, + "input": [ + "code = spot.parse_acc_code('parity min odd 4')\n", + "acc = spot.acc_cond(code.used_sets().max_set(), code)\n", + "print(acc)\n", + "print(acc.is_parity())\n", + "acc.set_generalized_buchi()\n", + "print(acc)\n", + "print(acc.is_parity())" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "(4, Fin(0) & (Inf(1) | (Fin(2) & Inf(3))))\n", + "[True, False, True]\n", + "(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))\n", + "[False, False, False]\n" + ] + } + ], + "prompt_number": 43 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "`acc_cond` contains a few function for manipulating `mark_t` instances, these are typically functions that require known the total number of accepting sets declared.\n", + "\n", + "For instance complementing a `mark_t`:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "m = spot.mark_t([1, 3])\n", + "print(acc.comp(m))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "{0,2}\n" + ] + } + ], + "prompt_number": 44 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "`all_sets()` returns a `mark_t` listing all the declared sets: " + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "acc.all_sets()" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 45, + "text": [ + "{0,1,2,3}" + ] + } + ], + "prompt_number": 45 + }, + { + "cell_type": "code", + "collapsed": false, "input": [], "language": "python", "metadata": {}, "outputs": [], - "prompt_number": null + "prompt_number": 45 } ], "metadata": {} } ] -} \ No newline at end of file +}