package finiteAutomata;
import java.util.Vector;
/**
 * Deterministic Finite Automaton.
 * 
 * <BR><BR>A dfa has a non-empty, finite set of states Q; an alphabet 
 * S; a transition function d which maps Q x S to Q; a unique "start" 
 * state; and zero or more "final" states.  The language L which is 
 * accepted by the dfa is the set of all strings s in S* which direct 
 * the dfa from "start" to any "final" state (according to the 
 * transition function d).
 * 
 * <BR><BR>Data Fields: 
 * In the DFA class we represent a DFA's transition function as a 
 * 2-dimensional array of integers.  Suppose the DFA has n states and m   
 * alphabet symbols. For any integer i from 0 through n-1 and any integer 
 * j from 0 through m-1, transition[i][j] indicates where to transition 
 * to (from state i) on reading the j-th alphabet symbol.  A 1-dimensional  
 * boolean array "isFinal" is used to indicate which states (if any) are  
 * final. In addition, each DFA has a Vector (stateLabel) of Strings to 
 * label the states, an Alphabet (alpha) of input symbols, a counter 
 * (numStates) for |Q|, and a variable start state (start).
 * 
 * <BR><BR>Methods: 
 * The DFA class has methods for generating the language of all strings 
 * accepted by the DFA (in lexicographic order, up through strings of the
 * specified length n), for testing whether or not a given input string 
 * is accepted by the DFA, for demonstrating the Pumping Lemma for 
 * Regular Languages on a given language string, and for pruning 
 * inaccessible states from the DFA.
 * 
 * <BR><BR>Note: From the user's point of view, states are referred to by label.  
 * Internally, states are numbered 0,1,2,... where 0 is not necessarily the start
 * state.
 * 
 * @author Barbara Wahl
 * @version Fall 2007
 */
public class DFA {
	// ** DATA FIELDS **
	/**
	 * number of states
	 */
	protected int numStates;
	
	/**
	 * list of labels for the states
	 */	
	protected Vector stateLabel;  
	
	/**
	 * Alphabet of input symbols
	 */
	protected Alphabet alpha;
	
	/**
	 * transition[i][j] tells where to transition 
	 * to (from state i) on reading the j-th alphabet symbol
	 */
	protected int[][] transition; 
	
	/**
	 * boolean array to designate final states
	 */
	protected boolean[] isFinal;
	
	/**
	 * start state
	 */
	protected int start;
		
	
	// ** CONSTRUCTORS **
	/**
	 * 0-parameter constructor, uses console input.
	 * @post constructs a DFA according to information obtained from the user
	 */
	public DFA() 
	{
		// predefined = true if user wants to use a predefined object
		boolean predefined = queryPredefined();
		if(predefined)
			predefinedDialog();
		else
		{   // get specs for user-defined DFA
			numStates = queryNumStates();		
			
			stateLabel = new Vector(numStates); // Vector for state labels
			queryLabels();                      // get state labels from user
			
			start = queryStart();               // initialize start state	
			queryAlphabet();                    // initialize alphabet
			
			isFinal = new boolean[numStates];   // allocate isFinal array
			queryFinal();                       // initialize isFinal array				
			
			// allocate & initialize transition array
			transition = new int[numStates][alpha.size()]; 
			queryTransition();   
		}

		System.out.println("\nYour DFA has been constructed as follows:");
		printDFA();
		
		// repeatedly display menu, allowing user to change transitions,
		// test strings, etc.
		int choice = 0;
		boolean done = false;
		while(!done)
		{
			choice = constructorMenu(); // get user action choice
			done = menuHandler(choice);
		} 		
	}
	
