# -*- coding: utf-8 -*-
#+TITLE: Custom print of an automaton
#+SETUPFILE: 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 tuple
of the form
$(\mathit{src},\mathit{dst},\mathit{cond},\mathit{accsets})$ where
$\mathit{src}$ and $\mathit{dst}$ are integer denoting the extremities
of the transition, $\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.

#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
ltl2tgba -U -H '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 auto& 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, true means "it's sure", false
    // means "I don't know".  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 any algorithm that always produce deterministic automata
    // would set the deterministic bit on its output.  In this example,
    // the properties that are set come from the "properties:" line of
    // the input file.
    out << "Deterministic: "
        << (aut->prop_deterministic() ? "yes\n" : "maybe\n");
    out << "Unambiguous: "
        << (aut->prop_unambiguous() ? "yes\n" : "maybe\n");
    out << "State-Based Acc: "
        << (aut->prop_state_acc() ? "yes\n" : "maybe\n");
    out << "Terminal: "
        << (aut->prop_terminal() ? "yes\n" : "maybe\n");
    out << "Weak: "
        << (aut->prop_weak() ? "yes\n" : "maybe\n");
    out << "Inherently Weak: "
        << (aut->prop_inherently_weak() ? "yes\n" : "maybe\n");
    out << "Stutter Invariant: "
        << (aut->prop_stutter_invariant() ? "yes\n" :
            aut->prop_stutter_sensitive() ? "no\n" : "maybe\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 edge 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:
#+begin_example
Acceptance: Inf(0)&Inf(1)
Number of sets: 2
Number of states: 4
Number of edges: 10
Initial state: 0
Atomic propositions: a (=0) b (=1) c (=2)
Name: Fa | G(Fb & Fc)
Deterministic: maybe
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
    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

* Python

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

#+BEGIN_SRC python :results output :exports both
  import spot


  def maybe_yes(pos, neg=False):
      if neg:
          return "no"
      return "yes" if pos else "maybe"


  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:", maybe_yes(aut.prop_deterministic()))
      print("Unambiguous:", maybe_yes(aut.prop_unambiguous()))
      print("State-Based Acc:", maybe_yes(aut.prop_state_acc()))
      print("Terminal:", maybe_yes(aut.prop_terminal()))
      print("Weak:", maybe_yes(aut.prop_weak()))
      print("Inherently Weak:", maybe_yes(aut.prop_inherently_weak()))
      print("Stutter Invariant:", maybe_yes(aut.prop_stutter_invariant(),
                                            aut.prop_stutter_sensitive()))

      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: maybe
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
    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