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

assert(buchiIsEmpty(nwa));
assert(numberOfStates(removeNonLiveStates(nwa)) == 0);

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