{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "import spot\n",
    "spot.setup()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(Inf(0) & Fin(1)) | (Inf(2) & Fin(3))\n"
     ]
    }
   ],
   "source": [
    "c = spot.acc_code('Inf(0)&Fin(1)|Inf(2)&Fin(3)'); print(c)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(Fin(1) & Inf(0)) | (Fin(3) & Inf(2))\n"
     ]
    }
   ],
   "source": [
    "print(c.to_dnf())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(Inf(0) | Inf(2)) & (Inf(0) | Fin(3)) & (Inf(2) | Fin(1)) & (Fin(1)|Fin(3))\n"
     ]
    }
   ],
   "source": [
    "print(c.to_cnf())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "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"
     ]
    }
   ],
   "source": [
    "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='')"
   ]
  }
 ],
 "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.6.7"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}