{
 "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+"
  },
  "name": ""
 },
 "nbformat": 3,
 "nbformat_minor": 0,
 "worksheets": [
  {
   "cells": [
    {
     "cell_type": "heading",
     "level": 1,
     "metadata": {},
     "source": [
      "Documentation for spot's randltl python binding"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": true,
     "input": [
      "import spot"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 1
    },
    {
     "cell_type": "heading",
     "level": 2,
     "metadata": {},
     "source": [
      "Basic usage"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Generate random formulas from specified atomic propositions:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.randltl(['a', 'b', 'c'])\n",
      "for i in range(3):\n",
      "    print(next(f))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "0\n",
        "0 R b\n",
        "F(XG(F!b M Fb) W (b R a))\n"
       ]
      }
     ],
     "prompt_number": 2
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Generate random formulas using 3 atomic propositions:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.randltl(3)\n",
      "for i in range(3):\n",
      "    print(next(f))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "0\n",
        "0 R p1\n",
        "F(XG(F!p1 M Fp1) W (p1 R p0))\n"
       ]
      }
     ],
     "prompt_number": 3
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "By default, there is no limit to the number of formulas generated.<br/>\n",
      "To specify a number of formulas:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.randltl(3, 4)\n",
      "for formula in f:\n",
      "    print(formula)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "0\n",
        "0 R p1\n",
        "F(XG(F!p1 M Fp1) W (p1 R p0))\n",
        "F(p0 R !p2)\n"
       ]
      }
     ],
     "prompt_number": 4
    },
    {
     "cell_type": "heading",
     "level": 2,
     "metadata": {},
     "source": [
      "Keyword arguments"
     ]
    },
    {
     "cell_type": "heading",
     "level": 2,
     "metadata": {},
     "source": [
      "seed"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Seed for the pseudo random number generator (default: 0)."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.randltl(3, seed=11)\n",
      "print(next(f))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "G(p1 U Gp0)\n"
       ]
      }
     ],
     "prompt_number": 5
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "output"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Type of formulas to output: 'ltl', 'psl', 'bool' or 'sere' (default: 'ltl')."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.randltl(3, output='psl', seed=332)\n",
      "print(next(f))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "{{p0 && p2}[*]}<>-> (Fp2 & Fp0)\n"
       ]
      }
     ],
     "prompt_number": 6
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "allow_dups"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Allow duplicate formulas (default: False)."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.randltl(1, allow_dups=True)\n",
      "print(next(f))\n",
      "print(next(f))\n",
      "print(next(f))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "0\n",
        "0\n",
        "Fp0\n"
       ]
      }
     ],
     "prompt_number": 7
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "tree_size"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Tree size of the formulas generated, before mandatory simplifications (default: 15)."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.randltl(3, tree_size=30, seed=11)\n",
      "print(next(f))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "G(((p0 U !Xp1) M Gp1) U Gp0)\n"
       ]
      }
     ],
     "prompt_number": 8
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "A range can be specified as a tuple:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.randltl(3, tree_size=(1, 40))\n",
      "print(next(f))\n",
      "print(next(f))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "X!(Gp1 M p2) R (!p2 M Xp1)\n",
        "F(G(F(Gp0 R (1 U Fp2)) M (p2 -> Gp0)) M F((p0 | Fp0) W Gp2))\n"
       ]
      }
     ],
     "prompt_number": 9
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "boolean_priorities, ltl_priorities, sere_priorities, dump_priorities"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.randltl(3, output='bool', boolean_priorities='and=10,or=0')\n",
      "for i in range(5):\n",
      "    print(next(f))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "0\n",
        "!p2 & (p1 <-> p2)\n",
        "p2\n",
        "p0 & ((p1 & p2) <-> !(!p0 & p1 & p2))\n",
        "1\n"
       ]
      }
     ],
     "prompt_number": 10
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "To see which operators are available along with their default priorities:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.randltl(3, output='psl', dump_priorities=True)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "Use argument ltl_priorities=STRING to set the following LTL priorities:\n",
        "\n",
        "ap\t3\n",
        "false\t1\n",
        "true\t1\n",
        "not\t1\n",
        "F\t1\n",
        "G\t1\n",
        "X\t1\n",
        "Closure\t1\n",
        "equiv\t1\n",
        "implies\t1\n",
        "xor\t1\n",
        "R\t1\n",
        "U\t1\n",
        "W\t1\n",
        "M\t1\n",
        "and\t1\n",
        "or\t1\n",
        "EConcat\t1\n",
        "UConcat\t1\n",
        "\n",
        "Use argument sere_priorities=STRING to set the following SERE priorities:\n",
        "\n",
        "ap\t3\n",
        "false\t1\n",
        "true\t1\n",
        "not\t1\n",
        "F\t1\n",
        "G\t1\n",
        "X\t1\n",
        "Closure\t1\n",
        "equiv\t1\n",
        "implies\t1\n",
        "xor\t1\n",
        "R\t1\n",
        "U\t1\n",
        "W\t1\n",
        "M\t1\n",
        "and\t1\n",
        "or\t1\n",
        "EConcat\t1\n",
        "UConcat\t1\n",
        "eword\t1\n",
        "boolform\t1\n",
        "star\t1\n",
        "star_b\t1\n",
        "fstar\t1\n",
        "fstar_b\t1\n",
        "and\t1\n",
        "andNLM\t1\n",
        "or\t1\n",
        "concat\t1\n",
        "fusion\t1\n",
        "\n",
        "Use argument boolean_priorities=STRING to set the following Boolean formula priorities:\n",
        "\n",
        "ap\t3\n",
        "false\t1\n",
        "true\t1\n",
        "not\t1\n",
        "F\t1\n",
        "G\t1\n",
        "X\t1\n",
        "Closure\t1\n",
        "equiv\t1\n",
        "implies\t1\n",
        "xor\t1\n",
        "R\t1\n",
        "U\t1\n",
        "W\t1\n",
        "M\t1\n",
        "and\t1\n",
        "or\t1\n",
        "EConcat\t1\n",
        "UConcat\t1\n",
        "eword\t1\n",
        "boolform\t1\n",
        "star\t1\n",
        "star_b\t1\n",
        "fstar\t1\n",
        "fstar_b\t1\n",
        "and\t1\n",
        "andNLM\t1\n",
        "or\t1\n",
        "concat\t1\n",
        "fusion\t1\n",
        "ap\t3\n",
        "false\t1\n",
        "true\t1\n",
        "not\t1\n",
        "equiv\t1\n",
        "implies\t1\n",
        "xor\t1\n",
        "and\t1\n",
        "or\t1\n",
        "\n"
       ]
      }
     ],
     "prompt_number": 11
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "simplify"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "0           No rewriting<br/>\n",
      "1           basic rewritings and eventual/universal rules<br/>\n",
      "2           additional syntactic implication rules<br/>\n",
      "3         better implications using containment<br/>\n",
      "default: 3"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.randltl(3, simplify=0, seed=5)\n",
      "print(next(f))\n",
      "f = spot.randltl(3, simplify=3, seed=5)\n",
      "print(next(f))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "G!(!p1 & (Xp2 | F(p0 R Xp2)))\n",
        "G(p1 | (X!p2 & G(!p0 U X!p2)))\n"
       ]
      }
     ],
     "prompt_number": 12
    },
    {
     "cell_type": "heading",
     "level": 2,
     "metadata": {},
     "source": [
      "Filters and maps"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "most boolean functions found in the class formula can be used to filter the random formula generator like this:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.randltl(3, 20).is_syntactic_stutter_invariant()\n",
      "for formula in f:\n",
      "    print(formula)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "0\n",
        "0 R p2\n",
        "F(p0 R !p1)\n",
        "G(p0 | Fp2) W (FGp2 R !p2)\n",
        "(p2 R G!p1) | G(p2 U !p0)\n",
        "(p2 W p0) U p2\n",
        "F!G(!Gp1 W p1)\n",
        "G!p1 & (!((p2 & Fp1) M p1) U p1)\n"
       ]
      }
     ],
     "prompt_number": 13
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "likewise, functions from formula to formula can be applied to map the iterator:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.randltl(2, 6).remove_x()\n",
      "for formula in f:\n",
      "    print(formula)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "0\n",
        "!(F!p1 M 1)\n",
        "(Gp0 | Fp1) M 1\n",
        "F!(!p1 <-> FGp1)\n",
        "Gp1 U (p1 U GFp1)\n",
        "(!p1 U p1) U ((p0 & (p0 U (!p0 & (!p0 -> Fp1))) & ((!p1 U !p0) | (p1 U !p0))) | (!p0 & (!p0 U (p0 & (!p0 -> Fp1))) & ((!p1 U p0) | (p1 U p0))) | (p1 & (p1 U (!p1 & (!p0 -> Fp1))) & ((!p0 U !p1) | (p0 U !p1))) | (!p1 & (!p1 U (p1 & (!p0 -> Fp1))) & ((!p0 U p1) | (p0 U p1))) | ((!p0 -> Fp1) & (Gp0 | G!p0) & (Gp1 | G!p1)))\n"
       ]
      }
     ],
     "prompt_number": 14
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "You may have noticed that the return type of randltl is 'formulaiterator'.<br/>\n",
      "Since the boolean functions and the 'mapping' functions return an iterator of the same type, this means these operations can be chained like this:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.randltl(3, 20).is_syntactic_stutter_invariant().relabel(spot.Abc).simplify()\n",
      "for formula in f:\n",
      "    print(formula)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "0\n",
        "Ga\n",
        "F(a R !b)\n",
        "G(a | Fb) | (FGb R !b)\n",
        "G!b | G(a U !c)\n",
        "b U a\n",
        "0\n",
        "0\n"
       ]
      }
     ],
     "prompt_number": 15
    }
   ],
   "metadata": {}
  }
 ]
}