Custom print of an automaton

C++
Python
Going further

This example demonstrates how to iterate over an automaton in C++ and Python. This case uses automata stored entirely in memory as a graph: states are numbered by integers, and transitions can be seen as tuples of the form \((\mathit{src},\mathit{dst},\mathit{cond},\mathit{accsets})\) where \(\mathit{src}\) and \(\mathit{dst}\) are integers denoting the source and destination states, \(\mathit{cond}\) is a BDD representing the label (a.k.a. guard), and \(\mathit{accsets}\) is an object of type acc_cond::mark_t encoding the membership to each acceptance sets (acc_cond::mark_t is basically a bit vector).

The interface available for those graph-based automata allows random access to any state of the graph, hence the code given bellow can do a simple loop over all states of the automaton. Spot also supports a different kind of interface (not demonstrated here) to iterate over automata that are constructed on-the-fly and where such a loop would be impossible.

First let's create an example automaton in HOA format. We use -U to request unambiguous automata, as this allows us to demonstrate how property bits are used.

ltl2tgba -U 'Fa | G(Fb&Fc)' | tee tut21.hoa

HOA: v1
name: "F(a | G(Fb & Fc))"
States: 17
Start: 0
AP: 3 "a" "b" "c"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels trans-acc unambiguous
properties: stutter-invariant
--BODY--
State: 0
[0] 1
[!0] 2
[!0&!2] 3
[!0&!2] 4
[!0&!1&2] 5
[!0&1&2] 6
State: 1
[t] 1 {0 1}
State: 2
[!1&!2] 2
[1&!2] 2 {0}
[!1&2] 2 {1}
[1&2] 2 {0 1}
State: 3
[!0&!2] 3
[!0&!1&2] 5
[!0&1&2] 6
[0&1&2] 7
[0&!1&!2] 8
[0&!1&2] 9
[0&1&!2] 10
[0&!1&2] 12
[0&!1&!2] 13
State: 4
[!0&!2] 4
[0&!2] 11
State: 5
[!0&!2] 3
[!0&1&!2] 4
[!0&!1&2] 5
[!0&1&2] 6
[0&1&2] 7
[0&!1&!2] 8
[0&!1&2] 9
[0&1&!2] 10
[0&1&!2] 11
[0&!1] 12
[!0&!1&!2] 14
[0&!1&!2] 15
State: 6
[!0&!2] 3
[!0&!2] 4
[!0&!1&2] 5
[!0&1&2] 6
[0&1&2] 7
[0&!1&!2] 8
[0&!1&2] 9
[0&1&!2] 10
[0&!2] 11
[0&!1&2] 12
[0&!1&!2] 13
State: 7
[1&2] 7
[!1&!2] 8
[!1&2] 9
[1&!2] 10
[!2] 11
[!1&2] 12
[!1&!2] 13
State: 8
[1&2] 7
[!1&!2] 8
[!1&2] 9
[1&!2] 10
State: 9
[1&2] 7
[!1&!2] 8
[!1&2] 9
[1&!2] 10
[1&!2] 11
[!1&!2] 15
State: 10
[1&2] 7
[!1&!2] 8
[!1&2] 9
[1&!2] 10
[!1&2] 12
[!1&!2] 13
State: 11
[!2] 11 {0 1}
State: 12
[!1] 12 {0 1}
State: 13
[!1&2] 12
[!1&!2] 13
State: 14
[!0&1&!2] 4
[0&1&!2] 11
[!0&!1&!2] 14
[0&!1&!2] 15
[0&!1&!2] 16
State: 15
[1&!2] 11
[!1&!2] 15
State: 16
[!1&!2] 16 {0 1}
--END--

C++

We now write some C++ to load this automaton as we did before, and in custom_print() we print it out in a custom way by explicitly iterating over its states and edges.

The only tricky part is to print the edge labels. Since they are BDDs, printing them directly would just show the identifiers of BDDs involved. Using bdd_print_formula and passing it the BDD dictionary associated to the automaton is one way to print the edge labels.

Each automaton stores a vector the atomic propositions it uses. You can iterate on that vector using the ap() member function. If you want to convert an atomic proposition (represented by a formula) into a BDD, use the bdd_dict::varnum() method to obtain the corresponding BDD variable number, and then use for instance bdd_ithvar() to convert this BDD variable number into an actual BDD.

#include <string>
#include <iostream>
#include <spot/parseaut/public.hh>
#include <spot/twa/bddprint.hh>

void custom_print(std::ostream& out, spot::twa_graph_ptr& aut);

