// Büchi automaton as in  Fig.3 of the Etessami paper (consisting of 10 states).
// Good example in common test, because it contains a lot of states that are in
// delayed simulation with each other.
// The resulting reduced automaton has two states, according to the paper.

// automaton has 10 states
// gamegraph has 570 states, infinity is 91
// gamegraph consists of 73 SCCs
// reduced automaton has 2 states and 3 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 == 10);
assert(shrinkNwaSize == 10);
assert(minimizeNwaPmaxSatDirectBiSize == 10);
assert(minimizeNwaPmaxSatDirectSize == 10);
assert(minimizeDfaSimulationSize == 10);
assert(reduceNwaDirectSimulationSize == 10);
assert(reduceNwaDirectSimulationBSize == 10);
assert(reduceNwaDirectFullMultipebbleSimulationSize == 10);
assert(buchiReduceSize == 2);
assert(reduceNwaDelayedSimulationSize == 2);
assert(reduceNwaDelayedSimulationBSize == 2);
// assert(reduceNwaDelayedFullMultipebbleSimulationSize == 2);
assert(reduceBuchiFairDirectSimulationSize == 2);
assert(reduceBuchiFairSimulationSize == 2);

NestedWordAutomaton nwa = (
	callAlphabet = {},
	internalAlphabet = {a b },
	returnAlphabet = {},
	states = {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 },
	initialStates = {s0 },
	finalStates = {s0  },
	callTransitions = {
	},
	internalTransitions = {
		 (s0 a s1)
		 (s1 a s2)
		 (s2 a s3)
		 (s3 a s4)
		 (s4 a s5)
		 (s5 a s6)
		 (s6 a s7)
		 (s7 a s8)
		 (s8 a s0)
		 (s9 b s0)
		 (s9 b s1)
		 (s9 b s2)
		 (s9 b s3)
		 (s9 b s4)
		 (s9 b s5)
		 (s9 b s6)
		 (s9 b s7)
		 (s9 b s8)
		 
		 (s0 b s9)
		 (s1 b s9)
		 (s2 b s9)
		 (s3 b s9)
		 (s4 b s9)
		 (s5 b s9)
		 (s6 b s9)
		 (s7 b s9)
		 (s8 b s9)
	},
	returnTransitions = {
	}
);