---

LTL.java

package gov.nasa.arc.ase.jpf;

//#ifdef BUCHI
import gov.nasa.arc.ase.util.Debug;
import java.util.Stack;

public class LTL implements iSearch {
  public static final boolean FIRST_DFS     = true;
  public static final boolean SECOND_DFS    = false;

  public static final int OLD_OFF_STACK     = -1;
  public static final int NEW           = -2;

  private boolean done = false;
  private boolean failed = false;
  private boolean deadlock = false;
  private Path errorPath;
  private ErrorTrailInterface error;

  private Stack buchiStack;
  private Stack buchiSchStack;
  private Stack acptStack;
  private int buchiState;
  private Sch buchiSch;
  private SM buchi;
  private BuchiSet buchiSet;
  private Stack buchiSetStack;

  public LTL() {
    Debug.println(Debug.MESSAGE, "LTL Search");
    initBuchi();
  }  
  public int acptStack_peek() {
    if(acptStack.size() == 0) return -1;

    return ((Integer)acptStack.peek()).intValue();
  }  
  public void acptStack_pop(int index) {
    if(buchi.accepting[buchiState])
      acptStack.pop();
  }  
  public void acptStack_push(int index) {
    if(buchi.accepting[buchiState])
      acptStack.push(new Integer(index));
  }  
  public void buchi_backtrack() {
    buchi_pop();
    buchiSch_pop();
  }  
  public boolean buchi_forward() {
    buchi_push();
    boolean buchi_move = buchi_next();
    buchiSch_push();

    return buchi_move;
  }  
  public boolean buchi_next() {
    SM b = buchi;
    b.setSch(buchiSch);

    int nt = b.getTransitionCount(buchiState);
    int t = -1;
    boolean enabled = false;
    boolean first = buchiSch.getTransition() == 0 && buchiSch.getRandom() == 0;

    if(!first) {
      while(buchiSch.getTransition() < nt) {
    t = buchiSch.getTransition();
    if(b.getGuard(buchiState, t) != null) {
      if(b.isEnabled(buchiState, t)) {
        enabled = true;
        break;
      } else
        buchiSch.getNextTransition();
    } else
      buchiSch.getNextTransition();
      }
    } else {
      while(buchiSch.getTransition() < nt) {
    t = buchiSch.getTransition();
    if(b.getGuard(buchiState, t) != null) {
      if(b.isEnabled(buchiState, t)) {
        enabled = true;
        break;
      } else
        buchiSch.getNextTransition();
    } else {
      enabled = true;
      break;
    }
      }
    }

    if(!enabled) {
      buchiSch.getNextTransition();
      return false;
    }

//#ifdef DEBUG

//#endif DEBUG
    int r = buchiSch.getRandom();
    buchiState = b.execute(buchiState, t);
    if(r == buchiSch.getRandom())
      buchiSch.getNextTransition();
//#ifdef DEBUG

//#endif DEBUG

    return true;
  }  
  public void buchi_pop() {
    buchiState = ((Integer)buchiStack.pop()).intValue();
  }  
  public void buchi_push() {
    buchiStack.push(new Integer(buchiState));
  }  
  public void buchi_undo() {
    int t = buchiSch.getTransition();
    int r = buchiSch.getRandom();

    buchi.backtrack(buchiState, r == 0 ? t-1 : t);
  }  
  public void buchiSch_pop() {
    buchiSch = (Sch)buchiSchStack.pop();
  }  
  public void buchiSch_push() {
    buchiSchStack.push(buchiSch.copy());
  }  
  private void buchiSet_get() {
    buchiSet = Engine.getJPF().vm.BuchiGet();
  }  
  private void buchiSet_pop() {
    buchiSet = (BuchiSet)buchiSetStack.pop();
  }  
  private void buchiSet_push() {
    buchiSetStack.push(buchiSet);
    buchiSet = null;
  }  
  private void error() {
    failed = true;
    if (Engine.options.bandera) {
      errorPath = Engine.getJPF().vm.getErrorTrail1();
    } else {
      error = Engine.getJPF().vm.getErrorTrail();        
    }
    done = !Engine.options.multiple_errors;
  }  
  public ErrorTrailInterface getError() {
    return error;
  }  
  public String getErrorMessage() {
    if(!failed) return "No Errors Found";

    if(deadlock) return "Deadlock found";

    return Engine.getJPF().vm.getErrorMessage();
  }  
  public Path getErrorPath() {
    return errorPath;
  }  
  public boolean hasFailed() {
    return failed;
  }  
  public void initBuchi() {
    buchi = SM.load(Engine.options.buchi);

    buchiStack = new Stack();
    buchiSchStack = new Stack();
    acptStack = new Stack();
    buchiSetStack = new Stack();

    buchiState = 0;
  }  
  private void off_stack(boolean first) {
    buchiSet.replace((first ? 0x80000000 : 0) | buchiState, OLD_OFF_STACK);
  }  
  public void search() {
//#ifdef DEBUG

//#endif DEBUG
    search(FIRST_DFS, 0);
//#ifdef DEBUG

//#endif DEBUG
  }  
  private boolean search(boolean first, int stack_start) {
    int index = stack_start;
    boolean up = false;
    iVirtualMachine vm = Engine.getJPF().vm;
    Status status = Engine.getJPF().status;

Down:
    while(true) {
      vm.BuchiInitSch();
      while(true) {
    boolean buchiSet_get = false;

    if(!up) {
      int result = vm.BuchiForward();

      if(TransitionResult.isError(result)) {
        error();
        return true;
      }

      if(TransitionResult.isEnd(result)) {
//#ifdef DEBUG

//#endif DEBUG
        break;
      }

//#ifdef DEBUG

//#endif DEBUG

      buchiSch = new Sch();
      buchiSet_get = true;
    }

    while(true) {
      if(up) {

        Debug.println(Debug.MESSAGE, "Going up");

        up = false; index--;
        buchiSet_pop();
        off_stack(first);
        acptStack_pop(index);
        buchi_backtrack();
        buchi_undo();
        continue;
      }

      if(!buchi_forward()) {
//#ifdef DEBUG

//#endif DEBUG
        buchi_backtrack();
        break;
      }

//#ifdef DEBUG

//#endif DEBUG

      if(buchiSet_get) buchiSet_get();
      vm.BuchiSetState(buchiState);
      int currently = store(first, index);

      if(buchi.trivial[buchiState])
        if(buchi.accepting[buchiState]) {
          error();
          return true;
        } else {
          Debug.println(Debug.ERROR, "Reached a non-accepting trivial state");
          buchi_backtrack();
          buchi_undo();
          break;
        }

      if(currently == NEW) {
//#ifdef DEBUG

//#endif DEBUG
        status.states++;
        if(index != 0) status.transitions++;
        acptStack_push(index);
        index++;
        buchiSet_push();
        continue Down;
      } else {
//#ifdef DEBUG

//#endif DEBUG
        status.transitions++;
        if(currently != OLD_OFF_STACK) {
//#ifdef DEBUG

//#endif DEBUG
          if(currently <= acptStack_peek()) {
        error();
        Debug.println(Debug.ERROR, "Cycle detected");
        return true;
          }
        } else {
//#ifdef DEBUG

//#endif DEBUG
        }
      }

      buchi_backtrack();
      buchi_undo();
    }

    vm.BuchiBacktrack();
      }

      if(first && buchi.accepting[buchiState]) {
    if(!buchi.persistant[buchiState]) {
//#ifdef DEBUG

//#endif DEBUG
      vm.BuchiInitSch();
      boolean violation = search(SECOND_DFS, index);
//#ifdef DEBUG

//#endif DEBUG
      if(violation) return true;
    }
      }

      if(index == stack_start) break;


      Debug.println(Debug.MESSAGE, "Going up now");

      up = true;
    }

    return false;
  }  
  private int store(boolean first, int index) {
    int b = 0x80000000 | buchiState;

//#ifdef DEBUG


//#endif DEBUG

    if(!first) {
      int d = buchiSet.get(b);
      if(d > OLD_OFF_STACK) {
//#ifdef DEBUG

//#endif DEBUG
    return d;
      }
      b &= 0x7FFFFFFF;
    }

    int d = buchiSet.get(b);
    if(d >= OLD_OFF_STACK) {
//#ifdef DEBUG

//#endif DEBUG
      return d;
    }

    buchiSet.add(b, index);

    return NEW;
  }  
}

---