	/**
	 * 6-parameter constructor.
	 * @param n number of states
	 * @param L String array of state labels
	 * @param startL String label for the start state
	 * @param a String representation of the input alphabet
	 * @param t array representation of the transition function
	 * @param f boolean array to determine final states
	 * @pre n > 0
	 * @pre L is an array containing n non-null String objects
	 * @pre startL equals one of the strings in L
	 * @pre a is a non-empty String with no repeated characters or 
	 * whitespace
	 * @pre t has dimensions n by a.length()
	 * @pre every integer i in array t satisfies 0 <= i < n
	 * @post constructs an n-state DFA with alphabet a and transition 
	 * array t, state labels given by L, and final states given by f
	 * @post deep copies are made of all the arguments so that subsequent
	 * changes to any of these arguments will not affect the DFA constructed
 	 * by this method
	 */
	public DFA(int n, String[] L, String startL, String a, int[][] t, boolean[] f)
	{
		Assert.pre(n > 0, "n is positive");
		numStates = n;                   // initialize numStates	
		
		stateLabel = new Vector(n);      // allocate stateLabel array		
		for(int i=0; i<n; i++)           // initialize stateLabel array
			stateLabel.add(new String(L[i]));		
		
		start = stateNumber(startL);     // initialize start state	
		Assert.pre(start >= 0, 
				"startL is one of the String objects in L");
		
		alpha = new Alphabet(a);         // initialize alphabet	
		
		transition = new int[n][alpha.size()];  // allocate transition array		
		for(int i=0; i<n; i++)           // initialize transition array
			for(int j=0; j<alpha.size(); j++)
			{
				Assert.pre(t[i][j] >= 0 && t[i][j] < n,
						"every integer i in array t satisfies 0 <= i < n");
				transition[i][j] = t[i][j];
			}		
		
		isFinal = new boolean[n];	    // allocate isFinal array	
		System.arraycopy(f,0,isFinal,0,n);     // copy f to isFinal
	}
	
	// ** PUBLIC METHODS **
	/**
	 * Tests whether this DFA accepts a given String.
	 * @param inString the String to be tested
	 * @return true iff this DFA accepts inString
	 * @pre inString is non-null
	 */		
	public boolean accepts(String inString)
	{		
		// Step 1:  Convert inString to an int array where each char is
		// represented by its position in the alphabet (return false
		// if find any symbols which are not in the alphabet)
		int len = inString.length(); // input length
		int[] charAt = new int[len];
		if(!alpha.indexArray(inString,charAt))
			return false; 
				
		// Step 2:  Run the DFA on s 
		int currentState = start; // start state
		for(int i=0; i<len; i++) // for each input symbol
			// move to the next state according to the transition function			
			currentState =  transition[currentState][charAt[i]];
		
		// Step 3:  Return result (is last state final?)
		return isFinal[currentState];	
	}
	
	/**
	 * Returns all the states which are reachable from start.
	 * @return IntSet of all the states which are reachable from start 
	 * in 0 or more transitions
	 */
	public IntSet accessible()
	// note: if a state is accessible, it must be possible to reach
	//       it in fewer than numStates transitions [can prove this 
	//       with the pigeonhole principle]
	{
		IntSet S = new IntSet(start); 
		return accessible(S,numStates-1);		
	}
	/**
	 * Returns all the states which are reachable from a given set of states 
	 * in a given number of steps.
	 * @param S IntSet of states from which to start
	 * @param steps maximum number of transitions allowed
	 * @return IntSet of all the states which are reachable from some state 
	 * in S in steps or fewer transitions
	 * @pre each state i in S satisfies 0 <= i < numStates
	 * @pre steps >= 0
	 */
	public IntSet accessible(IntSet S, int steps)
	// note: accessible(S,0) = S [ base case ] 
	// note: if steps >= numStates, 
	//              accessible(S,steps) = accessible(S,numStates-1)
	{
		if(S.isEmpty() || steps == 0) return S; // base case
		
		Assert.pre(steps >= 0, "steps is non-negative");
		Assert.pre(S.min() >= 0,
			"each state i in S satisfies i >= 0");
		Assert.pre(S.max() < numStates,
			"each state i in S satisfies i < numStates");
		
		if(steps > numStates-1) // these extra steps have no effect
			steps = numStates-1;  
		
		// recursive case -- make progress!
		IntSet previous = accessible(S,steps-1);
		// add in any states one transition away from "previous"
		int state;
		for(int i=0; i<previous.size(); i++)  // for each state in previous
		{
			state = previous.elementAt(i);
			for(int j=0; j<alpha.size(); j++) // try each symbol
				previous.add(transition[state][j]);	
		}
		return previous;
	}
	
	/**
	 * Returns the set of state numbers of all final states.
	 * @return an IntSet containing the state numbers of all final
	 * states
	 */
	public IntSet finalStates()
	{
		IntSet s = new IntSet();
		for(int i=0; i<numStates; i++)
			if(isFinal[i])
				s.add(i);
		return s;
	}
	
	
	/**
	 * Pretty-prints the DFA specifications.
	 */
	public void printDFA()
	{
		// report numStates
		System.out.println("numStates = " + numStates);	
		
		// report alphabet
		System.out.println("alphabet = " + alpha.toPrettyString());	
		
		// report starting state
		System.out.println("The start state is: " + stateName(start));
		
		// get state numbers of final states & report final states
		IntSet f = this.finalStates();		
		System.out.print("The final states are: ");
		if(f.isEmpty())
			System.out.println("(no final states)");
		else
			for(int i=0; i<f.size(); i++)
				System.out.print(stateName(f.elementAt(i)) + " ");
		System.out.println();	
		
		// report transitions
		System.out.println("Transition function:");
		this.printTransitions();
		System.out.println();	
	}
	
