---

Formula.java

package gov.nasa.arc.ase.ltl;

// Written by Dimitra Giannakopoulou, 19 Jan 2001
// Parser by Flavio Lerda, 8 Feb 2001
// Parser extended by Flavio Lerda, 21 Mar 2001
import java.util.*;

public class Formula implements Comparable {
  private char content;
  private boolean literal;
  private Formula left;
  private Formula right;
  private int id;
  private int untils_index; // index to the untils vector
  private int rightOfUntil_index;
  private String name;

  public static Vector untils = new Vector();
  public static Formula[] until_forms;

  private static int nId = 0;

  private static final int P_ALL        = 0;
  private static final int P_OR         = 1;
  private static final int P_AND        = 2;
  private static final int P_UNTIL      = 3;
  private static final int P_WUNTIL     = 3;
  private static final int P_RELEASE    = 4;
  private static final int P_WRELEASE   = 4;
  private static final int P_IMPLIES    = 5;
  private static final int P_NOT        = 6;
  private static final int P_NEXT       = 6;
  private static final int P_ALWAYS     = 6;
  private static final int P_EVENTUALLY = 6;


  public static class EndOfInputException extends Exception {
  }


  private static Hashtable ht = new Hashtable();

  private static class Input {
    private StringBuffer sb;


    public Input(String str) {
      sb = new StringBuffer(str);
    }


    public char get() throws EndOfInputException {
      try {
    return sb.charAt(0);
      } catch(StringIndexOutOfBoundsException e) {
    throw new EndOfInputException();
      }
    }


    public void skip() throws EndOfInputException {
      try {
    sb.deleteCharAt(0);
      } catch(StringIndexOutOfBoundsException e) {
    throw new EndOfInputException();
      }
    }
  }

  private static Hashtable matches = new Hashtable();

  private Formula(char c, boolean l, Formula sx, Formula dx, String n) {
    id = nId++;
    content = c;
    literal = l;
    left = sx;
    right = dx;
    name = n;
    rightOfUntil_index = -1;
    untils_index = -1;
  }  
  public void addLeft (Formula l)
  {
    left = l;
  }  
  private void addMatch(String name, Formula expr) {
    matches.put(name, expr);
  }  
  public void addRight (Formula r)
  {
    right = r;
  }  
  private static Formula Always(Formula f) {
    return unique(new Formula('V', false, False(), f, null));
  }  
  private static Formula And(Formula sx, Formula dx) {
    if(sx.id < dx.id)
      return unique(new Formula('A', false, sx, dx, null));
    else
      return unique(new Formula('A', false, dx, sx, null));
  }  
  private void clearMatches() {
    matches = new Hashtable();
  }  
  public int compareTo(Object f)
  {
    Formula ff = (Formula) f;
    return (this.id - ff.id);


  }  
  private static Formula Eventually(Formula f) {
    return unique(new Formula('U', false, True(), f, null));
  }  
  private static Formula False() {
    return unique(new Formula('f', true, null, null, null));
  }  
  public int get_rightOfUntils_index()
  {
    return (rightOfUntil_index);
  }  
  public int get_untils_index()
  {
    return (untils_index);
  }  
  public char getContent ()
  {
    return content;
  }  
  private Formula getMatch(String name) {
    return (Formula)matches.get(name);
  }  
  public String getName ()
  {
    return name;
  }  
  public Formula getNext()
  {
    switch (content)
    {
      case 'U':
      case 'W':
    return this;
      case 'V':
    return this;
      case 'O':
    return null;
      default:
    //    System.out.println(content + " Switch did not find a relevant case...");
    return null;
    }
  }  
  public Formula getSub1 ()
  {
    if (content == 'V')
      return right;
    else
      return left;
  }  
  public Formula getSub2 ()
  {
    if (content == 'V')
      return left;
    else
      return right;
  }  
  private static Formula Implies(Formula sx, Formula dx) {
    return Or(Not(sx), dx);
  }  
  public boolean is_literal()
  {
    return (literal);
  }  
  public static boolean is_reserved_char(char ch)
  {
    switch (ch)
    {
      //        case 't':
      //        case 'f':
      case 'U':
      case 'V':
      case 'W':
      case 'M':
      case 'X':
      case ' ':
      case '<':
      case '>' :
      case '(':
      case ')':
      case '[':
      case ']':
      case '-':
    // ! not allowed by Java identifiers anyway - maybe some above neither?
    return true;
      default :
    return false;
    }
  }  
  public boolean is_right_of_until()
  {
    return (rightOfUntil_index >=0);
  }  
  /*
     public boolean contradicts (Formula ita)
     {
  // only called for literals - that's an assumption
  // improve by not requiring that



  char otherContent = ita.getContent();

  if (otherContent == 't') return false;

  // one is the negation of the other
  if ( ((content == 'N') && (left ==  ita))  ||
  ((otherContent == 'N') && (ita.left == this)) )
  return true;



  return false; // if none of the cases above, no contradiction

  }
   */

