// Author: Christian Schilling (schillic@informatik.uni-freiburg.de)
// Date: 2016-10-03
// 
// This example showed that ReduceNwaDirectSimulationB could reduce more states
// than ReduceNwaDirectSimulation for finite automata.

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)); // TODO error

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


NestedWordAutomaton nwa = (
	callAlphabet = {},
	internalAlphabet = {a0 a1 a2 a3 a4 a5 a6 a7 },
	returnAlphabet = {},
	states = {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 },
	initialStates = {s10 },
	finalStates = {s0 s1 s3 s5 s7 s9 },
	callTransitions = {
	},
	internalTransitions = {
		 (s0 a0 s0)
		 (s0 a1 s0)
		 (s0 a2 s0)
		 (s0 a3 s0)
		 (s0 a4 s0)
		 (s0 a5 s0)
		 (s0 a6 s0)
		 (s0 a7 s0)
		 (s1 a2 s4)
		 (s1 a3 s6)
		 (s1 a5 s5)
		 (s1 a6 s5)
		 (s1 a7 s5)
		 (s2 a0 s0)
		 (s2 a1 s0)
		 (s2 a2 s2)
		 (s2 a2 s4)
		 (s2 a3 s3)
		 (s2 a3 s7)
		 (s2 a3 s8)
		 (s2 a3 s9)
		 (s2 a4 s0)
		 (s2 a5 s5)
		 (s2 a5 s10)
		 (s2 a6 s5)
		 (s2 a6 s10)
		 (s2 a7 s5)
		 (s2 a7 s10)
		 (s3 a2 s4)
		 (s3 a3 s5)
		 (s3 a5 s5)
		 (s3 a6 s5)
		 (s3 a7 s5)
		 (s4 a2 s4)
		 (s4 a3 s6)
		 (s4 a5 s5)
		 (s4 a6 s5)
		 (s4 a7 s5)
		 (s5 a2 s4)
		 (s5 a3 s5)
		 (s5 a5 s5)
		 (s5 a6 s5)
		 (s5 a7 s5)
		 (s6 a2 s1)
		 (s6 a3 s5)
		 (s6 a5 s5)
		 (s6 a6 s5)
		 (s6 a7 s5)
		 (s7 a2 s4)
		 (s7 a3 s5)
		 (s7 a5 s5)
		 (s7 a6 s5)
		 (s7 a7 s5)
		 (s8 a0 s0)
		 (s8 a1 s0)
		 (s8 a2 s2)
		 (s8 a2 s4)
		 (s8 a3 s5)
		 (s8 a3 s10)
		 (s8 a4 s0)
		 (s8 a5 s5)
		 (s8 a5 s10)
		 (s8 a6 s5)
		 (s8 a6 s10)
		 (s8 a7 s5)
		 (s8 a7 s10)
		 (s10 a0 s0)
		 (s10 a1 s0)
		 (s10 a2 s2)
		 (s10 a2 s4)
		 (s10 a3 s5)
		 (s10 a3 s10)
		 (s10 a4 s0)
		 (s10 a5 s5)
		 (s10 a5 s10)
		 (s10 a6 s5)
		 (s10 a6 s10)
		 (s10 a7 s5)
		 (s10 a7 s10)
	},
	returnTransitions = {
	}
);