In [1]:
import spot
spot.setup()

Acceptance conditions

The acceptance condition of an automaton specifies which of its paths are accepting.

The way acceptance conditions are stored in Spot is derived from the way acceptance conditions are specified in the HOA format. In HOA, acceptance conditions are given as a line of the form:

Acceptance: 3 (Inf(0)&Fin(1))|Inf(2)

The number 3 gives the number of acceptance sets used (numbered from 0 to 2 in that case), while the rest of the line is a positive Boolean formula over terms of the form:

  • Inf(n), that is true if and only if the set n is seen infinitely often,
  • Fin(n), that is true if and only if the set n should be seen finitely often,
  • t, always true,
  • f, always false.

The HOA specifications additionally allows terms of the form Inf(!n) or Fin(!n) but Spot automatically rewrites those away when reading an HOA file.

Note that the number of sets given can be larger than what is actually needed by the acceptance formula.

Transitions in automata can be tagged as being part of some member sets, and a path in the automaton is accepting if the set of acceptance sets visited along this path satify the acceptance condition.

Definining acceptance conditions in Spot involves three different types of C++ objects:

  • spot::acc_cond is used to represent an acceptance condition, that is: a number of sets and a formula.
  • spot::acc_cond::acc_code, is used to represent Boolean formula for the acceptance condition using a kind of byte code (hence the name)
  • spot::acc_cond::mark_t, is a type of bit-vector used to represent membership to acceptance sets.

In because Swig's support for nested class is limited, these types are available respectively as spot.acc_cond, spot.acc_code, and spot.mark_t in Python.

mark_t

Let's start with the simpler of these three objects. mark_t is a type of bit vector. Its main constructor takes a sequence of set numbers.

In [2]:
spot.mark_t()
Out[2]:
{}
In [3]:
spot.mark_t([0, 2, 3])
Out[3]:
{0,2,3}
In [4]:
spot.mark_t((0, 2, 3))
Out[4]:
{0,2,3}

As seen above, the sequence of set numbers can be specified using a list or a tuple. While from the Python language point of view, using a tuple is faster than using a list, the overhead to converting all the arguments from Python to C++ and then converting the resuslting back from C++ to Python makes this difference completely negligeable. In the following, we opted to use lists, because brackets are more readable than nested parentheses.

In [5]:
x = spot.mark_t([0, 2, 3])
y = spot.mark_t([0, 4])
print(x | y)
print(x & y)
print(x - y)

{0,2,3,4}
{0}
{2,3}

The bits can be set, cleared, and tested using the set(), clear(), and has() methods:

In [6]:
x.set(5)
print(x)

{0,2,3,5}
In [7]:
x.clear(3)
print(x)

{0,2,5}
In [8]:
print(x.has(2))
print(x.has(3))

True
False

Left-shifting will increment all set numbers. This operation is useful when building the product of two automata: all the set number of one automaton have to be shift by the number of sets used in the other automaton.

In [9]:
x << 2
Out[9]:
{2,4,7}

Internally, the mark_t stores the bit-vector as an integer. This also implies that we currently do not support more than 32 acceptance sets. The underlaying integer can be retrieved using .id.

In [10]:
print(x)
print(x.id)
print(bin(x.id))

{0,2,5}
37
0b100101

mark_t can also be initialized using an integer: in that case the integer is interpreted as a bit vector.

A frequent error is to use mark_t(n) when we really mean mark_t([n]) or mark_t((n,)).

In [11]:
# compare
print(spot.mark_t([5]))
# with
print(spot.mark_t(5))
print(spot.mark_t(0b10101))

{5}
{0,2}
{0,2,4}

The different sets can be iterated over with the sets() method, that returns a tuble with the index of all bits set.

In [12]:
print(x)
print(list(x.sets()))
for s in x.sets():
    print(s)

{0,2,5}
[0, 2, 5]
0
2
5

count() return the number of sets in a mark_t:

In [13]:
x.count()
Out[13]:
3

