---

SM.java

package gov.nasa.arc.ase.jpf;

//#ifdef BUCHI
import java.io.*;
import java.util.*;
import gov.nasa.arc.ase.util.Debug;
import gov.nasa.arc.ase.jpf.expr.Expr;
import gov.nasa.arc.ase.jpf.expr.SubExpr;

public class SM {
  private int nstates;
  private int[][] adjlist;
  private String[] attributes;
  private String[][] state_attributes;
  private String[][][] transition_attributes;

  private Expr expr;

  private SubExpr[][] guards;
  private SubExpr[][] actions;
  private Sch sch = null;

  boolean[] accepting;
  boolean[] trivial;
  boolean[] persistant;

  public static class Wrapper {
    private int[] data;
    private int h = 0;

    public Wrapper(int[] d) {
      data = d;
      for(int i = 0; i < data.length; i++)
    h += d[i];
    }

    public int hashCode() {
      return h;
    }

    public boolean equals(Object o) {
      Wrapper w = (Wrapper)o;

      if(h != w.h) return false;

      if(data.length != w.data.length) return false;

      for(int i = 0; i < data.length; i++)
    if(data[i] != w.data[i]) return false;

      return true;
    }
  }
  private SM(int ns) {
    nstates = ns;
    adjlist = new int[ns][];
    state_attributes = new String[ns][];
    transition_attributes = new String[ns][][];

    expr = new Expr();

    guards = new SubExpr[ns][];
    actions = new SubExpr[ns][];

    accepting = new boolean[ns];
    trivial = new boolean[ns];
    persistant = new boolean[ns];
  }  
  private static String attributesToString(String[] a) {
    StringBuffer sb = new StringBuffer();

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

    return sb.toString();
  }  
  public void backtrack(int s, int t) {
    actions[s][t].backtrack();
  }  
  public int execute(int s, int t) {
    actions[s][t].execute();

    return adjlist[s][t];
  }  
  public SubExpr getAction(int s, int t) {
    return actions[s][t];
  }  
  private static boolean getBooleanAttribute(String[] as, String a) {
    for(int i = 0; i < as.length; i++)
      if(as[i].equals(a)) return true;

    return false;
  }  
  public boolean getGraphBooleanAttribute(String a) {
    return getBooleanAttribute(attributes, a);
  }  
  public String getGraphStringAttribute(String a) {
    return getStringAttribute(attributes, a);
  }  
  public SubExpr getGuard(int s, int t) {
    return guards[s][t];
  }  
  public boolean getStateBooleanAttribute(int s, String a) {
    return getBooleanAttribute(state_attributes[s], a);
  }  
  public int getStateCount() {
    return nstates;
  }  
  public String getStateStringAttribute(int s, String a) {
    return getStringAttribute(state_attributes[s], a);
  }  
  private static String getStringAttribute(String[] as, String a) {
    for(int i = 0; i < as.length; i++)
      if(as[i].startsWith(a + "="))
    return as[i].substring(a.length() + 1);

    return null;
  }  
  public int getSuccessor(int s, int t) {
    return adjlist[s][t];
  }  
  public boolean getTransitionBooleanAttribute(int s, int t, String a) {
    return getBooleanAttribute(transition_attributes[s][t], a);
  }  
  public int getTransitionCount(int s) {
    return adjlist[s].length;
  }  
  public String getTransitionStringAttribute(int s, int t, String a) {
    return getStringAttribute(transition_attributes[s][t], a);
  }  
  private void init() {
  }  
  public boolean isEnabled(int s, int t) {
    return guards[s][t].evaluate();
  }  
  public static SM load(String fname) {
    try {
      BufferedReader in = new BufferedReader(new FileReader(fname));
      int ns = readInt(in);
      SM sm = new SM(ns);
      sm.setGraphAttributes(readAttributes(in));
      for(int i = 0; i < ns; i++) {
    int nt = readInt(in);
    sm.setStateAttributes(i, readAttributes(in));
    sm.accepting[i] = sm.getStateBooleanAttribute(i, "accepting");
    sm.trivial[i] = sm.getStateBooleanAttribute(i, "trivial");
    sm.persistant[i] = sm.getStateBooleanAttribute(i, "persistant");
    sm.setNTransitions(i, nt);

    for(int j = 0; j < nt; j++) {
      sm.setAdj(i, j, readInt(in));
      sm.setGuard(i, j, readString(in));
      sm.setAction(i, j, readString(in));
      sm.setTransitionAttribute(i, j, readAttributes(in));
    }
      }

      sm.init();
      
      return sm;
    } catch(FileNotFoundException e) {
      Debug.println(Debug.ERROR, "file not found -- " + fname);
      throw new JPFErrorException(""); //System.exit(1);
    } catch(IOException e) {
      Debug.println(Debug.ERROR, "error reading file -- " + fname);
      throw new JPFErrorException(""); //System.exit(1);
    }

    // not reached 
    // return null;
  }  
  private static String[] readAttributes(BufferedReader in) throws IOException {
    String line = readString(in);

    if(line.equals("-")) return new String[0];

    StringTokenizer st = new StringTokenizer(line, ",");
    int ntokens = st.countTokens();
    String[] tokens = new String[ntokens];
    for(int i = 0; i < ntokens; i++)
      tokens[i] = st.nextToken();

    return tokens;
  }  
  public static int readInt(BufferedReader in) throws IOException {
    String line;

    do {
      line = in.readLine();
      int idx = line.indexOf('#');
      if(idx != -1) line = line.substring(0, idx);
      line = line.trim();
    } while(line.length() == 0);

    return Integer.parseInt(line);
  }  
  public static String readString(BufferedReader in) throws IOException {
    String line;

    do {
      line = in.readLine();
      int idx = line.indexOf('#');
      if(idx != -1) line = line.substring(0, idx);
      line = line.trim();
    } while(line.length() == 0);

    return line;
  }  
  private void setAction(int s, int t, String a) {
    actions[s][t] = expr.parse(a);
  }  
  private void setAdj(int s, int t, int a) {
    adjlist[s][t] = a;
  }  
  private void setGraphAttributes(String[] a) {
    attributes = a;
  }  
  private void setGuard(int s, int t, String g) {
    if(g.equals("else"))
      guards[s][t] = null;
    else
      guards[s][t] = expr.parse(g);
  }  
  private void setNTransitions(int s, int nt) {
    adjlist[s] = new int[nt];
    guards[s] = new SubExpr[nt];
    actions[s] = new SubExpr[nt];
    transition_attributes[s] = new String[nt][];
  }  
  public void setSch(Sch s) {
    sch = s;
  }  
  private void setStateAttributes(int s, String[] a) {
    state_attributes[s] = a;
  }  
  private void setTransitionAttribute(int s, int t, String[] a) {
    transition_attributes[s][t] = a;
  }  
}

---