/*---------------------------------------------------------------------------
File:         			PDA.java
Package:                        JFLAP Version 1.0
Author:				Magda & Octavian Procopiuc V1.0 07/15/96
                                
Description of Contents:	Contains class PDA.
				
--------------------------------------------------------------------------*/

/* 
 * Susan H. Rodger, Magda Procopiuc, Octavian Procopiuc, Eric Gramond
 * Computer Science Department
 * Duke University
 * June 1998
 * Supported by National Science Foundation DUE-9596002 and DUE-9555084.
 *
 * Copyright (c) 1998
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms are permitted
 * provided that the above copyright notice and this paragraph are
 * duplicated in all such forms and that any documentation,
 * advertising materials, and other materials related to such
 * distribution and use acknowledge that the software was developed
 * by the author.  The name of the author may not be used to
 * endorse or promote products derived from this software without
 * specific prior written permission.
 * THIS SOFTWARE IS PROVIDED ``AS IS'' AND WITHOUT ANY EXPRESS OR
 * IMPLIED WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED
 * WARRANTIES OF MERCHANTIBILITY AND FITNESS FOR A PARTICULAR PURPOSE.
 */

package flap;

import java.util.*;
import java.awt.*;

/**
 * This class simulates the behavior of a 
 * pushdown automaton.
 *
 * @author	Magda & Octavian Procopiuc
 * @version	1.0 15 July 1996
 */ 
public class PDA extends Machine { 

// Acceptance types 
  final static String FINAL_STATE = "Final State";
  final static String EMPTY_STACK = "Empty Stack";
  final static String FINAL_AND_EMPTY = "Final State & Empty Stack";

  String	acceptanceType = FINAL_STATE;

/**
 * creates PDA corresponding to its desktop image.
 */
  public PDA(Desktop d) {
    super(d);
  }


    /**
     * creates a PDA corresponding to the argument PDA
     */

    public PDA(PDA p) {
      super(p);
    }

/*
 * Creates a new configuration starting from configuration c, according
 * to the transition rule of a PDA
 * Overrides Machine.expand()
 */
  boolean expand(Configuration c) {
    boolean willBeValid;
    Transition t;
    Configuration cc;

    String input, pop, push;

    willBeValid = false;
    for (Enumeration et=c.theState.transitions.elements(); et.hasMoreElements(); )   {
      t = (Transition) et.nextElement();
      StringTokenizer stk = new StringTokenizer(t.label, ",;", false);
      input = stk.nextToken().trim();
      pop = stk.nextToken().trim();
      push = stk.nextToken().trim();
      if (c.theString.startsWith(input) && c.theStack.startsWith(pop)) {
        willBeValid = true;
        cc = new Configuration(t.to, c.theString.substring(input.length()), push + c.theStack.substring(pop.length()), c, this);
        if (!isAlreadyIn(temp, cc)) {
          temp.addElement(cc);
          nCurrentConfigs++;
          if (cc.isAccept()) {
            acceptInput = true;
            acceptingConfig = cc;
          }
        }
      }
    }
    return willBeValid;
  }  // end of method expand

/*
 * Creates the initial configuration.
 * Overrides Machine.initialConfig().
 */
  Configuration initialConfig() {
    return new Configuration(d.initialState, input, "Z", null, this);
  } // end of method initialConfig



