Iterating over alternating automata

C++
Python

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 = {}

Iterating over alternating automata

Table of Contents

C++

Python