lowest() returns a mark_t containing only the lowest set number. This provides another way to iterate overs all set numbers in cases where you need the result as a mark_t.

In [14]:
spot.mark_t([1,3,5]).lowest()
Out[14]:
{1}
In [15]:
v = spot.mark_t([1, 3, 5])
while v:               # this stops once v is empty
    b = v.lowest()
    v -= b
    print(b)

{1}
{3}
{5}

max_set() returns the number of the highest set plus one. This is usually used to figure out how many sets we need to declare on the Acceptance: line of the HOA format:

In [16]:
spot.mark_t([1, 3, 5]).max_set()
Out[16]:
6

acc_code

acc_code encodes the formula of the acceptance condition using a kind of bytecode that basically corresponds to an encoding in reverse Polish notation in which conjunctions of Inf(n) terms, and disjunctions of Fin(n) terms are grouped. In particular, the frequently-used genaralized-Büchi acceptance conditions (like Inf(0)&Inf(1)&Inf(2)) are always encoded as a single term (like Inf({0,1,2})).

The simplest way to construct an acc_code by passing a string that represent the formula to build.

In [17]:
spot.acc_code('(Inf(0)&Fin(1))|Inf(2)')
Out[17]:
(Inf(0) & Fin(1)) | Inf(2)

You may also use a named acceptance condition:

In [18]:
spot.acc_code('Rabin 2')
Out[18]:
(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))

The recognized names are the valide values for acc-name: in the HOA format. Additionally numbers may be replaced by ranges of the form n..m, in which case a random number is selected in that range.

In [19]:
print(spot.acc_code('Streett 2..4'))
print(spot.acc_code('Streett 2..4'))

(Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & (Fin(4) | Inf(5)) & (Fin(6) | Inf(7))
(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))

It may also be convenient to generate a random acceptance condition:

In [20]:
spot.acc_code('random 3..5')
Out[20]:
(Fin(3) | Inf(1)) & Inf(4) & (Fin(0)|Fin(2))

The to_cnf() and to_dnf() functions can be used to rewrite the formula into Conjunctive or Disjunctive normal forms. This functions will simplify the resulting formulas to make them irredundant.

In [21]:
a = spot.acc_code('parity min odd 5')
a
Out[21]:
Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | Fin(4))))
In [22]:
a.to_cnf()
Out[22]:
Fin(0) & (Inf(1) | Fin(2)) & (Inf(1) | Inf(3) | Fin(4))
In [23]:
a.to_dnf()
Out[23]:
(Fin(0) & Inf(1)) | (Fin(0) & Fin(2) & Inf(3)) | (Fin(0) & Fin(2) & Fin(4))

The manipulation of acc_code objects is quite rudimentary at the moment: it easy to build, but it's harder take appart. In fact we won't attempt to disassemble an acc_code object in Python: those things are better done in C++

Operators |, |=, &, &=, <<, and <<= can be used with their obvious semantics. Whenever possible, the inplace versions (|=, &=, <<=) should be prefered, because they create less temporary acceptance conditions.

In [24]:
x = spot.acc_code('Rabin 2')
y = spot.acc_code('Rabin 2') << 4
print(x)
print(y)

