---

JPFOptions.java

package gov.nasa.arc.ase.jpf;

import gov.nasa.arc.ase.util.*;
//#ifdef BUCHI
import gov.nasa.arc.ase.ltl.LTL2Buchi;
//#endif BUCHI
//#ifdef BUCHI && BANDERA
import gov.nasa.arc.ase.jpf.tools.PredicateCompiler;
//#endif BUCHI && BANDERA
import java.util.*;
import java.net.*;
import java.io.*;

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

  public Debug      debugs          = null;

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

  public boolean    verify          = true;
  public boolean    assertions      = true;
  public boolean    deadlocks       = true;

  public boolean        random_order            = false;
  public long           random_seed             = 0L;
  public boolean        use_time_for_seed       = true;

//#ifdef BUCHI && BANDERA
  public String     predicate       = null;
  public String     predicate_class     = null;
  public String     predicate_method    = null;
//#endif BUCHI && BANDERA

  public int        search_depth        = -1;
  public boolean        no_storing              = false;

//#ifdef BUCHI
  public String     buchi           = null;
  public String     ltl         = null;
//#endif BUCHI

//#ifdef HEURISTIC









//#ifdef COVERAGE



//#endif COVERAGE
//#endif HEURISTIC

//#ifdef HEURISTIC_DEBUG

//#endif HEURISTIC_DEBUG

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

//#ifdef COVERAGE






//#endif COVERAGE

//#ifdef PARALLEL


//#endif PARALLEL
//#ifdef DISTRIBUTED










//#ifdef SIBLING_STORING

//#endif SIBLING_STORING
//#ifdef SIBLING_CACHING


//#endif SIBLING_CACHING
//#ifdef CHILDREN_LOOKAHEAD


//#endif CHILDREN_LOOKAHEAD
//#endif DISTRIBUTED
//#ifdef DISTRIBUTED || PARALLEL


//#endif DISTRIBUTED || PARALLEL

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

//#endif BUCHI && BANDERA
  public JPFOptions(Class m) {
    super(m, "class", true);
    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");
  }  
//#ifdef DISTRIBUTED























//#endif DISTRIBUTED

//#ifdef BUCHI
  private String loadLTL(String fname) {
    try {
      BufferedReader in = new BufferedReader(new FileReader(fname));

      return in.readLine();
    } catch(FileNotFoundException e) {
      throw new JPFErrorException("Can't load LTL formula: " + fname);
    } catch(IOException e) {
      throw new JPFErrorException("Error read on LTL formula: " + fname);
    }
  }  
  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 BUCHI && BANDERA
    if(predicate != null)
      translatePredicate();
//#endif BUCHI && BANDERA

//#ifdef DISTRIBUTED



























//#ifdef SIBLING_STORING && SIBLING_CACHING





//#endif SIBLING_STORING && SIBLING_CACHING

//#endif DISTRIBUTED

//#ifdef BUCHI
    if(ltl != null && buchi == null) {
      if(ltl.endsWith(".ltl")) {
    ltl = loadLTL(ltl);
      } else if(ltl.equals("-")) {
    ltl = readLTL();
      }

      if(ltl.equals(""))
    throw new JPFErrorException("empty LTL formula");

      try {
//#ifdef BANDERA
    LTL2Buchi.translate("!(" + ltl + ")").save(System.getProperty("user.dir")+File.separator+"ba.sm");
//#else BANDERA

//#endif BANDERA
      } catch(IOException e) {
    throw new JPFErrorException(e.getMessage());
      }
//#ifdef BANDERA
      buchi = System.getProperty("user.dir")+File.separator+"ba.sm";
//#else BANDERA

//#endif BANDERA
    }
//#endif BUCHI

    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();
  }  
  private String readLTL() {
    try {
      BufferedReader in = new BufferedReader(new InputStreamReader(System.in));

      System.out.print("Insert LTL formula: ");
      return in.readLine();
    } catch(IOException e) {
      throw new JPFErrorException("Invalid LTL formula");
    }
  }  
//#endif BUCHI

//#ifdef BUCHI && BANDERA
  private void translatePredicate() {
    String[] args;

    if(predicate_class != null) {
      if(predicate_method != null) {
    args = new String[3];
    args[0] = predicate;
    args[1] = predicate_class;
    args[2] = predicate_method;
      } else {
    args = new String[2];
    args[0] = predicate;
    args[1] = predicate_class;
      }
    } else {
      args = new String[1];
      args[0] = predicate;
    }
    
    PredicateCompiler.main(args);
    throw new JPFErrorException("Successful termination in translatePredicate"); //System.exit(0);
  }  
}

---