# -*- coding: utf-8 -*-
#+TITLE: Converting Rabin (or Other) to Büchi, and simplifying it
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tut.html

Consider the following Rabin automaton, generated by =ltl2dstar=:

#+BEGIN_SRC sh :results silent :exports both
ltldo ltl2dstar -f 'F(Xp1 xor XXp1)' > tut30.hoa
#+END_SRC

#+RESULTS:

#+NAME: tut30in
#+BEGIN_SRC sh :results verbatim :exports none
autfilt tut30.hoa --dot=.a
#+END_SRC

#+RESULTS: tut30in
#+begin_example
digraph G {
  rankdir=LR
  label=<(Fin(<font color="#5DA5DA">⓿</font>) &amp; Inf(<font color="#F17CB0">❶</font>)) | (Fin(<font color="#FAA43A">❷</font>) &amp; Inf(<font color="#B276B2">❸</font>)) | (Fin(<font color="#60BD68">❹</font>) &amp; Inf(<font color="#F15854">❺</font>))>
  labelloc="t"
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
  I [label="", style=invis, width=0]
  I -> 6
  0 [label=<0<br/><font color="#FAA43A">❷</font><font color="#F15854">❺</font>>]
  0 -> 2 [label=<!p1>]
  0 -> 4 [label=<p1>]
  1 [label=<1<br/><font color="#FAA43A">❷</font><font color="#F15854">❺</font>>]
  1 -> 4 [label=<!p1>]
  1 -> 3 [label=<p1>]
  2 [label=<2<br/><font color="#B276B2">❸</font><font color="#60BD68">❹</font>>]
  2 -> 0 [label=<!p1>]
  2 -> 4 [label=<p1>]
  3 [label=<3<br/><font color="#B276B2">❸</font><font color="#60BD68">❹</font>>]
  3 -> 4 [label=<!p1>]
  3 -> 1 [label=<p1>]
  4 [label=<4<br/><font color="#F17CB0">❶</font><font color="#FAA43A">❷</font><font color="#60BD68">❹</font>>]
  4 -> 4 [label=<!p1>]
  4 -> 4 [label=<p1>]
  5 [label=<5<br/><font color="#FAA43A">❷</font><font color="#60BD68">❹</font>>]
  5 -> 2 [label=<!p1>]
  5 -> 3 [label=<p1>]
  6 [label=<6<br/><font color="#FAA43A">❷</font><font color="#60BD68">❹</font>>]
  6 -> 5 [label=<!p1>]
  6 -> 5 [label=<p1>]
}
#+end_example

#+BEGIN_SRC dot :file tut30in.png :cmdline -Tpng :var txt=tut30in :exports results
$txt
#+END_SRC

#+RESULTS:
[[file:tut30in.png]]

Our goal is to generate an equivalent Büchi automaton, preserving
determinism if possible.  However nothing of what we will write is
specific to Rabin acceptance: the same code will convert automata with
any acceptance to Büchi acceptance.

* Shell

We use =autfilt= with option =-B= to request Büchi acceptance and
state-based output and =-D= to express a preference for deterministic
output.  Using option =-D/--deterministic= (or =--small=) actually
activates the "postprocessing" routines of Spot: the acceptance will
not only be changed to Büchi, but simplification routines (useless
SCCs removal, simulation-based reductions, acceptance sets
simplifications, WDBA-minimization, ...) will also be applied.

#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
autfilt -B -D tut30.hoa
#+END_SRC
#+RESULTS:
#+BEGIN_SRC hoa
HOA: v1
States: 5
Start: 1
AP: 1 "p1"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic weak
--BODY--
State: 0 {0}
[t] 0
State: 1
[t] 2
State: 2
[!0] 3
[0] 4
State: 3
[0] 0
[!0] 3
State: 4
[!0] 0
[0] 4
--END--
#+END_SRC

#+NAME: tut30out
#+BEGIN_SRC sh :results verbatim :exports none
autfilt -B -D -d tut30.hoa
#+END_SRC

