From 2927cf38acc860aeb72067780681856c7c61db45 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 16 Dec 2015 18:55:42 +0100 Subject: [PATCH] python: add some doc & tests for the acceptance bindings * wrap/python/tests/acc_cond.ipynb: New file. * wrap/python/tests/Makefile.am, doc/org/tut.org: Add it. * wrap/python/spot_impl.i: Add printer for acc_cond::mark_t. --- doc/org/tut.org | 2 + wrap/python/spot_impl.i | 21 +- wrap/python/tests/Makefile.am | 1 + wrap/python/tests/acc_cond.ipynb | 989 +++++++++++++++++++++++++++++++ 4 files changed, 1005 insertions(+), 8 deletions(-) create mode 100644 wrap/python/tests/acc_cond.ipynb diff --git a/doc/org/tut.org b/doc/org/tut.org index dc191f031..73db395fe 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -50,6 +50,8 @@ real notebooks instead. generated random automata, which are displayed in a table before and after acceptance simplification - [[https://spot.lrde.epita.fr/ipynb/accparse.html][accparse.ipynb]] exercises the acceptance condition parser +- [[https://spot.lrde.epita.fr/ipynb/acc_cond.html][acc_cond.ipynb]] documents the interface for manipulating acceptance + conditions - [[https://spot.lrde.epita.fr/ipynb/randltl.html][randltl.ipynb]] demonstrates a Python-version of [[file:randltl.org][=randltl=]] - [[https://spot.lrde.epita.fr/ipynb/decompose.html][decompose.ipynb]] illustrates the =decompose_strength()= function - [[https://spot.lrde.epita.fr/ipynb/testingaut.html][testingaut.ipynb]] shows the step necessary to build a testing diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 20385cb84..00e5f8616 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -441,14 +441,6 @@ namespace std { std::string __str__() { return spot::str_psl(*self); } } -%extend spot::acc_cond::mark_t { - // http://comments.gmane.org/gmane.comp.programming.swig/14822 - mark_t(const std::vector& f) - { - return new spot::acc_cond::mark_t(f.begin(), f.end()); - } -} - %extend spot::twa { void set_name(std::string name) { @@ -487,12 +479,25 @@ namespace std { } %extend spot::acc_cond::mark_t { + // http://comments.gmane.org/gmane.comp.programming.swig/14822 + mark_t(const std::vector& f) + { + return new spot::acc_cond::mark_t(f.begin(), f.end()); + } + std::string __str__() { std::ostringstream os; os << *self; return os.str(); } + + std::string __repr__() + { + std::ostringstream os; + os << *self; + return os.str(); + } } %extend spot::twa_run { diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am index 2e5e4cb19..1c3c45d8c 100644 --- a/wrap/python/tests/Makefile.am +++ b/wrap/python/tests/Makefile.am @@ -31,6 +31,7 @@ LOG_DRIVER = $(TEST_LOG_DRIVER) check_SCRIPTS = run TESTS = \ + acc_cond.ipynb \ accparse.ipynb \ accparse2.py \ alarm.py \ diff --git a/wrap/python/tests/acc_cond.ipynb b/wrap/python/tests/acc_cond.ipynb new file mode 100644 index 000000000..15c0af6c3 --- /dev/null +++ b/wrap/python/tests/acc_cond.ipynb @@ -0,0 +1,989 @@ +{ + "metadata": { + "name": "", + "signature": "sha256:f11212c3a17ce302ae81974af32b21c1ebda4aa54d8930f03787ce7ed1c9e5f5" + }, + "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` is via the `parse_acc_code()` function." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.parse_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.parse_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.parse_acc_code('Streett 2..4'))\n", + "print(spot.parse_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.parse_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.parse_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.parse_acc_code('Rabin 2')\n", + "y = spot.parse_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 `parse_acc_code()`, it is also possible to build a 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.parse_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.parse_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.parse_acc_code('Rabin 2'))\n", + "acc" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 34, + "text": [ + " >" + ] + } + ], + "prompt_number": 34 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "acc.num_sets()" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 35, + "text": [ + "4" + ] + } + ], + "prompt_number": 35 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "acc.get_acceptance()" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 36, + "text": [ + "(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))" + ] + } + ], + "prompt_number": 36 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "To be continued..." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 36 + } + ], + "metadata": {} + } + ] +} \ No newline at end of file