---

Scheduler.java

package gov.nasa.arc.ase.jpf;

import java.util.*;
import gov.nasa.arc.ase.util.Debug;
import gov.nasa.arc.ase.jpf.jvm.*;
import java.io.*;

public class Scheduler implements iScheduler,Cloneable{
  private int current_thread;
  private int current_notify;
  private int current_random;
  //private boolean isNotifying;
  private boolean lastMoveWasSafe;
  private boolean foundSafeMove = false;
  // use to indicate which threads has run, or must still run
  BitSet alreadyRan  = new BitSet(10); //default size = 64
  private int how_many_safe_moves = 0;

  private static BufferedReader br = new BufferedReader(new InputStreamReader(System.in));
  private static boolean quit = false;

  public Object clone(){
    try{
      Scheduler sd = (Scheduler) super.clone();
      if (Engine.options.po_reduction) {
        sd.alreadyRan = new BitSet();
        for(int i = 0; i < alreadyRan.size(); i++) {
          if (alreadyRan.get(i))
            sd.alreadyRan.set(i);
        }
      }
      return sd;
    }
    catch(CloneNotSupportedException e){
      throw new InternalError(e.toString());
    };
  }  
  public int getCurrentNotify(){
    return current_notify;
  }  
  public int getCurrentRandom(){
    return current_random;
  }  
// ifdef DEBUG












//#endif DEBUG

  public int getCurrentThread(){
    return current_thread;
  }  
  //public void setNotifying(){
  //  isNotifying = true;
  //}

  //public void clearNotifying(){
  //  isNotifying = false;
  //}

