---

RandomOrderScheduler.java

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

import gov.nasa.arc.ase.jpf.Engine;
import gov.nasa.arc.ase.jpf.iSystemState;
import gov.nasa.arc.ase.jpf.iThreadInfo;
import gov.nasa.arc.ase.jpf.JPFErrorException;
import gov.nasa.arc.ase.util.Debug;
import java.util.BitSet;
import java.util.Random;

public class RandomOrderScheduler extends Scheduler implements Cloneable {
  private static Random rand = 
    new Random(Engine.options.use_time_for_seed ? System.currentTimeMillis() :
           Engine.options.random_seed);
  public iSystemState ss;
  private int thread;
  private int random;
  private BitSet runThread;
  private BitSet[] runRandom;
  private int[] randomSize;

  public RandomOrderScheduler(iSystemState ss) {
    Debug.println(Debug.MESSAGE, "Random Order Scheduler");
    initialize(ss);
  }  
  public void backtrackTo(ArrayOffset storing, Object backtrack) {
    copy((RandomOrderScheduler)backtrack);
  }  
  public Object clone() {
    RandomOrderScheduler s = new RandomOrderScheduler (null);
    
    s.thread = thread;
    s.random = random;
    
    s.ss = null;
    if (runThread != null)
      s.runThread = (BitSet)runThread.clone();
    if (runRandom != null) {
      s.runRandom = new BitSet[runRandom.length];
      for (int i = 0; i < runRandom.length; i++)
    if (runRandom[i] != null)
      s.runRandom[i] = (BitSet)runRandom[i].clone();
    }
    if (randomSize != null)
      s.randomSize = (int[])randomSize.clone();
    return s;
  }  
  public void copy(RandomOrderScheduler sch) {
    if (sch.runThread != null)
      runThread = (BitSet)sch.runThread.clone();
    if (sch.runRandom != null) {
      runRandom = new BitSet[sch.runRandom.length];
      for (int i = 0; i < sch.runRandom.length; i++)
    runRandom[i] = (BitSet)sch.runRandom[i].clone();
    }
    if (sch.randomSize != null)
      randomSize = (int[])sch.randomSize.clone();
    thread = sch.thread;
    random = sch.random;
  }  
  public Object getBacktrackData() {
    return clone();
  }  
  public int getRandom() {
    return random;
  }  
  public int[] getStoringData() {
    return new int[0];
  }  
  public int getThread() {
    return thread;
  }  
  public void initialize(iSystemState ss) {
    this.ss = ss;
    thread = 0;
    random = 0;
    runThread = new BitSet();
    runRandom = null;
    randomSize = null;
  }  
  private boolean isComplete(int th) {
    if (randomSize[th] == 0) 
      return true;
    boolean finished = true;
    for (int i = 0; i < randomSize[th]; i++) {
      finished = finished && runRandom[th].get(i);
    }
    return finished;
  }  
  public iThreadInfo locateThread(iSystemState ss) {
    thread = pickNextThread(ss);
    if (thread == -1) {
      //thread = 0;
      return null;
    }

    return ss.getThreadInfo(thread);
  }  
  public void next() {
    if (isComplete(thread))
      runThread.set(thread);
  }  
  private int pickNextRandom(int th, int n) {
    randomSize[th] = n;

    int nchoices = 0;
    int [] choices = new int[n];
    for (int i = 0; i < n; i++)
      if (!runRandom[th].get(i))
    choices[nchoices++] = i;
    
    int r = rand.nextInt(nchoices);
    runRandom[th].set(choices[r]);

    return choices[r];
  }  
  private int pickNextThread(iSystemState ss) {
    int nthreads = 0;
    int n = ss.getThreadCount ();
    int[] refs = new int[n];

    if (runRandom == null) {
      runRandom = new BitSet[n];
      for (int i = 0; i < n; i++)
    runRandom[i] = new BitSet ();
    }

    if (randomSize == null)
      randomSize = new int[n];

    for(int i = 0; i < n; i++) {
      iThreadInfo th = ss.getThreadInfo(i);
      if (!(runThread.get(i)) && (th.isRunnable())) {
    refs[nthreads++] = i;
      }
    }

    if(nthreads == 0)
      return -1;

    int r = rand.nextInt(nthreads);

    return refs[r];
  }  
  public int random(int max) {
    random = pickNextRandom(thread, max);
    return random;
  }  
}

---