// Testfile dumped by Ultimate at 2012/09/04 13:34:19

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 == 10);
assert(reduceNwaDelayedSimulationSize == 10);
assert(reduceNwaDelayedSimulationBSize == 10);
// assert(reduceNwaDelayedFullMultipebbleSimulationSize == 10);
assert(reduceBuchiFairDirectSimulationSize == 10);
assert(reduceBuchiFairSimulationSize == 10);

NestedWordAutomaton nwa = (
	callAlphabet = {},
	internalAlphabet = {a20 a0 a10 },
	returnAlphabet = {},
	states = {q11 q01 q51 q41 q31 q21 q91 q81 q71 q61 },
	initialStates = {q01 },
	finalStates = {q81 q71 },
	callTransitions = {
	},
	internalTransitions = {
		 (q11 a10 q91)
		 (q11 a10 q71)
		 (q01 a0 q41)
		 (q01 a10 q81)
		 (q01 a10 q71)
		 (q51 a20 q61)
		 (q51 a10 q31)
		 (q51 a10 q61)
		 (q41 a20 q41)
		 (q41 a10 q51)
		 (q41 a10 q21)
		 (q31 a10 q11)
		 (q31 a10 q51)
		 (q31 a10 q71)
		 (q31 a10 q61)
		 (q21 a10 q41)
		 (q21 a10 q71)
		 (q91 a20 q21)
		 (q91 a20 q61)
		 (q91 a10 q51)
		 (q81 a20 q31)
		 (q81 a20 q91)
		 (q81 a10 q81)
		 (q71 a0 q91)
		 (q71 a10 q11)
		 (q71 a10 q31)
		 (q61 a20 q11)
		 (q61 a20 q61)
		 (q61 a10 q51)
		 (q61 a10 q31)
	},
	returnTransitions = {
	}
);