* tests/python/formulas.ipynb: Improve SONF example (fixes #578).
This commit is contained in:
Alexandre Duret-Lutz
parent
c5c3e905ae
commit
a826a4ae6f
1 changed files with 59 additions and 52 deletions
|
|
@ -10,7 +10,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 10,
|
||||
"execution_count": 1,
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
|
|
@ -27,7 +27,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 11,
|
||||
"execution_count": 2,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -39,7 +39,7 @@
|
|||
"spot.formula(\"p1 U (p2 R (p3 & !p4))\")"
|
||||
]
|
||||
},
|
||||
"execution_count": 11,
|
||||
"execution_count": 2,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -51,7 +51,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 12,
|
||||
"execution_count": 3,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -63,7 +63,7 @@
|
|||
"spot.formula(\"{a;first_match({b[*];c[+]}[:*3..5];b)}<>-> (c & GFb)\")"
|
||||
]
|
||||
},
|
||||
"execution_count": 12,
|
||||
"execution_count": 3,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -81,7 +81,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 13,
|
||||
"execution_count": 4,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -93,7 +93,7 @@
|
|||
"spot.formula(\"c & (a | b)\")"
|
||||
]
|
||||
},
|
||||
"execution_count": 13,
|
||||
"execution_count": 4,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -111,7 +111,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 14,
|
||||
"execution_count": 5,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -123,7 +123,7 @@
|
|||
"spot.formula(\"c & (a | b)\")"
|
||||
]
|
||||
},
|
||||
"execution_count": 14,
|
||||
"execution_count": 5,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -142,7 +142,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 15,
|
||||
"execution_count": 6,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -151,7 +151,7 @@
|
|||
"'p1 U (p2 R (p3 & !p4))'"
|
||||
]
|
||||
},
|
||||
"execution_count": 15,
|
||||
"execution_count": 6,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -169,7 +169,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 16,
|
||||
"execution_count": 7,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -201,7 +201,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 17,
|
||||
"execution_count": 8,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -237,7 +237,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 18,
|
||||
"execution_count": 9,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -299,7 +299,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 19,
|
||||
"execution_count": 10,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -308,7 +308,7 @@
|
|||
"True"
|
||||
]
|
||||
},
|
||||
"execution_count": 19,
|
||||
"execution_count": 10,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -319,7 +319,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 20,
|
||||
"execution_count": 11,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -328,7 +328,7 @@
|
|||
"False"
|
||||
]
|
||||
},
|
||||
"execution_count": 20,
|
||||
"execution_count": 11,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -346,7 +346,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 21,
|
||||
"execution_count": 12,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -355,7 +355,7 @@
|
|||
"True"
|
||||
]
|
||||
},
|
||||
"execution_count": 21,
|
||||
"execution_count": 12,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -366,7 +366,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 22,
|
||||
"execution_count": 13,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -375,7 +375,7 @@
|
|||
"False"
|
||||
]
|
||||
},
|
||||
"execution_count": 22,
|
||||
"execution_count": 13,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -386,7 +386,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 23,
|
||||
"execution_count": 14,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -395,7 +395,7 @@
|
|||
"True"
|
||||
]
|
||||
},
|
||||
"execution_count": 23,
|
||||
"execution_count": 14,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -413,7 +413,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 24,
|
||||
"execution_count": 15,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -425,7 +425,7 @@
|
|||
"spot.formula(\"\\\"a > b\\\" & \\\"proc[2]@init\\\" & GF_foo_\")"
|
||||
]
|
||||
},
|
||||
"execution_count": 24,
|
||||
"execution_count": 15,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -436,7 +436,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 25,
|
||||
"execution_count": 16,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -448,7 +448,7 @@
|
|||
"spot.formula(\"a & b & GFc\")"
|
||||
]
|
||||
},
|
||||
"execution_count": 25,
|
||||
"execution_count": 16,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -459,7 +459,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 26,
|
||||
"execution_count": 17,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -471,7 +471,7 @@
|
|||
"spot.formula(\"p0 & p1 & GFp2\")"
|
||||
]
|
||||
},
|
||||
"execution_count": 26,
|
||||
"execution_count": 17,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -489,7 +489,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 27,
|
||||
"execution_count": 18,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -710,7 +710,7 @@
|
|||
"<spot.jupyter.SVG object>"
|
||||
]
|
||||
},
|
||||
"execution_count": 27,
|
||||
"execution_count": 18,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -728,7 +728,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 28,
|
||||
"execution_count": 19,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -764,7 +764,7 @@
|
|||
"<spot.jupyter.SVG object>"
|
||||
]
|
||||
},
|
||||
"execution_count": 28,
|
||||
"execution_count": 19,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -775,7 +775,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 29,
|
||||
"execution_count": 20,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -784,7 +784,7 @@
|
|||
"'recurrence'"
|
||||
]
|
||||
},
|
||||
"execution_count": 29,
|
||||
"execution_count": 20,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -795,7 +795,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 30,
|
||||
"execution_count": 21,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -807,7 +807,7 @@
|
|||
"spot.formula(\"F(a & X(!a & b))\")"
|
||||
]
|
||||
},
|
||||
"execution_count": 30,
|
||||
"execution_count": 21,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -825,7 +825,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 31,
|
||||
"execution_count": 22,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -837,7 +837,7 @@
|
|||
"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": 31,
|
||||
"execution_count": 22,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -855,7 +855,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 32,
|
||||
"execution_count": 23,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -867,7 +867,7 @@
|
|||
"spot.formula(\"(0 R !(a <-> b)) -> (1 U (a <-> b))\")"
|
||||
]
|
||||
},
|
||||
"execution_count": 32,
|
||||
"execution_count": 23,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -879,7 +879,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 33,
|
||||
"execution_count": 24,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -891,7 +891,7 @@
|
|||
"spot.formula(\"(1 U ((a & b) | (!a & !b))) | !(0 R ((!a & b) | (a & !b)))\")"
|
||||
]
|
||||
},
|
||||
"execution_count": 33,
|
||||
"execution_count": 24,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
|
|
@ -909,7 +909,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 34,
|
||||
"execution_count": 25,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -945,7 +945,7 @@
|
|||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 35,
|
||||
"execution_count": 26,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -980,12 +980,12 @@
|
|||
"cell_type": "markdown",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Converting to Suffix Operator Normal Form:"
|
||||
"Converting to [Suffix Operator Normal Form](https://doi.org/10.1109/TCAD.2008.2003303):"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 36,
|
||||
"execution_count": 27,
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
|
|
@ -1003,10 +1003,10 @@
|
|||
{
|
||||
"data": {
|
||||
"text/latex": [
|
||||
"$\\mathsf{G} \\mathit{sonf\\_}_{0} \\land \\mathsf{G} (\\lnot \\mathit{sonf\\_}_{1} \\lor \\mathsf{F} a) \\land \\mathsf{G} (\\lnot \\mathit{sonf\\_}_{0} \\lor (\\{x^{\\star}\\}\\mathrel{\\Box\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} \\mathit{sonf\\_}_{1}))$"
|
||||
"$\\mathsf{G} p_{0} \\land \\mathsf{G} (\\lnot p_{1} \\lor \\mathsf{F} a) \\land \\mathsf{G} (\\lnot p_{0} \\lor (\\{x^{\\star}\\}\\mathrel{\\Box\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} p_{1}))$"
|
||||
],
|
||||
"text/plain": [
|
||||
"spot.formula(\"Gsonf_0 & G(!sonf_1 | Fa) & G(!sonf_0 | ({x[*]}[]-> sonf_1))\")"
|
||||
"spot.formula(\"Gp0 & G(!p1 | Fa) & G(!p0 | ({x[*]}[]-> p1))\")"
|
||||
]
|
||||
},
|
||||
"metadata": {},
|
||||
|
|
@ -1015,7 +1015,7 @@
|
|||
{
|
||||
"data": {
|
||||
"text/plain": [
|
||||
"('sonf_0', 'sonf_1')"
|
||||
"('p0', 'p1')"
|
||||
]
|
||||
},
|
||||
"metadata": {},
|
||||
|
|
@ -1027,10 +1027,17 @@
|
|||
"display(f)\n",
|
||||
"\n",
|
||||
"# In addition to the formula, returns a list of newly introduced APs\n",
|
||||
"f, aps = spot.suffix_operator_normal_form(f, 'sonf_')\n",
|
||||
"f, aps = spot.suffix_operator_normal_form(f, 'p')\n",
|
||||
"display(f)\n",
|
||||
"display(aps)"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": []
|
||||
}
|
||||
],
|
||||
"metadata": {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue