spot/doc/org/tut21.org

# -*- coding: utf-8 -*-
#+TITLE: Custom print of an automaton
#+DESCRIPTION: Code example for iterating over ω-automata in Spot
#+INCLUDE: setup.org
#+HTML_LINK_UP: tut.html

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
[[file:tut50.org][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.

#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
ltl2tgba -U 'Fa | G(Fb&Fc)' | tee tut21.hoa
#+END_SRC
#+RESULTS:
#+BEGIN_SRC hoa
HOA: v1
name: "Fa | G(Fb & Fc)"
States: 4
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] 3
State: 1
[t] 1 {0 1}
State: 2
[0] 1
[!0] 2
State: 3
[!0&1&2] 3 {0 1}
[!0&!1&2] 3 {1}
[!0&1&!2] 3 {0}
[!0&!1&!2] 3
--END--
#+END_SRC

* C++

We now write some C++ to load this automaton [[file:tut20.org][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.

#+BEGIN_SRC C++ :results verbatim :exports both
  #include <string>
  #include <iostream>
  #include <spot/parseaut/public.hh>
  #include <spot/twaalgos/hoa.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';
          }
      }
  }
#+END_SRC

#+RESULTS:

* Python

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

#+BEGIN_SRC python :results output :exports both
  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("State {}:".format(s))
          for t in aut.out(s):
              print("  edge({} -> {})".format(t.src, t.dst))
              # bdd_print_formula() is designed to print on a std::ostream, and
              # is inconveniant 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"))
#+END_SRC

#+RESULTS:
#+begin_example
Acceptance: Inf(0)&Inf(1)
Number of sets: 2
Number of states:  4
Initial states:  0
Atomic propositions: a (=0) b (=1) c (=2)
Name:  Fa | G(Fb & Fc)
Deterministic: no
Unambiguous: maybe
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
    acc sets = {}
State 1:
  edge(1 -> 1)
    label = 1
    acc sets = {0,1}
State 2:
  edge(2 -> 1)
    label = a
    acc sets = {}
  edge(2 -> 2)
    label = !a
    acc sets = {}
State 3:
  edge(3 -> 3)
    label = !a & b & c
    acc sets = {0,1}
  edge(3 -> 3)
    label = !a & !b & c
    acc sets = {1}
  edge(3 -> 3)
    label = !a & b & !c
    acc sets = {0}
  edge(3 -> 3)
    label = !a & !b & !c
    acc sets = {}
#+end_example


#+BEGIN_SRC sh :results silent :exports results
rm -f tut21.hoa
#+END_SRC