	/**
	 * Returns the language accepted by this DFA, thru a given max length.
	 * @param n maximum string length
	 * @return Vector containing the language accepted by this DFA, in lexicographic 
	 * order, up through strings of length n (returns null if n < 0)
	 */
	public Vector getLanguage(int n)
	{
		if(n<0)
			return null; // no strings have negative length
		
		Vector v = alpha.getLanguage(n); // v holds alpha* up through length n

		for(int i=1; i<v.size(); i++)
		// if ith element of v is not accepted by the DFA, remove it
			if(!this.accepts(v.elementAt(i).toString()))
				v.remove(i);	

		return v;	
	}

	/**
	 * Prints the language accepted by this DFA, thru a given max length.
	 * @param n maximum string length
	 * @post prints the language accepted by this DFA, in lexicographic 
	 * order, up through strings of length n 
	 * @post prints nothing if n < 0
	 * @post prints "<empty language>" if n >= 0 and no strings of length
	 * n or less are accepted
	 */
	public void printLanguage(int n)
	{
		if(n < 0)
			return; // prints nothing if n < 0
		
		Vector v = this.getLanguage(n);

		if(v.size() == 0)
		{
			System.out.println("<empty language>");
			return;
		}

		Alphabet.printLanguage(v);
	}
		
	/**
	 * Pretty-prints the DFA transitions.
	 * @post prints each transition on its own line in the form 
	 * "(from,x) -> to", where "from" and "to" are state names 
	 * and x is an input symbol
	 */
	public void printTransitions()
	{
		int d; // the destination state
		for(int i=0; i<numStates; i++)
			for(int j=0; j<alpha.size(); j++)
			{	
				d = transition[i][j];
				System.out.println("(" + stateName(i) + "," + 
						alpha.charAt(j) + ") -> " + stateName(d));				
			}				
	}
	

	/**
	 * Eliminates inaccessible states.
	 * @post eliminates all inaccessible states from this DFA; alpha 
	 * is unchanged, but all the other data fields may change
	 */
	public void prune()
	{
		IntSet accessible = this.accessible(); // states reachable from start
		int newSize = accessible.size();// number of states after pruning		
		if(newSize == numStates)        // if no states are inaccessible...
			return; 		   	        // done!
		// To finish, remove the inaccessible states and update the data fields
		// NOTE:  for each state x in "accessible", state # x in the 
		//        old dfa will become state # accessible.indexOf(x) 
		//        in the pruned dfa.  For example, if 
		//        accessible = [0,3,7] then state #0 becomes #0, 
		//        state #3 becomes #1, and state #7 becomes #2.

		// update stateLabel Vector, working tail to head
		for(int i = numStates - 1; i >= 0; i--)
			if(!accessible.contains(i)) // if state i is inaccessible
				stateLabel.removeElementAt(i);		
		
		// store new transition and isFinal arrays in temp arrays
		int[][] transTemp = new int[newSize][alpha.size()];
		boolean[] finalTemp = new boolean[newSize];
		int oldState;
		for(int i=0; i<newSize; i++) // for each state in new DFA...
		{
			oldState = accessible.elementAt(i);
			finalTemp[i] = isFinal[oldState]; 
			for(int j=0; j<alpha.size(); j++)   // for each symbol...
			    // record the correct transition in transTemp
				transTemp[i][j] = 
					accessible.indexOf(transition[oldState][j]);
		}			
		// record new values
		transition = transTemp;			
		isFinal = finalTemp;		
		numStates = newSize;
		start = accessible.indexOf(start);
	}
	
	
	/**
	 * Demonstrates the Pumping Lemma for Regular Languages.
	 * @param inString String to be pumped
	 * @pre inString.length() >= numStates
	 * @pre inString is accepted by this DFA
	 * @post prints info to the console to answer the following:
	 *         (i)   What is a "pumping length" p? 
	 *         (ii)  What are values of x, y, and z which satisfy 
	 *               Sipser's Thm 1.70 (Pumping Lemma for 
	 *               Regular Languages)? 
	 *         (iii) Which strings are generated by pumping inString 
	 *               down or up? (xz, xyyz, xyyyz, xyyyyz, ...)
	 */
	public void pump(String inString)
	{
		// print heading & test pre-conditions (false if pre-conditions fail)
		if(!pumpTest(inString)) return;
		
		// visited[i] == -1 indicates that state i has not been visited;
		// visited[i] == k means this DFA was in state i immediately before
		// reading the kth character of inString
		int[] visited = new int[numStates];
		for(int i=0; i<numStates; i++)
			visited[i] = -1;			
		int current = start;  // which state is currently active
		int pos = 0;          // which char in "inString" is next to be read		
		StringBuffer x, y, z; // as in Pumping Lemma p.78
		x = new StringBuffer();
		y = new StringBuffer();
		z = new StringBuffer();		
		while(true) // look for first repeated state
		{
			visited[current] = pos; // mark current state as visited
			int j = alpha.indexOf(inString.charAt(pos)); 
			current = transition[current][j]; // advance to next state
			pos++;                            // advance to next input char			
			if(visited[current] != -1)
				break; // break when repeated state is found
		}		 
		for(int i=0; i<visited[current]; i++)  // Fill "x" with first
			x.append(inString.charAt(i));      // segment of inString		
		for(int i=visited[current]; i<pos; i++) // Fill "y" with middle
			y.append(inString.charAt(i));       // segment of inString		
		for(int i=pos; i<inString.length(); i++) // Fill "z" with
			z.append(inString.charAt(i));        // rest of inString
		
		// Print Report
		System.out.println("   " + inString + " satisfies the pumping lemma " +
		"as follows:");
		System.out.print("     x = "); 
		Util.printString(x.toString());      // use in case x is empty
		System.out.println("\n     y = " + y); // y will not be empty!
		System.out.print("     z = "); 
		Util.printString(z.toString());      // use in case z is empty
		System.out.println("\n     note: |y| = " + y.length() + " > 0");
		System.out.println("     note: |xy| = " + pos + " <= p");
		System.out.print("   Pumping " + inString + " DOWN produces: ");
		// if "y" is all of inString, then pumping down produces xz = epsilon
		if(y.length() == inString.length()) 
			System.out.println("epsilon");
		else System.out.println(x.toString() + z.toString());
		System.out.println("   Pumping " + inString + " UP produces: " 
				+ x + y + y + z + ", "               // xyyz
				+ x + y + y + y + z +", "            // xyyyz
				+ x + y + y + y + y + z + ", etc."); // xyyyyz
	}
	
