11ca2803c9
* spot/gen/automata.hh, spot/gen/automata.cc: Hide ks_cobuchi() behind introduce aut_pattern(), as we have already done for the formulas. * bin/genaut.cc: Simplify using this interface. * python/spot/gen.i: Introduce aut_patterns(). * tests/python/gen.ipynb, tests/python/gen.py: Adjust.
545 lines
26 KiB
Text
545 lines
26 KiB
Text
{
|
|
"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.5.3"
|
|
},
|
|
"name": ""
|
|
},
|
|
"nbformat": 3,
|
|
"nbformat_minor": 0,
|
|
"worksheets": [
|
|
{
|
|
"cells": [
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"# Formulas & Automata generators\n",
|
|
"\n",
|
|
"The `spot.gen` package contains the functions used to generate the patterns produced by [`genltl`](https://spot.lrde.epita.fr/genltl.html) and [`genaut`](https://spot.lrde.epita.fr/genaut.html)."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"import spot\n",
|
|
"import spot.gen as sg\n",
|
|
"spot.setup()\n",
|
|
"from IPython.display import display"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"prompt_number": 1
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## LTL patterns\n",
|
|
"\n",
|
|
"Generation of LTL formulas is done via the `ltl_pattern()` function. This takes two arguments: a pattern id, and a pattern size (or index if the id refers to a list)."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"sg.ltl_pattern(sg.LTL_AND_GF, 3)"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"latex": [
|
|
"$\\mathsf{G} \\mathsf{F} p_{1} \\land \\mathsf{G} \\mathsf{F} p_{2} \\land \\mathsf{G} \\mathsf{F} p_{3}$"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "pyout",
|
|
"prompt_number": 2,
|
|
"text": [
|
|
"GFp1 & GFp2 & GFp3"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 2
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"sg.ltl_pattern(sg.LTL_CCJ_BETA_PRIME, 4)"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"latex": [
|
|
"$\\mathsf{F} (p \\land \\mathsf{X} p \\land \\mathsf{X} \\mathsf{X} p \\land \\mathsf{X} \\mathsf{X} \\mathsf{X} p) \\land \\mathsf{F} (q \\land \\mathsf{X} q \\land \\mathsf{X} \\mathsf{X} q \\land \\mathsf{X} \\mathsf{X} \\mathsf{X} q)$"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "pyout",
|
|
"prompt_number": 3,
|
|
"text": [
|
|
"F(p & Xp & XXp & XXXp) & F(q & Xq & XXq & XXXq)"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 3
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"To see the list of supported patterns, the easiest way is to look at the `--help` output of `genltl`. The above pattern for instance is attached to option `--ccj-beta-prime`. The name of the pattern identifier is the same using capital letters, underscores, and an `LTL_` prefix. If a pattern has multiple aliased options in `genltl`, the first one used for the identifier (e.g., `genltl` accept both `--dac-patterns` and `--spec-patterns` as synonyms to denote the patterns of `spot.gen.LTL_DAC_PATTERNS`).\n",
|
|
"\n",
|
|
"Multiple patterns can be generated using the `ltl_patterns()` function. It's arguments should be either can be:\n",
|
|
" - pairs of the form `(id, n)`: in this case the pattern `id` with size/index `n` is returned,\n",
|
|
" - triplets of the form `(id, min, max)`: in this case the patterns are output for all `n` between `min` and `max` included,\n",
|
|
" - an integer `id`: then this is equivalent to `(id, 1, 10)` if the pattern has now upper bound, or `(id, 1, upper)` if the patter `id` has an upper bound `upper`. This is mostly used when the pattern id correspond to a hard-coded list of formulas.\n",
|
|
"\n",
|
|
"Here is an example showing these three types of arguments:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"for f in sg.ltl_patterns((sg.LTL_GH_R, 3), (sg.LTL_AND_FG, 1, 3), sg.LTL_EH_PATTERNS):\n",
|
|
" display(f)"
|
|
],
|
|
"language": "python",
|
|
"metadata": {
|
|
"scrolled": false
|
|
},
|
|
"outputs": [
|
|
{
|
|
"latex": [
|
|
"$(\\mathsf{G} \\mathsf{F} p_{1} \\lor \\mathsf{F} \\mathsf{G} p_{2}) \\land (\\mathsf{G} \\mathsf{F} p_{2} \\lor \\mathsf{F} \\mathsf{G} p_{3}) \\land (\\mathsf{G} \\mathsf{F} p_{3} \\lor \\mathsf{F} \\mathsf{G} p_{4})$"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"(GFp1 | FGp2) & (GFp2 | FGp3) & (GFp3 | FGp4)"
|
|
]
|
|
},
|
|
{
|
|
"latex": [
|
|
"$\\mathsf{F} \\mathsf{G} p_{1}$"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"FGp1"
|
|
]
|
|
},
|
|
{
|
|
"latex": [
|
|
"$\\mathsf{F} \\mathsf{G} p_{1} \\land \\mathsf{F} \\mathsf{G} p_{2}$"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"FGp1 & FGp2"
|
|
]
|
|
},
|
|
{
|
|
"latex": [
|
|
"$\\mathsf{F} \\mathsf{G} p_{1} \\land \\mathsf{F} \\mathsf{G} p_{2} \\land \\mathsf{F} \\mathsf{G} p_{3}$"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"FGp1 & FGp2 & FGp3"
|
|
]
|
|
},
|
|
{
|
|
"latex": [
|
|
"$p_{0} \\mathbin{\\mathsf{U}} (p_{1} \\land \\mathsf{G} p_{2})$"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"p0 U (p1 & Gp2)"
|
|
]
|
|
},
|
|
{
|
|
"latex": [
|
|
"$p_{0} \\mathbin{\\mathsf{U}} (p_{1} \\land \\mathsf{X} (p_{2} \\mathbin{\\mathsf{U}} p_{3}))$"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"p0 U (p1 & X(p2 U p3))"
|
|
]
|
|
},
|
|
{
|
|
"latex": [
|
|
"$p_{0} \\mathbin{\\mathsf{U}} (p_{1} \\land \\mathsf{X} (p_{2} \\land \\mathsf{F} (p_{3} \\land \\mathsf{X} \\mathsf{F} (p_{4} \\land \\mathsf{X} \\mathsf{F} (p_{5} \\land \\mathsf{X} \\mathsf{F} p_{6})))))$"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))"
|
|
]
|
|
},
|
|
{
|
|
"latex": [
|
|
"$\\mathsf{F} (p_{0} \\land \\mathsf{X} \\mathsf{G} p_{1})$"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"F(p0 & XGp1)"
|
|
]
|
|
},
|
|
{
|
|
"latex": [
|
|
"$\\mathsf{F} (p_{0} \\land \\mathsf{X} (p_{1} \\land \\mathsf{X} \\mathsf{F} p_{2}))$"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"F(p0 & X(p1 & XFp2))"
|
|
]
|
|
},
|
|
{
|
|
"latex": [
|
|
"$\\mathsf{F} (p_{0} \\land \\mathsf{X} (p_{1} \\mathbin{\\mathsf{U}} p_{2}))$"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"F(p0 & X(p1 U p2))"
|
|
]
|
|
},
|
|
{
|
|
"latex": [
|
|
"$\\mathsf{G} \\mathsf{F} p_{0} \\lor \\mathsf{F} \\mathsf{G} p_{1}$"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"GFp0 | FGp1"
|
|
]
|
|
},
|
|
{
|
|
"latex": [
|
|
"$\\mathsf{G} (p_{0} \\rightarrow (p_{1} \\mathbin{\\mathsf{U}} p_{2}))$"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"G(p0 -> (p1 U p2))"
|
|
]
|
|
},
|
|
{
|
|
"latex": [
|
|
"$\\mathsf{G} (p_{0} \\land \\mathsf{X} \\mathsf{F} (p_{1} \\land \\mathsf{X} \\mathsf{F} (p_{2} \\land \\mathsf{X} \\mathsf{F} p_{3})))$"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"G(p0 & XF(p1 & XF(p2 & XFp3)))"
|
|
]
|
|
},
|
|
{
|
|
"latex": [
|
|
"$\\mathsf{G} \\mathsf{F} p_{1} \\land \\mathsf{G} \\mathsf{F} p_{2} \\land \\mathsf{G} \\mathsf{F} p_{3} \\land \\mathsf{G} \\mathsf{F} p_{0} \\land \\mathsf{G} \\mathsf{F} p_{4}$"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"GFp1 & GFp2 & GFp3 & GFp0 & GFp4"
|
|
]
|
|
},
|
|
{
|
|
"latex": [
|
|
"$(p_{0} \\mathbin{\\mathsf{U}} (p_{1} \\mathbin{\\mathsf{U}} p_{2})) \\lor (p_{1} \\mathbin{\\mathsf{U}} (p_{2} \\mathbin{\\mathsf{U}} p_{0})) \\lor (p_{2} \\mathbin{\\mathsf{U}} (p_{0} \\mathbin{\\mathsf{U}} p_{1}))$"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1))"
|
|
]
|
|
},
|
|
{
|
|
"latex": [
|
|
"$\\mathsf{G} (p_{0} \\rightarrow (p_{1} \\mathbin{\\mathsf{U}} (\\mathsf{G} p_{2} \\lor \\mathsf{G} p_{3})))$"
|
|
],
|
|
"metadata": {},
|
|
"output_type": "display_data",
|
|
"text": [
|
|
"G(p0 -> (p1 U (Gp2 | Gp3)))"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 4
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"# Automata patterns\n",
|
|
"\n",
|
|
"We currently have only one generator of automata:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"sg.aut_pattern(sg.AUT_KS_COBUCHI, 3).show('.a')"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"metadata": {},
|
|
"output_type": "pyout",
|
|
"prompt_number": 5,
|
|
"svg": [
|
|
"<svg height=\"295pt\" viewBox=\"0.00 0.00 734.00 295.41\" width=\"734pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
|
|
"<g class=\"graph\" id=\"graph0\" transform=\"scale(0.906173 0.906173) rotate(0) translate(4 322)\">\n",
|
|
"<title>G</title>\n",
|
|
"<polygon fill=\"white\" points=\"-4,4 -4,-322 806,-322 806,4 -4,4\" stroke=\"none\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"378.5\" y=\"-303.8\">Fin(</text>\n",
|
|
"<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"403.5\" y=\"-303.8\">\u24ff</text>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"419.5\" y=\"-303.8\">)</text>\n",
|
|
"<!-- I -->\n",
|
|
"<!-- 0 -->\n",
|
|
"<g class=\"node\" id=\"node2\"><title>0</title>\n",
|
|
"<ellipse cx=\"60\" cy=\"-127\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<ellipse cx=\"60\" cy=\"-127\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"60\" y=\"-123.3\">0</text>\n",
|
|
"</g>\n",
|
|
"<!-- I->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge1\"><title>I->0</title>\n",
|
|
"<path d=\"M1.16638,-127C2.84121,-127 16.884,-127 30.7112,-127\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"37.8555,-127 30.8556,-130.15 34.3555,-127 30.8555,-127 30.8555,-127 30.8555,-127 34.3555,-127 30.8555,-123.85 37.8555,-127 37.8555,-127\" stroke=\"black\"/>\n",
|
|
"</g>\n",
|
|
"<!-- 1 -->\n",
|
|
"<g class=\"node\" id=\"node3\"><title>1</title>\n",
|
|
"<ellipse cx=\"177\" cy=\"-244\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"177\" y=\"-240.3\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge2\"><title>0->1</title>\n",
|
|
"<path d=\"M64.3012,-148.616C68.7209,-170.194 78.6392,-202.826 100,-222 114.183,-234.731 135.317,-240.125 151.701,-242.394\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"158.853,-243.233 151.534,-245.546 155.377,-242.825 151.901,-242.418 151.901,-242.418 151.901,-242.418 155.377,-242.825 152.267,-239.289 158.853,-243.233 158.853,-243.233\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"120.5\" y=\"-243.8\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2 -->\n",
|
|
"<g class=\"node\" id=\"node4\"><title>2</title>\n",
|
|
"<ellipse cx=\"348\" cy=\"-187\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"348\" y=\"-183.3\">2</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge3\"><title>0->2</title>\n",
|
|
"<path d=\"M80.6443,-134.746C86.778,-136.976 93.6116,-139.271 100,-141 180.398,-162.766 278.283,-177.654 322.836,-183.815\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"330.019,-184.797 322.657,-186.97 326.551,-184.323 323.083,-183.849 323.083,-183.849 323.083,-183.849 326.551,-184.323 323.509,-180.728 330.019,-184.797 330.019,-184.797\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"177\" y=\"-165.8\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3 -->\n",
|
|
"<g class=\"node\" id=\"node5\"><title>3</title>\n",
|
|
"<ellipse cx=\"457\" cy=\"-135\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"457\" y=\"-131.3\">3</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge4\"><title>0->3</title>\n",
|
|
"<path d=\"M82.2369,-127.43C149.802,-128.799 359.56,-133.047 431.496,-134.504\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"438.797,-134.652 431.735,-137.659 435.298,-134.581 431.799,-134.51 431.799,-134.51 431.799,-134.51 435.298,-134.581 431.862,-131.36 438.797,-134.652 438.797,-134.652\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"262.5\" y=\"-135.8\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4 -->\n",
|
|
"<g class=\"node\" id=\"node6\"><title>4</title>\n",
|
|
"<ellipse cx=\"566\" cy=\"-89\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"566\" y=\"-85.3\">4</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge5\"><title>0->4</title>\n",
|
|
"<path d=\"M79.5054,-116.817C101.729,-105.561 140.464,-89 176,-89 176,-89 176,-89 458,-89 486.415,-89 519.075,-89 540.762,-89\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"547.951,-89 540.951,-92.1501 544.451,-89 540.951,-89.0001 540.951,-89.0001 540.951,-89.0001 544.451,-89 540.951,-85.8501 547.951,-89 547.951,-89\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"348\" y=\"-92.8\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5 -->\n",
|
|
"<g class=\"node\" id=\"node7\"><title>5</title>\n",
|
|
"<ellipse cx=\"675\" cy=\"-64\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"675\" y=\"-60.3\">5</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->5 -->\n",
|
|
"<g class=\"edge\" id=\"edge6\"><title>0->5</title>\n",
|
|
"<path d=\"M73.6216,-109.186C92.7218,-84.5283 131.496,-43 176,-43 176,-43 176,-43 567,-43 596.254,-43 629.179,-50.6519 650.683,-56.7178\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"657.517,-58.7008 649.916,-59.775 654.155,-57.7253 650.794,-56.7498 650.794,-56.7498 650.794,-56.7498 654.155,-57.7253 651.672,-53.7247 657.517,-58.7008 657.517,-58.7008\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"402.5\" y=\"-46.8\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 6 -->\n",
|
|
"<g class=\"node\" id=\"node8\"><title>6</title>\n",
|
|
"<ellipse cx=\"784\" cy=\"-64\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"784\" y=\"-60.3\">6</text>\n",
|
|
"</g>\n",
|
|
"<!-- 0->6 -->\n",
|
|
"<g class=\"edge\" id=\"edge7\"><title>0->6</title>\n",
|
|
"<path d=\"M67.626,-106.353C73.8972,-89.2423 84.6482,-65.0504 100,-48 126.732,-18.3106 136.049,-0 176,-0 176,-0 176,-0 676,-0 712.01,-0 746.404,-27.0268 766.075,-45.9541\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"771.222,-51.0486 764.031,-48.3631 768.735,-48.5865 766.247,-46.1243 766.247,-46.1243 766.247,-46.1243 768.735,-48.5865 768.463,-43.8855 771.222,-51.0486 771.222,-51.0486\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"457\" y=\"-3.8\">1</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->0 -->\n",
|
|
"<g class=\"edge\" id=\"edge8\"><title>1->0</title>\n",
|
|
"<path d=\"M165.954,-229.325C159.567,-220.812 150.692,-210.354 141,-203 125,-190.86 115.33,-196.974 100,-184 89.7476,-175.323 81.0004,-163.327 74.404,-152.576\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"70.7736,-146.426 77.0445,-150.853 72.5527,-149.44 74.3317,-152.454 74.3317,-152.454 74.3317,-152.454 72.5527,-149.44 71.619,-154.055 70.7736,-146.426 70.7736,-146.426\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"100\" y=\"-206.8\">!a & !b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge9\"><title>1->1</title>\n",
|
|
"<path d=\"M167.425,-259.541C164.73,-269.909 167.922,-280 177,-280 183.95,-280 187.45,-274.085 187.499,-266.659\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"186.575,-259.541 190.6,-266.077 187.026,-263.012 187.477,-266.483 187.477,-266.483 187.477,-266.483 187.026,-263.012 184.353,-266.889 186.575,-259.541 186.575,-259.541\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"160\" y=\"-283.8\">a & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 1->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge10\"><title>1->2</title>\n",
|
|
"<path d=\"M187.973,-229.425C194.214,-221.483 202.964,-212.233 213,-207 248.036,-188.73 294.791,-185.826 322.799,-185.988\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"329.836,-186.096 322.789,-189.138 326.337,-186.042 322.837,-185.989 322.837,-185.989 322.837,-185.989 326.337,-186.042 322.886,-182.839 329.836,-186.096 329.836,-186.096\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"213\" y=\"-210.8\">(!a & b) | (a & !b)</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge11\"><title>2->1</title>\n",
|
|
"<path d=\"M336.543,-201.086C330.263,-208.501 321.634,-217.057 312,-222 276.764,-240.079 230.071,-243.904 202.13,-244.398\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"195.11,-244.458 202.083,-241.248 198.61,-244.428 202.11,-244.398 202.11,-244.398 202.11,-244.398 198.61,-244.428 202.137,-247.548 195.11,-244.458 195.11,-244.458\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"244\" y=\"-246.8\">!a & b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->2 -->\n",
|
|
"<g class=\"edge\" id=\"edge12\"><title>2->2</title>\n",
|
|
"<path d=\"M338.767,-202.541C336.169,-212.909 339.246,-223 348,-223 354.702,-223 358.077,-217.085 358.124,-209.659\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"357.233,-202.541 361.229,-209.095 357.668,-206.014 358.103,-209.487 358.103,-209.487 358.103,-209.487 357.668,-206.014 354.977,-209.879 357.233,-202.541 357.233,-202.541\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"298.5\" y=\"-226.8\">(!a & !b) | (a & b)</text>\n",
|
|
"</g>\n",
|
|
"<!-- 2->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge13\"><title>2->3</title>\n",
|
|
"<path d=\"M364.788,-179.327C383.148,-170.405 413.562,-155.624 434.175,-145.607\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"440.495,-142.535 435.576,-148.428 437.347,-144.065 434.199,-145.595 434.199,-145.595 434.199,-145.595 437.347,-144.065 432.822,-142.762 440.495,-142.535 440.495,-142.535\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"384\" y=\"-171.8\">a & !b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->3 -->\n",
|
|
"<g class=\"edge\" id=\"edge14\"><title>3->3</title>\n",
|
|
"<path d=\"M447.767,-150.541C445.169,-160.909 448.246,-171 457,-171 463.702,-171 467.077,-165.085 467.124,-157.659\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"466.233,-150.541 470.229,-157.095 466.668,-154.014 467.103,-157.487 467.103,-157.487 467.103,-157.487 466.668,-154.014 463.977,-157.879 466.233,-150.541 466.233,-150.541\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"441.5\" y=\"-174.8\">!a | b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 3->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge15\"><title>3->4</title>\n",
|
|
"<path d=\"M473.788,-128.213C491.964,-120.399 521.954,-107.506 542.552,-98.6504\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"549.147,-95.8153 543.96,-101.474 545.932,-97.1977 542.716,-98.5801 542.716,-98.5801 542.716,-98.5801 545.932,-97.1977 541.472,-95.6861 549.147,-95.8153 549.147,-95.8153\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"493\" y=\"-121.8\">a & !b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->4 -->\n",
|
|
"<g class=\"edge\" id=\"edge16\"><title>4->4</title>\n",
|
|
"<path d=\"M556.767,-104.541C554.169,-114.909 557.246,-125 566,-125 572.702,-125 576.077,-119.085 576.124,-111.659\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"575.233,-104.541 579.229,-111.095 575.668,-108.014 576.103,-111.487 576.103,-111.487 576.103,-111.487 575.668,-108.014 572.977,-111.879 575.233,-104.541 575.233,-104.541\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"550.5\" y=\"-128.8\">!a | b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 4->5 -->\n",
|
|
"<g class=\"edge\" id=\"edge17\"><title>4->5</title>\n",
|
|
"<path d=\"M583.719,-85.0938C601.622,-80.9108 630.176,-74.2394 650.371,-69.5207\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"657.399,-67.8788 651.299,-72.5389 653.99,-68.6752 650.582,-69.4715 650.582,-69.4715 650.582,-69.4715 653.99,-68.6752 649.866,-66.4041 657.399,-67.8788 657.399,-67.8788\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"602\" y=\"-83.8\">a & !b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5->5 -->\n",
|
|
"<g class=\"edge\" id=\"edge18\"><title>5->5</title>\n",
|
|
"<path d=\"M665.767,-79.5414C663.169,-89.9087 666.246,-100 675,-100 681.702,-100 685.077,-94.0847 685.124,-86.6591\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"684.233,-79.5414 688.229,-86.0955 684.668,-83.0143 685.103,-86.4871 685.103,-86.4871 685.103,-86.4871 684.668,-83.0143 681.977,-86.8788 684.233,-79.5414 684.233,-79.5414\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"659.5\" y=\"-103.8\">!a | b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 5->6 -->\n",
|
|
"<g class=\"edge\" id=\"edge19\"><title>5->6</title>\n",
|
|
"<path d=\"M693.191,-64C710.897,-64 738.648,-64 758.616,-64\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"765.851,-64 758.851,-67.1501 762.351,-64 758.851,-64.0001 758.851,-64.0001 758.851,-64.0001 762.351,-64 758.851,-60.8501 765.851,-64 765.851,-64\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"711\" y=\"-67.8\">a & !b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 6->1 -->\n",
|
|
"<g class=\"edge\" id=\"edge20\"><title>6->1</title>\n",
|
|
"<path d=\"M782.177,-82.2688C778.801,-133.36 761.723,-274 676,-274 347,-274 347,-274 347,-274 287.12,-274 270.767,-275.766 213,-260 208.601,-258.799 204.06,-257.102 199.765,-255.257\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"193.275,-252.289 200.951,-252.336 196.458,-253.745 199.64,-255.2 199.64,-255.2 199.64,-255.2 196.458,-253.745 198.33,-258.065 193.275,-252.289 193.275,-252.289\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"493\" y=\"-277.8\">a & !b</text>\n",
|
|
"</g>\n",
|
|
"<!-- 6->6 -->\n",
|
|
"<g class=\"edge\" id=\"edge21\"><title>6->6</title>\n",
|
|
"<path d=\"M774.767,-79.5414C772.169,-89.9087 775.246,-100 784,-100 790.702,-100 794.077,-94.0847 794.124,-86.6591\" fill=\"none\" stroke=\"black\"/>\n",
|
|
"<polygon fill=\"black\" points=\"793.233,-79.5414 797.229,-86.0955 793.668,-83.0143 794.103,-86.4871 794.103,-86.4871 794.103,-86.4871 793.668,-83.0143 790.977,-86.8788 793.233,-79.5414 793.233,-79.5414\" stroke=\"black\"/>\n",
|
|
"<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"768.5\" y=\"-103.8\">!a | b</text>\n",
|
|
"</g>\n",
|
|
"</g>\n",
|
|
"</svg>"
|
|
],
|
|
"text": [
|
|
"<IPython.core.display.SVG object>"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 5
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"Multiple automata can be generated using the `aut_patterns()` function, which works similarly to `ltl_patterns()`."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": false,
|
|
"input": [
|
|
"for aut in sg.aut_patterns(sg.AUT_KS_COBUCHI):\n",
|
|
" print(aut.num_states())"
|
|
],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"output_type": "stream",
|
|
"stream": "stdout",
|
|
"text": [
|
|
"3\n",
|
|
"5\n",
|
|
"7\n",
|
|
"9\n",
|
|
"11\n",
|
|
"13\n",
|
|
"15\n",
|
|
"17\n",
|
|
"19\n",
|
|
"21\n"
|
|
]
|
|
}
|
|
],
|
|
"prompt_number": 6
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"collapsed": true,
|
|
"input": [],
|
|
"language": "python",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"prompt_number": null
|
|
}
|
|
],
|
|
"metadata": {}
|
|
}
|
|
]
|
|
}
|