---

DefaultScheduler.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 DefaultScheduler extends Scheduler {
  private int thread;
  private int random;
  private boolean lastRandom;

  public DefaultScheduler(iSystemState ss) {
    initialize(ss);
  }  
  public DefaultScheduler(DefaultScheduler ds) {
    thread = ds.thread;
    random = ds.random;
    lastRandom = ds.lastRandom;
    ss = null;
  }  
  public Object clone() {
    return new DefaultScheduler(this);
  }  
  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;
  }  
  public iThreadInfo locateThread(iSystemState ss) {
//    System.err.println("Starting thread = " + thread);
    for(int n = ss.getThreadCount(); thread < n; thread++) {
      iThreadInfo th = ss.getThreadInfo(thread);

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

    return null;
  }  
  public void next() {
    if(lastRandom) {
      random = 0;
      thread++;
    } else {
      random++;
    }
  }  
  public int random(int max) {
    lastRandom = (random == max-1);

    return random;
  }  
}

---