# -*- coding: utf-8 -*-
#+TITLE: Alternation removal
#+DESCRIPTION: Code example for removing alternation in Spot
#+INCLUDE: setup.org
#+HTML_LINK_UP: tut.html
#+PROPERTY: header-args:sh :results verbatim :exports both
#+PROPERTY: header-args:python :results output :exports both
#+PROPERTY: header-args:C+++ :results verbatim :exports both

Consider the following alternating co-Büchi automaton (see [[file:tut23.org][how to
create it]]):

#+NAME: tut31in
#+BEGIN_SRC hoa
HOA: v1
States: 3
Start: 0
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[0] 0
[!0] 0&1
State: 1
[!0] 1 {0}
[0] 2
State: 2
[t] 2
--END--
#+END_SRC

#+NAME: tut31dot
#+BEGIN_SRC sh :exports none :noweb strip-export
cat >tut31.hoa <<EOF
<<tut31in>>
EOF
autfilt --dot tut31.hoa
#+END_SRC

#+BEGIN_SRC dot :file tut31in.svg :var txt=tut31dot :exports results
  $txt
#+END_SRC

#+RESULTS:
[[file:tut31in.svg]]

Our goal is to transform this alternating automaton into a
non-alternating automaton.

Alternation support in Spot should be considered as experimental.
Currently, alternation removal is only supported for weak alternating
automata, i.e., SCCs should have all there transitions in the same
acceptance marks.  The =remove_alternation()= procedure of Spot will
produce a [[file:concepts.org::#trans-acc][TGBA]] for [[file:concepts.org::#property-flags][weak]] input, but the smallest automata are obtained
if the input is [[file:concepts.org::#property-flags][very-weak]].

* Shell

We simply use =autfilt= with option =--tgba=:

#+BEGIN_SRC sh :wrap SRC hoa
autfilt --tgba tut31.hoa
#+END_SRC
#+RESULTS:
#+BEGIN_SRC hoa
HOA: v1
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[!0] 0 {0}
[0] 1 {0}
State: 1
[0] 1 {0}
[!0] 1
--END--
#+END_SRC

#+NAME: tut31out
#+BEGIN_SRC sh :exports none
autfilt --tgba -d tut31.hoa
#+END_SRC

#+BEGIN_SRC dot :file tut31out.svg :var txt=tut31out :exports results
$txt
#+END_SRC

#+RESULTS:
[[file:tut31out.svg]]

* Python

In the Python version we call =remove_alternation()=

#+BEGIN_SRC python :wrap SRC hoa
import spot
aut = spot.remove_alternation(spot.automaton('tut31.hoa'))
print(aut.to_str('hoa'))
#+END_SRC
#+RESULTS:
#+begin_SRC hoa
HOA: v1
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[0] 0 {0}
[!0] 1
State: 1
[0] 0 {0}
[!0] 1
--END--
#+end_SRC

* C++

The C++ version calls =remove_alternation()= too.

#+BEGIN_SRC C++ :wrap SRC hoa
  #include <iostream>
  #include <spot/parseaut/public.hh>
  #include <spot/twaalgos/alternation.hh>
  #include <spot/twaalgos/hoa.hh>

  int main()
  {
    spot::parsed_aut_ptr pa = parse_aut("tut31.hoa", spot::make_bdd_dict());
    if (pa->format_errors(std::cerr))
      return 1;
    if (pa->aborted)
      {
        std::cerr << "--ABORT-- read\n";
        return 1;
      }
    auto aut = spot::remove_alternation(pa->aut);
    spot::print_hoa(std::cout, aut) << '\n';
    return 0;
  }
#+END_SRC

#+RESULTS:
#+begin_SRC hoa
HOA: v1
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[0] 0 {0}
[!0] 1
State: 1
[0] 0 {0}
[!0] 1
--END--
#+end_SRC

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