---

SFSReduction.java

package gov.nasa.arc.ase.util.graph;

import java.io.*;
import java.util.TreeSet;
import java.util.List;
import java.util.LinkedList;
import java.util.Iterator;
import java.util.Set;
import java.util.TreeSet;
import java.util.StringTokenizer;
import java.util.Vector;


public class SFSReduction {
  private static TreeSet getPrevN(Node currNode, boolean prevPO[][]) {
    List edges = currNode.getOutgoingEdges();
    LinkedList neighbors = new LinkedList();
    ITypeNeighbor iNeigh;
    TreeSet prevN = new TreeSet();


    for (Iterator i = edges.iterator(); i.hasNext();) {
      Edge currEdge = (Edge)i.next();
      iNeigh = new ITypeNeighbor(currEdge.getNext().
                                 getIntAttribute("_prevColor"),
                                 currEdge.getGuard());
      neighbors.add(iNeigh);
    }
    
    // No neighbors present
    if (neighbors.size() == 0)
      return prevN;


    // Get the first of the list. Remove it from the list. Compare
    // this element with the rest of the list. If element subsumes
    // something in remainder of list remove that thing from list. If
    // element is subsumed, throw element away, else put element in
    // set
    boolean useless;
    do {
      useless = false;
      iNeigh = (ITypeNeighbor)neighbors.removeFirst();
      for (Iterator i = neighbors.iterator(); i.hasNext();) {
        ITypeNeighbor nNeigh = (ITypeNeighbor)i.next();
        ITypeNeighbor dominating = iDominates(iNeigh, nNeigh, prevPO);
        if (dominating == iNeigh) 
          i.remove();
        if (dominating == nNeigh) {
          useless = true;
          break;
        }
      }
      if (!useless)  
        prevN.add(iNeigh);
    } while (neighbors.size() > 0);


    return prevN;
  }  
  /** Returns the neighbor that dominates. If none dominates the
   * other, then returns null
   */
  private static ITypeNeighbor iDominates(ITypeNeighbor iNeigh,
                                          ITypeNeighbor nNeigh,
                                          boolean prevPO[][]) {
    String iTerm = iNeigh.getTransition();
    String nTerm = nNeigh.getTransition();
    int iColor = iNeigh.getColor();
    int nColor = nNeigh.getColor();
    String theSubterm = subterm(iTerm, nTerm);
    if (theSubterm == iTerm) {
      if (prevPO[nColor-1][iColor-1]) {
        // iNeigh i-dominates nNeigh
        return iNeigh;
      } else {
        return null;
      }
    } 
    if (theSubterm == nTerm) {
      if (prevPO[iColor-1][nColor-1]) {
        // nNeigh i-dominates iNeigh
        return nNeigh;
      } else {
        return null;
      }
    } 
    if (theSubterm.equals("true")) {
      if (prevPO[nColor-1][iColor-1])
        // iNeigh i-dominates nNeigh
        return iNeigh;
      else if (prevPO[iColor-1][nColor-1]) 
        // nNeigh i-dominates iNeigh
        return nNeigh;
    } 
    return null;
  }  
  private static boolean iDominateSet(TreeSet setOne, TreeSet setTwo,
                                      boolean prevPO[][]) {
    TreeSet working = new TreeSet(setTwo);
    for (Iterator i = working.iterator(); i.hasNext();) {
      ITypeNeighbor neighTwo = (ITypeNeighbor)i.next();
      for (Iterator j = setOne.iterator(); j.hasNext();) {
        ITypeNeighbor neighOne = (ITypeNeighbor)j.next();
        ITypeNeighbor dominating = iDominates(neighOne, neighTwo, prevPO);
        if (dominating == neighOne) {
          i.remove();
          break;
        }
      }
    }
    if (working.size() == 0)
      return true;


    return false;
  }  
  private static boolean isAccepting(Node nodeIn) {
    return (nodeIn.getBooleanAttribute("accepting"));
  }  
  public static void main(String[] args) {
    if(args.length > 1) {
      System.out.println("usage:");
      System.out.println("\tjava gov.nasa.arc.ase.util.graph.SFSReduction [<filename>]");
      return;
    }


    Graph g = null;


    try {
      if(args.length == 0)
        g = Graph.load();
      else
        g = Graph.load(args[0]);
    } catch(IOException e) {
      System.out.println("Can't load the graph.");
      return;
    }



    Graph reduced = reduce(g);


    reduced.save();
  }  
  private static Graph reachabilityGraph(Graph g) {
    Vector work = new Vector();
    Vector reachable = new Vector();
    work.add(g.getInit());
    while(!work.isEmpty()) {
      Node currNode = (Node)work.firstElement();
      reachable.add(currNode);
      if (currNode != null) {
        List outgoingEdges = currNode.getOutgoingEdges();
        for (Iterator i=outgoingEdges.iterator();i.hasNext();) {
          Edge currEdge = (Edge)i.next();
          Node nextNode = (Node)currEdge.getNext();
          if (!(work.contains(nextNode) || reachable.contains(nextNode)))
            work.add(nextNode);
        }
      } 
      if (work.remove(0) != currNode)
        System.out.println("ERROR"); // should probably throw exception
    }
    List nodes = g.getNodes();
    if (nodes != null) {
      for (Iterator i=nodes.iterator();i.hasNext();) {
        Node n = (Node)i.next();
        if (!reachable.contains(n))
          g.removeNode(n);
      }
    }
    return g;
  }  
  public static Graph reduce(Graph g) {


    int currNumColors;
    int prevNumColors = 1;
    int currNumPO = 4;
    int prevNumPO = prevNumColors;
    TreeSet newColorSet = null;
    LinkedList newColorList = null;
    boolean accepting = false;
    boolean nonaccepting = false;


    // Initialization
    List nodes = g.getNodes();
    for (Iterator i = nodes.iterator(); i.hasNext();) {
      Node currNode = (Node)i.next();
      currNode.setIntAttribute("_prevColor", 1);
      if (isAccepting(currNode)) {
        currNode.setIntAttribute("_currColor", 1);
        accepting = true;
      }
      else {
        currNode.setIntAttribute("_currColor", 2);
        nonaccepting = true;
      }
    }
    if (accepting && nonaccepting) 
      currNumColors = 2;
    else
      currNumColors = 1;
    // po(i, j)
    boolean currPO[][] = new boolean[2][2];
    boolean prevPO[][];
    for (int i=0; i<2; i++) {
      for (int j=0; j<2; j++) {
        if (i >= j)
          currPO[i][j] = true;
        else
          currPO[i][j] = false;
      }
    }


    while ((currNumColors != prevNumColors) || (currNumPO != prevNumPO)) {
      // Incrementing i, equiv. current values become previous ones
      for (Iterator i = nodes.iterator(); i.hasNext();) {
        Node currNode = (Node)i.next();
        currNode.setIntAttribute("_prevColor", 
                                 currNode.getIntAttribute("_currColor"));
      } 
      prevPO = currPO;
      prevNumColors = currNumColors;


      // Getting the new color pairs
      newColorList = new LinkedList();
      newColorSet = new TreeSet();
      for (Iterator i = nodes.iterator(); i.hasNext();) {
        Node currNode = (Node)i.next();
        ColorPair currPair = 
          new ColorPair(currNode.getIntAttribute("_prevColor"),
                        getPrevN(currNode, prevPO));
        newColorList.add(new Pair(currNode.getId(), currPair));
        newColorSet.add(currPair);
      }
      currNumColors = newColorSet.size();
      
      if (prevNumColors == currNumColors)
        break;


      // Convert the set into a linked list so that rank of object is known
      LinkedList ordered = new LinkedList();
      for (Iterator i = newColorSet.iterator(); i.hasNext();) {
        ColorPair currPair = (ColorPair)i.next();
        ordered.add(currPair);
      }


      // Renaming color set
      for (Iterator i = newColorList.iterator(); i.hasNext();) {
        Pair cPair = (Pair)i.next();
        ColorPair currPair = (ColorPair)cPair.getElement();
        g.getNode(cPair.getValue()).setIntAttribute("_currColor",
                                                    ordered.indexOf(currPair) + 1);
      }
      
      // Update partial order
      currPO = new boolean[currNumColors][currNumColors];
      for (Iterator i = newColorList.iterator(); i.hasNext();) {
        ColorPair currPairOne = (ColorPair)((Pair)i.next()).getElement();
        for(Iterator j = newColorList.iterator(); j.hasNext();) {
          ColorPair currPairTwo = (ColorPair)((Pair)j.next()).getElement();
          boolean po = prevPO[currPairTwo.getColor()-1][currPairOne.getColor()-1];
          boolean dominate = iDominateSet(currPairOne.getIMaxSet(),
                                          currPairTwo.getIMaxSet(), prevPO);
          if (po && dominate ) {
            currPO[ordered.indexOf(currPairTwo)][ordered.indexOf(currPairOne)]
              = true;
          }
          else
            currPO[ordered.indexOf(currPairTwo)][ordered.indexOf(currPairOne)]
              = false;
        }
      } 
    }


    // Create new graph
    Graph result;
    if (newColorList == null)
      result = g;


    else {


      result = new Graph();
      Node newNodes[] = new Node[currNumColors];
      for (int i=0; i< currNumColors; i++) {
        Node n = new Node(result);
        newNodes[i] = n;
      }


      for (Iterator i = newColorList.iterator();i.hasNext();) {
        Pair nodePair = (Pair)i.next();
        int origNodeId = nodePair.getValue();
        ColorPair colPair = (ColorPair)nodePair.getElement();


        if (newColorSet.contains(colPair)) {
          newColorSet.remove(colPair);
          TreeSet pairSet = (TreeSet)colPair.getIMaxSet();
          int color = colPair.getColor();
          Node currNode = newNodes[color-1];
          
          for (Iterator j = pairSet.iterator(); j.hasNext();) {
            ITypeNeighbor neigh = (ITypeNeighbor)j.next();
            int neighPos = neigh.getColor()-1;
            Edge currEdge = new Edge(currNode, newNodes[neighPos], neigh.getTransition());
          }
          // starting node
          if (g.getInit().getId() == origNodeId) 
            result.setInit(currNode);


          // accepting node
          if (isAccepting(g.getNode(origNodeId)))
            currNode.setBooleanAttribute("accepting", true);


        }
      }
    } 
    return reachabilityGraph(result);
    //return result;
  }  
  private static String subterm(String pred1, String pred2) {


    if (pred1.equals("-") && pred2.equals("-"))
      return "true";
    if (pred1.equals("-"))
      return pred1;
    if (pred2.equals("-"))
      return pred2;
    
    if ((pred1.indexOf("true") != -1) && (pred2.indexOf("true") != -1))
      return "true";
    if (pred1.indexOf("true") != -1)
      return pred1;
    if (pred2.indexOf("true") != -1)
      return pred2;
    
    // ASSUMPTION: the shortest predicate, i.e. with less litterals,
    // will most probably be the subterm of the other predicate
    // (provided terms are simplified)
    // alpha subterm of tau, i.e. tau implies alpha
    String alphaStr;
    String tauStr;


    if (pred1.length() <= pred2.length()) {
      alphaStr = pred1;
      tauStr = pred2;
    } else {
      alphaStr = pred2;
      tauStr = pred1;
    }
      
    StringTokenizer alphaTk = new StringTokenizer(alphaStr, "&");
    StringTokenizer tauTk = new StringTokenizer(tauStr, "&");
    LinkedList tauLst = new LinkedList();


    // Putting the litterals of tau in a list - for easier access
    while (tauTk.hasMoreTokens()) {
      String token = tauTk.nextToken();
      tauLst.add(token);
    }
    while (alphaTk.hasMoreTokens()) {
      String alphaLit = alphaTk.nextToken();
      if (!tauLst.contains(alphaLit))
        return "false";
    }
    if (pred1.length() == pred2.length())
      return "true";
    return alphaStr;
  }  
}

---