	/**
	 * Returns the label for a given state number.
	 * @param i the state number
	 * @return the label for state i
	 * @pre i is a valid state number
	 */
	public String stateName(int i)
	{
		Assert.pre(this.validState(i),"i is a valid state number");
		return (String)this.stateLabel.elementAt(i);
	}
	
	 /** Returns the index of a given String in the stateLabel vector.
	 * @param s state label
	 * @return int i such that s equals stateLabel.elementAt(i), or -1
	 * if not found
	 * @pre s is not null
	 */
	public int stateNumber(String s)
	{
		return stateLabel.indexOf(s);
	}
	
	/**
	 * Tests whether a given String is a valid state label.
	 * @param s String to be tested
	 * @return true iff s is contained in the stateLabel vector
	 * @pre s is not null
	 */
	public boolean validLabel(String s)
	{
		return stateLabel.contains(s);
	}	
	
	/**
	 * Tests whether a given int is in the proper range to be a state
	 * number.
	 * @param i int value to be tested
	 * @return true iff 0 <= i < numStates
	 */
	public boolean validState(int i)
	{
		return (i >= 0 && i < numStates);
	}
	
	// ** MENU AND QUERY METHODS **	
	/**
	 * Displays constructor menu options until user makes a valid choice.
	 * @return choice (int from 1 thru 8)
	 */
	protected int constructorMenu()
	{
		boolean valid = false;
		int choice = -1;
		
		while(!valid)
		{		
			System.out.println("\nChoose an action: ");
			System.out.println("  1 = change a transition");
			System.out.println("  2 = print this DFA");
			System.out.println("  3 = print the language of this DFA");
			System.out.println("  4 = test a non-empty string");
			System.out.println("  5 = test the epsilon string");
			System.out.println("  6 = remove all inaccessible states");
			System.out.println("  7 = pump a string on this DFA");
			System.out.println("  8 = DONE with this DFA");
			
			choice = Util.readNum();
			if(1 <= choice && choice < 9)
				valid = true;
		}
		return choice;
	}
	