  /** Places all the states for the solved DFA solution */
  public void placeAllStates(Machine model, Machine nfa) {
	Dimension dim = d.getSize();
	
	if(d.theStates.size() != 3)
	    return;

	((State)d.theStates.elementAt(0)).p = new Point(dim.width/6, (5*dim.height)/6);
	((State)d.theStates.elementAt(1)).p = new Point(dim.width/2, (5*dim.height)/6);
	((State)d.theStates.elementAt(2)).p = new Point((5*dim.width)/6, (5*dim.height)/6);

  }



/*
 * Checks if a transition introduces non-determinism.
 * @param t	Transition to be checked.
 *        v	Vector of transitions against which t is checked.
 * @return	true if t does not introduce any non-determinism. 
 * Overrides Machine.isDeterministic().
 */
  boolean isDeterministic(Transition t, Vector v) {
    Enumeration e;
    Transition vt;
    String input, pop, push;
    String vinput, vpop, vpush;

    if (v.size() == 0) 
      return true;

    StringTokenizer stk = new StringTokenizer(t.label, ",;", false);
    input = stk.nextToken().trim();
    pop = stk.nextToken().trim();
    push = stk.nextToken().trim();

    for (e = v.elements(); e.hasMoreElements(); ) {
      vt = (Transition) e.nextElement();
      stk = new StringTokenizer(vt.label, ",;", false);
      vinput = stk.nextToken().trim();
      vpop = stk.nextToken().trim();
      vpush = stk.nextToken().trim();

      if (input.equals(vinput)) { 
         if (pop.equals(vpop))
           if ((t.to != vt.to) || (!push.equals(vpush)))
             return false;
           else {}
         else if (substringRelation(pop, vpop))
              return  false;  
      } else if (substringRelation(input, vinput) && substringRelation(pop, vpop))      
             return false;    
    }
  
    return true;
  }  // end of method isDeterministic




 /**  returns true if the Desktop matches the given PDA Desktop.
    * original should be null.
    */
  public String checkIfDone(Machine amodel, Machine original) {
    
    Enumeration e, e2, e3;
    State aState, aState2;
    Transition t, t1, t2;

    PDA model = (PDA) amodel;
    String error;
    
    if(mode == CFGtoPDA || mode == CFGtoPDALR) {
      try {        checkCFGtoPDAbase(model);    }
      catch (BadInputException ex) {        return ex.getMessage();   }
    }
    
    Vector list = d.makeLoopList();
    Vector listin = model.d.makeLoopList();
    boolean found = false;
    
      //check if everything in list is in listin (i.e. look for bad links)
    for(e = list.elements(); e.hasMoreElements(); ) {
      found = false;
      t = (Transition) e.nextElement();
      t.tokenizeLabel();
      for( e2 = listin.elements(); e2.hasMoreElements(); ) {
        t2 = (Transition) e2.nextElement();
        t2.tokenizeLabel();
        if(t.sublabel[0].trim().equals(t2.sublabel[0].trim()) &&
           t.sublabel[1].trim().equals(t2.sublabel[1].trim()) &&
           t.sublabel[2].trim().equals(t2.sublabel[2].trim()))
          found = true;
      }
      if(!found) {
        t.from.ss = State.FOCUSED;
        return "\nThere should be no transition labeled:\n" +
          t.sublabel[0].trim() + "," +
          t.sublabel[1].trim() + ";" + t.sublabel[2].trim() + 
          " on the highlighted state.";
      }
    }

      //check if everything in listin is in list (i.e. look for missing links)
    for(e = listin.elements(); e.hasMoreElements(); ) {
      found = false;
      t = (Transition) e.nextElement();
      t.tokenizeLabel();
      for( e2 = list.elements(); e2.hasMoreElements(); ) {
        t2 = (Transition) e2.nextElement();
        t2.tokenizeLabel();
        if(t.sublabel[0].trim().equals(t2.sublabel[0].trim()) &&
           t.sublabel[1].trim().equals(t2.sublabel[1].trim()) &&
           t.sublabel[2].trim().equals(t2.sublabel[2].trim()))
          found = true;
      }
      if(!found) {
        t.from.ss = State.FOCUSED;
        return "\nThere should be a loop transition labeled:\n" +
          t.sublabel[0].trim() + "," +
          t.sublabel[1].trim() + ";" + t.sublabel[2].trim();
      }
    }

    if(list.size() != listin.size()) 
      return "All transitions match but there\n should be exacly " + listin.size() +
        " loop transitions.\n (Check for identical transitions)";

    return "\n\nThe PDA is correct.";
  }
  
  
  private State checkState(State theState, State model, boolean loops) throws BadInputException {
    
    Transition t, tin = null;
    Enumeration e;
    theState.ss = State.FOCUSED;
    
    if(theState.isFinal != model.isFinal) {
      if(theState.isFinal)
        throw new BadInputException("\n\nThe highlighted state should not be final.");
      throw new BadInputException("\n\nThe highlighted state should be final.");
    }

      //if it's just a simple transition, no loops
    if(!loops) {
      if(theState.transitions.size() != 1) 
        throw new BadInputException("\nThere should be exactly one transition \nleaving from the highlighted state.");     
      
      t = (Transition) theState.transitions.elementAt(0);
      tin = (Transition) model.transitions.elementAt(0);
      t.tokenizeLabel();
      
      if(t.from == t.to) 
        throw new BadInputException("\nThe transition leaving from the \nhighlighted state cannot be a loop.");
      
      if(!t.sublabel[0].trim().equals(tin.sublabel[0].trim()) 
         || !t.sublabel[1].trim().equals(tin.sublabel[1].trim()) 
         || !t.sublabel[2].trim().equals(tin.sublabel[2].trim())) {

        throw new BadInputException("\nThe transition leaving from the \nhighlighted state should be labeled:\n" +
                                    tin.sublabel[0].trim() + "," + 
                                    tin.sublabel[1].trim() + ";" + 
                                    tin.sublabel[2].trim());
      }
      theState.ss = State.NORMAL;
      return t.to;
    }
      // skip the loops and check the 1 outgoing transition
    else {
	//find models next Transition
      for(e = model.transitions.elements(); e.hasMoreElements(); ) {
        tin = (Transition) e.nextElement();
        if(tin.to != model)
          break;
      }

      State nextState = null;
      Transition nextTrans = null;
      for(e = theState.transitions.elements(); e.hasMoreElements(); ) {
        t = (Transition) e.nextElement();
        if(t.from == t.to)
          continue;
        if(nextState != null) 
          throw new BadInputException("\nThere should only be one non-loop transition \nleaving the highlighted state");
        
        nextState = t.to;
        nextTrans = t;
      }
      if(nextState == null) 
        throw new BadInputException( "\nThe highlighted state has no \ntransition to the final state");
      tin.tokenizeLabel();
      nextTrans.tokenizeLabel();
      if(!nextTrans.sublabel[0].trim().equals(tin.sublabel[0].trim()) 
         || !nextTrans.sublabel[1].trim().equals(tin.sublabel[1].trim()) 
         || !nextTrans.sublabel[2].trim().equals(tin.sublabel[2].trim())) {
        System.out.println(nextTrans.sublabel[0]+nextTrans.sublabel[1]+nextTrans.sublabel[2]+"test2");

        System.out.println("test");
        throw new BadInputException( "\n\nThe transition leaving from the \nhighlighted state should be labeled:\n" +
          tin.sublabel[0].trim() + "," + tin.sublabel[1].trim() + ";" + 
          tin.sublabel[2].trim());
	}
      theState.ss= State.NORMAL;
      return nextState;
    }
  }
  

