alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/wrap/python/tests/randltl.ipynb
Alexandre Duret-Lutz 9689c4ccfc python: update the formulaiterator bindings 
* wrap/python/spot.py: Add the unabbreviate() method, and
remove unabbrivate_ltl() and get_literal().
* wrap/python/tests/randltl.ipynb: Demonstrate unabbreviate().
2015-10-18 11:54:51 +02:00

677 lines
No EOL
15 KiB
Text
Raw Blame History

{
"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": "",
"signature": "sha256:b69bb80f870979f9654dbf2c1bcc0f26f652956e1f1ea4189d5c8078caa067c6"
},
"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": [
"Since the boolean filters and mapping functions return an iterator of the same type, 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
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"for formula in spot.randltl(3, 10).simplify().unabbreviate(\"WMGFR\"): print(formula)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"0\n",
"!(1 U !p1)\n",
"1 U ((p0 U ((p0 & p1) | (p1 R p0))) | !(1 U !((1 U !p1) & (1 U p1))))\n",
"1 U (!p2 U ((p0 & !p2) | (p0 R !p2)))\n",
"(!p1 U (((1 U !(1 U !p1)) R !p1) | (!p1 & (1 U !(1 U !p1))))) | !(1 U !(p0 | (1 U p1)))\n",
"X(p2 & X(p2 U (!p0 | (p2 W !p0))))\n",
"(1 U p2) | (X(!p2 | !(1 U !p2)) U ((1 U p2) U (!p1 & (1 U p2))))\n",
"XX!(1 U !((X!p1 U (!p2 U (!p0 & !p2))) | X!(1 U !p0)))\n",
"XX(1 U (p1 U ((p0 & p1) | (p0 R p1))))\n",
"p2 & Xp0\n"
]
}
],
"prompt_number": 16
},
{
"cell_type": "code",
"collapsed": false,
"input": [],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 16
}
],
"metadata": {}
}
]
}
Reference in a new issue View git blame Copy permalink