{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"import spot\n",
"from spot.jupyter import display_inline\n",
"spot.setup(show_default='.a')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Containement checks\n",
"\n",
"The `spot.contains()` function checks whether the language of its right argument is included in the language of its left argument. The arguments may mix automata and formulas; the latter can be given as strings."
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [],
"source": [
"f = spot.formula('GFa'); aut_f = f.translate()\n",
"g = spot.formula('FGa'); aut_g = g.translate()"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(True, False)"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.contains(f, g), spot.contains(g, f)"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(True, False)"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.contains(aut_f, aut_g), spot.contains(aut_g, aut_f)"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(True, False)"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.contains(aut_f, g), spot.contains(aut_g, f)"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(True, False)"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.contains(f, aut_g), spot.contains(g, aut_f)"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(True, False)"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.contains(\"GFa\", aut_g), spot.contains(\"FGa\", aut_f)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Those functions are also usable as methods:"
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(True, False)"
]
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"f.contains(aut_g), g.contains(aut_f)"
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(True, False)"
]
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"aut_f.contains(\"FGa\"), aut_g.contains(\"GFa\")"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Equivalence checks\n",
"\n",
"The `spot.are_equivalent()` tests the equivalence of the languages of its two arguments. Note that the corresponding method is called `equivalent_to()`."
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(False, False)"
]
},
"execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.are_equivalent(f, g), spot.are_equivalent(aut_f, aut_g)"
]
},
{
"cell_type": "code",
"execution_count": 11,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(False, False)"
]
},
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"f.equivalent_to(aut_g), aut_f.equivalent_to(g)"
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"aut_f.equivalent_to('XXXGFa')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Containement checks between formulas with cache\n",
"\n",
"In the case of containement checks between formulas, `language_containement_checker` instances provide similar services, but they cache automata representing the formulas checked. This should be prefered when performing several containement checks using the same formulas."
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {},
"outputs": [],
"source": [
"lcc = spot.language_containment_checker()"
]
},
{
"cell_type": "code",
"execution_count": 14,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(True, False)"
]
},
"execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"lcc.contains(f, g), lcc.contains(g, f)"
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"False"
]
},
"execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"lcc.are_equivalent(f, g)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Help for distinguishing languages\n",
"\n",
"Assume you have computed two automata, that `are_equivalent(a1, a2)` returns `False`, and you want to know why. (This often occur when debugging some algorithm that produce an automaton that is not equivalent to which it should.) The automaton class has a method called `a1.exclusive_run(a2)` that can help with this task: it returns a run that recognizes a word is is accepted by one of the two automata but not by both. The method `a1.exclusive_run(a2)` will return just a word.\n",
"\n",
"For instance let's find a word that is exclusive between `aut_f` and `aut_g`. (The adjective *exlusive* is a reference to the *exclusive or* operator: the word belongs to L(aut_f) \"xor\" it belongs to L(aut_g).)"
]
},
{
"cell_type": "code",
"execution_count": 16,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"cycle{a; !a}"
]
},
"execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"aut_f.exclusive_word(aut_g)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We can even write a small function that highlights one difference between two automata. Note that the `run` returned will belong to either `left` or `right`, so calling the `highlight()` method will colorize one of those two automata."
]
},
{
"cell_type": "code",
"execution_count": 17,
"metadata": {},
"outputs": [],
"source": [
"def show_one_difference(left, right):\n",
" run = left.exclusive_run(right)\n",
" if not run:\n",
" print(\"The two automata are equivalent.\")\n",
" else:\n",
" print(\"The following word is only accepted by one automaton:\", spot.make_twa_word(run))\n",
" run.highlight(5)\n",
" display_inline(left, right)"
]
},
{
"cell_type": "code",
"execution_count": 18,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"The following word is only accepted by one automaton: cycle{!a; a; !a}\n"
]
},
{
"data": {
"text/html": [
"\n",
"\n",
"\n",
"\n",
"
\n",
"
\n",
"\n",
"\n",
"\n",
"
\n",
"