{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"from IPython.display import display, HTML\n",
"import spot\n",
"from spot.jupyter import display_inline # display multiple arguments side-by-side\n",
"import buddy\n",
"spot.setup(show_default='.tvb')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Anatomy of a product\n",
"\n",
"In this notebook, we write a Python function that constructs the product of two automata.\n",
"\n",
"This is obviously not a new feature: Spot can already make a product of two automata using its `product()` function. \n",
"For instance:"
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"
\n",
"\n",
"\n",
"\n",
"\n",
"
\n",
"\n",
"\n",
"\n",
"\n",
"
\n",
"\n",
"\n",
"\n",
"\n",
"
"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"a1 = spot.translate('FGa & GFb')\n",
"a2 = spot.translate('G(Fc U b)')\n",
"prod = spot.product(a1, a2)\n",
"display_inline(a1, a2, prod)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The builtin `spot.product()` function produces an automaton whose language is the intersection of the two input languages. It does so by building an automaton that keeps track of the runs in the two input automata. The states are labeled by pairs of input states so that we can more easily follow what is going on, but those labels are purely cosmetic. The acceptance condition is the conjunction of the two acceptance condition, but the acceptance sets of one input automaton have been shifted to not conflict with the other automaton.\n",
"\n",
"In fact, that automaton printer has an option to shift those sets in its output, and this is perfect for illustrating products. For instance `a.show('+3')` will display `a1` with all its acceptance sets shifted by 3. \n",
"\n",
"Let's define a function for displaying the three automata involved in a product, using this shift option so we can follow what is going on with the acceptance sets."
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"
\n",
"\n",
"\n",
"\n",
"\n",
"
\n",
"\n",
"\n",
"\n",
"\n",
"
\n",
"\n",
"\n",
"\n",
"\n",
"
"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"def show_prod(a1, a2, res):\n",
" s1 = a1.num_sets()\n",
" display_inline(a1, a2.show('.tvb+{}'.format(s1)), res)\n",
"\n",
"show_prod(a1, a2, prod)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Building a product\n",
"\n",
"Let's now rewrite `product()` in Python. We will do that in three steps.\n",
"\n",
"\n",
"## First attempt\n",
"\n",
"First, we build a product without taking care of the acceptance sets. We just want to get the general shape of the algorithm.\n",
"\n",
"We will build an automaton of type `twa_graph`, i.e., an automaton represented explicitely using a graph. In those automata, states are numbered by integers, starting from `0`. (Those states can also be given a different name, which is why the the `product()` shows us something that appears to be labeled by pairs, but the real identifier of each state is an integer.)\n",
"\n",
"We will use a dictionary to keep track of the association between a pair `(ls,rs)` of input states, and its number in the output."
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"
\n",
"\n",
"\n",
"\n",
"\n",
"
\n",
"\n",
"\n",
"\n",
"\n",
"
\n",
"\n",
"\n",
"\n",
"\n",
"
"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"def product1(left, right):\n",
" # A bdd_dict object associates BDD variables (that are \n",
" # used in BDDs labeleing the edges) to atomic propositions.\n",
" bdict = left.get_dict()\n",
" # If the two automata do not have the same BDD dict, then\n",
" # we cannot easily detect compatible transitions.\n",
" if right.get_dict() != bdict:\n",
" raise RuntimeError(\"automata should share their dictionary\")\n",
" \n",
" result = spot.make_twa_graph(bdict)\n",
" # This will be our state dictionary\n",
" sdict = {}\n",
" # The list of output states for which we have not yet\n",
" # computed the successors. Items on this list are triplets\n",
" # of the form (ls, rs, p) where ls,rs are the state number in\n",
" # the left and right automata, and p is the state number if\n",
" # the output automaton.\n",
" todo = []\n",
" # Transform a pair of state number (ls, rs) into a state number in\n",
" # the output automaton, creating a new state if needed. Whenever\n",
" # a new state is created, we can add it to todo.\n",
" def dst(ls, rs):\n",
" pair = (ls, rs)\n",
" p = sdict.get(pair)\n",
" if p is None:\n",
" p = result.new_state()\n",
" sdict[pair] = p\n",
" todo.append((ls, rs, p))\n",
" return p\n",
" \n",
" # Setup the initial state. It always exists.\n",
" result.set_init_state(dst(left.get_init_state_number(), \n",
" right.get_init_state_number()))\n",
"\n",
" # Build all states and edges in the product\n",
" while todo:\n",
" lsrc, rsrc, osrc = todo.pop()\n",
" for lt in left.out(lsrc):\n",
" for rt in right.out(rsrc):\n",
" cond = lt.cond & rt.cond\n",
" if cond != buddy.bddfalse:\n",
" result.new_edge(osrc, dst(lt.dst, rt.dst), cond)\n",
" return result\n",
"\n",
"p1 = product1(a1, a2)\n",
"show_prod(a1, a2, p1)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Besides the obvious lack of acceptance condition (which defaults to `t`) and acceptance sets, there is a less obvious problem: we never declared the set of atomic propositions used by the result automaton. This as two consequences:\n",
"- calling `p1.ap()` will return an empty set of atomic propositions"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"(spot.formula(\"a\"), spot.formula(\"b\"))\n",
"(spot.formula(\"c\"), spot.formula(\"b\"))\n",
"()\n"
]
}
],
"source": [
"print(a1.ap())\n",
"print(a2.ap())\n",
"print(p1.ap())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"- the `bdd_dict` instance that is shared by the three automata knows that the atomic propositions `a` and `b` are used by automata `a1` and that `b` and `c` are used by `a2`. But it is unaware of `p1`. That means that if we delete automata `a1` and `a2`, then the `bdd_dict` will release the associated BDD variables, and attempting to print automaton `p1` will either crash (because it uses bdd variables that are not associated to any atomic proposition) or display different atomic propositions (in case the BDD variables have been associated to different propositions in the meantime).\n",
"\n",
"These two issues are fixed by either calling `p1.register_ap(...)` for each atomic proposition, or in our case `p1.copy_ap_of(...)` to copy the atomic propositions of each input automaton. "
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Second attempt: a working product\n",
"\n",
"This fixes the list of atomtic propositions, as discussed above, and also sets the correct acceptance condition.\n",
"The `set_acceptance` method takes two arguments: a number of sets, and an acceptance function. In our case, both of these arguments are readily computed from the number of states and acceptance functions of the input automata."
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"
\n",
"\n",
"\n",
"\n",
"\n",
"
\n",
"\n",
"\n",
"\n",
"\n",
"
\n",
"\n",
"\n",
"\n",
"\n",
"
"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"(spot.formula(\"a\"), spot.formula(\"b\"), spot.formula(\"c\"))\n"
]
}
],
"source": [
"def product2(left, right):\n",
" bdict = left.get_dict()\n",
" if right.get_dict() != bdict:\n",
" raise RuntimeError(\"automata should share their dictionary\")\n",
" \n",
" result = spot.make_twa_graph(bdict)\n",
" # Copy the atomic propositions of the two input automata\n",
" result.copy_ap_of(left)\n",
" result.copy_ap_of(right)\n",
" \n",
" sdict = {}\n",
" todo = []\n",
" def dst(ls, rs):\n",
" pair = (ls, rs)\n",
" p = sdict.get(pair)\n",
" if p is None:\n",
" p = result.new_state()\n",
" sdict[pair] = p\n",
" todo.append((ls, rs, p))\n",
" return p\n",
" \n",
" result.set_init_state(dst(left.get_init_state_number(), \n",
" right.get_init_state_number()))\n",
"\n",
" # The acceptance sets of the right automaton will be shifted by this amount\n",
" shift = left.num_sets()\n",
" result.set_acceptance(shift + right.num_sets(),\n",
" left.get_acceptance() & (right.get_acceptance() << shift))\n",
" \n",
" while todo:\n",
" lsrc, rsrc, osrc = todo.pop()\n",
" for lt in left.out(lsrc):\n",
" for rt in right.out(rsrc):\n",
" cond = lt.cond & rt.cond\n",
" if cond != buddy.bddfalse:\n",
" # membership of this transitions to the new acceptance sets\n",
" acc = lt.acc | (rt.acc << shift)\n",
" result.new_edge(osrc, dst(lt.dst, rt.dst), cond, acc)\n",
" return result\n",
"\n",
"p2 = product2(a1, a2)\n",
"show_prod(a1, a2, p2)\n",
"print(p2.ap())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Third attempt: a more usable product\n",
"\n",
"We could stop with the previous function: the result is a correct product from a theoretical point of view. However our function is still inferior to `spot.product()` in a couple of points:\n",
"- states are not presented as pairs\n",
"- the properties of the resulting automaton are not set\n",
"\n",
"The former point could be addressed by calling `set_state_names()` and passing an array of strings: if a state number is smaller than the size of that array, then the string at that position will be displayed instead of the state number in the dot output. However we can do even better by using `set_product_states()` and passing an array of pairs of states. Besides the output routines, some algorithms actually retrieve this vector of pair of states to work on the product.\n",
"\n",
"Regarding the latter point, consider for instance the deterministic nature of these automata. In Spot an automaton is deterministic if it is both existential (no universal branching) and universal (no non-deterministic branching). In our case we will restrict the algorithm to existantial input (by asserting `is_existential()` on both operands), so we can consider that the `prop_universal()` property is an indication of determinism:"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"maybe\n",
"yes\n",
"maybe\n",
"maybe\n"
]
}
],
"source": [
"print(a1.prop_universal())\n",
"print(a2.prop_universal())\n",
"print(prod.prop_universal())\n",
"print(p1.prop_universal())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Because `a1` and `a2` are deterministic, their product is necessarily deterministic. This is a property that the `spot.product()` algorithm will preserve, but that our version does not *yet* preserve. We can fix that by adding\n",
"\n",
" if left.prop_universal() and right.prop_universal():\n",
" result.prop_universal(True)\n",
" \n",
"at the end of our function. Note that this is **not** the same as\n",
"\n",
" result.prop_universal(left.prop_universal() and right.prop_universal())\n",
"\n",
"because the results the `prop_*()` family of functions take and return instances of `spot.trival` values. These `spot.trival`, can, as their name implies, take one amongst three values representing `yes`, `no`, and `maybe`. `yes` and `no` should be used when we actually know that the automaton is deterministic or not (not deterministic meaning that there actually exists some non determinitic state in the automaton), and `maybe` when we do not know. \n",
"\n",
"The one-liner above is wrong for two reasons:\n",
"\n",
" - if `left` and `right` are non-deterministic, their product could be deterministic, so calling prop_universal(False) would be wrong. \n",
"\n",
" - the use of the `and` operator on `trival` is misleading in non-Boolean context. The `&` operator would be the correct operator to use if you want to work in threed-valued logic. Compare: "
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
" no & no = no no and no = no \n",
" no & maybe = no no and maybe = no \n",
" no & yes = no no and yes = no \n",
"maybe & no = no maybe and no = maybe\n",
"maybe & maybe = maybe maybe and maybe = maybe\n",
"maybe & yes = maybe maybe and yes = maybe\n",
" yes & no = no yes and no = no \n",
" yes & maybe = maybe yes and maybe = maybe\n",
" yes & yes = yes yes and yes = yes \n"
]
}
],
"source": [
"yes = spot.trival(True)\n",
"no = spot.trival(False)\n",
"maybe = spot.trival_maybe()\n",
"for u in (no, maybe, yes):\n",
" for v in (no, maybe, yes):\n",
" print(\"{u!s:>5} & {v!s:<5} = {r1!s:<5} {u!s:>5} and {v!s:<5} = {r2!s:<5}\"\n",
" .format(u=u, v=v, r1=(u&v), r2=(u and v)))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The reason `maybe and no` is equal to `maybe` is that Python evaluate it like `no if maybe else maybe`, but when a trival is evaluated in a Boolean context (as in `if maybe`) the result is True only if the trival is equal to yes.\n",
"\n",
"So our\n",
"\n",
" if left.prop_universal() and right.prop_universal():\n",
" result.prop_universal(True)\n",
"\n",
"is OK because the `if` body will only be entered of both input automata are known to be deterministic."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"However the question is in fact more general than just determinism: the product of two weak automata is weak, the product of two stutter-invariant automata is stutter-invariant, etc. So when writing an algorithm one should consider which of the [property bits](https://spot.lrde.epita.fr/hoa.html#property-bits) are naturally preserved by the algorithm, and set the relevant bits: this can save time later if the resulting automaton is used as input for another algorithm."
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"
\n",
"\n",
"\n",
"\n",
"\n",
"
\n",
"\n",
"\n",
"\n",
"\n",
"
\n",
"\n",
"\n",
"\n",
"\n",
"
"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"maybe\n"
]
}
],
"source": [
"def product3(left, right):\n",
" # the twa_graph.is_existential() method returns a Boolean, not a spot.trival\n",
" if not (left.is_existential() and right.is_existential()):\n",
" raise RuntimeError(\"alternating automata are not supported\")\n",
" bdict = left.get_dict()\n",
" if right.get_dict() != bdict:\n",
" raise RuntimeError(\"automata should share their dictionary\")\n",
" \n",
" result = spot.make_twa_graph(bdict)\n",
" result.copy_ap_of(left)\n",
" result.copy_ap_of(right)\n",
" \n",
" pairs = [] # our array of state pairs\n",
" sdict = {}\n",
" todo = []\n",
" def dst(ls, rs):\n",
" pair = (ls, rs)\n",
" p = sdict.get(pair)\n",
" if p is None:\n",
" p = result.new_state()\n",
" sdict[pair] = p\n",
" todo.append((ls, rs, p))\n",
" pairs.append((ls, rs)) # name each state\n",
" return p\n",
" \n",
" result.set_init_state(dst(left.get_init_state_number(), \n",
" right.get_init_state_number()))\n",
"\n",
" shift = left.num_sets()\n",
" result.set_acceptance(shift + right.num_sets(),\n",
" left.get_acceptance() & (right.get_acceptance() << shift))\n",
" \n",
" while todo:\n",
" lsrc, rsrc, osrc = todo.pop()\n",
" for lt in left.out(lsrc):\n",
" for rt in right.out(rsrc):\n",
" cond = lt.cond & rt.cond\n",
" if cond != buddy.bddfalse:\n",
" acc = lt.acc | (rt.acc << shift)\n",
" result.new_edge(osrc, dst(lt.dst, rt.dst), cond, acc)\n",
"\n",
" # Remember the origin of our states\n",
" result.set_product_states(pairs)\n",
" \n",
" # Loop over all the properties we want to preserve if they hold in both automata\n",
" for p in ('prop_universal', 'prop_complete', 'prop_weak', 'prop_inherently_weak', \n",
" 'prop_terminal', 'prop_stutter_invariant', 'prop_state_acc'):\n",
" if getattr(left, p)() and getattr(right, p)():\n",
" getattr(result, p)(True)\n",
" return result\n",
"\n",
"p3 = product3(a1, a2)\n",
"show_prod(a1, a2, p3)\n",
"print(p3.prop_universal())"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"For development, it is useful to know that we can force the automaton printer to show the real state numbers (not the pairs) by passing option `1`, and that we can retrieve the associated pairs ourselves. Note that the pairs also appear as tooltips when we mouse over the states."
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"0: (0, 0)\n",
"1: (0, 1)\n",
"2: (1, 0)\n",
"3: (1, 1)\n"
]
}
],
"source": [
"display(p3.show('.1'))\n",
"pairs = p3.get_product_states()\n",
"for s in range(p3.num_states()):\n",
" print(\"{}: {}\".format(s, pairs[s]))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Timings\n",
"\n",
"As an indication of how slow it is to implement such an algorithm using the Python bindings of Spot, consider the following comparison:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"%timeit product3(a1, a2)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"%timeit spot.product(a1, a2)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Depending on the machine where this notebook has been run, using the C++ version of the product can be 1 to 2 orders of magnitude faster. This is due to all the type conversions (converting Python types to C++ types) that occurs everytime a function/method of Spot is called from Python. When calling high-level C++ functions (such as `spot.product()`) from Python, the overhead is negligible because most of the time is spent on the C++ side, actually executing the function. However when calling low-level functions (such as `new_edge()`, `new_state()`, `out()`) most of the time is spent converting the arguments from Python to C++ and the results from C++ to Python.\n",
"\n",
"Despite that speed difference, Python can be useful to prototype an algorithm before implementing it in C++."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# The case of weak automata\n",
"\n",
"Finally, note that `spot.product()` actually does a bit more: it has some specializations for when one of the argument of the product is marked as weak (as indicated by `prop_weak()`). In this case, the resulting acceptance condition can be simplified a bit."
]
}
],
"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.5"
}
},
"nbformat": 4,
"nbformat_minor": 2
}