  public boolean is_special_case_of_V (TreeSet check_against)
  {
    Formula form = (Release(False(), this));
    if (check_against.contains(form))
      return true;
    else
      return false;
  }  
  public boolean is_synt_implied (TreeSet old, TreeSet next)
  {
    if (this.getContent() == 't')
      return true;
    if (old.contains(this))
      return true;


    if (! is_literal()) // non-elementary formula
    {
      Formula form1 = this.getSub1();
      Formula form2 = this.getSub2();
      Formula form3 = this.getNext();

      boolean condition1, condition2, condition3;

      if (form2 != null)
    condition2 = form2.is_synt_implied(old, next);
      else
    condition2 = true;
      if (form1 != null)
    condition1 = form1.is_synt_implied(old, next);
      else
    condition1 = true;
      if (form3 != null) {
    if (next != null)
      condition3 = next.contains(form3);
    else
      condition3 = false;
      }
      else
    condition3 = true;

      switch (getContent())
      {

    case 'U':
    case 'W':
    case 'O':
      return (condition2 || (condition1 && condition3));
    case 'V':
      return (  (condition1 && condition2)
          || (condition1 && condition3)
          );
    case 'X': if (form1!=null) {
            if (next != null)
              return (next.contains(form1));
            else
              return false;
          } else
            return (true);
    case 'A': return (condition2 && condition1);
    default:
          System.out.println("Default case of switch at Form.synt_implied");
          return false;

      }
    }
    else
    {
      return false;
    }
  }  
  private boolean match(Formula rule) {
    if(rule.content == 'p') {
      Formula match = getMatch(rule.name);

      if(match == null) {
    addMatch(rule.name, this);
    return true;
      }

      return match == this;
    }

    if(rule.content != content) return false;

    Hashtable saved = (Hashtable)matches.clone();

    switch(content) {
      case 'A':
      case 'O':
    if(left.match(rule.left) && right.match(rule.right))
      return true;

    matches = saved;
    if(right.match(rule.left) && left.match(rule.right))
      return true;

    matches = saved;
    return false;

      case 'U':
      case 'V':
      case 'W':
    if(left.match(rule.left) && right.match(rule.right))
      return true;

    matches = saved;
    return false;

      case 'X':
      case 'N':
    if(left.match(rule.left))
      return true;

    matches = saved;
    return false;

      case 't':
      case 'f':
    return true;
    }

    throw new RuntimeException("code should not be reached");
  }  
  public Formula negate ()
  {
    return Not(this);
  }  
  private static Formula Next(Formula f) {
    return unique(new Formula('X', false, f, null, null));
  }  
  private static Formula Not(Formula f) {
    if (f.literal)
      switch (f.content)
      {
    case 't': return False();
    case 'f': return True();
    case 'N': return f.left;
    default : return unique(new Formula('N', true, f, null, null));
      }

    // f is not a literal, so go on...


    switch(f.content) {
      case 'A': return Or(Not(f.left), Not(f.right));
      case 'O': return And(Not(f.left), Not(f.right));
      case 'U': return Release(Not(f.left), Not(f.right));
      case 'V': return Until(Not(f.left), Not(f.right));
      case 'W': return WRelease(Not(f.left), Not(f.right));
      //case 'M': return WUntil(Not(f.left), Not(f.right));
      case 'N': return f.left;
      case 'X': return Next(Not(f.left));
      default:  throw new ParserInternalError();
    }
  }  
  private static Formula Or(Formula sx, Formula dx) {
    if(sx.id < dx.id)
      return unique(new Formula('O', false, sx, dx, null));
    else
      return unique(new Formula('O', false, dx, sx, null));
  }  
  static private Formula parse(Input i, int precedence) throws ParseErrorException {
    try {
      Formula formula;
      char ch;


      while(i.get() == ' ') i.skip();


      switch(ch = i.get()) {
    case '/': // and
    case '\\': // or
    case 'U': // until
    case 'W': // weak until
    case 'V': // release
    case 'M': // dual of W - weak release
    case ')':
      throw new ParseErrorException("invalid character: " + ch);


    case '!': // not
      i.skip();
      formula = Not(parse(i, P_NOT));
      break;


    case 'X': // next
      i.skip();
      formula = Next(parse(i, P_NEXT));
      break;


    case '[': // always
      i.skip();
      if(i.get() != ']')
        throw new ParseErrorException("expected ]");
      i.skip();
      formula = Always(parse(i, P_ALWAYS));
      break;


    case '<': // eventually
      i.skip();
      if(i.get() != '>')
        throw new ParseErrorException("expected >");
      i.skip();
      formula = Eventually(parse(i, P_EVENTUALLY));
      break;


    case '(':
      i.skip();
      formula = parse(i, P_ALL);
      if(i.get() != ')')
        throw new ParseErrorException("invalid character: " + ch);
      i.skip();
      break;


    case '"':
      StringBuffer sb = new StringBuffer();

      i.skip();
      while((ch = i.get()) != '"') {
        sb.append(ch);
        i.skip();
      }
      i.skip();

      formula = Proposition(sb.toString());
      break;


    default:

      if (Character.isJavaIdentifierStart(ch))
      {
        StringBuffer sbf = new StringBuffer();

        sbf.append(ch);
        i.skip();

        try
        {
          while(Character.isJavaIdentifierPart(ch = i.get())&&
          (!Formula.is_reserved_char(ch)) )
          {
        sbf.append(ch);
        i.skip();

          }
        } catch(EndOfInputException e) {
          //    return Proposition(sbf.toString());
        }
        String id = sbf.toString();
        if (id.equals("true"))
        {
          formula = True();
        } else if(id.equals("false"))
        {
          formula = False();
        } else
        {
          formula = Proposition(sbf.toString());
        }

      }
      else
        throw new ParseErrorException("invalid character: " + ch);
      break;
      }


      try {
    while(i.get() == ' ') i.skip();
    ch = i.get();
      } catch(EndOfInputException e) {
    return formula;
      }


      while(true) {
    switch(ch) {
      case '/': // and
        if (precedence > P_AND) return formula;
        i.skip();
        if(i.get() != '\\')
          throw new ParseErrorException("expected \\");
        i.skip();
        formula = And(formula, parse(i, P_AND));
        break;


      case '\\': // or
        if (precedence > P_OR) return formula;
        i.skip();
        if(i.get() != '/')
          throw new ParseErrorException("expected /");
        i.skip();
        formula = Or(formula, parse(i, P_OR));
        break;


      case 'U': // until
        if (precedence > P_UNTIL) return formula;
        i.skip();
        formula = Until(formula, parse(i, P_UNTIL));
        break;

      case 'W': // weak until
        if (precedence > P_WUNTIL) return formula;
        i.skip();
        formula = WUntil(formula, parse(i, P_WUNTIL));
        break;

      case 'V': // release
        if (precedence > P_RELEASE) return formula;
        i.skip();
        formula = Release(formula, parse(i, P_RELEASE));
        break;

      case 'M': // weak_release
        if (precedence > P_WRELEASE) return formula;
        i.skip();
        formula = WRelease(formula, parse(i, P_WRELEASE));
        break;


      case '-': // implies
        if (precedence > P_IMPLIES) return formula;
        i.skip();
        if(i.get() != '>')
          throw new ParseErrorException("expected >");
        i.skip();
        formula = Implies(formula, parse(i, P_IMPLIES));
        break;


      case ')':
        return formula;


      case '!':
      case 'X':
      case '[':
      case '<':
      case '(':
      default:
        throw new ParseErrorException("invalid character: " + ch);
    }


    try {
      while(i.get() == ' ') i.skip();
      ch = i.get();
    } catch(EndOfInputException e) {
      break;
    }
      }
      return formula;
    } catch(EndOfInputException e) {
      throw new ParseErrorException("unexpected end of input");
    }
  }  
  static public Formula parse(String str) throws ParseErrorException { // "aObAc"
    Input i = new Input(str);
    return parse(i, P_ALL);
  }  
  public int processRightUntils()
  { int acc_sets = 0;


    if (getContent() == 'U')
    {
      untils.add(this);
      this.untils_index = right.rightOfUntil_index = untils.size() -1;
      //System.out.println("Formula " + this.toString() + " has index " + this.untils_index);
      //System.out.println("Vector at that position contains " + untils.get(this.untils_index).toString());
    }

    if (left != null) left.processRightUntils();
    if (right != null) right.processRightUntils();


    //  System.out.println("There are " + acc_sets + " acceptance sets");
    return untils.size();
  }  
  private static Formula Proposition(String name) {
    return unique(new Formula('p', true, null, null, name));
  }  
  private static Formula Release(Formula sx, Formula dx) {
    return unique(new Formula('V', false, sx, dx, null));
  }  
  public static void reset_static() 
  { 
    untils = new Vector();
    until_forms = null;
  }  
  private Formula rewrite() {
    if(content == 'p')
      return getMatch(name);

    switch(content) {
      case 'A': return And(left.rewrite(), right.rewrite());
      case 'O': return Or(left.rewrite(), right.rewrite());
      case 'U': return Until(left.rewrite(), right.rewrite());
      case 'V': return Release(left.rewrite(), right.rewrite());
      case 'W': return WUntil(left.rewrite(), right.rewrite());
      case 'X': return Next(left.rewrite());
      case 'N': return Not(left.rewrite());
      case 't': return True();
      case 'f': return False();
    }

    throw new RuntimeException("code should not be reached");
  }  
  public Formula rewrite(Formula rule, Formula rewritten) {
    switch(content) {
      case 'A':
      case 'O':
      case 'U':
      case 'V':
      case 'W':
    left = left.rewrite(rule, rewritten);
    right = right.rewrite(rule, rewritten);
    break;

      case 'X':
      case 'N':
    left = left.rewrite(rule, rewritten);
    break;

      case 't':
      case 'f':
      case 'p':
    break;
    }

    if(match(rule)) {
      Formula expr = rewritten.rewrite();

      clearMatches();

      return expr;
    }

    clearMatches();

    return this;
  }  
  public int size() {
    switch(content) {
      case 'A':
      case 'O':
      case 'U':
      case 'V':
      case 'W':
    return left.size() + right.size() + 1;

      case 'X':
      case 'N':
    return left.size() + 1;

      default:
    return 0;
    }
  }  
  public String toString() {
    switch(content) {
      case 'A': return "( " + left.toString() + " /\\ " + right.toString() + " )";
      case 'O': return "( " + left.toString() + " \\/ " + right.toString() + " )";
      case 'U': return "( " + left.toString() + " U " + right.toString() + " )";
      case 'V': return "( " + left.toString() + " V " + right.toString() + " )";
      case 'W': return "( " + left.toString() + " W " + right.toString() + " )";
      //case 'M': return "( " + left.toString() + " M " + right.toString() + " )";
      case 'X': return "( () " + left.toString() + " )";
      case 'N': return "( ! " + left.toString() + " )";
      case 't': return "( true )";
      case 'f': return "( false )";
      case 'p': return "( \"" + name + "\" )";
      default:  return new Character(content).toString();
    }
  }  
  public String toString(boolean exprId) {
    if(!exprId) return toString();


    switch(content) {
      case 'A': return "( " + left.toString(true) + " /\\ " + right.toString(true) + " )[" + id + "]";
      case 'O': return "( " + left.toString(true) + " \\/ " + right.toString(true) + " )[" + id + "]";
      case 'U': return "( " + left.toString(true) + " U " + right.toString(true) + " )[" + id + "]";
      case 'V': return "( " + left.toString(true) + " V " + right.toString(true) + " )[" + id + "]";
      case 'W': return "( " + left.toString(true) + " W " + right.toString(true) + " )[" + id + "]";
      //case 'M': return "( " + left.toString(true) + " M " + right.toString(true) + " )[" + id + "]";
      case 'X': return "( () " + left.toString(true) + " )[" + id + "]";
      case 'N': return "( ! " + left.toString(true) + " )[" + id + "]";
      case 't': return "( true )[" + id + "]";
      case 'f': return "( false )[" + id + "]";
      case 'p': return "( \"" + name + "\" )[" + id + "]";
      default:  return "( " + content + " )[" + id + "]";
    }
  }  
  private static Formula True() {
    return unique(new Formula('t', true, null, null, null));
  }  
  private static Formula unique(Formula f) {
    String s = f.toString();


    if(ht.containsKey(s))
      return (Formula)ht.get(s);


    ht.put(s, f);
    return f;
  }  
  private static Formula Until(Formula sx, Formula dx) {
    return unique(new Formula('U', false, sx, dx, null));
  }  
  private static Formula WRelease(Formula sx, Formula dx) {
    return unique(new Formula('U', false, dx, And(sx, dx), null));
  }  
  private static Formula WUntil(Formula sx, Formula dx) {
    return unique(new Formula('W', false, sx, dx, null));
  }  
}

---