    /**
     * checks if the base 3 states are there and linked properly.
     * Given how many dumb things the user could do this is probably going
     * to end up being huge.
     * @return an error String, or null if correct
     */
  
  public void checkCFGtoPDAbase(PDA model) throws BadInputException {
    
    Transition t, tin;
    State s, sin, s2;
    Enumeration e;
    
    if (d.theStates.size() != 3) 
      throw new BadInputException( "\n\nThe machine should have exactly 3 states.");

    d.setTransitions(d.initialState, false);
    model.d.setTransitions(model.d.initialState, false);
    s = checkState(d.initialState, model.d.initialState,(mode == CFGtoPDALR)? true : false);
    sin = (State) model.d.theStates.elementAt(1);

    d.setTransitions(s, false);
    model.d.setTransitions(sin, false);
    s2 = checkState(s, sin,(mode == CFGtoPDALR) ? false:true);
    if(s2 == d.initialState) {
      s.ss = State.FOCUSED;
      throw new BadInputException("There should be no transitions leading \nback to the start state"); 
    }
    sin = (State) model.d.theStates.elementAt(2);     
    d.setTransitions(s2, false);
    model.d.setTransitions(sin, false);
    if(s2.transitions.size() != sin.transitions.size()) {
      s2.ss = State.FOCUSED;
      throw new BadInputException("\nThe third state should have exactly \n" + sin.transitions.size() +
        " outgoing transitions.");
    }	
    return;
  }

}  // end of class PDA
