package jsetool.engine;

import java.util.Iterator;

import jsetool.data.*;
import jsetool.data.ExplorationStateContainer;
import jsetool.data.MachineState;
import jsetool.data.Transition;

/**
 * @author Mike Lawson
 * 
 * @since Oct 21, 2004
 * 
 * The StateExplorer class is the main-level driver of the state exploration
 * engine. Given a description of two communicating finite state machines, the
 * class will explore all the states that are possible between the two machines.
 * 
 *  
 */
public class StateExplorer
{

  protected MachineState machine1;

  protected MachineState machine2;
  
  protected long         millisToCompute;

  /**
   * Constructs a new StateExplorer object
   * 
   * @param machine1
   *          the first machine
   * @param machine2
   *          the second machine
   */
  public StateExplorer(MachineState machine1, MachineState machine2)
  {
    this.machine1 = machine1;
    this.machine2 = machine2;
  }

  /**
   * Explores the states of the two associated machines. Returns the "top" state
   * of the state tree for the results.
   * 
   * @return ExplorationState the top state of the resultant exploration.
   */
  public synchronized ExplorationState exploreStates()
  {
    long now = System.currentTimeMillis();
    
    // Always be sure to reset the factories cache.
    ExplorationState.resetKnownStates();
    
    ExplorationState initialState = buildInitialState();

    exploreState(initialState);

    long then = System.currentTimeMillis();
    
    millisToCompute = then - now;
    
    // The initial state will be populated with all found states.
    return initialState;

  }
  
  /**
   * Gets the time of computation in milliseconds.
   * 
   * @return long
   */
  public long getMillisToCompute()
  {
    return millisToCompute;
  }

  /**
   * Creates the initial (i1,i2,E,E) state.
   * 
   * @return ExplorationState
   */
  private ExplorationState buildInitialState()
  {
    // Constructs the initial (i1,i2,E,E) state.
    ExplorationState initialState = ExplorationState.emptyState(machine1, machine2);
    return initialState;
  }

  /**
   * Explores the given state in a depth-first manner.
   * 
   * @param stateToExplore
   */
  private void exploreState(ExplorationState stateToExplore)
  {
    
    // Prevent infinite recursion, if we have already visited this
    // state, we are done.
    if (stateToExplore.isExplored())
    {
      return;
    }
    else
    {
      stateToExplore.setExplored();

      examineM1(stateToExplore);
      examineC2ForM1(stateToExplore);
      examineM2(stateToExplore);
      examineC1ForM2(stateToExplore);

      // Check for deadlock and bail out if so.
      checkForDeadlock(stateToExplore);
      if (stateToExplore.isStateIsDeadlocked())
      {
        return;
      }
      else
      {
        // Otherwise, recurse for each state discovered.
        for (Iterator nextStateIter = stateToExplore.nextStateIterator(); nextStateIter.hasNext();)
        {
          ExplorationState.NextStateContainer nsc = (ExplorationState.NextStateContainer)nextStateIter.next();
          exploreState(nsc.getExplorationState());
        }
      }
    }

  }

  /**
   * Examines M1 for any send transitions, adds the new sub-states to the given
   * state.
   * 
   * @param stateToExplore
   */
  private void examineM1(ExplorationState stateToExplore)
  {

    // For each send transition in m1, allocate a new state that can be reached,
    // looking at m1 only.
    for (Iterator transitionIterator = stateToExplore.getMachine1().getMachineState().getSendTransitions(); transitionIterator.hasNext();)
    {
      Transition sendTransition = (Transition) transitionIterator.next();

      // Create a new state from the old state.
      ExplorationState newState = ExplorationState.newStateForM1(stateToExplore, sendTransition.getTargetState(), sendTransition.getMessage());

      // Add the new state to the state we are exploring.
      stateToExplore.addNextState(newState, "M1: -" + sendTransition.getMessage());

      // Mark the transition as visited.
      sendTransition.setExplored();
      
    } // for each send transition

    // Mark both machines in the exploration state as visited.
    stateToExplore.getMachine1().getMachineState().setExplored();
    stateToExplore.getMachine2().getMachineState().setExplored();

  }

