// Testfile dumped by Ultimate at 2012/01/09 13:33:53

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)); // TODO error
int reduceBuchiFairSimulationSize = numberOfStates(reduceBuchiFairSimulation(preprocessed));

assert(minimizeSevpaSize == 3);
assert(shrinkNwaSize == 3);
assert(minimizeNwaPmaxSatDirectBiSize == 3);
assert(minimizeNwaPmaxSatDirectSize == 3);
assert(minimizeDfaSimulationSize == 3);
assert(reduceNwaDirectSimulationSize == 3);
assert(reduceNwaDirectSimulationBSize == 3);
assert(reduceNwaDirectFullMultipebbleSimulationSize == 3);
assert(buchiReduceSize == 3);
assert(reduceNwaDelayedSimulationSize == 3);
assert(reduceNwaDelayedSimulationBSize == 3);
// assert(reduceNwaDelayedFullMultipebbleSimulationSize == 3);
// assert(reduceBuchiFairDirectSimulationSize == 3); // TODO add correct number after error is fixed
assert(reduceBuchiFairSimulationSize == 3);

NestedWordAutomaton nwa = (
	callAlphabet = {},
	internalAlphabet = {"blue30" "green986" },
	returnAlphabet = {},
	states = {F1 F2 Init Q1 Q2 },
	initialStates = {Init },
	finalStates = {F1 F2 },
	callTransitions = {
	},
	internalTransitions = {
		 (Init "blue30" Q1)
		 (Init "blue30" F1)
		 (Init "green986" Init)
		 (Init "green986" F2)
		 (Q1 "blue30" Q1)
		 (Q1 "blue30" F1)
		 (Q1 "green986" Init)
		 (Q1 "green986" F2)
		 (F1 "blue30" Q2)
		 (F1 "green986" F2)
		 (F2 "blue30" Q2)
		 (F2 "green986" F2)
		 (Q2 "blue30" Q2)
		 (Q2 "green986" F2)
	},
	returnTransitions = {
	}
);