3bf3d2c8a1
* wrap/python/spot.i: Rename to... * wrap/python/spot_impl.i: ...this, and import spot_impl from spot.py so that it is not needed to recompile everything when modifying python code. * wrap/python/spot.py: Adding python functions to mirror the functionalities found in src/bin. * src/bin/common_r.cc: Move simplification level... * src/ltlvisit/simplify.hh: ... here as a constructor of ltl_simplifier_options, to make it available in wrap/python. * src/bin/ltlfilt.cc: Set simplification level using the new ltl_simplifier_options constructor. * src/bin/randltl.cc: Move most of the code... * src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh: ... here, as a class named randltlgenerator. * wrap/python/tests/bddnqueen.py, wrap/python/tests/minato.py: Avoid calling bdd_init twice by moving 'import spot' after bdd initialization. * wrap/python/Makefile.am: Rename spot to spot_impl * wrap/python/tests/Makefile.am: Add ipnbdoctest.py. * wrap/python/.gitignore: Rename spot.py to spot_impl.py * src/ltlvisit/tostring.cc: \ttrue and \ffalse should be \top and \bot. * wrap/python/tests/ipnbdoctest.py: Run code cells of a python notebook and compare the output to the actual content of the notebook. * wrap/python/tests/randltl.ipynb: Document and test randltl. * wrap/python/tests/run.in: Call ipnbdoctest.py to run ipython notebooks.
632 lines
No EOL
13 KiB
Text
632 lines
No EOL
13 KiB
Text
{
|
|
"metadata": {
|
|
"name": "",
|
|
"signature": "sha256:b16de2c9883c0fecb450f9d7f4885937abcfc1d1fef584d47109fcee13a68c9a"
|
|
},
|
|
"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": 12
|
|
},
|
|
{
|
|
"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": 26
|
|
},
|
|
{
|
|
"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": 27
|
|
},
|
|
{
|
|
"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 !Xp2) M Gp2) U Gp0)\n"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 29
|
|
},
|
|
{
|
|
"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!(Gp2 M p1) R (!p1 M Xp2)\n",
|
|
"F(G(F(Gp0 R (1 U Fp1)) M (p1 -> Gp0)) M F((p0 | Fp0) W Gp1))\n"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 30
|
|
},
|
|
{
|
|
"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",
|
|
"!p1 & (p1 <-> p2)\n",
|
|
"p1\n",
|
|
"p0 & ((p1 & p2) <-> !(!p0 & p1 & p2))\n",
|
|
"1\n"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 31
|
|
},
|
|
{
|
|
"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": 32
|
|
},
|
|
{
|
|
"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!(!p2 & (Xp1 | F(p0 R Xp1)))\n",
|
|
"G(p2 | (X!p1 & G(!p0 U X!p1)))\n"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 36
|
|
},
|
|
{
|
|
"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 p1\n",
|
|
"F(p0 R !p2)\n",
|
|
"G(p0 | Fp1) W (FGp1 R !p1)\n",
|
|
"(p1 R G!p2) | G(p1 U !p0)\n",
|
|
"(p1 W p0) U p1\n",
|
|
"F!G(!Gp2 W p2)\n",
|
|
"G!p2 & (!((p1 & Fp2) M p2) U p2)\n"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 40
|
|
},
|
|
{
|
|
"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",
|
|
"(Fp1 | Gp0) 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": 42
|
|
},
|
|
{
|
|
"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": 44
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": []
|
|
}
|
|
],
|
|
"metadata": {}
|
|
}
|
|
]
|
|
} |