  /**
   * Examines communication channel for machine 2 to see if there are any
   * messages that m1 can respond to.
   * 
   * @param stateToExplore
   */
  private void examineC2ForM1(ExplorationState stateToExplore)
  {
    // Take a peek at the first message in c2.
    String currentMessage = stateToExplore.getMachine2().peekFirstMessage();
    
    if (currentMessage == null)
    {
      return;
    }

    // This will be populated with the new state based on the reception or null
    // if we don't get a message we understand.
    ExplorationState newStateBasedOnReceive = null;

    // True if any message was found in the channel.
    boolean messageFound = false;

    //for each receive transition in m1
    for (Iterator receivesTransitionsInM1 = stateToExplore.getMachine1().getMachineState().getReceiveTransitions(); receivesTransitionsInM1.hasNext();)
    {
      messageFound = true;
      Transition receiveTransition = (Transition) receivesTransitionsInM1.next();
      String allowedToReceiveMessage = receiveTransition.getMessage();

      // if m1 can receive the current message, allocate a new ExplorationState,
      // changing m1
      if (allowedToReceiveMessage.equals(currentMessage))
      {        
        ExplorationState tempState = new ExplorationState(stateToExplore);
        tempState.getMachine2().getCommunicationChannel().remove(0);
        newStateBasedOnReceive = ExplorationState.newStateForM1(tempState, receiveTransition.getTargetState(), null);
        stateToExplore.addNextState(newStateBasedOnReceive, "M1: +" + currentMessage);        
        receiveTransition.setExplored();        
      }

    } // end for each possible reception

    // If there was at least one message, and we did not understand
    // any of them, then we have an unspecified reception error.
    if (messageFound && newStateBasedOnReceive == null)
    {
      stateToExplore.setStateIsUnspecifiedReception();
    }
  }

  /**
   * Examines M2 for any send transitions, adds the new sub-states to the given
   * state.
   * 
   * @param stateToExplore
   */
  private void examineM2(ExplorationState stateToExplore)
  {
    //  For each send transition in m2, allocate a new state that can be reached,
    // looking
    // at m1 only.
    for (Iterator transitionIterator = stateToExplore.getMachine2().getMachineState().getSendTransitions(); transitionIterator.hasNext();)
    {
      Transition sendTransition = (Transition) transitionIterator.next();

      // Create a new state from the old state.
      ExplorationState newState = ExplorationState.newStateForM2(stateToExplore, sendTransition.getTargetState(), sendTransition.getMessage());

      // Add the new state to the state we are exploring.
      stateToExplore.addNextState(newState, "M2: -" + sendTransition.getMessage());

      // Mark the transition as visited.
      sendTransition.setExplored();
      
    } // for each send transition

    // Mark both machines in the exploration state as visited.
    stateToExplore.getMachine1().getMachineState().setExplored();
    stateToExplore.getMachine2().getMachineState().setExplored();

  }

  /**
   * Examines communication channel for machine 1 to see if there are any
   * messages that m2 can respond to.
   * 
   * @param stateToExplore
   */
  private void examineC1ForM2(ExplorationState stateToExplore)
  {
    //  Take a peek at the first message in c1.
    String currentMessage = stateToExplore.getMachine1().peekFirstMessage();
    
    if (currentMessage == null)
    {
      return;
    }

    // This will be populated with the new state based on the reception or null
    // if we don't get a message we understand.
    ExplorationState newStateBasedOnReceive = null;

    // True if any message was found in the channel.
    boolean messageFound = false;

    //for each receive transition in m2
    for (Iterator receivesTransitionsInM2 = stateToExplore.getMachine2().getMachineState().getReceiveTransitions(); receivesTransitionsInM2.hasNext();)
    {
      messageFound = true;
      Transition receiveTransition = (Transition) receivesTransitionsInM2.next();
      String allowedToReceiveMessage = receiveTransition.getMessage();

      // if m2 can receive the current message, allocate a new ExplorationState,
      // changing m2
      if (allowedToReceiveMessage.equals(currentMessage))
      {
        
        ExplorationState tempState = new ExplorationState(stateToExplore);
        tempState.getMachine1().getCommunicationChannel().remove(0);
        newStateBasedOnReceive = ExplorationState.newStateForM2(tempState, receiveTransition.getTargetState(),null);        
        stateToExplore.addNextState(newStateBasedOnReceive, "M2: +" + currentMessage);
        
        receiveTransition.setExplored();        
      }

    } // end for each possible reception

    // If there was at least one message, and we did not understand
    // any of them, then we have an unspecified reception error.
    if (messageFound && newStateBasedOnReceive == null)
    {
      stateToExplore.setStateIsUnspecifiedReception();
    }

  }

  /**
   * Examines the exploration state for deadlock.
   * 
   * @param s
   */
  private void checkForDeadlock(ExplorationState s)
  {
    // Deadlock is: both sending communication channels are empty and 
    // there are no next states.
    
    if (s.getNumberOfNextStates() > 0)
    {
      // There are next states, continue processing.
      return;
    }
    
    ExplorationStateContainer m1 = s.getMachine1();
    ExplorationStateContainer m2 = s.getMachine2();
    
    int m1TransmissionSize = m1.getCommunicationChannel().size();
    int m2TransmissionSize = m2.getCommunicationChannel().size();
    
    boolean somethingIsBeingSent = (m1TransmissionSize > 0 || m2TransmissionSize > 0);
    
    if (somethingIsBeingSent == true)
    {
      // Something being sent is sufficient to denote that this is not a deadlock.
      return;
    }
    else
    {
      s.setStateIsDeadlocked();
    }
 
  }

}