{
"cells": [
{
"cell_type": "markdown",
"id": "edc9ac7a",
"metadata": {},
"source": [
"In Spot, automata edges are labeled by Boolean functions over atomic propositions.\n",
"As a consequence, it is sometimes difficult to adapt algorithms that expect automata labeled by letters. This notebook presents methods that can be used to split those edge labels to make it easier to consider them as letters."
]
},
{
"cell_type": "code",
"execution_count": 10,
"id": "f9791763",
"metadata": {},
"outputs": [],
"source": [
"import spot\n",
"from spot.jupyter import display_inline\n",
"spot.setup(show_default=\".A\")"
]
},
{
"cell_type": "markdown",
"id": "81867c56",
"metadata": {},
"source": [
"Consider the labels appearing in the following automaton:"
]
},
{
"cell_type": "code",
"execution_count": 11,
"id": "28ab6c77",
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/html": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7f31fe0369d0> >"
]
},
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"aut = spot.translate(\"a & X(a->b) & XX(!a&!b&c)\")\n",
"aut"
]
},
{
"cell_type": "markdown",
"id": "dcd554c8",
"metadata": {},
"source": [
"We try to use the word \"edge\" to refer to an edge of the automaton, labeled by a Boolean formula over AP. These edges can be seen as representing several \"transitions\", each labeled by a valuation of all atomic propositions. So the above automaton uses 4 edges to represent 19 transitions"
]
},
{
"cell_type": "code",
"execution_count": 12,
"id": "3679412a",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"4 19\n"
]
}
],
"source": [
"s = spot.sub_stats_reachable(aut)\n",
"print(s.edges, s.transitions)"
]
},
{
"cell_type": "markdown",
"id": "0804e219",
"metadata": {},
"source": [
"We can split the edges into the corresponding transitions using `split_edges()`."
]
},
{
"cell_type": "code",
"execution_count": 13,
"id": "6f373fde",
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/html": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7f31fd7cfd20> >"
]
},
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"aut_split = spot.split_edges(aut)\n",
"aut_split"
]
},
{
"cell_type": "markdown",
"id": "101a7100",
"metadata": {},
"source": [
"The opposite operation is `merge_edges()`, but it works in place:"
]
},
{
"cell_type": "code",
"execution_count": 14,
"id": "cf014f95",
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/html": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7f31fd7cfd20> >"
]
},
"execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"aut_split.merge_edges()\n",
"aut_split"
]
},
{
"cell_type": "markdown",
"id": "2bc773cf",
"metadata": {},
"source": [
"Another way to split edges is `separate_edges()` this tweaks the labels so that any two labels can only be equal or disjoint. Note how this creates fewer edges."
]
},
{
"cell_type": "code",
"execution_count": 15,
"id": "3a130b23",
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/html": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7f31fd7cff90> >"
]
},
"execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.separate_edges(aut)"
]
},
{
"cell_type": "markdown",
"id": "3f523aba",
"metadata": {},
"source": [
"A slightly lower-level interface is the `edge_separator` class. This makes it possible to declare a \"basis\" (a set of labels) that will be used to separate the edge of an automaton.\n",
"\n",
"`separate_edges()` is actually implemented as follows:"
]
},
{
"cell_type": "code",
"execution_count": 16,
"id": "2716cc20",
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/html": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7f31fd7dcf00> >"
]
},
"execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"es = spot.edge_separator()\n",
"es.add_to_basis(aut) # create a basis from the labels of aut\n",
"es.separate_implying(aut) # replace labels by all labels of the basis that imply them"
]
},
{
"cell_type": "markdown",
"id": "9a46e347",
"metadata": {},
"source": [
"The `edge_separator` can also be used to separate the edges of *another* automaton:"
]
},
{
"cell_type": "code",
"execution_count": 19,
"id": "25d779a9",
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"
\n",
"\n",
"\n",
"\n",
"\n",
"
\n",
"\n",
"\n",
"\n",
"\n",
"
"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"aut2 = spot.translate('a W Gd')\n",
"# replace labels based on \"compatibility\" with those from the basis\n",
"aut2sep = es.separate_compat(aut2)\n",
"display_inline(aut2, aut2sep)"
]
},
{
"cell_type": "markdown",
"id": "d448df40",
"metadata": {},
"source": [
"Now, if we take any label A in `aut2sep` and any label B in `aut`, we necessarily \n",
"have A∧B ∈ {A,0}. I.e., either A implies B, or A and B are incompatible. This is useful in certain algorithm that want to check that the inclusion of on automaton in another one, because they can arange to onlu check the inclusion (with `bdd_implies`) of the labels from the small automaton into the labels of the larger automaton."
]
},
{
"cell_type": "markdown",
"id": "db0b203b",
"metadata": {},
"source": [
"We could also use `edge_separator` to create a combined basis for two automata:"
]
},
{
"cell_type": "code",
"execution_count": 20,
"id": "2de45a46",
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/html": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7f31fe037180> >"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/html": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7f31fd7dd2c0> >"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"es2 = spot.edge_separator()\n",
"es2.add_to_basis(aut)\n",
"es2.add_to_basis(aut2)\n",
"display(es2.separate_implying(aut), es2.separate_implying(aut2))"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "9f5035f7",
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3 (ipykernel)",
"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.11.8"
}
},
"nbformat": 4,
"nbformat_minor": 5
}