// Date: 2014-09-19
// Author: heizmann@informatik.uni-freiburg.de
//
// Revealed a bug in MinimizeDFASimulation.
// Contains a dead-end state (qs).

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

NestedWordAutomaton nwa = (
    callAlphabet = {},
    internalAlphabet = {a },
    returnAlphabet = {},
    states = {q1 qs },
    initialStates = {q1 },
    finalStates = {q1 },
    callTransitions = {
    },
    internalTransitions = {
         (q1 a qs)
         (qs a qs)
    },
    returnTransitions = {
    }
);