{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Handling LTL and PSL formulas\n",
"============================="
]
},
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"import spot\n",
"from IPython.display import display # not needed with recent Jupyter"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"For interactive use, formulas can be entered as text strings and passed to the `spot.formula` constructor."
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$p_{1} \\mathbin{\\mathsf{U}} (p_{2} \\mathbin{\\mathsf{R}} (p_{3} \\land \\lnot p_{4}))$"
],
"text/plain": [
"spot.formula(\"p1 U (p2 R (p3 & !p4))\")"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"f = spot.formula('p1 U p2 R (p3 & !p4)')\n",
"f"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$\\{a \\mathbin{\\mathsf{;}} b^{\\star} \\mathbin{\\mathsf{;}} c^+\\}\\mathrel{\\Diamond\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} (c \\land \\mathsf{G} \\mathsf{F} b)$"
],
"text/plain": [
"spot.formula(\"{a;b[*];c[+]}<>-> (c & GFb)\")"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"g = spot.formula('{a;b*;c[+]}<>->(GFb & c)'); g"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"By default the parser recognizes an infix syntax, but when this fails, it tries to read the formula with the [LBT](http://www.tcs.hut.fi/Software/maria/tools/lbt/) syntax:"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$c \\land (a \\lor b)$"
],
"text/plain": [
"spot.formula(\"c & (a | b)\")"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"h = spot.formula('& | a b c'); h"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Passing a `formula` to `spot.formula` simply returns the formula."
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$c \\land (a \\lor b)$"
],
"text/plain": [
"spot.formula(\"c & (a | b)\")"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.formula(h)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"By default, a formula object is presented using mathjax as above.\n",
"When a formula is converted to string you get Spot's syntax by default:"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"'p1 U (p2 R (p3 & !p4))'"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"str(f)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"If you prefer to print the string in another syntax, you may use the `to_str()` method, with an argument that indicates the output format to use. The `latex` format assumes that you will the define macros such as `\\U`, `\\R` to render all operators as you wish. On the otherhand, the `sclatex` (with `sc` for self-contained) format hard-codes the rendering of each of those operators: this is almost the same output that is used to render formulas using MathJax in a notebook. `sclatex` and `mathjax` only differ in the rendering of double-quoted atomic propositions."
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"spot p1 U (p2 R (p3 & !p4))\n",
"spin p1 U (p2 V (p3 && !p4))\n",
"lbt U p1 V p2 & p3 ! p4\n",
"wring (p1=1) U ((p2=1) R ((p3=1) * (p4=0)))\n",
"utf8 p1 U (p2 R (p3∧¬p4))\n",
"latex p_{1} \\U (p_{2} \\R (p_{3} \\land \\lnot p_{4}))\n",
"sclatex p_{1} \\mathbin{\\mathsf{U}} (p_{2} \\mathbin{\\mathsf{R}} (p_{3} \\land \\lnot p_{4}))\n",
"mathjax p_{1} \\mathbin{\\mathsf{U}} (p_{2} \\mathbin{\\mathsf{R}} (p_{3} \\land \\lnot p_{4}))\n"
]
}
],
"source": [
"for i in ['spot', 'spin', 'lbt', 'wring', 'utf8', 'latex', 'sclatex', 'mathjax']:\n",
" print(\"%-10s%s\" % (i, f.to_str(i)))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Formulas output via `format()` can also use some convenient shorthand to select the syntax:"
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Spin: p1 U (p2 V (p3 && !p4))\n",
"Spin+parentheses: (p1) U ((p2) V ((p3) && (!(p4))))\n",
"Spot (default): p1 U (p2 R (p3 & !p4))\n",
"Spot+shell quotes: 'p1 U (p2 R (p3 & !p4))'\n",
"LBT, right aligned: ~~~~~~~~~~~~~~~~~~~~~U p1 V p2 & p3 ! p4\n",
"LBT, no M/W/R: U p1 U & p3 ! p4 | & & p2 p3 ! p4 G & p3 ! p4\n"
]
}
],
"source": [
"print(\"\"\"\\\n",
"Spin: {0:s}\n",
"Spin+parentheses: {0:sp}\n",
"Spot (default): {0}\n",
"Spot+shell quotes: {0:q}\n",
"LBT, right aligned: {0:l:~>40}\n",
"LBT, no M/W/R: {0:[MWR]l}\"\"\".format(f))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The specifiers that can be used with `format` are documented as follows:"
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Help on function __format__ in module spot:\n",
"\n",
"__format__(self, spec)\n",
" Format the formula according to `spec`.\n",
" \n",
" Parameters\n",
" ----------\n",
" spec : str, optional\n",
" a list of letters that specify how the formula\n",
" should be formatted.\n",
" \n",
" Supported specifiers\n",
" --------------------\n",
" \n",
" - 'f': use Spot's syntax (default)\n",
" - '8': use Spot's syntax in UTF-8 mode\n",
" - 's': use Spin's syntax\n",
" - 'l': use LBT's syntax\n",
" - 'w': use Wring's syntax\n",
" - 'x': use LaTeX output\n",
" - 'X': use self-contained LaTeX output\n",
" - 'j': use self-contained LaTeX output, adjusted for MathJax\n",
" \n",
" Add some of those letters for additional options:\n",
" \n",
" - 'p': use full parentheses\n",
" - 'c': escape the formula for CSV output (this will\n",
" enclose the formula in double quotes, and escape\n",
" any included double quotes)\n",
" - 'h': escape the formula for HTML output\n",
" - 'd': escape double quotes and backslash,\n",
" for use in C-strings (the outermost double\n",
" quotes are *not* added)\n",
" - 'q': quote and escape for shell output, using single\n",
" quotes or double quotes depending on the contents.\n",
" - '[...]': rewrite away all the operators specified in brackets,\n",
" using spot.unabbreviate().\n",
" \n",
" - ':spec': pass the remaining specification to the\n",
" formating function for strings.\n",
"\n"
]
}
],
"source": [
"help(spot.formula.__format__)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"A `spot.formula` object has a number of built-in predicates whose value have been computed when the formula was constructed. For instance you can check whether a formula is in negative normal form using `is_in_nenoform()`, and you can make sure it is an LTL formula (i.e. not a PSL formula) using `is_ltl_formula()`:"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"f.is_in_nenoform() and f.is_ltl_formula()"
]
},
{
"cell_type": "code",
"execution_count": 11,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"False"
]
},
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"g.is_ltl_formula()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Similarly, `is_syntactic_stutter_invariant()` tells wether the structure of the formula guarranties it to be stutter invariant. For LTL formula, this means the `X` operator should not be used. For PSL formula, this function capture all formulas built using the [siPSL grammar](http://www.daxc.de/eth/paper/09atva.pdf)."
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"f.is_syntactic_stutter_invariant()"
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"False"
]
},
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.formula('{a[*];b}<>->c').is_syntactic_stutter_invariant()"
]
},
{
"cell_type": "code",
"execution_count": 14,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.formula('{a[+];b[*]}<>->d').is_syntactic_stutter_invariant()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"`spot.relabel` renames the atomic propositions that occur in a formula, using either letters, or numbered propositions:"
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$\\unicode{x201C}\\mathit{a > b}\\unicode{x201D} \\land \\unicode{x201C}\\mathit{proc[2]@init}\\unicode{x201D} \\land \\mathsf{G} \\mathsf{F} \\mathit{\\_foo\\_}$"
],
"text/plain": [
"spot.formula(\"\\\"a > b\\\" & \\\"proc[2]@init\\\" & GF_foo_\")"
]
},
"execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"gf = spot.formula('(GF_foo_) && \"a > b\" && \"proc[2]@init\"'); gf"
]
},
{
"cell_type": "code",
"execution_count": 16,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$a \\land b \\land \\mathsf{G} \\mathsf{F} c$"
],
"text/plain": [
"spot.formula(\"a & b & GFc\")"
]
},
"execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.relabel(gf, spot.Abc)"
]
},
{
"cell_type": "code",
"execution_count": 17,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$p_{0} \\land p_{1} \\land \\mathsf{G} \\mathsf{F} p_{2}$"
],
"text/plain": [
"spot.formula(\"p0 & p1 & GFp2\")"
]
},
"execution_count": 17,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.relabel(gf, spot.Pnn)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The AST of any formula can be displayed with `show_ast()`. Despite the name, this is not a tree but a DAG, because identical subtrees are merged. Binary operators have their left and right operands denoted with `L` and `R`, while non-commutative n-ary operators have their operands numbered."
]
},
{
"cell_type": "code",
"execution_count": 18,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"{a;b[*];c[+]}<>-> (c & GFb)\n"
]
},
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"execution_count": 18,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"print(g); g.show_ast()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Any formula can also be classified in the temporal hierarchy of Manna & Pnueli"
]
},
{
"cell_type": "code",
"execution_count": 19,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"execution_count": 19,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"g.show_mp_hierarchy()"
]
},
{
"cell_type": "code",
"execution_count": 20,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"'recurrence'"
]
},
"execution_count": 20,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.mp_class(g, 'v')"
]
},
{
"cell_type": "code",
"execution_count": 21,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$\\mathsf{F} (a \\land \\mathsf{X} (\\lnot a \\land b))$"
],
"text/plain": [
"spot.formula(\"F(a & X(!a & b))\")"
]
},
"execution_count": 21,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"f = spot.formula('F(a & X(!a & b))'); f"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Etessami's rule for removing X (valid only in stutter-invariant formulas)"
]
},
{
"cell_type": "code",
"execution_count": 22,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$\\mathsf{F} (a \\land ((a \\land (a \\mathbin{\\mathsf{U}} (\\lnot a \\land b)) \\land ((\\lnot b \\mathbin{\\mathsf{U}} \\lnot a) \\lor (b \\mathbin{\\mathsf{U}} \\lnot a))) \\lor (\\lnot a \\land (\\lnot a \\mathbin{\\mathsf{U}} (a \\land \\lnot a \\land b)) \\land ((\\lnot b \\mathbin{\\mathsf{U}} a) \\lor (b \\mathbin{\\mathsf{U}} a))) \\lor (b \\land (b \\mathbin{\\mathsf{U}} (\\lnot a \\land b \\land \\lnot b)) \\land ((\\lnot a \\mathbin{\\mathsf{U}} \\lnot b) \\lor (a \\mathbin{\\mathsf{U}} \\lnot b))) \\lor (\\lnot b \\land (\\lnot b \\mathbin{\\mathsf{U}} (\\lnot a \\land b)) \\land ((\\lnot a \\mathbin{\\mathsf{U}} b) \\lor (a \\mathbin{\\mathsf{U}} b))) \\lor (\\lnot a \\land b \\land (\\mathsf{G} \\lnot a \\lor \\mathsf{G} a) \\land (\\mathsf{G} \\lnot b \\lor \\mathsf{G} b))))$"
],
"text/plain": [
"spot.formula(\"F(a & ((a & (a U (!a & b)) & ((!b U !a) | (b U !a))) | (!a & (!a U (a & !a & b)) & ((!b U a) | (b U a))) | (b & (b U (!a & b & !b)) & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b)) & ((!a U b) | (a U b))) | (!a & b & (G!a | Ga) & (G!b | Gb))))\")"
]
},
"execution_count": 22,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.remove_x(f)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Removing abbreviated operators"
]
},
{
"cell_type": "code",
"execution_count": 23,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$(\\bot \\mathbin{\\mathsf{R}} \\lnot (a \\leftrightarrow b)) \\rightarrow (\\top \\mathbin{\\mathsf{U}} (a \\leftrightarrow b))$"
],
"text/plain": [
"spot.formula(\"(0 R !(a <-> b)) -> (1 U (a <-> b))\")"
]
},
"execution_count": 23,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"f = spot.formula(\"G(a xor b) -> F(a <-> b)\")\n",
"spot.unabbreviate(f, \"GF^\")"
]
},
{
"cell_type": "code",
"execution_count": 24,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$(\\top \\mathbin{\\mathsf{U}} ((a \\land b) \\lor (\\lnot a \\land \\lnot b))) \\lor \\lnot (\\bot \\mathbin{\\mathsf{R}} ((\\lnot a \\land b) \\lor (a \\land \\lnot b)))$"
],
"text/plain": [
"spot.formula(\"(1 U ((a & b) | (!a & !b))) | !(0 R ((!a & b) | (a & !b)))\")"
]
},
"execution_count": 24,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.unabbreviate(f, \"GF^ei\")"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Nesting level of operators"
]
},
{
"cell_type": "code",
"execution_count": 25,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"U 3\n",
"F 2\n",
"U 3\n",
"F 2\n",
"FU 4\n"
]
}
],
"source": [
"f = spot.formula('F(b & X(a U b U ((a W Fb) | (c U d))))')\n",
"print(\"U\", spot.nesting_depth(f, spot.op_U))\n",
"print(\"F\", spot.nesting_depth(f, spot.op_F))\n",
"# These following two are syntactic sugar for the above two\n",
"print(\"U\", spot.nesting_depth(f, \"U\"))\n",
"print(\"F\", spot.nesting_depth(f, \"F\"))\n",
"# If you want to consider \"U\" and \"F\" are a similar type of\n",
"# operator, you can count both with\n",
"print(\"FU\", spot.nesting_depth(f, \"FU\"))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Collecting the set of atomic propositions used by a formula:"
]
},
{
"cell_type": "code",
"execution_count": 26,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"spot.atomic_prop_set([spot.formula(\"a\"), spot.formula(\"b\"), spot.formula(\"c\"), spot.formula(\"d\")])\n",
"{\"a\", \"b\", \"c\", \"d\"}\n"
]
},
{
"data": {
"text/latex": [
"$\\{\\unicode{x201C}a\\unicode{x201D}, \\unicode{x201C}b\\unicode{x201D}, \\unicode{x201C}c\\unicode{x201D}, \\unicode{x201C}d\\unicode{x201D}\\}$"
],
"text/plain": [
"spot.atomic_prop_set([spot.formula(\"a\"), spot.formula(\"b\"), spot.formula(\"c\"), spot.formula(\"d\")])"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"ap = spot.atomic_prop_collect(f)\n",
"print(repr(ap)) # print as an atomic_prop_set object\n",
"print(ap) # print as a string\n",
"display(ap) # LaTeX-style, for notebooks"
]
}
],
"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.7.1"
}
},
"nbformat": 4,
"nbformat_minor": 2
}