	/**
	 * Takes the appropriate action based on constructorMenu options.
	 * @param choice user's desired action code
	 * @return true iff user is done with menu
	 * @pre 1 <= choice <= 8
	 */
	protected boolean menuHandler(int choice)
	{
		Assert.pre(1 <= choice && choice <= 8,
				"1 <= choice <= 8");
		switch (choice)
		{
		case 8: // quit from menu
			System.out.println("Ciao!");
			return true;
		case 7: // pump
			System.out.println("Enter an accepted string with " +
				"length >= " + numStates);
			this.pump(Util.readString());
			break;
		case 6: // prune
			this.prune();
			break;
		case 5: // test epsilon string
			this.testEpsilonDialog();
			break;
		case 4: // test a non-epsilon string
			testStringDialog();
			break;
		case 3: // print language
			printLanguageDialog();
			break;
		case 2: // print 
			printDFA();
			break;
		case 1: // change a transition
			changeTransitionDialog();
		} 
		return false;
	}
	
	/**
	 * Allows the user to repeatedly test strings or print this
	 * DFA's language.
	 * @post each input string is echoed back to the console with
	 * a report of the string's length and whether or not it is
	 * accepted
	 */
	protected void testingHandler()
	{
		int n;
		boolean done = false;
		while(!done)
		{
			n = testingMenu(); // get menu choice from user
			
			// take the appropriate action
			switch (n) { 
			case 4: // quit
				done = true;
				break;
			case 3: // print the FA's language
				printLanguageDialog();
				break;
			case 2: // test a non-empty string
				testStringDialog();
				break;
			case 1: // test epsilon string
				testEpsilonDialog();
			}
		}			
		System.out.println("Good-bye!");
	}
	
	/**
	 * Presents testing menu options to user and obtains valid choice.
	 * @return choice (int from 1 thru 4)
	 */
	protected int testingMenu()
	{
		int n;
		while(true) // present menu until valid choice is made
		{
			System.out.println("\nTesting Menu Options " +
				"(enter your choice): " +
				"\n  1 = test the empty string (epsilon) " +
				"\n  2 = test a non-empty string " +
				"\n  3 = print the FA's language " +
				"\n  4 = DONE testing");
			n = Util.readNum();		
			if(n>0 && n<=4) break;
			System.out.println("TRY AGAIN!");
		}
		return n;
	}
	
	/**
	 * Tests whether the epsilon string is accepted.
	 * @post reports string length (0) and result
	 */
	protected void testEpsilonDialog()
	{
		System.out.print("input = epsilon, length = 0");
		if(this.accepts(""))
			System.out.println(" -- ACCEPTED!");
		else
			System.out.println(" -- REJECTED!");
		
	}
	
	/**
	 * Queries user for string to test and reports back.
	 * @post reports string length and result
	 */
	protected void testStringDialog()
	{
		String inString;
		System.out.print("Enter the test string (no spaces): ");
		inString = Util.readString();
		System.out.print("input = " + inString +
				", length = " + inString.length());				
		if(this.accepts(inString))
			System.out.println(" -- ACCEPTED!\n");
		else
			System.out.println(" -- REJECTED!\n");
	}
	
	/**
	 * Reports language of DFA up through user-specified max length.
	 * @post queries user for max string length; reports language of
	 * DFA up through that max length
	 */
	protected void printLanguageDialog()
	{
		int n;
		System.out.print("Enter a positive integer (maxLength): ");
		n = Util.readNum();
		this.printLanguage(n);
	}
	
	/**
	 * Prints constructor menu banner and asks user how many states in DFA.
	 * @return positive int obtained from user for numStates
	 */
	protected int queryNumStates()
	{
		int num; // temp storage for integer input
		
		System.out.println("****** DFA CONSTRUCTOR MENU ******");
					
		// ask user how many states; don't accept inappropriate input
		num = 0; // an inappropriate input
		while(num < 1)
		{
			System.out.print(">> Enter a positive integer " +
					"(number of states): ");
			num = Util.readNum();
		}
		return num;
	}
	
	/**
	 * Obtains and initializes state labels based on user input.
	 * @post user is prompted to enter a label for each state; 
	 * responses are stored in stateLabel vector
	 */
	protected void queryLabels()
	{
		String inString;
		for(int i=0; i<numStates; i++)  
		{
			System.out.print(">> Enter a string to label state # " 
				+ i + ": ");
			inString = Util.readString();
			stateLabel.add(new String(inString));
		}
	}
	
	/**
	 * Asks user if they want to use a pre-defined DFA.
	 * @return true iff user response begins with 'Y' or 'y'
	 */
	protected boolean queryPredefined()
	{
		System.out.print("Do you want to use a pre-defined DFA? Enter Y or N: ");
		return Util.answerIsYes();
	}
	
