---

JPFOptions.java

package gov.nasa.arc.ase.jpf;

import gov.nasa.arc.ase.util.*;
import java.util.*;
import java.net.*;

public class JPFOptions extends Options {
  public boolean    help            = false;
  public boolean    version         = false;
  
  public boolean    debug           = false;
  public boolean    verbose         = false;
  public boolean    quiet           = false;

  public Debug      debugs          = null;

  public boolean    bandera         = false;
  public boolean    po_reduction        = false;
  public boolean    notify          = false;

  public boolean    verify          = true;
  public boolean    assertions      = false;

// ifdef BUCHI

//#endif BUCHI

  /**************************************************************/
  public boolean        real_counterexample     = false;
  public boolean        path_simulation         = false;
  /**************************************************************/

// ifdef DISTRIBUTED










// ifdef SIBLING_STORING

//#endif SIBLING_STORING
// ifdef SIBLING_CACHING


//#endif SIBLING_CACHING
// ifdef CHILDREN_LOOKAHEAD


//#endif CHILDREN_LOOKAHEAD
//#endif DISTRIBUTED

  public boolean    interactive     = false;
  public int        report_period       = 10;

  public boolean    atomic_lines        = true;

// ifdef DISTRIBUTED























//#endif DISTRIBUTED
  public JPFOptions(Class m) {
    super(m, "class", false);
    addParser("[Ljava.lang.String;", "parseStringArray");
    addParser("gov.nasa.arc.ase.util.Debug", "parseDebug");
    addPrinter("[Ljava.lang.String;", "printStringArray");
    addPrinter("gov.nasa.arc.ase.util.Debug", "printDebug");
  }  
  public String[] parse(String[] args) {
    String[] p = super.parse(args);

    if(debug)
      Debug.setDebugLevel(Debug.DEBUG);
    else if(verbose)
      Debug.setDebugLevel(Debug.MESSAGE);
    else if(quiet)
      Debug.setDebugLevel(Debug.ERROR);
    else
      Debug.setDebugLevel(Debug.WARNING);

// ifdef DISTRIBUTED



























// ifdef SIBLING_STORING





//#endif SIBLING_STORING

//#endif DISTRIBUTED

    return p;
  }  
  public Object parseDebug(String s) {
    if(s == null) throw new IllegalArgumentException();

    StringTokenizer ps = new StringTokenizer(s, ",");

    while(ps.hasMoreTokens()) {
      String p = ps.nextToken();

      StringTokenizer st = new StringTokenizer(p, "=");
      if(st.countTokens() == 1) {
    String kind = st.nextToken();
    int k;

    if((k = Debug.mapKind(kind)) == -1) {
      Debug.println(Debug.ERROR, "invalid debug kind -- " + kind);
      return null;
    }

    Debug.setDebugLevel(Debug.DEBUG, k);
      } else if(st.countTokens() == 2) {
    String kind = st.nextToken();
    String level = st.nextToken();
    int k, l;

    if((k = Debug.mapKind(kind)) == -1) {
      Debug.println(Debug.ERROR, "invalid debug kind -- " + kind);
      return null;
    }
    if((l = Debug.mapLevel(level)) == -1) {
      Debug.println(Debug.ERROR, "invalid debug level -- " + level);
      return null;
    }

    Debug.setDebugLevel(l, k);
      } else {
    Debug.println(Debug.ERROR, "invalid syntax -- -debugs " + s);
    return null;
      }
    }

    return null;
  }  
  public Object parseStringArray(String s) {
    if(s == null) throw new IllegalArgumentException();
    StringTokenizer st = new StringTokenizer(s, ",");
    int l = st.countTokens();
    String[] strs = new String[l];

    for(int i = 0; i < l; i++)
      strs[i] = st.nextToken();

    return strs;
  }  
  public String printDebug(Object o) {
    return Debug.status();
  }  
  public String printStringArray(Object o) {
    if(o == null) return "null";

    String[] s = (String[])o;
    StringBuffer sb = new StringBuffer("[");

    for(int i = 0; i < s.length; i++) {
      if(i != 0) sb.append(",");
      sb.append(" ");
      sb.append(s[i]);
    }
    if(s.length != 0) sb.append(" ");
    sb.append("]");

    return sb.toString();
  }  
}

---