// Testfile dumped by Ultimate at 2017/01/14 09:22:18
// Reduced by Christian Schilling on 2017-01-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 == 5);
assert(shrinkNwaSize == 5);
assert(minimizeNwaPmaxSatDirectBiSize == 5);
assert(minimizeNwaPmaxSatDirectSize == 5);
assert(minimizeDfaSimulationSize == 5);
assert(reduceNwaDirectSimulationSize == 5);
assert(reduceNwaDirectSimulationBSize == 5);
assert(reduceNwaDirectFullMultipebbleSimulationSize == 5);
assert(buchiReduceSize == 5);
assert(reduceNwaDelayedSimulationSize == 5);
assert(reduceNwaDelayedSimulationBSize == 5);
// assert(reduceNwaDelayedFullMultipebbleSimulationSize == 5);
assert(reduceBuchiFairDirectSimulationSize == 5);
assert(reduceBuchiFairSimulationSize == 5);

NestedWordAutomaton nwa = (
	alphabet = {"a" "b" },
	states = {"q_1" "qF_1" "q_3" "q_2" "q_4" "q_0" },
	initialStates = {"q_0" },
	finalStates = {"qF_1" },
	transitions = {
		("q_0" "a" "q_1")
		("q_1" "b" "q_2")
		("q_2" "a" "q_2")
		("q_2" "a" "q_3")
		("q_3" "b" "qF_1")
		
		("qF_1" "a" "q_4")
		("q_1" "a" "q_4")
		("q_4" "b" "qF_1")
	}
);