	/**
	 * Queries user which pre-defined DFA they will use.
	 * @post initializes "this" DFA to match user choice
	 */
	protected void predefinedDialog()
	{
		int num;
		while(true)
		{
			System.out.println("Choose a pre-defined DFA: ");
			System.out.println("  1 = Sipser, Figure 1.4");
			System.out.println("  2 = Sipser, Figure 1.8");
			System.out.println("  3 = Sipser, Figure 1.10");
			System.out.println("  4 = Sipser, Figure 1.12");
			System.out.println("  5 = Sipser, Figure 1.14");
			System.out.println("  6 = Sipser, Figure 1.22");
			num = Util.readNum();
			if(0 < num && num < 7) 
				break;
		}
		switch(num){
		case 1: 
			constructD1();
			break;
		case 2: 
			constructD2();
			break;
		case 3: 
			constructD3();
			break;
		case 4: 
			constructD4();
			break;
		case 5: 
			constructD5();
			break;
		case 6: 
			constructD6();
		}
	}
	
	/**
	 * Asks user for start state.
	 * @return valid state number (int from 0 thru numStates - 1)
	 */
	protected int queryStart()
	{
		String inString = " ";  // temp storage for String input
		System.out.print(">> Enter the label of the start state: ");

		// get a valid state label
		while(true)
		{
			inString = Util.readString();
			if(validLabel(inString))
				break; 
			else 
				System.out.print(">> TRY AGAIN! Enter the label" +
						" of the start state: ");
		}		
		return stateNumber(inString);
	}
	
	/**
	 * Initializes alpha according to user input.
	 * @post input Alphabet is initialized
	 */
	protected void queryAlphabet()
	{
		System.out.print(">> Enter a string with no spaces or " +
				"repeated characters (alphabet): ");
		alpha = new Alphabet(Util.readString());   
	}
	
	/**
	 * Initializes isFinal array according to user input.
	 * @post final states are initialized as requested by user
	 */
	protected void queryFinal()
	{
		for(int i=0; i<numStates; i++)
		{
			System.out.print(">> Enter true or false -- is state \"" + 
				stateName(i) + "\" final? ");
			isFinal[i] = Util.readBoolean();
		}
	}
	
	/**
	 * Queries user repeatedly to enter a state label.
	 * @return corresponding state number of the first valid 
	 * state label obtained
	 */
	protected int queryValidState()
	{
		String inString;
		while(true)
		{
			System.out.print("Enter LABEL of state: ");
			inString = Util.readString();
			if(validLabel(inString))
				break;
			else System.out.println("TRY AGAIN!");
		}
		return stateNumber(inString);
	}
	
	/**
	 * Queries user repeatedly to enter an input symbol.
	 * @return corresponding symbol number of the first 
	 * valid symbol obtained
	 */
	protected int queryValidSymbol()
	{
		char symbol;
		String inString;
		while(true)
		{
			System.out.print("Enter input symbol: ");
			inString = Util.readString();
			if(inString.length() == 1 && alpha.contains(inString.charAt(0)))
					break;
		}
		symbol = inString.charAt(0);
		return alpha.indexOf(symbol);
	}
	
	/**
	 * Queries user repeatedly to enter a valid destination state.
	 * @param i current state number
	 * @param j index of input symbol being read (position in alpha)
	 * @return destination state number (int from 0 thru numStates - 1)
	 * @pre 0 <= i < numStates and 0 <= j < alpha.size()
	 */
	protected int queryValidTransition(int i, int j)
	{
		Assert.pre(0 <= i && i < numStates,
			"0 <= i < numStates");
		Assert.pre(0 <= j && j < numStates,
			"0 <= j < numStates");
		String inString;
		while(true)
		{
			System.out.print(">> In state \"" + stateName(i) + 
					"\", on input symbol " + alpha.charAt(j) + 
					", go to (enter LABEL of next state): ");
			inString = Util.readString();
			if(validLabel(inString))  
				break;
			else System.out.println(">> TRY AGAIN! ");					
		}
		return stateNumber(inString);
	}
	
	/**
	 * For each state and each alphabet symbol, asks user for destination.
	 * @post transition array is filled with valid state numbers as given
	 * by user
	 */
	protected void queryTransition()
	{
		int toState;
		
		// Discover, for each state and each alphabet symbol, where to 
		// go?  Use responses to initialize transition array.  

		for(int i=0; i<numStates; i++) // for each "from" state 
			for(int j=0; j<alpha.size(); j++) // for each alphabet symbol 
			{
				toState = queryValidTransition(i,j);
				transition[i][j] = toState;
			}
	}
	