  public iThreadInfo getCurrentThreadInfo(iKernelState ks){
    return ks.getThreadInfo(current_thread);
  }  
  public int getSafeMoves() {
    return how_many_safe_moves;
  }  
  public void incCurrentNotify(iScheduler current){
    int n = ((Scheduler)current).current_notify;
    //current_notify++;
    current_notify = n+1;
  }  
  public void incCurrentRandom(iScheduler current){
    int n = ((Scheduler)current).current_random;
    //current_random++;
    current_random = n+1;
  }  
  public void incCurrentThread(iScheduler current) {
    int th = ((Scheduler)current).current_thread;
    setAlreadyRanThread(th);
    current_thread = th+1;
    lastMoveWasSafe = foundSafeMove;
    /*
    setAlreadyRanThread(current_thread);
    current_thread = current_thread+1;
    lastMoveWasSafe = foundSafeMove;
    */
  }  
  public void initialize(){
    current_thread = 0;
    current_notify = 0;
    current_random = 0;
    //isNotifying = false;
    lastMoveWasSafe = false;
    if (Engine.options.po_reduction) {
      for(int i= 0; i < alreadyRan.size(); i++)
        alreadyRan.clear(i);
    }
  }  
  // used during simulation
  public iThreadInfo locateRandomRunningThread(iKernelState ks){
    boolean flag;
    int limit = ks.getThreadCount();

    //Random r = new Random();

    //current_thread = r.nextInt() % limit;
    //while(current_thread < 0) {
    //  current_thread = r.nextInt() % limit;
    //}
    current_thread = (current_thread + 1) % limit;
    //Debug.println(Debug.DEBUG, "Cthread Thread " + current_thread);
    while (current_thread < limit &&
           !ks.getThreadInfo(current_thread).isEnabled()) {
      current_thread++;
    }
    if (current_thread == limit) {
// ifdef DEBUG

//#endif DEBUG
      // make sure there was not something that could run
      current_thread = 0;
      while (current_thread < limit &&
             !ks.getThreadInfo(current_thread).isEnabled()) {
        current_thread++;
      }
    }
    if (current_thread == limit)
      return null;
    else {
      //Debug.println(Debug.DEBUG, "Cthread Thread " + current_thread);
      return ks.getThreadInfo(current_thread);
    }
  }  
  public iThreadInfo locateRunningThread(iSystemState ss, iKernelState ks) {
    if(Engine.options.interactive)
      return locateRunningThreadInteractive(ss, ks);
// ifdef DEBUG


//#endif DEBUG
    int limit = ks.getThreadCount();

    while(current_thread < limit) {
      iThreadInfo th = ks.getThreadInfo(current_thread);
      if(th.isRunnable(ss, ks)) break;
      current_thread++;
    }

    if (current_thread >= limit)
      return null;
    else {
      return ks.getThreadInfo(current_thread);
    }
  }  
  public iThreadInfo locateRunningThreadInteractive(iSystemState ss, iKernelState ks) {
    if (quit) return null;

    int nthreads = ks.getThreadCount();
    int nrunnable = 0;
    BitSet runnable = new BitSet();

    for(int i = 0; i < nthreads; i++) {
      iThreadInfo th = ks.getThreadInfo(i);
      if(th.isRunnable(ss, ks)) {
    runnable.set(i);
    nrunnable++;
      }
    }

    if(nrunnable == 0) {
      System.out.println("Deadlock: backing up");
      return null;
    }

    System.out.print("Runnable threads [" + nrunnable + "]: ");
    for(int i = 0; i < nthreads; i++) {
      if(runnable.get(i)) {
    if(i == current_thread) {
      System.err.print("[" + i + "] ");
    } else {
      System.err.print(i + " ");
    }
      }
    }
    System.out.println();

    while(true) {
      try {
    System.out.print("> ");
    String s = br.readLine();
    if(s.equals("quit") || s.equals("q")) {
      quit = true;
      return null;
    } else if(s.equals("backtrack") || s.equals("back") || s.equals("b")) {
      return null;
    } else if(s.equals("show") || s.equals("s")) {
      while(true) {
        System.out.print("show> ");
        s = br.readLine();
        if(s.equals("")) break;
        try {
          int l = Integer.parseInt(s);
          if(runnable.get(l)) {
        ThreadInfo th = (ThreadInfo)ks.getThreadInfo(l);
        System.out.print(th.getTrailInfo());
        break;
          }
        } catch(NumberFormatException e) {
        }
      }
    } else if(s.equals("random") || s.equals("r")) {
      while(true) {
        System.out.println("Current random: " + current_random);
        System.out.print("random> ");
        s = br.readLine();
        if(s.equals("")) break;
        try {
          current_random = Integer.parseInt(s);
          break;
        } catch(NumberFormatException e) {
        }
      }
    } else if(s.equals("help") || s.equals("h") || s.equals("?")) {
      System.out.println("command:");
      System.out.println("  quit");
      System.out.println("  random");
      System.out.println("  backtrack");
      System.out.println("  help");
    } else {
      if(runnable.get(current_thread) && s.equals(""))
        break;
      try {
        int i = Integer.parseInt(s);
        if(runnable.get(i)) {
          current_thread = i;
          break;
        }
      } catch(NumberFormatException e) {
      }
    }
      } catch(IOException e) {
    throw new InternalError();
      }
    }

    System.out.println("Running thread " + current_thread);

    return ks.getThreadInfo(current_thread);
  }  
  public iThreadInfo locateSafeThread(iSystemState ss, iKernelState ks) {
    int limit = ks.getThreadCount();
    int unsafe_thread = 999;

// ifdef DEBUG

//#endif DEBUG
    foundSafeMove = false;
    if (lastMoveWasSafe) return null;
// ifdef DEBUG

//#endif DEBUG
    //current_thread = 0; is WRONG here! why?
    while (current_thread < limit) {
      if (ks.getThreadInfo(current_thread).isRunnable(ss, ks)) {
        if (!alreadyRan.get(current_thread)) {
          if (!ks.getThreadInfo(current_thread).isSafe()) {
            if (unsafe_thread == 999)
              unsafe_thread = current_thread;
          }
      else // enabled && !Ran && Safe
        break;
    }
      }
      current_thread++;
    }
    if (current_thread >= limit) { // could not find safe move
      if (unsafe_thread != 999) { // maybe there was an unsafe one
    current_thread = unsafe_thread;
// ifdef DEBUG

//#endif DEBUG
    foundSafeMove = false;
    return ks.getThreadInfo(current_thread);
      }
      else // there was no move at all
    return null;
    } else { // found safe move
      how_many_safe_moves++;
// ifdef DEBUG

//#endif DEBUG
      foundSafeMove = true;
      return ks.getThreadInfo(current_thread);
    }
  }  
  /************************************************************************/


  public void print(){
// ifdef DEBUG

//#endif DEBUG
  }  
  public void setAlreadyRanThread(int i) {
    alreadyRan.set(i);
  }  
  /************************************************************************/
  // used in path simulation
  public void setCurrentRandom(int random){
    current_random = random;
  }  
  public void setCurrentThread(int thread){
    lastMoveWasSafe = foundSafeMove;
    current_thread = thread;
  }  
  public void setLastSafeMove(boolean v) {
    lastMoveWasSafe = v;
  }  
}

---