(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
(Fin(4) & Inf(5)) | (Fin(6) & Inf(7))
In [25]:
print(x | y)
print(x & y)

(Fin(4) & Inf(5)) | (Fin(6) & Inf(7)) | (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
((Fin(4) & Inf(5)) | (Fin(6) & Inf(7))) & ((Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))

The complement() method returns the complemented acceptance condition:

In [26]:
print(x)
print(x.complement())

(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
(Inf(0) | Fin(1)) & (Inf(2) | Fin(3))

Instead of using acc_code('string'), it is also possible to build an acceptance formula from atoms like Inf({...}), Fin({...}), t, or f.

Remember that in our encoding for the formula, terms like Inf(1)&Inf(2) and Fin(3)|Fin(4)|Fin(5) are actually stored as Inf({1,2}) and Fin({3,4,5}), where {1,2} and {3,4,5} are instance of mark_t. These terms can be generated with the functions spot.acc_code.inf(mark) and spot.acc_code.fin(mark).

Inf({}) is equivalent to t, and Fin({}) is equivalent to f, but it's better to use the functions spot.acc_code.t() or spot.acc_code.f() directly.

In [27]:
spot.acc_code.inf([1,2]) & spot.acc_code.fin([3,4,5])
Out[27]:
(Fin(3)|Fin(4)|Fin(5)) & (Inf(1)&Inf(2))
In [28]:
spot.acc_code.inf([])
Out[28]:
t
In [29]:
spot.acc_code.t()
Out[29]:
t
In [30]:
spot.acc_code.fin([])
Out[30]:
f
In [31]:
spot.acc_code.f()
Out[31]:
f

To evaluate an acceptance condition formula on a run, build a mark_t containing all the acceptance sets that are seen infinitely often along this run, and call the accepting() method.

In [32]:
acc = spot.acc_code('Fin(0) & Inf(1) | Inf(2)')
print("acc =", acc)
for x in ([0, 1, 2], [1, 2], [0, 1], [0, 2], [0], [1], [2], []):
    print("acc.accepting({}) = {}".format(x, acc.accepting(x)))

acc = (Fin(0) & Inf(1)) | Inf(2)
acc.accepting([0, 1, 2]) = True
acc.accepting([1, 2]) = True
acc.accepting([0, 1]) = False
acc.accepting([0, 2]) = True
acc.accepting([0]) = False
acc.accepting([1]) = True
acc.accepting([2]) = True
acc.accepting([]) = False

Finally the method used_sets() returns a mark_t with all the sets appearing in the formula:

In [33]:
acc = spot.acc_code('Fin(0) & Inf(2)')
print(acc)
print(acc.used_sets())
print(acc.used_sets().max_set())

Fin(0) & Inf(2)
{0,2}
3

acc_cond

Automata store their acceptance condition as an instance of the acc_cond class. This class can be thought of as a pair (n, code), where n is an integer that tells how many acceptance sets are used, while the code is an instance of acc_code and encodes the formula over a subset of these acceptance sets. We usually have n == code.used_sets().max_set()), but n can be larger.

It is OK if an automaton declares that is used 3 sets, even if the acceptance condition formula only uses set number 1.

The acc_cond objects are usually not created by hand: automata have dedicated methods for that. But for the purpose of this notebook, let's do it:

In [34]:
acc = spot.acc_cond(4, spot.acc_code('Rabin 2'))
acc
Out[34]:
(4, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))

For convenience, you can pass the string directly:

In [35]:
acc = spot.acc_cond(4, 'Rabin 2')
acc
Out[35]:
(4, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))
In [36]:
acc.num_sets()
Out[36]:
4
In [37]:
acc.get_acceptance()
Out[37]:
(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))

The acc_cond object can also be constructed using only a number of sets. In that case, the acceptance condition defaults to t, and it can be changed to something else later (using set_acceptance()). The number of acceptance sets can also be augmented with add_sets().

In [38]:
acc = spot.acc_cond(4)
acc
Out[38]:
(4, t)
In [39]:
acc.add_sets(2)
acc
Out[39]:
(6, t)
In [40]:
acc.set_acceptance('Streett 2')
acc
Out[40]:
(6, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))

Calling the constructor of acc_cond by passing just an instance of acc_code (or a string that will be passed to the acc_code constructor) will automatically set the number of acceptance sets to the minimum needed by the formula:

In [41]:
acc = spot.acc_cond('Streett 2')
acc
Out[41]:
(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))

The above is in fact just syntactic sugar for:

In [42]:
code = spot.acc_code('Streett 2')
acc = spot.acc_cond(code.used_sets().max_set(), code)
acc
Out[42]:
(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))

The common scenario of setting generalized Büchi acceptance can be achieved more efficiently by first setting the number of acceptance sets, and then requiring generalized Büchi acceptance:

