acc_cond: allow ctor from acc_code only + bind unsat_mark()

* spot/twa/acc.hh: Here.
* wrap/python/spot_impl.i: Adjust for the strange return type of
unsat_mark().
* wrap/python/tests/acc_cond.ipynb: Augment.

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": [],
+     "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": [],
-     "prompt_number": 45
+     "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": [
+      "print(acc)\n",
+      "print(acc.unsat_mark())"
+     ],
+     "language": "python",
+     "metadata": {},
+     "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": {}
   }
  ]
-}
+}