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

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

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

NestedWordAutomaton finitelyManyAWithSinkState = (
    callAlphabet = { },
    internalAlphabet = {a b},
    returnAlphabet = { },
    states = {q f s},
    initialStates = {q},
    finalStates = {f},
    callTransitions = { },
    internalTransitions = { (q a q) (q b q) (q b f) (f b f) (f a s) (s a s) (s b s) }, 
    returnTransitions = { }
);

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

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

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

NestedWordAutomaton all = (
	callAlphabet = { },
	internalAlphabet = {a b},
	returnAlphabet = { },
	states = {q0},
	initialStates = {q0},
	finalStates = {q0},
	callTransitions = { },
	internalTransitions = { (q0 a q0) (q0 b q0) }, 
	returnTransitions = { }
);

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