In [43]:
acc = spot.acc_cond(4)
acc.set_generalized_buchi()
acc
Out[43]:
(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))

The acc_cond class has several methods for detecting acceptance conditions that match the named acceptance conditions of the HOA format. Note that in the HOA format, Inf(0)&Inf(1)&Inf(2)&Inf(3) is only called generalized Büchi if exactly 4 acceptance sets are used. So the following behavior should not be surprising:

In [44]:
print(acc)
print(acc.is_generalized_buchi())
acc.add_sets(1)
print(acc)
print(acc.is_generalized_buchi())

(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))
True
(5, Inf(0)&Inf(1)&Inf(2)&Inf(3))
False

Similar methods like is_t(), is_f(), is_buchi(), is_co_buchi(), is_generalized_co_buchi() all return a Boolean.

The is_rabin() and is_streett() methods, however, return a number of pairs. The number of pairs is always num_sets()/2 on success, or -1 on failure.

In [45]:
acc = spot.acc_cond('Rabin 2')
print(acc)
print(acc.is_rabin())
print(acc.is_streett())

(4, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))
2
-1

The check for parity acceptance returns three Boolean in a list of the form [matched, max?, odd?]. If matched is False, the other values should be ignored.

In [46]:
acc = spot.acc_cond('parity min odd 4')
print(acc)
print(acc.is_parity())
acc.set_generalized_buchi()
print(acc)
print(acc.is_parity())

(4, Fin(0) & (Inf(1) | (Fin(2) & Inf(3))))
[True, False, True]
(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))
[False, False, False]

If the acceptance condition has some known name, it can be retrieved using the name() method. By default the name given is a human-readable string close that used in the HOA format, but with proper accents, and support for name like Streett-like or Rabin-like. The argument arg can specify a different style using the same syntax as in --format='%[arg]g' when using the command-line tools.

In [47]:
print(acc.name())
print(acc.name("d"))  # <- Style used by print_dot(aut, "a")
print(acc.name("0"))  # <- no parameters

generalized-Büchi 4
gen. Büchi 4
generalized-Buchi

acc_cond contains a few functions for manipulating mark_t instances, these are typically functions that require known the total number of accepting sets declared.

For instance complementing a mark_t:

In [48]:
m = spot.mark_t([1, 3])
print(acc.comp(m))

{0,2}

all_sets() returns a mark_t listing all the declared sets:

In [49]:
acc.all_sets()
Out[49]:
{0,1,2,3}

For convencience, the accepting() method of acc_cond delegates to that of the acc_code.
Any set passed to accepting() that is not used by the acceptance formula has no influence.

In [50]:
print("acc =", acc)
for x in ([0, 1, 2, 3, 10], [1, 2]):
    print("acc.accepting({}) = {}".format(x, acc.accepting(x)))

acc = (4, Inf(0)&Inf(1)&Inf(2)&Inf(3))
acc.accepting([0, 1, 2, 3, 10]) = True
acc.accepting([1, 2]) = False

Finally the unsat_mark() method of acc_cond computes an instance of mark_t that is unaccepting (i.e., passing this value to acc.accepting(...) will return False when such a value exist. Not all acceptance conditions have an satisfiable mark. Obviously the t acceptance is always satisfiable, and so are all equivalent acceptances (for instance Fin(1)|Inf(1)).

For this reason, unsat_mark() actually returns a pair: (bool, mark_t) where the Boolean is False iff the acceptance is always satisfiable. When the Boolean is True, then the second element of the pair gives a non-accepting mark.

In [51]:
print(acc)
print(acc.unsat_mark())

(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))
(True, {})
In [52]:
acc = spot.acc_cond(0)   # use 0 acceptance sets, and the default formula (t)
print(acc)
print(acc.unsat_mark())

(0, t)
(False, {})
In [53]:
acc = spot.acc_cond('Streett 2')
print(acc)
print(acc.unsat_mark())

(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))
(True, {2})