{
 "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.5.3+"
  },
  "name": ""
 },
 "nbformat": 3,
 "nbformat_minor": 0,
 "worksheets": [
  {
   "cells": [
    {
     "cell_type": "code",
     "collapsed": true,
     "input": [
      "import spot\n",
      "spot.setup()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 1
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "c = spot.acc_code('Inf(0)&Fin(1)|Inf(2)&Fin(3)'); c"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 2,
       "text": [
        "(Inf(0) & Fin(1)) | (Inf(2) & Fin(3))"
       ]
      }
     ],
     "prompt_number": 2
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "c.to_dnf()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 3,
       "text": [
        "(Fin(1) & Inf(0)) | (Fin(3) & Inf(2))"
       ]
      }
     ],
     "prompt_number": 3
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "c.to_cnf()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 4,
       "text": [
        "(Inf(0) | Inf(2)) & (Inf(0) | Fin(3)) & (Inf(2) | Fin(1)) & (Fin(1)|Fin(3))"
       ]
      }
     ],
     "prompt_number": 4
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "for acc in ['all', 't', \n",
      "            'Buchi', 'generalized-Buchi 3', 'generalized-Buchi 0',\n",
      "            'co-Buchi', 'generalized-co-Buchi 3', 'generalized-co-Buchi 0',\n",
      "            'Rabin 2', 'Rabin 0',\n",
      "            'Streett 2', 'Streett 0',\n",
      "            'generalized-Rabin 3 1 2 3', 'generalized-Rabin 0',\n",
      "            'parity min even 6', 'parity max odd 6', 'parity max even 6', 'parity min odd 6',\n",
      "            'parity min even 5', 'parity max odd 5', 'parity max even 5', 'parity min odd 5',\n",
      "            'parity min even 2', 'parity max odd 2', 'parity max even 2', 'parity min odd 2',\n",
      "            'parity min even 1', 'parity max odd 1', 'parity max even 1', 'parity min odd 1',\n",
      "            'parity min even 0', 'parity max odd 0', 'parity max even 0', 'parity min odd 0',\n",
      "            ]:\n",
      "    print(acc, ': ', spot.acc_code(acc), sep='')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "all: t\n",
        "t: t\n",
        "Buchi: Inf(0)\n",
        "generalized-Buchi 3: Inf(0)&Inf(1)&Inf(2)\n",
        "generalized-Buchi 0: t\n",
        "co-Buchi: Fin(0)\n",
        "generalized-co-Buchi 3: Fin(0)|Fin(1)|Fin(2)\n",
        "generalized-co-Buchi 0: f\n",
        "Rabin 2: (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\n",
        "Rabin 0: f\n",
        "Streett 2: (Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\n",
        "Streett 0: t\n",
        "generalized-Rabin 3 1 2 3: (Fin(0) & Inf(1)) | (Fin(2) & (Inf(3)&Inf(4))) | (Fin(5) & (Inf(6)&Inf(7)&Inf(8)))\n",
        "generalized-Rabin 0: f\n",
        "parity min even 6: Inf(0) | (Fin(1) & (Inf(2) | (Fin(3) & (Inf(4) | Fin(5)))))\n",
        "parity max odd 6: Inf(5) | (Fin(4) & (Inf(3) | (Fin(2) & (Inf(1) | Fin(0)))))\n",
        "parity max even 6: Fin(5) & (Inf(4) | (Fin(3) & (Inf(2) | (Fin(1) & Inf(0)))))\n",
        "parity min odd 6: Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | (Fin(4) & Inf(5)))))\n",
        "parity min even 5: Inf(0) | (Fin(1) & (Inf(2) | (Fin(3) & Inf(4))))\n",
        "parity max odd 5: Fin(4) & (Inf(3) | (Fin(2) & (Inf(1) | Fin(0))))\n",
        "parity max even 5: Inf(4) | (Fin(3) & (Inf(2) | (Fin(1) & Inf(0))))\n",
        "parity min odd 5: Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | Fin(4))))\n",
        "parity min even 2: Inf(0) | Fin(1)\n",
        "parity max odd 2: Inf(1) | Fin(0)\n",
        "parity max even 2: Fin(1) & Inf(0)\n",
        "parity min odd 2: Fin(0) & Inf(1)\n",
        "parity min even 1: Inf(0)\n",
        "parity max odd 1: Fin(0)\n",
        "parity max even 1: Inf(0)\n",
        "parity min odd 1: Fin(0)\n",
        "parity min even 0: t\n",
        "parity max odd 0: t\n",
        "parity max even 0: f\n",
        "parity min odd 0: f\n"
       ]
      }
     ],
     "prompt_number": 5
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 5
    }
   ],
   "metadata": {}
  }
 ]
}