int main()
{
  spot::parsed_aut_ptr pa = parse_aut("tut21.hoa", spot::make_bdd_dict());
  if (pa->format_errors(std::cerr))
    return 1;
  // This cannot occur when reading a never claim, but
  // it could while reading a HOA file.
  if (pa->aborted)
    {
      std::cerr << "--ABORT-- read\n";
      return 1;
    }
  custom_print(std::cout, pa->aut);
}

void custom_print(std::ostream& out, spot::twa_graph_ptr& aut)
{
  // We need the dictionary to print the BDDs that label the edges
  const spot::bdd_dict_ptr& dict = aut->get_dict();

  // Some meta-data...
  out << "Acceptance: " << aut->get_acceptance() << '\n';
  out << "Number of sets: " << aut->num_sets() << '\n';
  out << "Number of states: " << aut->num_states() << '\n';
  out << "Number of edges: " << aut->num_edges() << '\n';
  out << "Initial state: " << aut->get_init_state_number() << '\n';
  out << "Atomic propositions:";
  for (spot::formula ap: aut->ap())
      out << ' ' << ap << " (=" << dict->varnum(ap) << ')';
  out << '\n';

  // Arbitrary data can be attached to automata, by giving them
  // a type and a name.  The HOA parser and printer both use the
  // "automaton-name" to name the automaton.
  if (auto name = aut->get_named_prop<std::string>("automaton-name"))
     out << "Name: " << *name << '\n';

  // For the following prop_*() methods, the return value is an
  // instance of the spot::trival class that can represent
  // yes/maybe/no.  These properties correspond to bits stored in the
  // automaton, so they can be queried in constant time.  They are
  // only set whenever they can be determined at a cheap cost: for
  // instance an algorithm that always produces deterministic automata
  // would set the deterministic property on its output.  In this
  // example, the properties that are set come from the "properties:"
  // line of the input file.
  out << "Complete: " << aut->prop_complete() << '\n';
  out << "Deterministic: " << (aut->prop_universal()
                               && aut->is_existential()) << '\n';
  out << "Unambiguous: " << aut->prop_unambiguous() << '\n';
  out << "State-Based Acc: " << aut->prop_state_acc() << '\n';
  out << "Terminal: " << aut->prop_terminal() << '\n';
  out << "Weak: " << aut->prop_weak() << '\n';
  out << "Inherently Weak: " << aut->prop_inherently_weak() << '\n';
  out << "Stutter Invariant: " << aut->prop_stutter_invariant() << '\n';

  // States are numbered from 0 to n-1
  unsigned n = aut->num_states();
  for (unsigned s = 0; s < n; ++s)
    {
      out << "State " << s << ":\n";

      // The out(s) method returns a fake container that can be
      // iterated over as if the contents was the edges going
      // out of s.  Each of these edges is a quadruplet
      // (src,dst,cond,acc).  Note that because this returns
      // a reference, the edge can also be modified.
      for (auto& t: aut->out(s))
        {
          out << "  edge(" << t.src << " -> " << t.dst << ")\n    label = ";
          spot::bdd_print_formula(out, dict, t.cond);
          out << "\n    acc sets = " << t.acc << '\n';
        }
    }
}

Acceptance: Inf(0)&Inf(1)
Number of sets: 2
Number of states: 17
Number of edges: 80
Initial state: 0
Atomic propositions: a (=0) b (=1) c (=2)
Name: F(a | G(Fb & Fc))
Complete: no
Deterministic: no
Unambiguous: yes
State-Based Acc: maybe
Terminal: maybe
Weak: maybe
Inherently Weak: maybe
Stutter Invariant: yes
State 0:
  edge(0 -> 1)
    label = a
    acc sets = {}
  edge(0 -> 2)
    label = !a
    acc sets = {}
  edge(0 -> 3)
    label = !a & !c
    acc sets = {}
  edge(0 -> 4)
    label = !a & !c
    acc sets = {}
  edge(0 -> 5)
    label = !a & !b & c
    acc sets = {}
  edge(0 -> 6)
    label = !a & b & c
    acc sets = {}
State 1:
  edge(1 -> 1)
    label = 1
    acc sets = {0,1}
State 2:
  edge(2 -> 2)
    label = !b & !c
    acc sets = {}
  edge(2 -> 2)
    label = b & !c
    acc sets = {0}
  edge(2 -> 2)
    label = !b & c
    acc sets = {1}
  edge(2 -> 2)
    label = b & c
    acc sets = {0,1}
