// Testfile dumped by Ultimate at 2012/10/01 11:24:24

// Automaton where minimizeSevpa(senwa(nwa)) has more states than the original
// automaton.
// 
// Reason: The senwa operation splits spExit to sExit and pExit (in fact, to
// one copy of spExit with entry sEntry and one copy of pExit with entry 
// pEntry).
// Both states sExit and pExit are not merged again in the minimization. Why?
// The senwa operation splits the return transition
// ("spExit" "sEntry" "returnVonPNachS" "spExit")
// into the following four return transitions.
// ("sExit" "sEntry" "returnVonPNachS" "sExit")
// ("sExit" "sEntry" "returnVonPNachS" "pExit")
// ("pExit" "sEntry" "returnVonPNachS" "sExit")
// ("pExit" "sEntry" "returnVonPNachS" "pExit")
//
//
//
//
//

print(senwa( reachableStatesCopy(nwa)));

NestedWordAutomaton nwa = (
	callAlphabet = {"callVonSNachP" "callVonQNachS" },
	internalAlphabet = {"b"},
	returnAlphabet = {"returnVonSNachQ" "returnVonPNachS" },
	states = {"p1" "sEntry" "spExit" "pEntry" "qFin" "s2" "qInit" },
	initialStates = {"qInit" },
	finalStates = {"qFin" },
	callTransitions = {
		 ("sEntry" "callVonSNachP" "pEntry")
		 ("qInit" "callVonQNachS" "sEntry")
	},
	internalTransitions = {
		 ("pEntry" "b" "spExit")
	},
	returnTransitions = {
		 ("spExit" "qInit" "returnVonSNachQ" "qFin")
		 ("spExit" "sEntry" "returnVonPNachS" "spExit")
	}
);