{ "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.2" }, "name": "", "signature": "sha256:8277d563756e7b9333f4900705ae07524e2902b49f4c79ceb40739a865a177c4" }, "nbformat": 3, "nbformat_minor": 0, "worksheets": [ { "cells": [ { "cell_type": "code", "collapsed": false, "input": [ "import os\n", "# Note that Spot (loaded by the kernel) will store a copy of\n", "# the environment variable the first time it reads them, so\n", "# if you change those variables, the new values will be ignored\n", "# until you restart the kernel.\n", "os.environ['SPOT_DOTEXTRA'] = 'size=\"10.2,5\" node[style=filled,fillcolor=\"#ffffaa\"] edge[arrowhead=vee, arrowsize=.7]'\n", "os.environ['SPOT_DOTDEFAULT'] = 'rbcf(Lato)'\n", "import spot" ], "language": "python", "metadata": {}, "outputs": [], "prompt_number": 1 }, { "cell_type": "code", "collapsed": false, "input": [ "a = spot.translate('(a U b) & GFc & GFd', 'BA', complete=True); a" ], "language": "python", "metadata": {}, "outputs": [ { "metadata": {}, "output_type": "pyout", "prompt_number": 2, "svg": [ "\n", "\n", "\n", "\n", "\n", "\n", "G\n", "\n", "\n", "\n", "0\n", "\n", "0\n", "\n", "\n", "I->0\n", "\n", "\n", "\n", "\n", "0->0\n", "\n", "\n", "a & !b\n", "\n", "\n", "1\n", "\n", "1\n", "\u24ff\n", "\n", "\n", "0->1\n", "\n", "\n", "b\n", "\n", "\n", "4\n", "\n", "4\n", "\n", "\n", "0->4\n", "\n", "\n", "!a & !b\n", "\n", "\n", "1->1\n", "\n", "\n", "c & d\n", "\n", "\n", "2\n", "\n", "2\n", "\n", "\n", "1->2\n", "\n", "\n", "!c & d\n", "\n", "\n", "3\n", "\n", "3\n", "\n", "\n", "1->3\n", "\n", "\n", "!d\n", "\n", "\n", "4->4\n", "\n", "\n", "1\n", "\n", "\n", "2->1\n", "\n", "\n", "c\n", "\n", "\n", "2->2\n", "\n", "\n", "!c\n", "\n", "\n", "3->1\n", "\n", "\n", "c & d\n", "\n", "\n", "3->2\n", "\n", "\n", "!c & d\n", "\n", "\n", "3->3\n", "\n", "\n", "!d\n", "\n", "\n", "\n" ], "text": [ " *' at 0x7f87301e0180> >" ] } ], "prompt_number": 2 }, { "cell_type": "code", "collapsed": false, "input": [ "a.show(\"\")" ], "language": "python", "metadata": {}, "outputs": [ { "metadata": {}, "output_type": "pyout", "prompt_number": 3, "svg": [ "\n", "\n", "G\n", "\n", "\n", "\n", "0\n", "\n", "0\n", "\n", "\n", "I->0\n", "\n", "\n", "\n", "\n", "0->0\n", "\n", "\n", "a & !b\n", "\n", "\n", "1\n", "\n", "\n", "1\n", "\n", "\n", "0->1\n", "\n", "\n", "b\n", "\n", "\n", "4\n", "\n", "4\n", "\n", "\n", "0->4\n", "\n", "\n", "!a & !b\n", "\n", "\n", "1->1\n", "\n", "\n", "c & d\n", "\n", "\n", "2\n", "\n", "2\n", "\n", "\n", "1->2\n", "\n", "\n", "!c & d\n", "\n", "\n", "3\n", "\n", "3\n", "\n", "\n", "1->3\n", "\n", "\n", "!d\n", "\n", "\n", "4->4\n", "\n", "\n", "1\n", "\n", "\n", "2->1\n", "\n", "\n", "c\n", "\n", "\n", "2->2\n", "\n", "\n", "!c\n", "\n", "\n", "3->1\n", "\n", "\n", "c & d\n", "\n", "\n", "3->2\n", "\n", "\n", "!c & d\n", "\n", "\n", "3->3\n", "\n", "\n", "!d\n", "\n", "\n", "" ], "text": [ "" ] } ], "prompt_number": 3 }, { "cell_type": "code", "collapsed": false, "input": [ "a.show(\".ast\")" ], "language": "python", "metadata": {}, "outputs": [ { "metadata": {}, "output_type": "pyout", "prompt_number": 4, "svg": [ "\n", "\n", "G\n", "\n", "Inf(\n", "\u24ff\n", ")\n", "cluster_0\n", "\n", "\n", "cluster_1\n", "\n", "\n", "cluster_2\n", "\n", "\n", "\n", "\n", "0\n", "\n", "0\n", "\n", "\n", "I->0\n", "\n", "\n", "\n", "\n", "0->0\n", "\n", "\n", "a & !b\n", "\n", "\n", "1\n", "\n", "1\n", "\n", "\n", "0->1\n", "\n", "\n", "b\n", "\n", "\n", "4\n", "\n", "4\n", "\n", "\n", "0->4\n", "\n", "\n", "!a & !b\n", "\n", "\n", "1->1\n", "\n", "\n", "c & d\n", "\u24ff\n", "\n", "\n", "3\n", "\n", "3\n", "\n", "\n", "1->3\n", "\n", "\n", "!d\n", "\u24ff\n", "\n", "\n", "2\n", "\n", "2\n", "\n", "\n", "1->2\n", "\n", "\n", "!c & d\n", "\u24ff\n", "\n", "\n", "3->1\n", "\n", "\n", "c & d\n", "\n", "\n", "3->3\n", "\n", "\n", "!d\n", "\n", "\n", "3->2\n", "\n", "\n", "!c & d\n", "\n", "\n", "2->1\n", "\n", "\n", "c\n", "\n", "\n", "2->2\n", "\n", "\n", "!c\n", "\n", "\n", "4->4\n", "\n", "\n", "1\n", "\n", "\n", "" ], "text": [ "" ] } ], "prompt_number": 4 }, { "cell_type": "code", "collapsed": false, "input": [ "f = spot.formula('a U b'); f" ], "language": "python", "metadata": {}, "outputs": [ { "latex": [ "$a \\mathbin{\\mathsf{U}} b$" ], "metadata": {}, "output_type": "pyout", "prompt_number": 5, "text": [ "a U b" ] } ], "prompt_number": 5 }, { "cell_type": "code", "collapsed": false, "input": [ "spot.translate(f)" ], "language": "python", "metadata": {}, "outputs": [ { "metadata": {}, "output_type": "pyout", "prompt_number": 6, "svg": [ "\n", "\n", "\n", "\n", "\n", "\n", "G\n", "\n", "\n", "\n", "1\n", "\n", "1\n", "\n", "\n", "I->1\n", "\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "a & !b\n", "\n", "\n", "0\n", "\n", "0\n", "\u24ff\n", "\n", "\n", "1->0\n", "\n", "\n", "b\n", "\n", "\n", "0->0\n", "\n", "\n", "1\n", "\n", "\n", "\n" ], "text": [ " *' at 0x7f87301b6990> >" ] } ], "prompt_number": 6 }, { "cell_type": "code", "collapsed": false, "input": [ "f.translate()" ], "language": "python", "metadata": {}, "outputs": [ { "metadata": {}, "output_type": "pyout", "prompt_number": 7, "svg": [ "\n", "\n", "\n", "\n", "\n", "\n", "G\n", "\n", "\n", "\n", "1\n", "\n", "1\n", "\n", "\n", "I->1\n", "\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "a & !b\n", "\n", "\n", "0\n", "\n", "0\n", "\u24ff\n", "\n", "\n", "1->0\n", "\n", "\n", "b\n", "\n", "\n", "0->0\n", "\n", "\n", "1\n", "\n", "\n", "\n" ], "text": [ " *' at 0x7f87301b6bd0> >" ] } ], "prompt_number": 7 }, { "cell_type": "code", "collapsed": false, "input": [ "f.translate('mon')" ], "language": "python", "metadata": {}, "outputs": [ { "metadata": {}, "output_type": "pyout", "prompt_number": 8, "svg": [ "\n", "\n", "\n", "\n", "\n", "\n", "G\n", "\n", "\n", "\n", "1\n", "\n", "1\n", "\n", "\n", "I->1\n", "\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "a & !b\n", "\n", "\n", "0\n", "\n", "0\n", "\n", "\n", "1->0\n", "\n", "\n", "b\n", "\n", "\n", "0->0\n", "\n", "\n", "1\n", "\n", "\n", "\n" ], "text": [ " *' at 0x7f87301b6a20> >" ] } ], "prompt_number": 8 }, { "cell_type": "code", "collapsed": false, "input": [ "f = spot.formula('Ga | Gb | Gc'); f" ], "language": "python", "metadata": {}, "outputs": [ { "latex": [ "$\\mathsf{G} a \\lor \\mathsf{G} b \\lor \\mathsf{G} c$" ], "metadata": {}, "output_type": "pyout", "prompt_number": 9, "text": [ "Ga | Gb | Gc" ] } ], "prompt_number": 9 }, { "cell_type": "code", "collapsed": false, "input": [ "f.translate('ba', 'small').show('v')" ], "language": "python", "metadata": {}, "outputs": [ { "metadata": {}, "output_type": "pyout", "prompt_number": 10, "svg": [ "\n", "\n", "G\n", "\n", "\n", "\n", "0\n", "\n", "0\n", "\n", "\n", "I->0\n", "\n", "\n", "\n", "\n", "1\n", "\n", "\n", "1\n", "\n", "\n", "0->1\n", "\n", "\n", "c\n", "\n", "\n", "2\n", "\n", "\n", "2\n", "\n", "\n", "0->2\n", "\n", "\n", "a\n", "\n", "\n", "3\n", "\n", "\n", "3\n", "\n", "\n", "0->3\n", "\n", "\n", "b\n", "\n", "\n", "1->1\n", "\n", "\n", "c\n", "\n", "\n", "2->2\n", "\n", "\n", "a\n", "\n", "\n", "3->3\n", "\n", "\n", "b\n", "\n", "\n", "" ], "text": [ "" ] } ], "prompt_number": 10 }, { "cell_type": "code", "collapsed": false, "input": [ "f.translate('ba', 'det').show('v.')" ], "language": "python", "metadata": {}, "outputs": [ { "metadata": {}, "output_type": "pyout", "prompt_number": 11, "svg": [ "\n", "\n", "G\n", "\n", "\n", "\n", "6\n", "\n", "6\n", "\u24ff\n", "\n", "\n", "I->6\n", "\n", "\n", "\n", "\n", "6->6\n", "\n", "\n", "a & b & c\n", "\n", "\n", "0\n", "\n", "0\n", "\u24ff\n", "\n", "\n", "6->0\n", "\n", "\n", "!a & !b & c\n", "\n", "\n", "1\n", "\n", "1\n", "\u24ff\n", "\n", "\n", "6->1\n", "\n", "\n", "!a & b & !c\n", "\n", "\n", "2\n", "\n", "2\n", "\u24ff\n", "\n", "\n", "6->2\n", "\n", "\n", "a & !b & !c\n", "\n", "\n", "3\n", "\n", "3\n", "\u24ff\n", "\n", "\n", "6->3\n", "\n", "\n", "!a & b & c\n", "\n", "\n", "4\n", "\n", "4\n", "\u24ff\n", "\n", "\n", "6->4\n", "\n", "\n", "a & b & !c\n", "\n", "\n", "5\n", "\n", "5\n", "\u24ff\n", "\n", "\n", "6->5\n", "\n", "\n", "a & !b & c\n", "\n", "\n", "0->0\n", "\n", "\n", "c\n", "\n", "\n", "1->1\n", "\n", "\n", "b\n", "\n", "\n", "2->2\n", "\n", "\n", "a\n", "\n", "\n", "3->0\n", "\n", "\n", "!b & c\n", "\n", "\n", "3->1\n", "\n", "\n", "b & !c\n", "\n", "\n", "3->3\n", "\n", "\n", "b & c\n", "\n", "\n", "4->1\n", "\n", "\n", "!a & b\n", "\n", "\n", "4->2\n", "\n", "\n", "a & !b\n", "\n", "\n", "4->4\n", "\n", "\n", "a & b\n", "\n", "\n", "5->0\n", "\n", "\n", "!a & c\n", "\n", "\n", "5->2\n", "\n", "\n", "a & !c\n", "\n", "\n", "5->5\n", "\n", "\n", "a & c\n", "\n", "\n", "" ], "text": [ "" ] } ], "prompt_number": 11 }, { "cell_type": "code", "collapsed": false, "input": [ "a = spot.translate('F(a & X(!a &Xb))', pref=\"any\"); a" ], "language": "python", "metadata": {}, "outputs": [ { "metadata": {}, "output_type": "pyout", "prompt_number": 12, "svg": [ "\n", "\n", "\n", "\n", "\n", "\n", "G\n", "\n", "\n", "\n", "0\n", "\n", "0\n", "\n", "\n", "I->0\n", "\n", "\n", "\n", "\n", "0->0\n", "\n", "\n", "1\n", "\n", "\n", "1\n", "\n", "1\n", "\n", "\n", "0->1\n", "\n", "\n", "a\n", "\n", "\n", "2\n", "\n", "2\n", "\n", "\n", "1->2\n", "\n", "\n", "!a\n", "\n", "\n", "3\n", "\n", "3\n", "\n", "\n", "2->3\n", "\n", "\n", "b\n", "\u24ff\n", "\n", "\n", "3->3\n", "\n", "\n", "1\n", "\u24ff\n", "\n", "\n", "\n" ], "text": [ " *' at 0x7f87301b6cc0> >" ] } ], "prompt_number": 12 }, { "cell_type": "code", "collapsed": false, "input": [ "spot.sl(a)" ], "language": "python", "metadata": {}, "outputs": [ { "metadata": {}, "output_type": "pyout", "prompt_number": 13, "svg": [ "\n", "\n", "\n", "\n", "\n", "\n", "G\n", "\n", "\n", "\n", "0\n", "\n", "0\n", "\n", "\n", "I->0\n", "\n", "\n", "\n", "\n", "1\n", "\n", "1\n", "\n", "\n", "0->1\n", "\n", "\n", "a & b\n", "\n", "\n", "2\n", "\n", "2\n", "\n", "\n", "0->2\n", "\n", "\n", "!a & b\n", "\n", "\n", "3\n", "\n", "3\n", "\n", "\n", "0->3\n", "\n", "\n", "a & !b\n", "\n", "\n", "4\n", "\n", "4\n", "\n", "\n", "0->4\n", "\n", "\n", "!a & !b\n", "\n", "\n", "5\n", "\n", "5\n", "\n", "\n", "0->5\n", "\n", "\n", "a & b\n", "\n", "\n", "6\n", "\n", "6\n", "\n", "\n", "0->6\n", "\n", "\n", "a & !b\n", "\n", "\n", "1->1\n", "\n", "\n", "a & b\n", "\n", "\n", "1->2\n", "\n", "\n", "!a & b\n", "\n", "\n", "1->3\n", "\n", "\n", "a & !b\n", "\n", "\n", "1->4\n", "\n", "\n", "!a & !b\n", "\n", "\n", "1->5\n", "\n", "\n", "a & b\n", "\n", "\n", "1->6\n", "\n", "\n", "a & !b\n", "\n", "\n", "2->1\n", "\n", "\n", "a & b\n", "\n", "\n", "2->2\n", "\n", "\n", "!a & b\n", "\n", "\n", "2->3\n", "\n", "\n", "a & !b\n", "\n", "\n", "2->4\n", "\n", "\n", "!a & !b\n", "\n", "\n", "2->5\n", "\n", "\n", "a & b\n", "\n", "\n", "2->6\n", "\n", "\n", "a & !b\n", "\n", "\n", "3->1\n", "\n", "\n", "a & b\n", "\n", "\n", "3->2\n", "\n", "\n", "!a & b\n", "\n", "\n", "3->3\n", "\n", "\n", "a & !b\n", "\n", "\n", "3->4\n", "\n", "\n", "!a & !b\n", "\n", "\n", "3->5\n", "\n", "\n", "a & b\n", "\n", "\n", "3->6\n", "\n", "\n", "a & !b\n", "\n", "\n", "4->1\n", "\n", "\n", "a & b\n", "\n", "\n", "4->2\n", "\n", "\n", "!a & b\n", "\n", "\n", "4->3\n", "\n", "\n", "a & !b\n", "\n", "\n", "4->4\n", "\n", "\n", "!a & !b\n", "\n", "\n", "4->5\n", "\n", "\n", "a & b\n", "\n", "\n", "4->6\n", "\n", "\n", "a & !b\n", "\n", "\n", "5->5\n", "\n", "\n", "a & b\n", "\n", "\n", "7\n", "\n", "7\n", "\n", "\n", "5->7\n", "\n", "\n", "!a & b\n", "\n", "\n", "8\n", "\n", "8\n", "\n", "\n", "5->8\n", "\n", "\n", "!a & !b\n", "\n", "\n", "6->6\n", "\n", "\n", "a & !b\n", "\n", "\n", "6->7\n", "\n", "\n", "!a & b\n", "\n", "\n", "6->8\n", "\n", "\n", "!a & !b\n", "\n", "\n", "7->7\n", "\n", "\n", "!a & b\n", "\n", "\n", "9\n", "\n", "9\n", "\n", "\n", "7->9\n", "\n", "\n", "a & b\n", "\u24ff\n", "\n", "\n", "10\n", "\n", "10\n", "\n", "\n", "7->10\n", "\n", "\n", "!a & b\n", "\u24ff\n", "\n", "\n", "8->8\n", "\n", "\n", "!a & !b\n", "\n", "\n", "8->9\n", "\n", "\n", "a & b\n", "\u24ff\n", "\n", "\n", "8->10\n", "\n", "\n", "!a & b\n", "\u24ff\n", "\n", "\n", "9->9\n", "\n", "\n", "a & b\n", "\u24ff\n", "\n", "\n", "9->10\n", "\n", "\n", "!a & b\n", "\u24ff\n", "\n", "\n", "11\n", "\n", "11\n", "\n", "\n", "9->11\n", "\n", "\n", "a & !b\n", "\u24ff\n", "\n", "\n", "12\n", "\n", "12\n", "\n", "\n", "9->12\n", "\n", "\n", "!a & !b\n", "\u24ff\n", "\n", "\n", "10->9\n", "\n", "\n", "a & b\n", "\u24ff\n", "\n", "\n", "10->10\n", "\n", "\n", "!a & b\n", "\u24ff\n", "\n", "\n", "10->11\n", "\n", "\n", "a & !b\n", "\u24ff\n", "\n", "\n", "10->12\n", "\n", "\n", "!a & !b\n", "\u24ff\n", "\n", "\n", "11->9\n", "\n", "\n", "a & b\n", "\u24ff\n", "\n", "\n", "11->10\n", "\n", "\n", "!a & b\n", "\u24ff\n", "\n", "\n", "11->11\n", "\n", "\n", "a & !b\n", "\u24ff\n", "\n", "\n", "11->12\n", "\n", "\n", "!a & !b\n", "\u24ff\n", "\n", "\n", "12->9\n", "\n", "\n", "a & b\n", "\u24ff\n", "\n", "\n", "12->10\n", "\n", "\n", "!a & b\n", "\u24ff\n", "\n", "\n", "12->11\n", "\n", "\n", "a & !b\n", "\u24ff\n", "\n", "\n", "12->12\n", "\n", "\n", "!a & !b\n", "\u24ff\n", "\n", "\n", "\n" ], "text": [ " *' at 0x7f87301b6ba0> >" ] } ], "prompt_number": 13 } ], "metadata": {} } ] }