UP | HOME

Alternation removal

Table of Contents

Consider the following alternating co-Büchi automaton (see how to create it): 

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

Sorry, your browser does not support 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 TGBA for weak input, but the smallest automata are obtained if the input is very-weak.

Shell

We simply use autfilt with option --tgba: 

autfilt --tgba tut31.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--

Sorry, your browser does not support SVG.

Python

In the Python version we call remove_alternation() 

import spot
aut = spot.remove_alternation(spot.automaton('tut31.hoa'))
print(aut.to_str('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--

C++

The C++ version calls remove_alternation() too. 

#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;
}

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