// collection of some small and interesting nested word automata
// Author: heizmann@informatik.uni-freiburg.de
 
NestedWordAutomaton sameCalldifferentReturns = (
	callAlphabet = { call },
	internalAlphabet = { },
	returnAlphabet = { ret },
	states = {q0 q1 q2 },
	initialStates = { q0 },
	finalStates = { q2 },
	callTransitions = {
		 (q0 call q0)
	},
	internalTransitions = {
	},
	returnTransitions = {
		 (q0 q0 ret q1)
		 (q1 q0 ret q2)
	}
);
 
 
 
// Xiaolin, heizmann@informatik.uni-freiburg.de, 7.3.2011

print(determinize(wBenjamin));

NestedWordAutomaton wBenjamin = (
	callAlphabet = {c},
	internalAlphabet = {a},
	returnAlphabet = {r},
	states = {q0 q1 q2 q3},
	initialStates = {q0},
	finalStates = {q3},
	callTransitions = {
		(q0 c q0)
		(q0 c q1)
	},
	internalTransitions = { 
		(q3 a q0) 
	},
	returnTransitions = {
		(q1 q0 r q2)
		(q2 q0 r q3)
	}
);
 

 
// Date: 8.6.2011
// Author: heizmann@informatik.uni-freiburg.de

// Problem:
// DeterminizeJM used initial state as hierarchical Predecessor.
// I don't know yet if this can lead to a real bug.
// Anyway, this might be a useful test.
assert(!accepts(pendingReturnNwa, [ >r ]));
assert(!accepts(determinize(pendingReturnNwa), [ >r ]));
print(determinize(pendingReturnNwa));

NestedWordAutomaton pendingReturnNwa = (
	callAlphabet = { c },
	internalAlphabet = { a },
	returnAlphabet = { r },
	states = { q0 q1 },
	initialStates = { q0 },
	finalStates = { q1 },
	callTransitions = {
	},
	internalTransitions = {
	},
	returnTransitions = {
	    (q0 q0 r q1)
	}
);

 




assert(!isEmpty(bugBfsEmptinessLowPriorityCallQueue));
print(bugBfsEmptinessLowPriorityCallQueue);

NestedWordAutomaton bugBfsEmptinessLowPriorityCallQueue = (
	callAlphabet = {m1_call_gInit gInitCallSelfloop },
	internalAlphabet = {mInit_To_m1 _2_gExit mLast_2_fin },
	returnAlphabet = {gExit_m1_return_mLast gExit_gInit_return_m2 },
	states = {gInit gExit mLast m1 m2 },
	initialStates = {gInit m1 },
	finalStates = {mLast },
	callTransitions = {
		 (gInit gInitCallSelfloop gInit)
		 (m1 m1_call_gInit gInit)
	},
	internalTransitions = {
		 (m2 _2_gExit gExit)
		 (gInit _2_gExit gExit)
	},
	returnTransitions = {
		 (gExit gInit gExit_gInit_return_m2 m2)
		 (gExit m1 gExit_m1_return_mLast mLast)
	}
);