# Iterating over alternating automata

Alternating automata can be explored in a very similar way as non-alternating automata. Most of the code from our custom automaton printer will still work; the only problem is with universal edges.

We will use the following example automaton as input (it is just a slight variation over an alternating automaton created previously to demonstrate a universal initial state).

HOA: v1 States: 3 Start: 0&1 AP: 1 "a" acc-name: co-Buchi Acceptance: 1 Fin(0) --BODY-- State: 0 [0] 0 [!0] 0&1 State: 1 [!0] 1 {0} [0] 2 State: 2 [t] 2 --END--

## C++

Let us assume that this automaton has been loaded in variable `aut`

,
and that we run the following code, similar to what we did in the
custom automaton printer.

std::cout << "Initial state: " << aut->get_init_state_number() << '\n'; const spot::bdd_dict_ptr& dict = aut->get_dict(); unsigned n = aut->num_states(); for (unsigned s = 0; s < n; ++s) { std::cout << "State " << s << ":\n"; for (auto& t: aut->out(s)) { std::cout << " edge(" << t.src << " -> " << t.dst << ")\n label = "; spot::bdd_print_formula(std::cout, dict, t.cond); std::cout << "\n acc sets = " << t.acc << '\n'; } }

Initial state: 4294967295 State 0: edge(0 -> 0) label = a acc sets = {} edge(0 -> 4294967295) label = !a acc sets = {} State 1: edge(1 -> 1) label = !a acc sets = {0} edge(1 -> 2) label = a acc sets = {} State 2: edge(2 -> 2) label = 1 acc sets = {}

This output seems correct only for non-universal edges. The reason is that Spot always store all edges as a tuple (src,dst,label,acc sets), but universal edges are indicated by setting the most significant bit of the destination (or of the initial state).

The "universality" of an edge can be tested using the
`twa_graph::is_univ_dest()`

method: it takes a destination state as
input, as in `aut->is_univ_dest(t.dst)`

or
`aut->is_univ_dest(aut->get_init_state_number())`

. For convenience
this method can also be called on an edge, as in `aut->is_univ_dest(t)`

.

The set of destination states of a universal edge can be iterated over
via the `twa_graph::univ_dests()`

method. This takes either a
destination state (`twa_graph::univ_dests(t.dst)`

) or more simply an
edge (`twa_graph::univ_dests(t)`

). The `univ_dests()`

method will
also work on non-universal edges, but in this case it will simply
iterate on the given state.

Therefor in order to print the universal destinations of any universal
edge in an alternating automaton, we can use `univ_dests()`

unconditionally. In this example, we simply call `is_univ_dest()`

to
decide whether to enclose the destinations in braces.

unsigned init = aut->get_init_state_number(); std::cout << "Initial state:"; if (aut->is_univ_dest(init)) std::cout << " {"; for (unsigned i: aut->univ_dests(init)) std::cout << ' ' << i; if (aut->is_univ_dest(init)) std::cout << " }"; std::cout << '\n'; const spot::bdd_dict_ptr& dict = aut->get_dict(); unsigned n = aut->num_states(); for (unsigned s = 0; s < n; ++s) { std::cout << "State " << s << ":\n"; for (auto& t: aut->out(s)) { std::cout << " edge(" << t.src << " ->"; if (aut->is_univ_dest(t)) std::cout << " {"; for (unsigned dst: aut->univ_dests(t)) std::cout << ' ' << dst; if (aut->is_univ_dest(t)) std::cout << " }"; std::cout << ")\n label = "; spot::bdd_print_formula(std::cout, dict, t.cond); std::cout << "\n acc sets = " << t.acc << '\n'; } }

Initial state: { 0 1 } State 0: edge(0 -> 0) label = a acc sets = {} edge(0 -> { 0 1 }) label = !a acc sets = {} State 1: edge(1 -> 1) label = !a acc sets = {0} edge(1 -> 2) label = a acc sets = {} State 2: edge(2 -> 2) label = 1 acc sets = {}

## Python

Here is the Python version of this code:

import spot aut = spot.automaton("tut24.hoa") def format_dest(s): if not aut.is_univ_dest(s): return s else: return f'{{ {" ".join(map(str, aut.univ_dests(s)))} }}' bdict = aut.get_dict() init = aut.get_init_state_number() print(f"Initial states: {format_dest(init)}") for s in range(0, aut.num_states()): print("State {}:".format(s)) for t in aut.out(s): print(f" edge({t.src} -> {format_dest(t.dst)})") print(" label =", spot.bdd_format_formula(bdict, t.cond)) print(" acc sets =", t.acc)

Initial states: { 0 1 } State 0: edge(0 -> 0) label = a acc sets = {} edge(0 -> { 0 1 }) label = !a acc sets = {} State 1: edge(1 -> 1) label = !a acc sets = {0} edge(1 -> 2) label = a acc sets = {} State 2: edge(2 -> 2) label = 1 acc sets = {}