// Testfile dumped by Ultimate at 2017/01/12 17:23:27
// Shrunk by Christian Schilling 2017/01/13
//
// Revealed a problem in the (delayed) simulation for dead ends.
// The problem is that q1 does not simulate q1 according to the method, but it
//  should. Consequently q0 should not simulate qF, but it does.
//
// Contains dead end states (q2, q3).

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 == 4);
assert(shrinkNwaSize == 4);
assert(minimizeNwaPmaxSatDirectBiSize == 4);
assert(minimizeNwaPmaxSatDirectSize == 4);
assert(minimizeDfaSimulationSize == 5);
assert(reduceNwaDirectSimulationSize == 4);
assert(reduceNwaDirectSimulationBSize == 4);
assert(reduceNwaDirectFullMultipebbleSimulationSize == 4);
assert(buchiReduceSize == 4);
assert(reduceNwaDelayedSimulationSize == 4);
assert(reduceNwaDelayedSimulationBSize == 4);
// assert(reduceNwaDelayedFullMultipebbleSimulationSize == 4);
assert(reduceBuchiFairDirectSimulationSize == 4);
assert(reduceBuchiFairSimulationSize == 4);

NestedWordAutomaton nwa = (
	alphabet = {"a"},
	states = {"qF" "q0" "q1" "q3" "q2"},
	initialStates = {"q0"},
	finalStates = {"qF"},
	transitions = {
		("q0" "a" "q1")
		
		("q1" "a" "q2")
		("q1" "a" "qF")
		
		("qF" "a" "q3")
	}
);