---

Evaluate.java

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

import gov.nasa.arc.ase.jpf.Engine;
import gov.nasa.arc.ase.jpf.JPFErrorException;
import gov.nasa.arc.ase.jpf.jvm.Reference;
import gov.nasa.arc.ase.jpf.jvm.ReferenceWrapper;
import gov.nasa.arc.ase.jpf.jvm.State;
import gov.nasa.arc.ase.util.Debug;
import gov.nasa.arc.ase.util.Lexer;
import gov.nasa.arc.ase.util.FileClassLoader;
import gov.nasa.arc.ase.util.LexerException;
import java.lang.reflect.InvocationTargetException;
import java.lang.reflect.Method;
import java.util.Vector;

//#ifdef BUCHI
class Evaluate implements SubExpr {
  private Method method;
  private Object[] args = null;

  Evaluate(String expr) {
    try {
      Lexer l = new Lexer(expr);

      if(l.lex() != Lexer.ID)
    throw new JPFErrorException("Identified expected: " + expr);

      StringBuffer sb = new StringBuffer();
      sb.append(l.getStringValue());
      
      char token;

      while((token = l.lex()) == '.') {
    sb.append(token);
    if(l.lex() != Lexer.ID)
      throw new JPFErrorException("Identified expected: " + expr);
    sb.append(l.getStringValue());
      }
      
      String name = sb.toString();

      Class[] types;


      switch(token) {
    case Lexer.END:
      // no arguments
      types = new Class[1];
      types[0] = State.class;
      break;

    case '(':
      Vector t = new Vector();
      Vector v = new Vector();
      t.add(State.class);

      token = l.lex();

      if(token != ')')
        while(true) {
          switch(token) {
        case Lexer.ID:
          sb = new StringBuffer(l.getStringValue());
          for(token = l.lex(); token == '.'; token = l.lex()) {
            sb.append('.');
            if(l.lex() != Lexer.ID)
              throw new JPFErrorException("Identified expected: " + expr);

            sb.append(l.getStringValue());
          }
          t.add(Reference.class);
          v.add(new ReferenceWrapper(sb.toString()));
          break;

        case Lexer.INTEGER:
          t.add(Integer.TYPE);
          v.add(new Integer(l.getIntValue()));
          token = l.lex();
          break;

        case Lexer.STRING:
          t.add(String.class);
          v.add(l.getStringValue());
          token = l.lex();
          break;

        default:
          throw new JPFErrorException("Expression expected: " + expr);
          }

          if(token == ')')
        break;

          if(token != ',')
        throw new JPFErrorException("',' expected: " + expr);

          token = l.lex();
        }

      if(l.lex() != Lexer.END)
        throw new JPFErrorException("Unexpected token: " + expr);

      types = new Class[t.size()];
      for(int i = 0; i < t.size(); i++)
        types[i] = (Class)t.get(i);

      args = new Object[v.size()];
      for(int i = 0; i < v.size(); i++)
        args[i] = v.get(i);

      break;

    default:
      throw new JPFErrorException("'(' expected: " + expr);
      }

      Class cls;

      try {
//#ifdef BANDERA
    cls = FileClassLoader.load(name);
//#else BANDERA

//#endif BANDERA
      } catch(ClassNotFoundException e) {
    throw new JPFErrorException("Expression not defined: " + name);
      }

      try {
    method = cls.getDeclaredMethod("evaluate", types);
      } catch(NoSuchMethodException e) {
    throw new JPFErrorException("No evaluate defined for expression: " + expr);
      }

      int n = 0;

      for(int i = 1; i < types.length; i++)
    if(types[i] != Reference.class)
      n++;

      Class[] otypes = new Class[n];
      Object[] oargs = new Object[n];

      n = 0;
      for(int i = 1; i < types.length; i++)
    if(types[i] != Reference.class) {
      otypes[n] = types[i];
      oargs[n] = args[i-1];
      n++;
    }

      try {
    try {
      Method o = cls.getDeclaredMethod("observable", otypes);
      String os = (String)o.invoke(null, oargs);

      Debug.println(Debug.WARNING, "Observable added: " + os);
      Engine.getJPF().vm.BuchiObservable(os);
    } catch(NoSuchMethodException e) {
      try {
        otypes = new Class[0];
        oargs = new Object[0];

        Method o = cls.getDeclaredMethod("observable", otypes);
        String os = (String)o.invoke(null, oargs);

        Debug.println(Debug.WARNING, "Observable added: " + os);
        Engine.getJPF().vm.BuchiObservable(os);
      } catch(NoSuchMethodException ee) {
      }
    }
      } catch(IllegalAccessException e) {
    throw new JPFErrorException("Observable is not accessible for expression: " + expr);
      } catch(InvocationTargetException e) {
    throw new JPFErrorException("Observable cannot be evaluate for expression: " + expr);
      }
    } catch(LexerException e) {
      throw new JPFErrorException(e.getMessage());
    }
  }  
  public void backtrack() {
    throw new RuntimeException("Expression is not executable");
  }  
  public boolean evaluate() {
    if(args == null)
      return Engine.getJPF().vm.BuchiEvaluate(method);
    else
      return Engine.getJPF().vm.BuchiEvaluate(method, args);
  }  
  public void execute() {
    throw new RuntimeException("Expression is not executable");
  }  
  public String toString() {
    if(args == null)
      return method.getDeclaringClass().getName();
    else {
      StringBuffer sb = new StringBuffer();
      sb.append(method.getDeclaringClass().getName());
      sb.append('(');
      for(int i = 0; i < args.length; i++) {
    if(i != 0) sb.append(',');
    sb.append(args[i]);
      }
      sb.append(')');

      return sb.toString();
    }
  }  
}

---