In [1]:
from IPython.display import display, HTML
import spot
import buddy
spot.setup(show_default='.tavb')
def horiz(*args):
s = '<table><tr>'
for arg in args:
s += '<td style=\"vertical-align: top;\">' + arg.data + '</td>'
return HTML(s + '</tr></table>')
In [2]:
a1 = spot.translate('X(a W b)')
a2 = spot.translate('G(Fc U b)')
prod = spot.product(a1, a2)
horiz(a1.show(), a2.show(), prod.show())
Out[2]:
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.
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.
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.
In [3]:
def show_prod(a1, a2, res):
s1 = a1.num_sets()
display(horiz(a1.show(), a2.show('.tavb+{}'.format(s1)), res.show()))
show_prod(a1, a2, prod)
Let's now rewrite product() in Python. We will do that in three steps.
First, we build a product without taking care of the acceptance sets. We just want to get the general shape of the algorithm.
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.)
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.
In [4]:
def product1(left, right):
# A bdd_dict object associates BDD variables (that are
# used in BDDs labeleing the edges) to atomic propositions.
bdict = left.get_dict()
# If the two automata do not have the same BDD dict, then
# we cannot easily detect compatible transitions.
if right.get_dict() != bdict:
raise RuntimeError("automata should share their dictionary")
result = spot.make_twa_graph(bdict)
# This will be our state dictionary
sdict = {}
# The list of output states for which we have not yet
# computed the successors. Items on this list are triplets
# of the form (ls, rs, p) where ls,rs are the state number in
# the left and right automata, and p is the state number if
# the output automaton.
todo = []
# Transform a pair of state number (ls, rs) into a state number in
# the output automaton, creating a new state if needed. Whenever
# a new state is created, we can add it to todo.
def dst(ls, rs):
pair = (ls, rs)
p = sdict.get(pair)
if p is None:
p = result.new_state()
sdict[pair] = p
todo.append((ls, rs, p))
return p
# Setup the initial state. It always exists.
result.set_init_state(dst(left.get_init_state_number(),
right.get_init_state_number()))
# Build all states and edges in the product
while todo:
lsrc, rsrc, osrc = todo.pop()
for lt in left.out(lsrc):
for rt in right.out(rsrc):
cond = lt.cond & rt.cond
if cond != buddy.bddfalse:
result.new_edge(osrc, dst(lt.dst, rt.dst), cond)
return result
p1 = product1(a1, a2)
show_prod(a1, a2, p1)
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:
p1.ap() will return an empty set of atomic propositions
In [5]:
print(a1.ap())
print(a2.ap())
print(p1.ap())
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).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.
This fixes the list of atomtic propositions, as discussed above, and also sets the correct acceptance condition.
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.
In [6]:
def product2(left, right):
bdict = left.get_dict()
if right.get_dict() != bdict:
raise RuntimeError("automata should share their dictionary")
result = spot.make_twa_graph(bdict)
# Copy the atomic propositions of the two input automata
result.copy_ap_of(left)
result.copy_ap_of(right)
sdict = {}
todo = []
def dst(ls, rs):
pair = (ls, rs)
p = sdict.get(pair)
if p is None:
p = result.new_state()
sdict[pair] = p
todo.append((ls, rs, p))
return p
result.set_init_state(dst(left.get_init_state_number(),
right.get_init_state_number()))
# The acceptance sets of the right automaton will be shifted by this amount
shift = left.num_sets()
result.set_acceptance(shift + right.num_sets(),
left.get_acceptance() & (right.get_acceptance() << shift))
while todo:
lsrc, rsrc, osrc = todo.pop()
for lt in left.out(lsrc):
for rt in right.out(rsrc):
cond = lt.cond & rt.cond
if cond != buddy.bddfalse:
# membership of this transitions to the new acceptance sets
acc = lt.acc | (rt.acc << shift)
result.new_edge(osrc, dst(lt.dst, rt.dst), cond, acc)
return result
p2 = product2(a1, a2)
show_prod(a1, a2, p2)
print(p2.ap())
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:
The former point can 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.
(Note: the original spot.product() is in fact not naming states. The spot.product() function actually attaches a vector of pairs of integers to the automaton because some algorithms need to project a state of the product onto the original automaton. The dot printer knows how to display those pairs for states that are not named. Here we shall name states because (1) that is more flexible, and (2) there is a Python interface for this.)
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:
In [7]:
print(a1.prop_universal())
print(a2.prop_universal())
print(prod.prop_universal())
print(p1.prop_universal())
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
if left.prop_universal() and right.prop_universal():
result.prop_universal(True)
at the end of our function. Note that this is not the same as
result.prop_universal(left.prop_universal() and right.prop_universal())
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.
The one-liner above is wrong for two reasons:
if left and right are non-deterministic, their product could be deterministic, so calling prop_universal(False) would be wrong.
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:
In [8]:
yes = spot.trival(True)
no = spot.trival(False)
maybe = spot.trival_maybe()
for u in (no, maybe, yes):
for v in (no, maybe, yes):
print("{u!s:>5} & {v!s:<5} = {r1!s:<5} {u!s:>5} and {v!s:<5} = {r2!s:<5}"
.format(u=u, v=v, r1=(u&v), r2=(u and v)))
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.
So our
if left.prop_universal() and right.prop_universal():
result.prop_universal(True)
is OK because the if body will only be entered of both input automata are known to be deterministic.
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 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.
In [14]:
def product3(left, right):
# the twa_graph.is_existential() method returns a Boolean, not a spot.trival
if not (left.is_existential() and right.is_existential()):
raise RuntimeError("alternating automata are not supported")
bdict = left.get_dict()
if right.get_dict() != bdict:
raise RuntimeError("automata should share their dictionary")
result = spot.make_twa_graph(bdict)
result.copy_ap_of(left)
result.copy_ap_of(right)
names = [] # our array of state names
sdict = {}
todo = []
def dst(ls, rs):
pair = (ls, rs)
p = sdict.get(pair)
if p is None:
p = result.new_state()
sdict[pair] = p
todo.append((ls, rs, p))
names.append("{},{}".format(ls, rs)) # name each state
return p
result.set_init_state(dst(left.get_init_state_number(),
right.get_init_state_number()))
shift = left.num_sets()
result.set_acceptance(shift + right.num_sets(),
left.get_acceptance() & (right.get_acceptance() << shift))
while todo:
lsrc, rsrc, osrc = todo.pop()
for lt in left.out(lsrc):
for rt in right.out(rsrc):
cond = lt.cond & rt.cond
if cond != buddy.bddfalse:
acc = lt.acc | (rt.acc << shift)
result.new_edge(osrc, dst(lt.dst, rt.dst), cond, acc)
# Remember the names of our states
result.set_state_names(names)
# Loop over all the properties we want to preserve if they hold in both automata
for p in ('prop_universal', 'prop_complete', 'prop_weak', 'prop_inherently_weak',
'prop_terminal', 'prop_stutter_invariant', 'prop_state_acc'):
if getattr(left, p)() and getattr(right, p)():
getattr(result, p)(True)
return result
p3 = product3(a1, a2)
show_prod(a1, a2, p3)
print(p3.prop_universal())
In [10]:
%timeit product3(a1, a2)
In [11]:
%timeit spot.product(a1, a2)
Depending on the machine where this notebook has been run, using the C++ version of the product can be 1 to 2 order 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.
Despite that speed difference, Python can be useful to prototype an algorithm before implementing it in C++.