---

POScheduler.java

package gov.nasa.arc.ase.jpf.jvm;

import gov.nasa.arc.ase.jpf.iSystemState;
import gov.nasa.arc.ase.jpf.iThreadInfo;
import gov.nasa.arc.ase.jpf.JPFErrorException;

public class POScheduler extends Scheduler {
  private static final int NONE = -1;
  private static final int UNKNOWN = -2;

  private int thread;
  private int random;
  private boolean lastRandom;
  private int safeThread;
  private boolean safeMove;

  public POScheduler(iSystemState ss) {
    initialize(ss);
  }  
  public POScheduler(POScheduler ps) {
    thread = ps.thread;
    random = ps.random;
    lastRandom = ps.lastRandom;
    safeThread = ps.safeThread;
    safeMove = ps.safeMove;
    ss = null;
  }  
  public Object clone() {
    return new POScheduler(this);
  }  
  public void failedProviso() {
    safeMove = false;
    thread = 0;
    random = 0;
    lastRandom = true;
  }  
  public int getRandom() {
    return random;
  }  
  public int getThread() {
    return thread;
  }  
  public void initialize(iSystemState ss) {
    this.ss = (SystemState)ss;
    thread = 0;
    random = 0;
    lastRandom = true;
    safeThread = UNKNOWN;
    safeMove = false;
  }  
  public iThreadInfo locateThread(iSystemState ss) {
    int limit = ss.getThreadCount();
    int unsafeThread = -1;

    if(safeMove) return null;

    if(safeThread == UNKNOWN) {
      // check for a safe move the first time
      for(int n = ss.getThreadCount(); thread < n; thread++) {
    iThreadInfo th = ss.getThreadInfo(thread);

    if(th.isSafe() && th.isRunnable()) {
      safeThread = thread;
      safeMove = true;
      return th;
    }
      }
      thread = 0;
      safeThread = NONE;
    }

    for(int n = ss.getThreadCount(); thread < n; thread++)
      if(thread != safeThread) {
    iThreadInfo th = ss.getThreadInfo(thread);

    if(th.isRunnable())
      return th;
      }

    return null;
  }  
  public void next() {
    if(safeMove)
      ((SystemState)ss).ti.addComment("safe move");
    else
      ((SystemState)ss).ti.addComment("non safe move");
    if(lastRandom) {
      random = 0;
      thread++;
    } else {
      random++;
    }
  }  
  public int random(int max) {
    lastRandom = (random == max-1);

    return random;
  }  
}

---