{
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.4.3+"
  },
  "name": "",
  "signature": "sha256:9abaa081794db5d5479c8c9c179c8518aa52b60abdb4b7a106045646e277d43a"
 },
 "nbformat": 3,
 "nbformat_minor": 0,
 "worksheets": [
  {
   "cells": [
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "import spot\n",
      "spot.setup()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 1
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "# Acceptance conditions\n",
      "\n",
      "The acceptance condition of an automaton specifies which of its paths are accepting.\n",
      "\n",
      "The way acceptance conditions are stored in Spot is derived from the way acceptance conditions are specified in the [HOA format](http://adl.github.io/hoaf/).  In HOA, acceptance conditions are given as a line of the form:\n",
      "\n",
      "    Acceptance: 3 (Inf(0)&Fin(1))|Inf(2)\n",
      "\n",
      "The number `3` gives the number of acceptance sets used (numbered from `0` to `2` in that case), while the rest of the line is a positive Boolean formula over terms of the form:\n",
      "- `Inf(n)`, that is true if and only if the set `n` is seen infinitely often,\n",
      "- `Fin(n)`, that is true if and only if the set `n` should be seen finitely often,\n",
      "- `t`, always true,\n",
      "- `f`, always false.\n",
      "\n",
      "The HOA specifications additionally allows terms of the form `Inf(!n)` or `Fin(!n)` but Spot automatically rewrites those away when reading an HOA file.\n",
      "\n",
      "Note that the number of sets given can be larger than what is actually needed by the acceptance formula.\n",
      "\n",
      "Transitions in automata can be tagged as being part of some member sets, and a path in the automaton is accepting if the set of acceptance sets visited along this path satify the acceptance condition.\n",
      "\n",
      "Definining acceptance conditions in Spot involves three different types of C++ objects:\n",
      "\n",
      "- `spot::acc_cond` is used to represent an acceptance condition, that is: a number of sets and a formula.\n",
      "- `spot::acc_cond::acc_code`, is used to represent Boolean formula for the acceptance condition using a kind of byte code (hence the name)\n",
      "- `spot::acc_cond::mark_t`, is a type of bit-vector used to represent membership to acceptance sets.\n",
      "\n",
      "In because Swig's support for nested class is limited, these types are available respectively as `spot.acc_cond`, `spot.acc_code`, and `spot.mark_t` in Python.\n",
      "\n",
      "## `mark_t`\n",
      "\n",
      "Let's start with the simpler of these three objects. `mark_t` is a type of bit vector.  Its main constructor takes a sequence of set numbers."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.mark_t()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 2,
       "text": [
        "{}"
       ]
      }
     ],
     "prompt_number": 2
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.mark_t([0, 2, 3])"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 3,
       "text": [
        "{0,2,3}"
       ]
      }
     ],
     "prompt_number": 3
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.mark_t((0, 2, 3))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 4,
       "text": [
        "{0,2,3}"
       ]
      }
     ],
     "prompt_number": 4
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "As seen above, the sequence of set numbers can be specified using a list or a tuple.  While from the Python language point of view, using a tuple is faster than using a list, the overhead to converting all the arguments from Python to C++ and then converting the resuslting back from C++ to Python makes this difference completely negligeable.  In the following, we opted to use lists, because brackets are more readable than nested parentheses."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "x = spot.mark_t([0, 2, 3])\n",
      "y = spot.mark_t([0, 4])\n",
      "print(x | y)\n",
      "print(x & y)\n",
      "print(x - y)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "{0,2,3,4}\n",
        "{0}\n",
        "{2,3}\n"
       ]
      }
     ],
     "prompt_number": 5
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The bits can be set, cleared, and tested using the `set()`, `clear()`, and `has()` methods:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "x.set(5)\n",
      "print(x)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "{0,2,3,5}\n"
       ]
      }
     ],
     "prompt_number": 6
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "x.clear(3)\n",
      "print(x)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "{0,2,5}\n"
       ]
      }
     ],
     "prompt_number": 7
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "print(x.has(2))\n",
      "print(x.has(3))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "True\n",
        "False\n"
       ]
      }
     ],
     "prompt_number": 8
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Left-shifting will increment all set numbers.\n",
      "This operation is useful when building the product of two automata: all the set number of one automaton have to be shift by the number of sets used in the other automaton."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "x << 2"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 9,
       "text": [
        "{2,4,7}"
       ]
      }
     ],
     "prompt_number": 9
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Internally, the `mark_t` stores the bit-vector as an integer.  This also implies that we currently do not support more than 32 acceptance sets.  The underlaying integer can be retrieved using `.id`."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "print(x)\n",
      "print(x.id)\n",
      "print(bin(x.id))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "{0,2,5}\n",
        "37\n",
        "0b100101\n"
       ]
      }
     ],
     "prompt_number": 10
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "`mark_t` can also be initialized using an integer: in that case the integer is interpreted as a bit vector.\n",
      "\n",
      "A frequent error is to use `mark_t(n)` when we really mean `mark_t([n])` or `mark_t((n,))`."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "# compare\n",
      "print(spot.mark_t([5]))\n",
      "# with\n",
      "print(spot.mark_t(5))\n",
      "print(spot.mark_t(0b10101))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "{5}\n",
        "{0,2}\n",
        "{0,2,4}\n"
       ]
      }
     ],
     "prompt_number": 11
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The different sets can be iterated over with the `sets()` method, that returns a tuble with the index of all bits set."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "print(x)\n",
      "print(x.sets())\n",
      "for s in x.sets():\n",
      "    print(s)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "{0,2,5}\n",
        "(0, 2, 5)\n",
        "0\n",
        "2\n",
        "5\n"
       ]
      }
     ],
     "prompt_number": 12
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "`count()` return the number of sets in a `mark_t`:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "x.count()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 13,
       "text": [
        "3"
       ]
      }
     ],
     "prompt_number": 13
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "`lowest()` returns a `mark_t` containing only the lowest set number.  This provides another way to iterate overs all set numbers in cases where you need the result as a `mark_t`."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.mark_t([1,3,5]).lowest()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 14,
       "text": [
        "{1}"
       ]
      }
     ],
     "prompt_number": 14
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "v = spot.mark_t([1, 3, 5])\n",
      "while v:               # this stops once v is empty\n",
      "    b = v.lowest()\n",
      "    v -= b\n",
      "    print(b)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "{1}\n",
        "{3}\n",
        "{5}\n"
       ]
      }
     ],
     "prompt_number": 15
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "`max_set()` returns the number of the highest set plus one.  This is usually used to figure out how many sets we need to declare on the `Acceptance:` line of the HOA format:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.mark_t([1, 3, 5]).max_set()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 16,
       "text": [
        "6"
       ]
      }
     ],
     "prompt_number": 16
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "## `acc_code`\n",
      "\n",
      "`acc_code` encodes the formula of the acceptance condition using a kind of bytecode that basically corresponds to an encoding in [reverse Polish notation](http://en.wikipedia.org/wiki/Reverse_Polish_notation) in which conjunctions of `Inf(n)` terms, and disjunctions of `Fin(n)` terms are grouped.  In particular, the frequently-used genaralized-B\u00fcchi acceptance conditions (like `Inf(0)&Inf(1)&Inf(2)`) are always encoded as a single term (like `Inf({0,1,2})`).\n",
      "\n",
      "The simplest way to construct an `acc_code` by passing a string that represent the formula to build."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.acc_code('(Inf(0)&Fin(1))|Inf(2)')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 17,
       "text": [
        "(Fin(1) & Inf(0)) | Inf(2)"
       ]
      }
     ],
     "prompt_number": 17
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "You may also use a named acceptance condition:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.acc_code('Rabin 2')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 18,
       "text": [
        "(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))"
       ]
      }
     ],
     "prompt_number": 18
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The recognized names are the valide values for `acc-name:` in the [HOA format](http://adl.github.io/hoaf/).  Additionally numbers may be replaced by ranges of the form `n..m`, in which case a random number is selected in that range."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "print(spot.acc_code('Streett 2..4'))\n",
      "print(spot.acc_code('Streett 2..4'))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "(Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & (Fin(4) | Inf(5)) & (Fin(6) | Inf(7))\n",
        "(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\n"
       ]
      }
     ],
     "prompt_number": 19
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "It may also be convenient to generate a random acceptance condition:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.acc_code('random 3..5')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 20,
       "text": [
        "(Fin(3) | Inf(1)) & (Fin(0)|Fin(2)) & Inf(4)"
       ]
      }
     ],
     "prompt_number": 20
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The `to_cnf()` and `to_dnf()` functions can be used to rewrite the formula into Conjunctive or Disjunctive normal forms.  This functions will simplify the resulting formulas to make them irredundant."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "a = spot.acc_code('parity min odd 5')\n",
      "a"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 21,
       "text": [
        "Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | Fin(4))))"
       ]
      }
     ],
     "prompt_number": 21
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "a.to_cnf()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 22,
       "text": [
        "Fin(0) & (Fin(2) | Inf(1)) & (Fin(4) | Inf(1) | Inf(3))"
       ]
      }
     ],
     "prompt_number": 22
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "a.to_dnf()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 23,
       "text": [
        "(Fin(0) & Inf(1)) | (Fin(0) & Fin(2) & Inf(3)) | (Fin(0) & Fin(2) & Fin(4))"
       ]
      }
     ],
     "prompt_number": 23
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The manipulation of `acc_code` objects is quite rudimentary at the moment: it easy to build, but it's harder take appart.  In fact we won't attempt to disassemble an `acc_code` object in Python: those things are better done in C++\n",
      "\n",
      "Operators `|`, `|=`, `&`, `&=`, `<<`, and `<<=` can be used with their obvious semantics.\n",
      "Whenever possible, the inplace versions (`|=`, `&=`, `<<=`) should be prefered, because they create less temporary acceptance conditions."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "x = spot.acc_code('Rabin 2')\n",
      "y = spot.acc_code('Rabin 2') << 4\n",
      "print(x)\n",
      "print(y)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\n",
        "(Fin(4) & Inf(5)) | (Fin(6) & Inf(7))\n"
       ]
      }
     ],
     "prompt_number": 24
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "print(x | y)\n",
      "print(x & y)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "(Fin(4) & Inf(5)) | (Fin(6) & Inf(7)) | (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\n",
        "((Fin(4) & Inf(5)) | (Fin(6) & Inf(7))) & ((Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))\n"
       ]
      }
     ],
     "prompt_number": 25
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The `complement()` method returns the complemented acceptance condition:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "print(x)\n",
      "print(x.complement())"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\n",
        "(Inf(0) | Fin(1)) & (Inf(2) | Fin(3))\n"
       ]
      }
     ],
     "prompt_number": 26
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Instead of using `acc_code('string')`, it is also possible to build an acceptance formula from atoms like `Inf({...})`, `Fin({...})`, `t`, or `f`.\n",
      "\n",
      "Remember that in our encoding for the formula, terms like `Inf(1)&Inf(2)` and `Fin(3)|Fin(4)|Fin(5)` are actually stored as `Inf({1,2})` and `Fin({3,4,5})`, where `{1,2}` and `{3,4,5}` are instance of `mark_t`.  These terms can be generated with the\n",
      "functions `spot.acc_code.inf(mark)` and `spot.acc_code.fin(mark)`.\n",
      "\n",
      "`Inf({})` is equivalent to `t`, and `Fin({})` is equivalent to `f`, but it's better to use the functions `spot.acc_code.t()` or `spot.acc_code.f()` directly."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.acc_code.inf([1,2]) & spot.acc_code.fin([3,4,5])"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 27,
       "text": [
        "(Fin(3)|Fin(4)|Fin(5)) & (Inf(1)&Inf(2))"
       ]
      }
     ],
     "prompt_number": 27
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.acc_code.inf([])"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 28,
       "text": [
        "t"
       ]
      }
     ],
     "prompt_number": 28
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.acc_code.t()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 29,
       "text": [
        "t"
       ]
      }
     ],
     "prompt_number": 29
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.acc_code.fin([])"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 30,
       "text": [
        "f"
       ]
      }
     ],
     "prompt_number": 30
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.acc_code.f()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 31,
       "text": [
        "f"
       ]
      }
     ],
     "prompt_number": 31
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "To evaluate an acceptance condition formula on a run, build a `mark_t` containing all the acceptance sets that are seen infinitely often along this run, and call the `accepting()` method."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "acc = spot.acc_code('Fin(0) & Inf(1) | Inf(2)')\n",
      "print(\"acc =\", acc)\n",
      "for x in ([0, 1, 2], [1, 2], [0, 1], [0, 2], [0], [1], [2], []):\n",
      "    print(\"acc.accepting({}) = {}\".format(x, acc.accepting(x)))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "acc = (Fin(0) & Inf(1)) | Inf(2)\n",
        "acc.accepting([0, 1, 2]) = True\n",
        "acc.accepting([1, 2]) = True\n",
        "acc.accepting([0, 1]) = False\n",
        "acc.accepting([0, 2]) = True\n",
        "acc.accepting([0]) = False\n",
        "acc.accepting([1]) = True\n",
        "acc.accepting([2]) = True\n",
        "acc.accepting([]) = False\n"
       ]
      }
     ],
     "prompt_number": 32
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Finally the method `used_sets()` returns a `mark_t` with all the sets appearing in the formula:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "acc = spot.acc_code('Fin(0) & Inf(2)')\n",
      "print(acc)\n",
      "print(acc.used_sets())\n",
      "print(acc.used_sets().max_set())"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "Fin(0) & Inf(2)\n",
        "{0,2}\n",
        "3\n"
       ]
      }
     ],
     "prompt_number": 33
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "# `acc_cond`\n",
      "\n",
      "Automata store their acceptance condition as an instance of the `acc_cond` class.\n",
      "This class can be thought of as a pair `(n, code)`, where `n` is an integer that tells how many acceptance sets are used, while the `code` is an instance of `acc_code` and encodes the formula over *a subset* of these acceptance sets.  We usually have `n == code.used_sets().max_set())`, but `n` can be larger.\n",
      "\n",
      "It is OK if an automaton declares that is used 3 sets, even if the acceptance condition formula only uses set number 1.\n",
      "\n",
      "The `acc_cond` objects are usually not created by hand: automata have dedicated methods for that.  But for the purpose of this notebook, let's do it:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "acc = spot.acc_cond(4, spot.acc_code('Rabin 2'))\n",
      "acc"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 34,
       "text": [
        "(4, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))"
       ]
      }
     ],
     "prompt_number": 34
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "For convenience, you can pass the string directly:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "acc = spot.acc_cond(4, 'Rabin 2')\n",
      "acc"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 35,
       "text": [
        "(4, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))"
       ]
      }
     ],
     "prompt_number": 35
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "acc.num_sets()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 36,
       "text": [
        "4"
       ]
      }
     ],
     "prompt_number": 36
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "acc.get_acceptance()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 37,
       "text": [
        "(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))"
       ]
      }
     ],
     "prompt_number": 37
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The `acc_cond` object can also be constructed using only a number of sets.  In that case, the acceptance condition defaults to `t`, and it can be changed to something else later (using `set_acceptance()`).  The number of acceptance sets can also be augmented with `add_sets()`."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "acc = spot.acc_cond(4)\n",
      "acc"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 38,
       "text": [
        "(4, t)"
       ]
      }
     ],
     "prompt_number": 38
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "acc.add_sets(2)\n",
      "acc"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 39,
       "text": [
        "(6, t)"
       ]
      }
     ],
     "prompt_number": 39
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "acc.set_acceptance('Streett 2')\n",
      "acc"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 40,
       "text": [
        "(6, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))"
       ]
      }
     ],
     "prompt_number": 40
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Calling the constructor of `acc_cond` by passing just an instance of `acc_code` (or a string that will be passed to the `acc_code` constructor) 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('Streett 2')\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 above is in fact just syntactic sugar for:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "code = spot.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": 42,
       "text": [
        "(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))"
       ]
      }
     ],
     "prompt_number": 42
    },
    {
     "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:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "acc = spot.acc_cond(4)\n",
      "acc.set_generalized_buchi()\n",
      "acc"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 43,
       "text": [
        "(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))"
       ]
      }
     ],
     "prompt_number": 43
    },
    {
     "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 4 acceptance sets are used.  So the following behavior should not be surprising:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "print(acc)\n",
      "print(acc.is_generalized_buchi())\n",
      "acc.add_sets(1)\n",
      "print(acc)\n",
      "print(acc.is_generalized_buchi())"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))\n",
        "True\n",
        "(5, Inf(0)&Inf(1)&Inf(2)&Inf(3))\n",
        "False\n"
       ]
      }
     ],
     "prompt_number": 44
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Similar methods like `is_t()`, `is_f()`, `is_buchi()`, `is_co_buchi()`, `is_generalized_co_buchi()` all return a Boolean.\n",
      "\n",
      "The `is_rabin()` and `is_streett()` methods, however, return a number of pairs.  The number of pairs is always `num_sets()/2` on success, or -1 on failure."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "acc = spot.acc_cond('Rabin 2')\n",
      "print(acc)\n",
      "print(acc.is_rabin())\n",
      "print(acc.is_streett())"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "(4, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))\n",
        "2\n",
        "-1\n"
       ]
      }
     ],
     "prompt_number": 45
    },
    {
     "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": false,
     "input": [
      "acc = spot.acc_cond('parity min odd 4')\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": 46
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "`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`:"
     ]
    },
    {
     "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": 47
    },
    {
     "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": 48,
       "text": [
        "{0,1,2,3}"
       ]
      }
     ],
     "prompt_number": 48
    },
    {
     "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": 49
    },
    {
     "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": 50
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "acc = spot.acc_cond(0)   # use 0 acceptance sets, and the default formula (t)\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": 51
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "acc = spot.acc_cond('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": 52
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 52
    }
   ],
   "metadata": {}
  }
 ]
}