	/**
	 * Changes one transition based on user input.
	 * @post transition array is altered in zero or one places, as
	 * requested by user
	 */
	protected void changeTransitionDialog()
	{
		System.out.println("To change a transition, enter FROM STATE "+
				"and SYMBOL");
		int i = queryValidState();
		int j = queryValidSymbol();
		int k = queryValidTransition(i,j);
		transition[i][j] = k;
		System.out.println("The transition ("+stateName(i)+","+
				alpha.charAt(j)+") -> " + stateName(k) + " has "
				+ "been recorded");		
	}
	
	// ** PUMPTEST METHOD (TO SUPPORT PUMP METHOD) **
	/**
	 * Prints header for pump report and tests the pumping preconditions.
	 * @param inString String to be pumped
	 * @return true iff inString.length() >= numStates and inString
	 * is accepted
	 * @post (1) prints header for "pump" report 
	 *       (2) reports error if inString.length() < numStates 
	 *       (3) reports error if inString is not accepted 
	 */
	protected boolean pumpTest(String inString)
	{
		System.out.println("\n>> Trying to PUMP \"" + inString + 
			"\" on current FA...");
		System.out.println("A sufficient pumping length is p = " + 
			numStates);		
		// return false if inString is too short or is not accepted ...
		if(inString.length() < numStates)
		{
			System.out.println("ERROR: \"" + inString + "\" is too SHORT;" +
				" it's not guaranteed to be pumpable.");
			System.out.println("(The Pumping Lemma only applies to " + 
				"strings which are \"long\".)");
			return false;
		}		
		if(!this.accepts(inString))
		{
			System.out.println("ERROR: \"" + inString + "\" is NOT ACCEPTED " 
				+ "by this FA, so it is not pumpable.");
			System.out.println("(The Pumping Lemma only applies to strings " 
				+ "which are accepted by the FA.)");		
			return false;
		}
		return true;
	}
	
	// ** PRE-DEFINED DFA OBJECTS **	
	/**
	 * Initializes this to be the DFA corresponding to Sipser, Figure 1.4.
	 * @post all data fields are initialized to make a DFA equivalent to
	 * Sipser, Figure 1.4
	 */
	protected void constructD1()
	{
		numStates = 3;
		start = 0;
		alpha = new Alphabet("01");
		
		// store state labels
		stateLabel = new Vector();
		stateLabel.add(new String("q1"));
		stateLabel.add(new String("q2"));
		stateLabel.add(new String("q3"));
		
		// store transitions in array "t"
		transition = new int[numStates][alpha.size()];
		transition[0][0] = 0; // (q1,0)->q1
		transition[0][1] = 1; // (q1,1)->q2
		transition[1][0] = 2; // (q2,0)->q3
		transition[1][1] = 1; // (q2,1)->q2
		transition[2][0] = 1; // (q3,0)->q2
		transition[2][1] = 1; // (q3,1)->q2
		
		// store boolean values to set final states (q2)
		isFinal = new boolean[numStates];
		isFinal[1] = true;		
	}
	
	/**
	 * Initializes this to be the DFA corresponding to Sipser, Figure 1.8.
	 * @post all data fields are initialized to make a DFA equivalent to
	 * Sipser, Figure 1.8
	 */
	protected void constructD2()
	{
		numStates = 2; 
		start = 0;
		alpha = new Alphabet("01");
		
		// store state labels
		stateLabel = new Vector();
		stateLabel.add(new String("q1"));
		stateLabel.add(new String("q2"));
		
		// store transitions 
		transition = new int[numStates][alpha.size()];
		transition[0][0] = 0; // (q1,0)->q1
		transition[0][1] = 1; // (q1,1)->q2
		transition[1][0] = 0; // (q2,0)->q1
		transition[1][1] = 1; // (q2,1)->q2

		// store boolean values to set final states (q2)
		isFinal = new boolean[numStates];
		isFinal[1] = true;
	}
	
	/**
	 * Initializes this to be the DFA corresponding to Sipser, Figure 1.10.
	 * @post all data fields are initialized to make a DFA equivalent to
	 * Sipser, Figure 1.10
	 */
	protected void constructD3()
	{
		numStates = 2; 
		start = 0;
		alpha = new Alphabet("01");
		
		// store state labels
		stateLabel = new Vector();
		stateLabel.add(new String("q1"));
		stateLabel.add(new String("q2"));
		
		// store transitions 
		transition = new int[numStates][alpha.size()];
		transition[0][0] = 0; // (q1,0)->q1
		transition[0][1] = 1; // (q1,1)->q2
		transition[1][0] = 0; // (q2,0)->q1
		transition[1][1] = 1; // (q2,1)->q2

		// store boolean values to set final states (q1)
		isFinal = new boolean[numStates];
		isFinal[0] = true;
	}
	
