accparse.ipynb 5.12 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
{
 "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+"
  },
20 21
  "name": "",
  "signature": "sha256:1ee7951bed30652ae110a14b210541829221552eb944ff01f25236179673dd5b"
22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43
 },
 "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": [
44
      "c = spot.acc_code('Inf(0)&Fin(1)|Inf(2)&Fin(3)'); c"
45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 2,
       "text": [
        "(Fin(1) & Inf(0)) | (Fin(3) & Inf(2))"
       ]
      }
     ],
     "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)) & (Fin(3) | Inf(0)) & (Fin(1) | Inf(2)) & (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",
109 110 111 112 113 114 115
      "            '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",
116
      "    print(acc, ': ', spot.acc_code(acc), sep='')"
117 118 119 120 121 122 123 124 125 126 127 128 129 130
     ],
     "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",
131 132
        "generalized-co-Buchi 3: Fin(0)|Fin(1)|Fin(2)\n",
        "generalized-co-Buchi 0: f\n",
133 134 135 136 137
        "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",
138
        "generalized-Rabin 0: f\n",
139 140
        "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",
141 142 143
        "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",
144
        "parity max odd 5: Fin(4) & (Inf(3) | (Fin(2) & (Inf(1) | Fin(0))))\n",
145
        "parity max even 5: Inf(4) | (Fin(3) & (Inf(2) | (Fin(1) & Inf(0))))\n",
146 147 148
        "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",
149 150 151
        "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",
152
        "parity max odd 1: Fin(0)\n",
153
        "parity max even 1: Inf(0)\n",
154 155 156
        "parity min odd 1: Fin(0)\n",
        "parity min even 0: t\n",
        "parity max odd 0: t\n",
157 158
        "parity max even 0: f\n",
        "parity min odd 0: f\n"
159 160 161 162
       ]
      }
     ],
     "prompt_number": 5
163 164 165 166 167 168 169 170 171
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 5
172 173 174 175 176 177
    }
   ],
   "metadata": {}
  }
 ]
}