{
"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",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"import spot\n",
"import spot.gen as sg\n",
"spot.setup()\n",
"from IPython.display import display"
]
},
{
"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",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$\\mathsf{G} \\mathsf{F} p_{1} \\land \\mathsf{G} \\mathsf{F} p_{2} \\land \\mathsf{G} \\mathsf{F} p_{3}$"
],
"text/plain": [
"GFp1 & GFp2 & GFp3"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"sg.ltl_pattern(sg.LTL_AND_GF, 3)"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"text/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)$"
],
"text/plain": [
"F(p & Xp & XXp & XXXp) & F(q & Xq & XXq & XXXq)"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"sg.ltl_pattern(sg.LTL_CCJ_BETA_PRIME, 4)"
]
},
{
"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",
"execution_count": 4,
"metadata": {
"scrolled": false
},
"outputs": [
{
"data": {
"text/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})$"
],
"text/plain": [
"(GFp1 | FGp2) & (GFp2 | FGp3) & (GFp3 | FGp4)"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$\\mathsf{F} \\mathsf{G} p_{1}$"
],
"text/plain": [
"FGp1"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$\\mathsf{F} \\mathsf{G} p_{1} \\land \\mathsf{F} \\mathsf{G} p_{2}$"
],
"text/plain": [
"FGp1 & FGp2"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$\\mathsf{F} \\mathsf{G} p_{1} \\land \\mathsf{F} \\mathsf{G} p_{2} \\land \\mathsf{F} \\mathsf{G} p_{3}$"
],
"text/plain": [
"FGp1 & FGp2 & FGp3"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$p_{0} \\mathbin{\\mathsf{U}} (p_{1} \\land \\mathsf{G} p_{2})$"
],
"text/plain": [
"p0 U (p1 & Gp2)"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$p_{0} \\mathbin{\\mathsf{U}} (p_{1} \\land \\mathsf{X} (p_{2} \\mathbin{\\mathsf{U}} p_{3}))$"
],
"text/plain": [
"p0 U (p1 & X(p2 U p3))"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/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})))))$"
],
"text/plain": [
"p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$\\mathsf{F} (p_{0} \\land \\mathsf{X} \\mathsf{G} p_{1})$"
],
"text/plain": [
"F(p0 & XGp1)"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$\\mathsf{F} (p_{0} \\land \\mathsf{X} (p_{1} \\land \\mathsf{X} \\mathsf{F} p_{2}))$"
],
"text/plain": [
"F(p0 & X(p1 & XFp2))"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$\\mathsf{F} (p_{0} \\land \\mathsf{X} (p_{1} \\mathbin{\\mathsf{U}} p_{2}))$"
],
"text/plain": [
"F(p0 & X(p1 U p2))"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$\\mathsf{G} \\mathsf{F} p_{0} \\lor \\mathsf{F} \\mathsf{G} p_{1}$"
],
"text/plain": [
"GFp0 | FGp1"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$\\mathsf{G} (p_{0} \\rightarrow (p_{1} \\mathbin{\\mathsf{U}} p_{2}))$"
],
"text/plain": [
"G(p0 -> (p1 U p2))"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/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})))$"
],
"text/plain": [
"G(p0 & XF(p1 & XF(p2 & XFp3)))"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/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}$"
],
"text/plain": [
"GFp1 & GFp2 & GFp3 & GFp0 & GFp4"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/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}))$"
],
"text/plain": [
"(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1))"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/latex": [
"$\\mathsf{G} (p_{0} \\rightarrow (p_{1} \\mathbin{\\mathsf{U}} (\\mathsf{G} p_{2} \\lor \\mathsf{G} p_{3})))$"
],
"text/plain": [
"G(p0 -> (p1 U (Gp2 | Gp3)))"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"for f in sg.ltl_patterns((sg.LTL_GH_R, 3), (sg.LTL_AND_FG, 1, 3), sg.LTL_EH_PATTERNS):\n",
" display(f)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Automata patterns\n",
"\n",
"We currently have only a couple of generators of automata:"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"display(sg.aut_pattern(sg.AUT_KS_NCA, 3).show('.a'),\n",
" sg.aut_pattern(sg.AUT_L_DSA, 3).show('.a'),\n",
" sg.aut_pattern(sg.AUT_L_NBA, 3).show('.a'))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Multiple automata can be generated using the `aut_patterns()` function, which works similarly to `ltl_patterns()`."
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"3\n",
"5\n",
"7\n",
"9\n",
"11\n",
"13\n",
"15\n",
"17\n",
"19\n",
"21\n"
]
}
],
"source": [
"for aut in sg.aut_patterns(sg.AUT_KS_NCA):\n",
" print(aut.num_states())"
]
}
],
"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.6.5"
}
},
"nbformat": 4,
"nbformat_minor": 2
}