State 3:
  edge(3 -> 3)
    label = !a & !c
    acc sets = {}
  edge(3 -> 5)
    label = !a & !b & c
    acc sets = {}
  edge(3 -> 6)
    label = !a & b & c
    acc sets = {}
  edge(3 -> 7)
    label = a & b & c
    acc sets = {}
  edge(3 -> 8)
    label = a & !b & !c
    acc sets = {}
  edge(3 -> 9)
    label = a & !b & c
    acc sets = {}
  edge(3 -> 10)
    label = a & b & !c
    acc sets = {}
  edge(3 -> 12)
    label = a & !b & c
    acc sets = {}
  edge(3 -> 13)
    label = a & !b & !c
    acc sets = {}
State 4:
  edge(4 -> 4)
    label = !a & !c
    acc sets = {}
  edge(4 -> 11)
    label = a & !c
    acc sets = {}
State 5:
  edge(5 -> 3)
    label = !a & !c
    acc sets = {}
  edge(5 -> 4)
    label = !a & b & !c
    acc sets = {}
  edge(5 -> 5)
    label = !a & !b & c
    acc sets = {}
  edge(5 -> 6)
    label = !a & b & c
    acc sets = {}
  edge(5 -> 7)
    label = a & b & c
    acc sets = {}
  edge(5 -> 8)
    label = a & !b & !c
    acc sets = {}
  edge(5 -> 9)
    label = a & !b & c
    acc sets = {}
  edge(5 -> 10)
    label = a & b & !c
    acc sets = {}
  edge(5 -> 11)
    label = a & b & !c
    acc sets = {}
  edge(5 -> 12)
    label = a & !b
    acc sets = {}
  edge(5 -> 14)
    label = !a & !b & !c
    acc sets = {}
  edge(5 -> 15)
    label = a & !b & !c
    acc sets = {}
State 6:
  edge(6 -> 3)
    label = !a & !c
    acc sets = {}
  edge(6 -> 4)
    label = !a & !c
    acc sets = {}
  edge(6 -> 5)
    label = !a & !b & c
    acc sets = {}
  edge(6 -> 6)
    label = !a & b & c
    acc sets = {}
  edge(6 -> 7)
    label = a & b & c
    acc sets = {}
  edge(6 -> 8)
    label = a & !b & !c
    acc sets = {}
  edge(6 -> 9)
    label = a & !b & c
    acc sets = {}
  edge(6 -> 10)
    label = a & b & !c
    acc sets = {}
  edge(6 -> 11)
    label = a & !c
    acc sets = {}
  edge(6 -> 12)
    label = a & !b & c
    acc sets = {}
  edge(6 -> 13)
    label = a & !b & !c
    acc sets = {}
State 7:
  edge(7 -> 7)
    label = b & c
    acc sets = {}
  edge(7 -> 8)
    label = !b & !c
    acc sets = {}
  edge(7 -> 9)
    label = !b & c
    acc sets = {}
  edge(7 -> 10)
    label = b & !c
    acc sets = {}
  edge(7 -> 11)
    label = !c
    acc sets = {}
  edge(7 -> 12)
    label = !b & c
    acc sets = {}
  edge(7 -> 13)
    label = !b & !c
    acc sets = {}
State 8:
  edge(8 -> 7)
    label = b & c
    acc sets = {}
  edge(8 -> 8)
    label = !b & !c
    acc sets = {}
  edge(8 -> 9)
    label = !b & c
    acc sets = {}
  edge(8 -> 10)
    label = b & !c
    acc sets = {}
State 9:
  edge(9 -> 7)
    label = b & c
    acc sets = {}
  edge(9 -> 8)
    label = !b & !c
    acc sets = {}
  edge(9 -> 9)
    label = !b & c
    acc sets = {}
  edge(9 -> 10)
    label = b & !c
    acc sets = {}
  edge(9 -> 11)
    label = b & !c
    acc sets = {}
  edge(9 -> 15)
    label = !b & !c
    acc sets = {}
State 10:
  edge(10 -> 7)
    label = b & c
    acc sets = {}
  edge(10 -> 8)
    label = !b & !c
    acc sets = {}
  edge(10 -> 9)
    label = !b & c
    acc sets = {}
  edge(10 -> 10)
    label = b & !c
    acc sets = {}
  edge(10 -> 12)
    label = !b & c
    acc sets = {}
  edge(10 -> 13)
    label = !b & !c
    acc sets = {}
State 11:
  edge(11 -> 11)
    label = !c
    acc sets = {0,1}
State 12:
  edge(12 -> 12)
    label = !b
    acc sets = {0,1}
State 13:
  edge(13 -> 12)
    label = !b & c
    acc sets = {}
  edge(13 -> 13)
    label = !b & !c
    acc sets = {}
