---

StateStack.java

package gov.nasa.arc.ase.jpf;

import java.util.*;
import gov.nasa.arc.ase.util.Debug;
import gov.nasa.arc.ase.jpf.jvm.SystemState;
import gov.nasa.arc.ase.jpf.jvm.ArrayWrapper;

public class StateStack extends Stack implements iStateStack  {
  int max_depth = 0;

  public boolean Full() {
    return (size() == max_depth); 
  }  
  public boolean Full(int extra) {
    return ((max_depth != -1) && 
            (size() == (max_depth+extra)));
  }  
  public iSystemState Peek() {
    return (iSystemState)peek();
  }  
  public iSystemState Pop() {
    pop();
    return TopOfStack();
  }  
  public boolean Push(iSystemState s) {
    push(s);
    if (size() > Runner.max_stack_depth)
      Runner.max_stack_depth = size();
    return (size() != max_depth); 
  }  
  public void setMaxDepth(int value) {
    max_depth = value;
  }  
  iSystemState TopOfStack() {
    if (isEmpty())
      return null;
    else  
      return (iSystemState)peek();
  }  
  public void UpdateTop(iScheduler current) {
    iSystemState s = TopOfStack();
    Scheduler sch = s.getScheduler();

    if (TransitionResult.isRandom()) {
// ifdef DEBUG

//#endif DEBUG
      sch.incCurrentRandom(current);
    } else if (TransitionResult.isNotified() && Engine.options.notify) {
// ifdef DEBUG

//#endif DEBUG
      sch.incCurrentNotify(current);
      //sch.setNotifying();
    } else {
// ifdef DEBUG

//#endif DEBUG
      sch.incCurrentThread(current);
      //sch.clearNotifying();
    }
  }  
  public void UpdateTopExtra(iSystemState ss) {
    iSystemState top = TopOfStack();

    top.updateExtra(ss);
  }  
}

---