	/**
	 * Initializes this to be the DFA corresponding to Sipser, Figure 1.12.
	 * @post all data fields are initialized to make a DFA equivalent to
	 * Sipser, Figure 1.12
	 */
	protected void constructD4()
	{
		numStates = 5; 
		start = 0;
		alpha = new Alphabet("ab");
		
		// store state labels
		stateLabel = new Vector();
		stateLabel.add(new String("s"));
		stateLabel.add(new String("q1"));
		stateLabel.add(new String("q2"));
		stateLabel.add(new String("r1"));
		stateLabel.add(new String("r2"));
		
		// store transitions 
		transition = new int[numStates][alpha.size()];
		transition[0][0] = 1; // (s,a)->q1
		transition[0][1] = 3; // (s,b)->r1
		transition[1][0] = 1; // (q1,a)->q1
		transition[1][1] = 2; // (q1,b)->q2
		transition[2][0] = 1; // (q2,a)->q1
		transition[2][1] = 2; // (q2,b)->q2
		transition[3][0] = 4; // (r1,a)->r2
		transition[3][1] = 3; // (r1,b)->r1
		transition[4][0] = 4; // (r2,a)->r2
		transition[4][1] = 3; // (r2,b)->r1

		// store boolean values to set final states (q1, r1)
		isFinal = new boolean[numStates];
		isFinal[1] = true;
		isFinal[3] = true;
	}
	
	/**
	 * Initializes this to be the DFA corresponding to Sipser, Figure 1.14.
	 * @post all data fields are initialized to make a DFA equivalent to
	 * Sipser, Figure 1.14
	 */
	protected void constructD5()
	{
		numStates = 3; 
		start = 0;
		alpha = new Alphabet("R012");
		
		// store state labels
		stateLabel = new Vector();
		stateLabel.add(new String("q0"));
		stateLabel.add(new String("q1"));
		stateLabel.add(new String("q2"));
		
		// store transitions
		transition = new int[numStates][alpha.size()];
		transition[0][0] = 0; // (q0,R)->q0
		transition[0][1] = 0; // (q0,0)->q0
		transition[0][2] = 1; // (q0,1)->q1
		transition[0][3] = 2; // (q0,2)->q2
		transition[1][0] = 0; // (q1,R)->q0
		transition[1][1] = 1; // (q1,0)->q1
		transition[1][2] = 2; // (q1,1)->q2
		transition[1][3] = 0; // (q1,2)->q0
		transition[2][0] = 0; // (q2,R)->q0
		transition[2][1] = 2; // (q2,0)->q2
		transition[2][2] = 0; // (q2,1)->q0
		transition[2][3] = 1; // (q2,2)->q1

		// store boolean values to set final states (q0)
		isFinal = new boolean[numStates];
		isFinal[0] = true;
	}
	
	/**
	 * Initializes this to be the DFA corresponding to Sipser, Figure 1.22.
	 * @post all data fields are initialized to make a DFA equivalent to
	 * Sipser, Figure 1.22
	 */
	protected void constructD6()
	{
		numStates = 4; 
		start = 0;
		alpha = new Alphabet("01");
		
		// store state labels
		stateLabel = new Vector();
		stateLabel.add(new String("q"));
		stateLabel.add(new String("q0"));
		stateLabel.add(new String("q00"));
		stateLabel.add(new String("q001"));
		
		// store transitions 
		transition = new int[numStates][alpha.size()];
		transition[0][0] = 1; // (q,0)->q0
		transition[0][1] = 0; // (q,1)->q
		transition[1][0] = 2; // (q0,0)->q00
		transition[1][1] = 0; // (q0,1)->q
		transition[2][0] = 2; // (q00,0)->q00
		transition[2][1] = 3; // (q00,1)->q001
		transition[3][0] = 3; // (q001,0)->q001
		transition[3][1] = 3; // (q001,1)->q001
		
		// store boolean values to set final states (q2)
		isFinal = new boolean[numStates];
		isFinal[3] = true;
	}

	// ** TEST METHOD **
	public static void main(String[] args) 
	{
		new DFA(); // runs DFA menu
	}
}