State 14:
  edge(14 -> 4)
    label = !a & b & !c
    acc sets = {}
  edge(14 -> 11)
    label = a & b & !c
    acc sets = {}
  edge(14 -> 14)
    label = !a & !b & !c
    acc sets = {}
  edge(14 -> 15)
    label = a & !b & !c
    acc sets = {}
  edge(14 -> 16)
    label = a & !b & !c
    acc sets = {}
State 15:
  edge(15 -> 11)
    label = b & !c
    acc sets = {}
  edge(15 -> 15)
    label = !b & !c
    acc sets = {}
State 16:
  edge(16 -> 16)
    label = !b & !c
    acc sets = {0,1}

Python

Here is the very same example, but written in Python:

import spot


def custom_print(aut):
    bdict = aut.get_dict()
    print("Acceptance:", aut.get_acceptance())
    print("Number of sets:", aut.num_sets())
    print("Number of states: ", aut.num_states())
    print("Initial states: ", aut.get_init_state_number())
    print("Atomic propositions:", end='')
    for ap in aut.ap():
        print(' ', ap, ' (=', bdict.varnum(ap), ')', sep='', end='')
    print()
    # Templated methods are not available in Python, so we cannot
    # retrieve/attach arbitrary objects from/to the automaton.  However the
    # Python bindings have get_name() and set_name() to access the
    # "automaton-name" property.
    name = aut.get_name()
    if name:
        print("Name: ", name)
    print("Deterministic:", aut.prop_universal() and aut.is_existential())
    print("Unambiguous:", aut.prop_unambiguous())
    print("State-Based Acc:", aut.prop_state_acc())
    print("Terminal:", aut.prop_terminal())
    print("Weak:", aut.prop_weak())
    print("Inherently Weak:", aut.prop_inherently_weak())
    print("Stutter Invariant:", aut.prop_stutter_invariant())

    for s in range(0, aut.num_states()):
        print(f"State {s}:")
        for t in aut.out(s):
            print(f"  edge({t.src} -> {t.dst})")
            # bdd_print_formula() is designed to print on a std::ostream, and
            # is inconvenient to use in Python.  Instead we use
            # bdd_format_formula() as this simply returns a string.
            print("    label =", spot.bdd_format_formula(bdict, t.cond))
            print("    acc sets =", t.acc)


custom_print(spot.automaton("tut21.hoa"))

Acceptance: Inf(0)&Inf(1)
Number of sets: 2
Number of states:  17
Initial states:  0
Atomic propositions: a (=0) b (=1) c (=2)
Name:  F(a | G(Fb & Fc))
Deterministic: no
Unambiguous: yes
State-Based Acc: maybe
Terminal: maybe
Weak: maybe
Inherently Weak: maybe
Stutter Invariant: yes
State 0:
  edge(0 -> 1)
    label = a
    acc sets = {}
  edge(0 -> 2)
    label = !a
    acc sets = {}
  edge(0 -> 3)
    label = !a & !c
    acc sets = {}
  edge(0 -> 4)
    label = !a & !c
    acc sets = {}
  edge(0 -> 5)
    label = !a & !b & c
    acc sets = {}
  edge(0 -> 6)
    label = !a & b & c
    acc sets = {}
State 1:
  edge(1 -> 1)
    label = 1
    acc sets = {0,1}
State 2:
  edge(2 -> 2)
    label = !b & !c
    acc sets = {}
  edge(2 -> 2)
    label = b & !c
    acc sets = {0}
  edge(2 -> 2)
    label = !b & c
    acc sets = {1}
  edge(2 -> 2)
    label = b & c
    acc sets = {0,1}
State 3:
  edge(3 -> 3)
    label = !a & !c
    acc sets = {}
  edge(3 -> 5)
    label = !a & !b & c
    acc sets = {}
  edge(3 -> 6)
    label = !a & b & c
    acc sets = {}
  edge(3 -> 7)
    label = a & b & c
    acc sets = {}
  edge(3 -> 8)
    label = a & !b & !c
    acc sets = {}
  edge(3 -> 9)
    label = a & !b & c
    acc sets = {}
  edge(3 -> 10)
    label = a & b & !c
    acc sets = {}
  edge(3 -> 12)
    label = a & !b & c
    acc sets = {}
  edge(3 -> 13)
    label = a & !b & !c
    acc sets = {}
State 4:
  edge(4 -> 4)
    label = !a & !c
    acc sets = {}
  edge(4 -> 11)
    label = a & !c
    acc sets = {}
