diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 39cb174208feab4692e394296640520dfdae6734..496dd4cebfd00d33a9dc3613455efde2083748ab 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -894,14 +894,23 @@ namespace spot friend std::ostream& operator<<(std::ostream& os, const acc_code& code); }; - acc_cond(unsigned n_sets = 0, acc_code code = {}) + acc_cond(unsigned n_sets = 0, const acc_code& code = {}) : num_(0U), all_(0U), code_(code) { add_sets(n_sets); + uses_fin_acceptance_ = check_fin_acceptance(); + } + + acc_cond(const acc_code& code) + : num_(0U), all_(0U), code_(code) + { + add_sets(code.used_sets().max_set()); + uses_fin_acceptance_ = check_fin_acceptance(); } acc_cond(const acc_cond& o) - : num_(o.num_), all_(o.all_), code_(o.code_) + : num_(o.num_), all_(o.all_), code_(o.code_), + uses_fin_acceptance_(o.uses_fin_acceptance_) { } diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 8157c839b831241de3ea3b28efeebdb2c3588482..5622b5c82f06282660fc82431aacfb57a6a8107c 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -34,6 +34,7 @@ %include "std_list.i" %include "std_set.i" %include "std_map.i" +%include "std_pair.i" %include "stdint.i" %include "exception.i" %include "typemaps.i" @@ -356,6 +357,8 @@ namespace std { %feature("flatnested") spot::acc_cond::acc_code; %apply bool* OUTPUT {bool& max, bool& odd}; %include +%template(pair_bool_mark) std::pair; + %include %include diff --git a/wrap/python/tests/acc_cond.ipynb b/wrap/python/tests/acc_cond.ipynb index facbfd7541a51a6a56a48e22b1e12fdc85cd070b..4ad9c85c89b7cb85040f5352ecfa758bb71b1385 100644 --- a/wrap/python/tests/acc_cond.ipynb +++ b/wrap/python/tests/acc_cond.ipynb @@ -18,7 +18,7 @@ "version": "3.4.3+" }, "name": "", - "signature": "sha256:bcc334639d07643d72b406a76d5aa91c5accb4e05a55128c0f909ad73b4b2491" + "signature": "sha256:c447381803e03318b0d23c721f53fa232f91ec81af26a7c09c817463eee5d417" }, "nbformat": 3, "nbformat_minor": 0, @@ -1057,7 +1057,64 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "The common scenario of setting generalized B\u00fcchi acceptance can be achieved more efficiently as follows:" + "Calling the constructor of `acc_cond` by passing just an instance of `acc_code` will automatically set the number of acceptance sets to the minimum needed by the formula:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "acc = spot.acc_cond(spot.parse_acc_code('Streett 2'))\n", + "acc" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 40, + "text": [ + "(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))" + ] + } + ], + "prompt_number": 40 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The above is in fact just syntactic sugar for:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "code = spot.parse_acc_code('Streett 2')\n", + "acc = spot.acc_cond(code.used_sets().max_set(), code)\n", + "acc" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 41, + "text": [ + "(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))" + ] + } + ], + "prompt_number": 41 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The common scenario of setting generalized B\u00fcchi acceptance can be achieved more efficiently by first setting the number of acceptance sets, and then requiring generalized B\u00fcchi acceptance:" ] }, { @@ -1074,13 +1131,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 40, + "prompt_number": 42, "text": [ "(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))" ] } ], - "prompt_number": 40 + "prompt_number": 42 }, { "cell_type": "markdown", @@ -1113,7 +1170,7 @@ ] } ], - "prompt_number": 41 + "prompt_number": 43 }, { "cell_type": "markdown", @@ -1128,8 +1185,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "code = spot.parse_acc_code('Rabin 2')\n", - "acc = spot.acc_cond(code.used_sets().max_set(), code)\n", + "acc = spot.acc_cond(spot.parse_acc_code('Rabin 2'))\n", "print(acc)\n", "print(acc.is_rabin())\n", "print(acc.is_streett())" @@ -1147,7 +1203,7 @@ ] } ], - "prompt_number": 42 + "prompt_number": 44 }, { "cell_type": "markdown", @@ -1160,8 +1216,7 @@ "cell_type": "code", "collapsed": false, "input": [ - "code = spot.parse_acc_code('parity min odd 4')\n", - "acc = spot.acc_cond(code.used_sets().max_set(), code)\n", + "acc = spot.acc_cond(spot.parse_acc_code('parity min odd 4'))\n", "print(acc)\n", "print(acc.is_parity())\n", "acc.set_generalized_buchi()\n", @@ -1182,13 +1237,13 @@ ] } ], - "prompt_number": 43 + "prompt_number": 45 }, { "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", + "`acc_cond` contains a few functions 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`:" ] @@ -1211,7 +1266,7 @@ ] } ], - "prompt_number": 44 + "prompt_number": 46 }, { "cell_type": "markdown", @@ -1232,25 +1287,121 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 45, + "prompt_number": 47, "text": [ "{0,1,2,3}" ] } ], - "prompt_number": 45 + "prompt_number": 47 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "For convencience, the `accepting()` method of `acc_cond` delegates to that of the `acc_code`. \n", + "Any set passed to `accepting()` that is not used by the acceptance formula has no influence." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "print(\"acc =\", acc)\n", + "for x in ([0, 1, 2, 3, 10], [1, 2]):\n", + " print(\"acc.accepting({}) = {}\".format(x, acc.accepting(x)))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "acc = (4, Inf(0)&Inf(1)&Inf(2)&Inf(3))\n", + "acc.accepting([0, 1, 2, 3, 10]) = True\n", + "acc.accepting([1, 2]) = False\n" + ] + } + ], + "prompt_number": 48 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Finally the `unsat_mark()` method of `acc_cond` computes an instance of `mark_t` that is unaccepting (i.e., passing this value to `acc.accepting(...)` will return `False` when such a value exist. Not all acceptance conditions have an satisfiable mark. Obviously the `t` acceptance is always satisfiable, and so are all equivalent acceptances (for instance `Fin(1)|Inf(1)`).\n", + "\n", + "For this reason, `unsat_mark()` actually returns a pair: `(bool, mark_t)` where the Boolean is `False` iff the acceptance is always satisfiable. When the Boolean is `True`, then the second element of the pair gives a non-accepting mark." + ] }, { "cell_type": "code", "collapsed": false, - "input": [], + "input": [ + "print(acc)\n", + "print(acc.unsat_mark())" + ], "language": "python", "metadata": {}, - "outputs": [], - "prompt_number": 45 + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))\n", + "(True, {})\n" + ] + } + ], + "prompt_number": 49 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "acc = spot.acc_cond(0)\n", + "print(acc)\n", + "print(acc.unsat_mark())" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "(0, t)\n", + "(False, {})\n" + ] + } + ], + "prompt_number": 50 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "acc = spot.acc_cond(spot.parse_acc_code('Streett 2'))\n", + "print(acc)\n", + "print(acc.unsat_mark())" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))\n", + "(True, {2})\n" + ] + } + ], + "prompt_number": 51 } ], "metadata": {} } ] -} +} \ No newline at end of file