---

RandomScheduler.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;
import java.util.Random;

public class RandomScheduler extends Scheduler {
  private static Random rand = new Random();
  private int thread;
  private int random;

  public RandomScheduler(iSystemState ss) {
    initialize(ss);
  }  
  public RandomScheduler(RandomScheduler rs) {
    thread = rs.thread;
    random = rs.random;
    ss = null;
  }  
  public Object clone() {
    return new RandomScheduler(this);
  }  
  public int getRandom() {
    return random;
  }  
  public int getThread() {
    return thread;
  }  
  public void initialize(iSystemState ss) {
    this.ss = (SystemState)ss;
    thread = 0;
    random = -1;
  }  
  public iThreadInfo locateThread(iSystemState ss) {
    int n = ss.getThreadCount();
    int nthreads = 0;
    iThreadInfo[] threads = new iThreadInfo[n];
    int[] refs = new int[n];
    
    for(int i = 0; i < n; i++) {
      iThreadInfo th = ss.getThreadInfo(i);
      if(th.isRunnable()) {
    refs[nthreads] = i;
    threads[nthreads++] = th;
      }
    }

    if(nthreads == 0) return null;

//#ifdef JDK11

//#else JDK11
    int r = rand.nextInt(nthreads);
//#endif JDK11

    thread = refs[r];

    return threads[r];
  }  
  public void next() {
    initialize(ss);
  }  
  public int random(int max) {
//#ifdef JDK11

//#else JDK11
    return random = rand.nextInt(max);
//#endif JDK11
  }  
}

---