State 5:
  edge(5 -> 3)
    label = !a & !c
    acc sets = {}
  edge(5 -> 4)
    label = !a & b & !c
    acc sets = {}
  edge(5 -> 5)
    label = !a & !b & c
    acc sets = {}
  edge(5 -> 6)
    label = !a & b & c
    acc sets = {}
  edge(5 -> 7)
    label = a & b & c
    acc sets = {}
  edge(5 -> 8)
    label = a & !b & !c
    acc sets = {}
  edge(5 -> 9)
    label = a & !b & c
    acc sets = {}
  edge(5 -> 10)
    label = a & b & !c
    acc sets = {}
  edge(5 -> 11)
    label = a & b & !c
    acc sets = {}
  edge(5 -> 12)
    label = a & !b
    acc sets = {}
  edge(5 -> 14)
    label = !a & !b & !c
    acc sets = {}
  edge(5 -> 15)
    label = a & !b & !c
    acc sets = {}
State 6:
  edge(6 -> 3)
    label = !a & !c
    acc sets = {}
  edge(6 -> 4)
    label = !a & !c
    acc sets = {}
  edge(6 -> 5)
    label = !a & !b & c
    acc sets = {}
  edge(6 -> 6)
    label = !a & b & c
    acc sets = {}
  edge(6 -> 7)
    label = a & b & c
    acc sets = {}
  edge(6 -> 8)
    label = a & !b & !c
    acc sets = {}
  edge(6 -> 9)
    label = a & !b & c
    acc sets = {}
  edge(6 -> 10)
    label = a & b & !c
    acc sets = {}
  edge(6 -> 11)
    label = a & !c
    acc sets = {}
  edge(6 -> 12)
    label = a & !b & c
    acc sets = {}
  edge(6 -> 13)
    label = a & !b & !c
    acc sets = {}
State 7:
  edge(7 -> 7)
    label = b & c
    acc sets = {}
  edge(7 -> 8)
    label = !b & !c
    acc sets = {}
  edge(7 -> 9)
    label = !b & c
    acc sets = {}
  edge(7 -> 10)
    label = b & !c
    acc sets = {}
  edge(7 -> 11)
    label = !c
    acc sets = {}
  edge(7 -> 12)
    label = !b & c
    acc sets = {}
  edge(7 -> 13)
    label = !b & !c
    acc sets = {}
State 8:
  edge(8 -> 7)
    label = b & c
    acc sets = {}
  edge(8 -> 8)
    label = !b & !c
    acc sets = {}
  edge(8 -> 9)
    label = !b & c
    acc sets = {}
  edge(8 -> 10)
    label = b & !c
    acc sets = {}
State 9:
  edge(9 -> 7)
    label = b & c
    acc sets = {}
  edge(9 -> 8)
    label = !b & !c
    acc sets = {}
  edge(9 -> 9)
    label = !b & c
    acc sets = {}
  edge(9 -> 10)
    label = b & !c
    acc sets = {}
  edge(9 -> 11)
    label = b & !c
    acc sets = {}
  edge(9 -> 15)
    label = !b & !c
    acc sets = {}
State 10:
  edge(10 -> 7)
    label = b & c
    acc sets = {}
  edge(10 -> 8)
    label = !b & !c
    acc sets = {}
  edge(10 -> 9)
    label = !b & c
    acc sets = {}
  edge(10 -> 10)
    label = b & !c
    acc sets = {}
  edge(10 -> 12)
    label = !b & c
    acc sets = {}
  edge(10 -> 13)
    label = !b & !c
    acc sets = {}
State 11:
  edge(11 -> 11)
    label = !c
    acc sets = {0,1}
State 12:
  edge(12 -> 12)
    label = !b
    acc sets = {0,1}
State 13:
  edge(13 -> 12)
    label = !b & c
    acc sets = {}
  edge(13 -> 13)
    label = !b & !c
    acc sets = {}
State 14:
  edge(14 -> 4)
    label = !a & b & !c
    acc sets = {}
  edge(14 -> 11)
    label = a & b & !c
    acc sets = {}
  edge(14 -> 14)
    label = !a & !b & !c
    acc sets = {}
  edge(14 -> 15)
    label = a & !b & !c
    acc sets = {}
  edge(14 -> 16)
    label = a & !b & !c
    acc sets = {}
State 15:
  edge(15 -> 11)
    label = b & !c
    acc sets = {}
  edge(15 -> 15)
    label = !b & !c
    acc sets = {}
State 16:
  edge(16 -> 16)
    label = !b & !c
    acc sets = {0,1}

Going further

As another example of printing an autoamton, see our page about printing a Büchi automaton in "BA format".

Custom print of an automaton

Table of Contents

C++

Python

Going further