#+RESULTS: tut30out
#+begin_example
digraph G {
  rankdir=LR
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
  I [label="", style=invis, width=0]
  I -> 1
  0 [label="0", peripheries=2]
  0 -> 0 [label=<1>]
  1 [label="1"]
  1 -> 2 [label=<1>]
  2 [label="2"]
  2 -> 3 [label=<!p1>]
  2 -> 4 [label=<p1>]
  3 [label="3"]
  3 -> 0 [label=<p1>]
  3 -> 3 [label=<!p1>]
  4 [label="4"]
  4 -> 0 [label=<!p1>]
  4 -> 4 [label=<p1>]
}
#+end_example

#+BEGIN_SRC dot :file tut30out.png :cmdline -Tpng :var txt=tut30out :exports results
$txt
#+END_SRC

#+RESULTS:
[[file:tut30out.png]]

In the general case transforming an automaton with a complex
acceptance condition into a Büchi automaton can make the output
bigger.  However the postprocessing routines may manage to simplify
the result further.


* Python

The Python version uses the =postprocess()= routine:

#+BEGIN_SRC python :results output :exports both :wrap SRC hoa
import spot
aut = spot.automaton('tut30.hoa').postprocess('BA', 'deterministic')
print(aut.to_str('hoa'))
#+END_SRC
#+RESULTS:
#+BEGIN_SRC hoa
HOA: v1
States: 5
Start: 1
AP: 1 "p1"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic weak
--BODY--
State: 0 {0}
[t] 0
State: 1
[t] 2
State: 2
[!0] 3
[0] 4
State: 3
[0] 0
[!0] 3
State: 4
[!0] 0
[0] 4
--END--
#+END_SRC

The =postprocess()= function has an interface similar to
[[file:tut10.org][the =translate()= function discussed previously]]:

#+BEGIN_SRC python :results output :exports both
import spot
help(spot.postprocess)
#+END_SRC

#+RESULTS:
#+begin_example
Help on function postprocess in module spot:

postprocess(automaton, *args)
    Post process an automaton.

    This applies a number of simlification algorithms, depending on
    the options supplied. Keep in mind that 'Deterministic' expresses
    just a preference that may not be satisfied if the input is
    not already 'Deterministic'.

    The optional arguments should be strings among the following:
    - at most one in 'Generic', 'TGBA', 'BA', or 'Monitor'
      (type of automaton to build)
    - at most one in 'Small', 'Deterministic', 'Any'
      (preferred characteristics of the produced automaton)
    - at most one in 'Low', 'Medium', 'High'
      (optimization level)
    - any combination of 'Complete' and 'StateBasedAcceptance'
      (or 'SBAcc' for short)

    The default corresponds to 'generic', 'small' and 'high'.

#+end_example


* C++

The C++ version of this code is a bit more verbose, because the
=postprocess()= function does not exist.  You have to instantiate a
=postprocessor= object, configure it, and then call it for each
automaton to process.

#+BEGIN_SRC C++ :results verbatim :exports both :wrap SRC hoa
  #include <iostream>
  #include <spot/parseaut/public.hh>
  #include <spot/twaalgos/postproc.hh>
  #include <spot/twaalgos/hoa.hh>

  int main()
  {
    spot::parsed_aut_ptr pa = parse_aut("tut30.hoa", spot::make_bdd_dict());
    if (pa->format_errors(std::cerr))
      return 1;
    if (pa->aborted)
      {
        std::cerr << "--ABORT-- read\n";
        return 1;
      }
    spot::postprocessor post;
    post.set_type(spot::postprocessor::BA);
    post.set_pref(spot::postprocessor::Deterministic);
    post.set_level(spot::postprocessor::High);
    auto aut = post.run(pa->aut);
    spot::print_hoa(std::cout, aut) << '\n';
    return 0;
  }
#+END_SRC

#+RESULTS:
#+BEGIN_SRC hoa
HOA: v1
States: 5
Start: 1
AP: 1 "p1"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic weak
--BODY--
State: 0 {0}
[t] 0
State: 1
[t] 2
State: 2
[!0] 3
[0] 4
State: 3
[0] 0
[!0] 3
State: 4
[!0] 0
[0] 4
--END--
#+END_SRC

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