{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"id": "4ea4978c",
"metadata": {},
"outputs": [],
"source": [
"import spot\n",
"from spot.jupyter import display_inline\n",
"from buddy import bdd_ithvar\n",
"spot.setup()"
]
},
{
"cell_type": "markdown",
"id": "4dc12445",
"metadata": {},
"source": [
"Aliases is a feature of the HOA format that allows Boolean formulas to be named and reused to label automata. This can be helpful to reduce the size of a file, but it can also be abused to \"fake\" arbitrary alphabets by using an alphabet of $n$ aliases encoded over $\\log_2(n)$ atomic propositions. \n",
"\n",
"Spot knows how to read HOA files containing aliases since version 2.0. However support for producing files with aliases was only added in version 2.11.\n",
"\n",
"When a HOA file containing aliases is read, the aliases are automatically expanded to define the automaton."
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "09bc3560",
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"
\n",
"\n",
"\n",
"\n",
"\n",
"
\n",
"\n",
"\n",
"\n",
"\n",
"
"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"a = spot.automaton(\"\"\"HOA: v1\n",
"States: 1\n",
"Start: 0\n",
"AP: 2 \"p0\" \"p1\"\n",
"Acceptance: 2 Inf(0)&Inf(1)\n",
"Alias: @a !0&!1\n",
"Alias: @b 0&!1\n",
"Alias: @c !0&1\n",
"Alias: @d 0&1\n",
"--BODY--\n",
"State: 0\n",
"[@a] 0\n",
"[@b] 0 {0}\n",
"[@c] 0 {1}\n",
"[@d] 0 {0 1}\n",
"--END--\n",
"\"\"\")\n",
"display_inline(a, a.show_storage(), per_row=2)"
]
},
{
"cell_type": "markdown",
"id": "593d8b93",
"metadata": {},
"source": [
"For more information about how to interpret the output of `show_storage()`, please see the `twagraph-internals.ipynb` notebook.\n",
"\n",
"Here, observe that the edges, labeled with aliases `@a`, `@b`, `@c`, and `@d` in the input file, actually store the expanded values of the aliases. Algorithms in Spot know nothing about the aliases, and only work with edges labeled by Boolean formulas of atomic propositions.\n",
"\n",
"However since Spot 2.11, the automaton now stores an `aliases` named-property. This property is used by the HOA printer to *attempt* to recreate edge labels using those aliases."
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "49b2efcb",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"HOA: v1\n",
"States: 1\n",
"Start: 0\n",
"AP: 2 \"p0\" \"p1\"\n",
"acc-name: generalized-Buchi 2\n",
"Acceptance: 2 Inf(0)&Inf(1)\n",
"properties: trans-labels explicit-labels trans-acc complete\n",
"properties: deterministic\n",
"Alias: @a !0&!1\n",
"Alias: @b 0&!1\n",
"Alias: @c !0&1\n",
"Alias: @d !@c&!@b&!@a\n",
"--BODY--\n",
"State: 0\n",
"[@a] 0\n",
"[@b] 0 {0}\n",
"[@c] 0 {1}\n",
"[@d] 0 {0 1}\n",
"--END--\n"
]
}
],
"source": [
"print(a.to_str('hoa'))"
]
},
{
"cell_type": "markdown",
"id": "6f93a48e",
"metadata": {},
"source": [
"Additionally, passing option `@` to the Dot printer will ask it to use aliases as well."
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "9802e266",
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
""
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"a.show('.@')"
]
},
{
"cell_type": "markdown",
"id": "3b9c1b57",
"metadata": {},
"source": [
"It should be noted that aside from input and output functions, algorithm do not care about aliases. In particular, they will not preserve the `aliases` property while creating a new automaton:"
]
},
{
"cell_type": "code",
"execution_count": 5,
"id": "e36d1446",
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
""
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"b = spot.degeneralize_tba(a)\n",
"b.show('.@')"
]
},
{
"cell_type": "markdown",
"id": "32483b2e",
"metadata": {},
"source": [
"This situation can be fixed by copying the aliases manually from the input automaton to the output automaton. (This is something that `autfilt` does by default, unless `--aliases=drop` is passed.)"
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "a9c0578c",
"metadata": {},
"outputs": [],
"source": [
"spot.set_aliases(b, spot.get_aliases(a))"
]
},
{
"cell_type": "code",
"execution_count": 7,
"id": "d3958e30",
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
""
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"b.show('.@')"
]
},
{
"cell_type": "markdown",
"id": "9a51f316",
"metadata": {},
"source": [
"Notice how `p0` and `!p0` were rewritten as disjunction of aliases because no direct aliases could be found for them. \n",
"\n",
"Generally, the display code tries to format formulas as a sum of product. It will recognize conjunctions and disjunctions of aliases, but if it fails, it will resort to printing the original atomic propositions (maybe mixed with aliases)."
]
},
{
"cell_type": "code",
"execution_count": 8,
"id": "f0dc410f",
"metadata": {},
"outputs": [],
"source": [
"a = spot.automaton(\"\"\"HOA: v1\n",
"States: 3\n",
"Start: 0\n",
"AP: 4 \"p0\" \"p1\" \"p2\" \"p3\"\n",
"Acceptance: 0 t\n",
"Alias: @a !0&!1\n",
"Alias: @b 0&!1\n",
"Alias: @c !0&1\n",
"Alias: @x 2&3\n",
"Alias: @y !2&!3\n",
"Alias: @z !2&3\n",
"--BODY--\n",
"State: 0\n",
"[@a&@x] 0\n",
"[@b&!@x] 1 \n",
"State: 1\n",
"[@c&@y] 0 \n",
"[!@c&!@y] 2 \n",
"State: 2\n",
"[(@a|@b)&@x] 2\n",
"[(@b|@c)&@x] 2\n",
"[@a|@b|@c] 0\n",
"--END--\n",
"\"\"\")"
]
},
{
"cell_type": "code",
"execution_count": 9,
"id": "d5366983",
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
""
]
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"a.show('.@')"
]
},
{
"cell_type": "markdown",
"id": "e1e89823",
"metadata": {},
"source": [
"The above shows that the aliasing may fail to recover some non-trivial aliases combinations. Look in particular at the loops above state 2. `(@b|@c)&@x`, was recovered as `(@x&@c)|(@x&@b)`, but for\n",
"`(@a|@b)&@x`, which is equivalent to `!p1&p2&p3`, the code failed to translate `!p1` as `@a|@b`, so it kept `!p1`.\n",
"\n",
"\n",
"When the automaton uses the `synthesis-outputs` property to distinguish in and out variables (see the `synthesis.ipnb` notebook for more details), aliasing is done on inputs and output separately."
]
},
{
"cell_type": "code",
"execution_count": 10,
"id": "0947b601",
"metadata": {},
"outputs": [],
"source": [
"spot.set_synthesis_outputs(a, bdd_ithvar(a.register_ap('p2')) & bdd_ithvar(a.register_ap('p3')))"
]
},
{
"cell_type": "code",
"execution_count": 11,
"id": "4290d8ca",
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
""
]
},
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"a.show('.@')"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "bcba9188",
"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.9.2"
}
},
"nbformat": 4,
"nbformat_minor": 5
}