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

// Typical example for exponential blowup while determinizing
// finite automata.
// assert(!accepts(9thFromLast, [b a a a a a a a a]));
// assert(accepts(9thFromLast, [a a a a a a a a a]));
// assert(!accepts(9thFromLast, [b b b b b a a a a a a a a]));
// assert(!isEmpty(9thFromLast));
// assert(!isEmpty(complement(9thFromLast)));

//print(removeDeadEnds(determinizeLazyTest(9thFromLast)));

assert(numberOfStates(determinize(9thFromLast)) == 512);


NestedWordAutomaton 9thFromLast = (
  callAlphabet = {},
  internalAlphabet = {a b},
  returnAlphabet = {},
  states = {q0 q1 q2 q3 q4 q5 q6 q7 q8 q9 },
  initialStates = {q0},
  finalStates = {q9},
  callTransitions = {},
  internalTransitions = {
	(q0 a q0) (q0 b q0) (q0 a q1)
	(q1 a q2) (q1 b q2)
	(q2 a q3) (q2 b q3)
	(q3 a q4) (q3 b q4)
	(q4 a q5) (q4 b q5)
	(q5 a q6) (q5 b q6)
	(q6 a q7) (q6 b q7)
	(q7 a q8) (q7 b q8)
	(q8 a q9) (q8 b q9)
  }, 
  returnTransitions = {}
);