// Büchi automaton that consists of two copies of the automaton depicted in 
// Fig.3 of the Etessami paper (each automaton has 8 states).
//
// automaton has 19 states
// gamegraph has 2052 states, infinity is 324
// gamegraph consists of 1264 SCCs
// reduced automaton has 5 states and 8 internal transitions

// Author: saukho@informatik.uni-freiburg.de
// Author: lindenmm@informatik.uni-freiburg.de
// Date: 15.12.2011

NestedWordAutomaton preprocessed = removeUnreachable(nwa);

int minimizeSevpaSize = numberOfStates(minimizeSevpa(preprocessed));
int shrinkNwaSize = numberOfStates(shrinkNwa(preprocessed));
int minimizeNwaPmaxSatDirectBiSize = numberOfStates(minimizeNwaPmaxSatDirectBi(preprocessed));
int minimizeNwaPmaxSatDirectSize = numberOfStates(minimizeNwaPmaxSatDirect(preprocessed));
int minimizeDfaSimulationSize = numberOfStates(minimizeDfaSimulation(preprocessed));
int reduceNwaDirectSimulationSize = numberOfStates(reduceNwaDirectSimulation(preprocessed));
int reduceNwaDirectSimulationBSize = numberOfStates(reduceNwaDirectSimulationB(preprocessed));
int reduceNwaDirectFullMultipebbleSimulationSize = numberOfStates(reduceNwaDirectFullMultipebbleSimulation(preprocessed));
int buchiReduceSize = numberOfStates(buchiReduce(preprocessed));
int reduceNwaDelayedSimulationSize = numberOfStates(reduceNwaDelayedSimulation(preprocessed));
int reduceNwaDelayedSimulationBSize = numberOfStates(reduceNwaDelayedSimulationB(preprocessed));
// int reduceNwaDelayedFullMultipebbleSimulationSize = numberOfStates(reduceNwaDelayedFullMultipebbleSimulation(preprocessed));
int reduceBuchiFairDirectSimulationSize = numberOfStates(reduceBuchiFairDirectSimulation(preprocessed));
int reduceBuchiFairSimulationSize = numberOfStates(reduceBuchiFairSimulation(preprocessed));

assert(minimizeSevpaSize == 19);
assert(shrinkNwaSize == 19);
assert(minimizeNwaPmaxSatDirectBiSize == 19);
assert(minimizeNwaPmaxSatDirectSize == 19);
assert(minimizeDfaSimulationSize == 19);
assert(reduceNwaDirectSimulationSize == 19);
assert(reduceNwaDirectSimulationBSize == 19);
assert(reduceNwaDirectFullMultipebbleSimulationSize == 19);
assert(buchiReduceSize == 5);
assert(reduceNwaDelayedSimulationSize == 5);
assert(reduceNwaDelayedSimulationBSize == 5);
// assert(reduceNwaDelayedFullMultipebbleSimulationSize == 5);
assert(reduceBuchiFairDirectSimulationSize == 5);
assert(reduceBuchiFairSimulationSize == 5);

NestedWordAutomaton nwa = (
  callAlphabet = { },
  internalAlphabet = {a b c d x y},
  returnAlphabet = { },
  states = {I0 q0 q1 q2 q3 q4 q5 q6 q7 q8 p0 p1 p2 p3 p4 p5 p6 p7 p8},
  initialStates = {I0},
  finalStates = {q0 p0},
  callTransitions = {},
  internalTransitions = {
      (I0 y p0)
      (I0 x q0)
      (q0 a q1)
      (q1 a q2)
      (q2 a q3)
      (q3 a q4)
      (q4 a q5)
      (q5 a q6)
      (q6 a q7)
      (q7 a q0)
      (q8 b q0)
      (q8 b q1)
      (q8 b q2)
      (q8 b q3)
      (q8 b q4)
      (q8 b q5)
      (q8 b q6)
      (q8 b q7)
      (q0 b q8)
      (q1 b q8)
      (q2 b q8)
      (q3 b q8)
      (q4 b q8)
      (q5 b q8)
      (q6 b q8)
      (q7 b q8)
      (p0 c p1)
      (p1 c p2)
      (p2 c p3)
      (p3 c p4)
      (p4 c p5)
      (p5 c p6)
      (p6 c p7)
      (p7 c p0)
      (p8 d p0)
      (p8 d p1)
      (p8 d p2)
      (p8 d p3)
      (p8 d p4)
      (p8 d p5)
      (p8 d p6)
      (p8 d p7)
      (p0 d p8)
      (p1 d p8)
      (p2 d p8)
      (p3 d p8)
      (p4 d p8)
      (p5 d p8)
      (p6 d p8)
      (p7 d p8)
  }, 
  returnTransitions = {}
);