---

Rewriter.java

package gov.nasa.arc.ase.ltl;

import gov.nasa.arc.ase.jpf.jvm.ClassPath;
import gov.nasa.arc.ase.jpf.JPFErrorException;
import java.io.BufferedReader;
import java.io.File;
import java.io.FileNotFoundException;
import java.io.FileReader;
import java.io.InputStreamReader;
import java.io.IOException;
// Added by ckong - Sept 7, 2001
import java.io.StringReader;

public class Rewriter {
  public static Formula applyRule(Formula expr, Formula rule, Formula rewritten) {
    return expr.rewrite(rule, rewritten);
  }  
  public static void main(String[] args) {
    int osize = 0;
    int rsize = 0;

    try {
      if(args.length != 0) {
    for(int i = 0; i < args.length; i++) {
      Formula f = Formula.parse(args[i]);

      osize += f.size();
      System.out.println(f = rewrite(f));
      rsize += f.size();
      
      System.err.println(rsize * 100 / osize + "% (" + osize + " => " + rsize + ")" );
    }
      } else {
    BufferedReader in = new BufferedReader(new InputStreamReader(System.in));

    while(true) {
      try {
        String line = in.readLine();

        if(line == null) break;
        if(line.equals("")) continue;

        Formula f = Formula.parse(line);

        osize += f.size();
        System.out.println(f = rewrite(f));
        rsize += f.size();

        System.err.println(rsize * 100 / osize + "% (" + osize + " => " + rsize + ")" );
      } catch(IOException e) {
        System.out.println("error");
        break;
      }
    }
      }
    } catch(ParseErrorException e) {
      System.err.println("parse error: " + e.getMessage());
    }
  }  
  public static Formula[] readRules() {
    Formula[] rules = new Formula[0];

    try {
      // Modified by ckong - Sept 7, 2001
      /*
      FileReader fr = null;

      for(int i = 0, l = ClassPath.length(); i < l; i++)
    try {
      fr = new FileReader(ClassPath.get(i) + File.separator + "gov.nasa.arc.ase.ltl.rules".replace('.', File.separatorChar));
    } catch(FileNotFoundException e) {
    }

      if(fr == null) {
    try {
      fr = new FileReader("rules");
    } catch(FileNotFoundException e) {
    }
      }

      if(fr == null) return null;
      
      BufferedReader in = new BufferedReader(fr);
      */
      BufferedReader in = new BufferedReader(new StringReader
    (RulesClass.getRules()));

      while(true) {
    String line = in.readLine();
    if(line == null) break;
    if(line.equals("")) continue;

    Formula rule = Formula.parse(line);

    Formula[] n = new Formula[rules.length+1];
    System.arraycopy(rules, 0, n, 0, rules.length);
    n[rules.length] = rule;
    rules = n;
      }
    } catch(IOException e) {
    } catch(ParseErrorException e) {
      System.err.println("parse error: " + e.getMessage());
      throw new JPFErrorException(""); // remove for stand-alone
      //System.exit(1);
    }

    return rules;
  }  
  public static Formula rewrite(Formula expr) {
    Formula[] rules = readRules();
    if(rules == null) return expr;

    try {
      boolean negated = false;
      boolean changed;

      do {
    Formula old;
    changed = false;

    do {
      old = expr;
      for(int i = 0; i < rules.length; i+=2)
        expr = applyRule(expr, rules[i], rules[i+1]);
      if(old != expr) changed = true;
    } while(old != expr);

    negated = !negated;
    expr = Formula.parse("!" + expr.toString());
      } while(changed || negated);

      return expr;
    } catch(ParseErrorException e) {
      return null;
    }
  }  
  public static String rewrite(String expr)/* throws ParseErrorException*/ {
    try {
      return rewrite(Formula.parse(expr)).toString();
    } catch(ParseErrorException e) {
      return null;
    }
  }  
}

---