Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/Tools/GraphBrowser/graphbrowser/   (Beweissystem Isabelle Version 2025-1©)  Datei vom 16.11.2025 mit Größe 30 kB image not shown  

Quelle  Graph.java   Sprache: JAVA

 
/***************************************************************************
  Title:      graphbrowser/Graph.java
  Author:     Stefan Berghofer, TU Muenchen
  Options:    :tabSize=4:

  This class contains the core of the layout algorithm and methods for
  drawing and PostScript output.
***************************************************************************/


package isabelle.graphbrowser;

import java.util.*;
import java.awt.*;
import java.io.*;

public class Graph {
 /**** parameters for layout ****/

 public int box_height=0;
 public int box_height2;
 public Graphics gfx;

 Vector vertices=new Vector(10,10);
 Vector splines=new Vector(10,10);
 Vector numEdges=new Vector(10,10);
 Vertex []vertices2;

 public int min_x=0,min_y=0,max_x=10,max_y=10;

 /********************************************************************/
 /*                         clone graph object                       */
 /********************************************************************/

 public Object clone() {
  Graph gr=new Graph();
  Enumeration e1;
  int i;

  gr.splines=(Vector)(splines.clone());

  e1=vertices.elements();
  while (e1.hasMoreElements())
   gr.addVertex((Vertex)(((Vertex)(e1.nextElement())).clone()));

  for (i=0;i<vertices.size();i++) {
   Vertex vx1=(Vertex)(gr.vertices.elementAt(i));
   e1=((Vertex)(vertices.elementAt(i))).getChildren();
   while (e1.hasMoreElements()) {
    Vertex vx2=(Vertex)(gr.vertices.elementAt(vertices.indexOf(e1.nextElement())));
    vx1.addChild(vx2);
   }
  }

  gr.vertices2 = new Vertex[vertices.size()];
  gr.vertices.copyInto(gr.vertices2);

  gr.min_x=min_x;gr.max_x=max_x;
  gr.min_y=min_y;gr.max_y=max_y;

  return gr;
 }

 Graph() {}

 /********************************************************************/
 /*                      Read graph from stream                      */
 /********************************************************************/

 public Graph(InputStream s,TreeNode tn) throws IOException, ParseError {
  StreamTokenizer tok=new StreamTokenizer(new InputStreamReader(s));
  String name,dir,vertexID;
  Vertex ve1,ve2;
  boolean children,unfoldDir;
  int index=0;

  tok.nextToken();
  while (tok.ttype!=StreamTokenizer.TT_EOF) {
   if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
    throw new ParseError("expected: vertex name\nfound : "+tok.toString());
   name=tok.sval;
                        tok.nextToken();
   if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
    throw new ParseError("expected: vertex identifier\nfound : "+tok.toString());
   vertexID=tok.sval;
   tok.nextToken();
   if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
    throw new ParseError("expected: directory name\nfound : "+tok.toString());
   dir=tok.sval;
   tok.nextToken();
   if (tok.ttype=='+') {
    unfoldDir=true;
    tok.nextToken();
   } else
    unfoldDir=false;
   if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
    throw new ParseError("expected: path name\nfound : "+tok.toString());
   ve1=findVertex(vertexID);
   if (ve1==null) {
    ve1=new NormalVertex("");
    ve1.setID(vertexID);
    ve1.setNumber(index++);
    addVertex(ve1);
   }
   ve1.setPath(tok.sval);
   ve1.setDir(dir);
                        ve1.setLabel(name);
   tn.insertNode(name,dir,tok.sval,ve1.getNumber(),unfoldDir);
   tok.nextToken();
   if (tok.ttype=='<') {
    children=true;
    tok.nextToken();
   } else if (tok.ttype=='>') {
     children=false;
     tok.nextToken();
   } else children=true;
   while (tok.ttype!=';') {
    if (tok.ttype!=StreamTokenizer.TT_WORD && tok.ttype!='"')
     throw new ParseError("expected: child vertex identifier or ';'\nfound : "+tok.toString());    
    ve2=findVertex(tok.sval);
    if (ve2==null) {
     ve2=new NormalVertex("");
     ve2.setID(tok.sval);
     ve2.setNumber(index++);
     addVertex(ve2);
    }
    if (children)
     ve1.addChild(ve2);
    else
     ve1.addParent(ve2);
    tok.nextToken();
   }
   tok.nextToken();
  }
  vertices2 = new Vertex[vertices.size()];
  vertices.copyInto(vertices2);
 }
 
 /*** Find vertex with identifier vertexID ***/

 public Vertex findVertex(String vertexID) {
  Enumeration e1=vertices.elements();
  Vertex v1;

  while (e1.hasMoreElements()) {
   v1=(Vertex)(e1.nextElement());
   if ((v1.getID()).equals(vertexID))
    return v1;
  }
  return null;
 }
   
 public void addVertex(Vertex v) {
  vertices.addElement(v);
  v.setGraph(this);
 }

 public void removeVertex(Vertex v) {
  vertices.removeElement(v);
 }

 public Enumeration getVertices() {
  return vertices.elements();
 }

 /********************************************************************/
 /*                          graph layout                            */
 /********************************************************************/

 public void layout(Graphics g) {
  splines.removeAllElements();
  hasseDiagram();
  Vector layers=min_crossings(insert_dummies((Vector)(sort().elementAt(0))));
  setParameters(g);
  init_coordinates(layers);
  pendulum(layers);
  rubberband(layers);
  calcSplines(layers);
  calcBoundingBox();
 }

 /********************************************************************/
 /*                      set layout parameters                       */
 /********************************************************************/

 public void setParameters(Graphics g) {
  Enumeration e1=vertices.elements();
  int h;
  h=Integer.MIN_VALUE;

  while (e1.hasMoreElements()) {
    Box dim=((Vertex)(e1.nextElement())).getLabelSize(g);
   h=Math.max(h,dim.height);
  }
  box_height=h+4;
  box_height2=box_height/2;
  gfx=g;
 }

 /********************************************************************/
 /*                       topological sorting                        */
 /********************************************************************/

 public Vector sort() {
  Vector todo=(Vector)(vertices.clone());
  Vector layers=new Vector(10,10);
  Vector todo2;
  Enumeration e1,e2;
  Vertex v,v2;

  e1=vertices.elements();
  while (e1.hasMoreElements())
   ((Vertex)(e1.nextElement())).setDegree(0);

  e1=vertices.elements();
  while (e1.hasMoreElements()) {
   v=(Vertex)(e1.nextElement());
   e2=v.getChildren();
   while (e2.hasMoreElements()) {
    v2=(Vertex)(e2.nextElement());
    todo.removeElement(v2);
    v2.setDegree(1+v2.getDegree());
   }
  }
  while (!todo.isEmpty()) {
   layers.addElement(todo);
   todo2=new Vector(10,10);
   e1=todo.elements();
   while (e1.hasMoreElements()) {
    e2=((Vertex)(e1.nextElement())).getChildren();
    while (e2.hasMoreElements()) {
     v=(Vertex)(e2.nextElement());
     v.setDegree(v.getDegree()-1);
     if (v.getDegree()==0) {
      todo2.addElement(v);
      v.setDegree(layers.size());
     }
    }
   }
   todo=todo2;
  }
  return layers;
 }

 /********************************************************************/
 /*                      compute hasse diagram                       */
 /********************************************************************/

 public void hasseDiagram() {
  Enumeration e1,e2;
  Vertex vx1,vx2;

  /** construct adjacence matrix **/

  int vs=vertices.size();
  boolean adj[][]=new boolean[vs][vs];
  boolean adj2[][]=new boolean[vs][vs];
  int i,j,k;

  e1=getVertices();
  for (i=0;i<vs;i++) {
   vx1=(Vertex)(e1.nextElement());
   e2=vx1.getChildren();
   while (e2.hasMoreElements()) {
    vx2=(Vertex)(e2.nextElement());
    j=vertices.indexOf(vx2);
    adj[i][j]=true;
    adj2[i][j]=true;
   }
  }

  /** compute transitive closure R+ **/

  for (k=0;k<vs;k++)
   for (i=0;i<vs;i++)
    if (adj[i][k])
     for (j=0;j<vs;j++)
      adj[i][j] = adj[i][j] || adj[k][j];

  /** compute R \ (R+)^2 **/

  for (i=0;i<vs;i++)
   for (j=0;j<vs;j++)
    if (adj2[i][j]) {
     vx1=(Vertex)(vertices.elementAt(i));
     vx2=(Vertex)(vertices.elementAt(j));
     for (k=0;k<vs;k++)
      if (adj[i][k] && adj[k][j]) {
       vx1.removeChild(vx2);
       break;
      }
    }
 }
    
 /********************************************************************/
 /*                      insert dummy vertices                       */
 /********************************************************************/

 public Vector insert_dummies(Vector v) {
  Vector layers2=new Vector(10,10);
  int n_edges;

  do {
   Enumeration e1=v.elements(),e2;
   Vector next=new Vector(10,10);

   layers2.addElement(v);
   n_edges=0;
   while (e1.hasMoreElements()) {
    Vertex v1=(Vertex)(e1.nextElement());
    e2=v1.getChildren();
    while (e2.hasMoreElements()) {
     n_edges++;
     Vertex v2=(Vertex)(e2.nextElement());
     if (v2.getDegree()!=v1.getDegree()+1) {
      Vertex v3=new DummyVertex();
      v3.addChild(v2);
      v3.setDegree(v1.getDegree()+1);
      v1.removeChild(v2);
      v1.addChild(v3);
      next.addElement(v3);
      addVertex(v3);
     } else if (next.indexOf(v2)<0) next.addElement(v2);
    }
   }
   v=next;
   numEdges.addElement(Integer.valueOf(n_edges));
  } while (!v.isEmpty());
  return layers2;
 }

 /********************************************************************/
 /*                     calculation of crossings                     */
 /********************************************************************/

 public int count_crossings(Vector layers,int oldcr) {
  int i,j,y1,y2,cr=0,l;
  for (l=0;l<layers.size()-1;l++) {
   Vector v1=(Vector)(layers.elementAt(l));
   for (i=0;i<v1.size();i++) {
    Enumeration e2=((Vertex)(v1.elementAt(i))).getChildren();
    while (e2.hasMoreElements()) {
     y1=((Vector)(layers.elementAt(l+1))).indexOf(e2.nextElement());
     for (j=0;j<i;j++) {
      Enumeration e3=((Vertex)(v1.elementAt(j))).getChildren();
      while (e3.hasMoreElements()) {
       y2=((Vector)(layers.elementAt(l+1))).indexOf(e3.nextElement());
       if (y1<y2) {
        cr++;
        if (cr>=oldcr) return cr;
       }
      }
     }
    }
   }
  }
  return cr;
 }

 /********************************************************************/
 /* calculation of crossings where vertices vx1 and vx2 are involved */
 /* vx1 and vx2 must be in same layer and vx1 is left from vx2       */
 /********************************************************************/

 public int count_crossings_2(Vector layers,Vertex vx1,Vertex vx2,int oldcr) {
  int i,cr=0,l=vx1.getDegree();
  Vertex va,vb;
  Vector layer;
  Enumeration e1,e2;

  if (l>0) {
   layer=(Vector)(layers.elementAt(l-1));
   e1=vx1.getParents();
   while (e1.hasMoreElements()) {
    va=(Vertex)(e1.nextElement());
    i=layer.indexOf(va);
    e2=vx2.getParents();
    while (e2.hasMoreElements()) {
     vb=(Vertex)(e2.nextElement());
     if (layer.indexOf(vb)<i) {
      cr++;
      if (cr>=oldcr) return cr;
     }
    }
   }
  }
  if (l<layers.size()-1) {
   layer=(Vector)(layers.elementAt(l+1));
   e1=vx1.getChildren();
   while (e1.hasMoreElements()) {
    va=(Vertex)(e1.nextElement());
    i=layer.indexOf(va);
    e2=vx2.getChildren();
    while (e2.hasMoreElements()) {
     vb=(Vertex)(e2.nextElement());
     if (layer.indexOf(vb)<i) {
      cr++;
      if (cr>=oldcr) return cr;
     }
    }
   }
  }
  return cr;
 }

 /********************************************************************/
 /*       reduction of crossings by exchanging adjacent vertices     */
 /********************************************************************/

 public void exchangeVertices(Vector layers,int oldcr) {
  int i,l,c1,c2;
  Vertex vx1,vx2;
  Vector v1;

  for (l=0;l<layers.size();l++) {
   v1=(Vector)(layers.elementAt(l));
   for (i=0;i<v1.size()-1;i++) {
    vx1=(Vertex)(v1.elementAt(i));
    vx2=(Vertex)(v1.elementAt(i+1));
    c1=count_crossings_2(layers,vx1,vx2,oldcr);
    c2=count_crossings_2(layers,vx2,vx1,c1);
    if (c2<c1) {
     v1.setElementAt(vx2,i);
     v1.setElementAt(vx1,i+1);
    }
   }
  }
 }

 /********************************************************************/
 /*                    minimization of crossings                     */
 /********************************************************************/

 public Vector min_crossings(Vector layers) {
  int n,i,l,k,z=0,cr2,cr=count_crossings(layers,Integer.MAX_VALUE);
  boolean topdown=true,first=true;
  Enumeration e1,e2;
  Vector v1,v2,layers2=null,best=layers;
  Vertex vx1,vx2;
  n=0;
  while (n<3 && cr>0) {
   if (topdown) {
    /** top-down-traversal **/

    layers2=new Vector(10,10);
    for (l=0;l<layers.size();l++) {
     v1=(Vector)(layers.elementAt(l));
     if (l==0) layers2.addElement(v1.clone());
     else {
      v2=new Vector(10,10);
      layers2.addElement(v2);
      e1=v1.elements();
      while (e1.hasMoreElements()) {
       vx1=(Vertex)(e1.nextElement());
       k=0;z=0;
       e2=vx1.getParents();
       while (e2.hasMoreElements()) {
        k+=((Vector)(layers2.elementAt(l-1))).indexOf(e2.nextElement());
        z++;
       }
       if (z>0)
        vx1.setWeight(((double)(k))/z);
       else if (first)
        vx1.setWeight(Double.MAX_VALUE);
       for (i=0;i<v2.size();i++)
        if (vx1.getWeight()<((Vertex)(v2.elementAt(i))).getWeight()) break;
       if (i==v2.size()) v2.addElement(vx1);
       else v2.insertElementAt(vx1,i);
      }
     }
    }
   } else {
    /** bottom-up-traversal **/

    layers2=new Vector(10,10);
    for (l=layers.size()-1;l>=0;l--) {
     v1=(Vector)(layers.elementAt(l));
     if (l==layers.size()-1) layers2.addElement(v1.clone());
     else {
      v2=new Vector(10,10);
      layers2.insertElementAt(v2,0);
      e1=v1.elements();
      while (e1.hasMoreElements()) {
       vx1=(Vertex)(e1.nextElement());
       k=0;z=0;
       e2=vx1.getChildren();
       while (e2.hasMoreElements()) {
        k+=((Vector)(layers2.elementAt(1))).indexOf(e2.nextElement());
        z++;
       }
       if (z>0)
        vx1.setWeight(((double)(k))/z);
       else if (first)
        vx1.setWeight(Double.MAX_VALUE);
       for (i=0;i<v2.size();i++)
        if (vx1.getWeight()<((Vertex)(v2.elementAt(i))).getWeight()) break;
       if (i==v2.size()) v2.addElement(vx1);
       else v2.insertElementAt(vx1,i);
      }
     }
    }
   }
   //exchangeVertices(layers2,cr);
   topdown=!topdown;
   first=false;
   layers=layers2;

   cr2=count_crossings(layers2,cr);
   if (cr2<cr) {
    best=layers2;
    cr=cr2;     
   } else n++;
  }

  while (true) {
   exchangeVertices(best,cr);
   cr2=count_crossings(best,cr);
   if (cr2<cr)
    cr=cr2;
   else
    break;
  }

  return best;
 }

 /********************************************************************/
 /*                   set initial coordinates                        */
 /********************************************************************/

 public void init_coordinates(Vector layers) {
  int y=0;
  Enumeration e1=layers.elements();
  Enumeration e3=numEdges.elements();
  while (e1.hasMoreElements()) {
   Vector v1=(Vector)(e1.nextElement());
   Enumeration e2=v1.elements();
   int x=0;
   while (e2.hasMoreElements()) {
    Vertex ve=(Vertex)(e2.nextElement());
    ve.setX(x+ve.box_width2());
    ve.setY(y);
    x+=ve.box_width()+20;
   }
   y+=box_height+Math.max(35,7*(((Integer)(e3.nextElement())).intValue()));
  }
 }

 /********************************************************************/
 /*                       pendulum method                            */
 /********************************************************************/

 public void pendulum(Vector layers) {
  Vector layers2=new Vector(10,10);
  Enumeration e1=layers.elements(),e2;
  int i,j,d1,d2,k,offset,dsum;
  Region r1,r2;
  boolean change;

  while (e1.hasMoreElements()) {
   e2=((Vector)(e1.nextElement())).elements();
   Vector layer=new Vector(10,10);
   layers2.addElement(layer);
   while (e2.hasMoreElements()) {
    Region r=new Region(this);
    r.addVertex((Vertex)(e2.nextElement()));
    layer.addElement(r);
   }
  }
  for (k=0;k<10;k++) {
   dsum=0;
   for (j=1;j<layers2.size();j++) {
    Vector l=(Vector)(layers2.elementAt(j));
    if (l.size()>=2) {
     do {
      change=false;
      d1=((Region)(l.firstElement())).pred_deflection();
      for (i=0;i<l.size()-1;i++) {
       r1=(Region)(l.elementAt(i));
       r2=(Region)(l.elementAt(i+1));
       d2=r2.pred_deflection();
       if (r1.touching(r2) && (d1 <= 0 && d2 < d1 ||
        d2 > 0 && d1 > d2 || d1 > 0 && d2 < 0)) {
        r1.combine(r2);
        l.removeElement(r2);
        change=true;
        d2=r1.pred_deflection();
       }
       d1=d2;
      }
     } while (change);
    }
    for (i=0;i<l.size();i++) {
     r1=(Region)(l.elementAt(i));
     d1=r1.pred_deflection();
     offset=d1;
     if (d1<0 && i>0) offset=-Math.min(
      ((Region)(l.elementAt(i-1))).spaceBetween(r1),-d1);
     if (d1>=0 && i<l.size()-1) offset=Math.min(
      r1.spaceBetween((Region)(l.elementAt(i+1))),d1);
     r1.move(offset);
     dsum+=Math.abs(d1);
    }  
   }
   if (dsum==0) break;
  }
 }  

 /********************************************************************/
 /*                      rubberband method                           */
 /********************************************************************/

 public void rubberband(Vector layers) {
  Enumeration e1,e2;
  int i,n,k,d,d2;
  Vector v;
  Vertex vx;

  for (k=0;k<10;k++) {
   e1=layers.elements();
   while (e1.hasMoreElements()) {
    v=(Vector)(e1.nextElement());
    for (i=0;i<v.size();i++) {
     n=0;d=0;
     vx=(Vertex)(v.elementAt(i));
     e2=vx.getChildren();
     while (e2.hasMoreElements()) {
      d+=((Vertex)(e2.nextElement())).getX()-vx.getX();
      n++;
     }
     e2=vx.getParents();
     while (e2.hasMoreElements()) {
      d+=((Vertex)(e2.nextElement())).getX()-vx.getX();
      n++;
     }
     d2=(n!=0?d/n:0);

     if (d<0 && (i==0 || ((Vertex)(v.elementAt(i-1))).rightX()+20 < vx.leftX()+d2) ||
      d>0 && (i==v.size()-1 || ((Vertex)(v.elementAt(i+1))).leftX()-20 > vx.rightX()+d2))
      vx.setX(vx.getX()+d2);
    }
   }
  }
 }

 /**** Intersection point of two lines (auxiliary function for calcSplines)   ****/
 /**** Calculate intersection point of line which is parallel to line (p1,p2) ****/
 /**** and leads through p5, with line (p3,p4)                                ****/

 Point intersect(Point p1,Point p2,Point p3,Point p4,Point p5) {
  float x=0,y=0,s1=0,s2=0;

  if (p1.x!=p2.x)
   s1=((float)(p2.y-p1.y))/(p2.x-p1.x);
  if (p3.x!=p4.x)
   s2=((float)(p4.y-p3.y))/(p4.x-p3.x);
  if (p1.x==p2.x) {
   x=p5.x;
   y=s2*(p5.x-p3.x)+p3.y;
  } else if (p3.x==p4.x) {
   x=p3.x;
   y=s1*(p3.x-p5.x)+p5.y;
  } else {
   x=(p5.x*s1-p3.x*s2+p3.y-p5.y)/(s1-s2);
   y=s2*(x-p3.x)+p3.y;
  }
  return new Point(Math.round(x),Math.round(y));
 }

 /**** Calculate control points (auxiliary function for calcSplines) ****/

 Points calcPoint(Point p1,Point p2,Point p3,int lboxx,int rboxx,int boxy) {

  /*** Points p1 , p2 , p3 define a triangle which encloses the spline.  ***/
  /*** Check if adjacent boxes (specified by lboxx,rboxx and boxy)       ***/
  /*** collide with the spline. In this case p1 and p3 are shifted by an ***/
  /*** appropriate offset before they are returned                       ***/

  int xh1,xh2,bx=0,by=0;
  boolean pt1 = boxy >= p1.y && boxy <= p3.y || boxy >= p3.y && boxy <= p1.y;
  boolean pt2 = boxy+box_height >= p1.y && boxy+box_height <= p3.y ||
                              boxy+box_height >= p3.y && boxy+box_height <= p1.y;
  boolean move = false;
  Point b;

  xh1 = p1.x+(boxy-p1.y)*(p3.x-p1.x)/(p3.y-p1.y);
  xh2 = p1.x+(boxy+box_height-p1.y)*(p3.x-p1.x)/(p3.y-p1.y);

  if (xh1 <= lboxx && pt1 && xh2 <= lboxx && pt2) {
   move = true;
   bx = lboxx;
   by = boxy + (xh1 < xh2 ? 0 : box_height ) ;
  } else if (xh1 >= rboxx && pt1 && xh2 >= rboxx && pt2) {
   move = true;
   bx = rboxx;
   by = boxy + (xh1 > xh2 ? 0 : box_height ) ;
  } else if ( (xh1 <= lboxx || xh1 >= rboxx) && pt1) {
   move = true;
   bx = (xh1 <= lboxx ? lboxx : rboxx ) ;
   by = boxy;
  } else if ( (xh2 <= lboxx || xh2 >= rboxx) && pt2) {
   move = true;
   bx = (xh2 <= lboxx ? lboxx : rboxx ) ;
   by = boxy+box_height;
  }
  b=new Point(bx,by);
  if (move) return new Points(intersect(p1,p3,p1,p2,b),intersect(p1,p3,p2,p3,b));
  else return new Points(p1,p3);
 }

 /********************************************************************/
 /*                        calculate splines                         */
 /********************************************************************/

 public void calcSplines(Vector layers) {
  Enumeration e2,e1=vertices.elements();
  Vertex vx1,vx2,vx3;
  Vector pos,layer;
  int x1,y1,x2,y2,x3,y3,xh,k,leftx,rightx,spc;

  while (e1.hasMoreElements()) {
   vx1=(Vertex)(e1.nextElement());
   if (!vx1.isDummy()) {
    e2=vx1.getChildren();
    while (e2.hasMoreElements()) {
     vx2=(Vertex)(e2.nextElement());
     if (vx2.isDummy()) {
      vx3=vx2;
      /**** convert edge to spline ****/
      pos=new Vector(10,10);
      x1=vx1.getX();
      y1=vx1.getY()+box_height;

      do {
       /*** calculate position of control points ***/
       x2=vx2.getX();
       y2=vx2.getY();
       layer=(Vector)(layers.elementAt(vx2.getDegree()));
       k=layer.indexOf(vx2);
       vx2=(Vertex)((vx2.getChildren()).nextElement());
       x3=vx2.getX();
       y3=vx2.getY();
       spc=0;
       leftx = k==0 /* || ((Vertex)(layer.elementAt(k-1))).isDummy() */ ?
        Integer.MIN_VALUE:
        ((Vertex)(layer.elementAt(k-1))).rightX()+spc;
       rightx = k==layer.size()-1 /* || ((Vertex)(layer.elementAt(k+1))).isDummy() */ ?
        Integer.MAX_VALUE:
        ((Vertex)(layer.elementAt(k+1))).leftX()-spc;
       xh=x2+box_height*(x3-x2)/(y3-y2);
       if (!(x2<=x3 && xh>=rightx || x2>x3 && xh<=leftx)) {
        /* top control point */
        pos.addElement(Integer.valueOf(1));
        y1=y2;
       } else {
        xh=x1+(y2-y1)*(x2-x1)/(y2+box_height-y1);
        if (!(x2<=x1 && xh>=rightx || x2>x1 && xh<=leftx))
         /* bottom control point */
         pos.addElement(Integer.valueOf(2));
        else
         /* two control points needed */
         pos.addElement(Integer.valueOf(3));
        y1=y2+box_height;
       }
       x1=x2;
      } while (vx2.isDummy());
      pos.addElement(Integer.valueOf(1));

      /**** calculate triangles ****/
      vx2=vx3;

      int pos1,pos2,i=0;
      Vector pts=new Vector(10,10);
      int lboxx,rboxx,boxy;

      x1=vx1.getX();
      y1=vx1.getY()+box_height;
      pts.addElement(new Point(x1,y1)); /** edge starting point **/
      do {
       x2=vx2.getX();
       y2=vx2.getY();
       pos1=((Integer)(pos.elementAt(i))).intValue();
       pos2=((Integer)(pos.elementAt(i+1))).intValue();
       i++;
       layer=(Vector)(layers.elementAt(vx2.getDegree()));
       k=layer.indexOf(vx2);
       boxy=vx2.getY();
       vx2=(Vertex)((vx2.getChildren()).nextElement());
       x3=vx2.getX();
       y3=vx2.getY();
       if (pos1==2) y2+=box_height;
       if (pos2==2) y3+=box_height;

       lboxx = (k==0 /* || ((Vertex)(layer.elementAt(k-1))).isDummy() */ ) ?
        Integer.MIN_VALUE :
        ((Vertex)(layer.elementAt(k-1))).rightX();

       rboxx = (k==layer.size()-1 /* || ((Vertex)(layer.elementAt(k+1))).isDummy() */ ) ?
        Integer.MAX_VALUE :
        ((Vertex)(layer.elementAt(k+1))).leftX();

       Point p1,p2,p3;
       Points ps;

       p1 = new Point((x1+x2)/2,(y1+y2)/2);

       if (pos1<=2) {
        /** one control point **/
        p2 = new Point(x2,y2);
        ps = calcPoint(p1,p2,new Point((x2+x3)/2,(y2+y3)/2),lboxx,rboxx,boxy);
        pts.addElement(ps.p);
        pts.addElement(p2);
        pts.addElement(ps.q);
       } else {
        /** two control points **/
        p2 = new Point(x2,y2-box_height);
        p3 = new Point(x2,y2+box_height2);
        ps = calcPoint(p1,p2,p3,lboxx,rboxx,boxy);
        pts.addElement(ps.p);
        pts.addElement(p2);
        pts.addElement(ps.q);
        p2 = new Point(x2,y2+box_height*2);
        ps = calcPoint(p3,p2,new Point((p2.x+x3)/2,(p2.y+y3)/2),
                       lboxx,rboxx,boxy);
        pts.addElement(ps.p);
        pts.addElement(p2);
        pts.addElement(ps.q);
       }
       x1=p2.x;
       y1=p2.y;
      } while (vx2.isDummy());

      pts.addElement(new Point(vx2.getX(),vx2.getY())); /** edge end point **/
      splines.addElement(new Spline(pts));
     }
    }
   }
  }
 }

 /********************************************************************/
 /*                      calculate bounding box                      */
 /********************************************************************/

 public void calcBoundingBox() {
  min_y=min_x=Integer.MAX_VALUE;
  max_y=max_x=Integer.MIN_VALUE;

  Enumeration e1=vertices.elements();
  Vertex v;

  while (e1.hasMoreElements()) {
   v=(Vertex)(e1.nextElement());
   min_x=Math.min(min_x,v.leftX());
   max_x=Math.max(max_x,v.rightX());
   min_y=Math.min(min_y,v.getY());
   max_y=Math.max(max_y,v.getY()+box_height);
  }
  min_x-=20;
  min_y-=20;
  max_x+=20;
  max_y+=20;
 }

 /********************************************************************/
 /*                           draw graph                             */
 /********************************************************************/
      
 public void draw(Graphics g) {
  if (box_height==0) layout(g);

  g.translate(-min_x,-min_y);

  Enumeration e1=vertices.elements();
  while (e1.hasMoreElements())
   ((Vertex)(e1.nextElement())).draw(g);

  e1=splines.elements();
  while (e1.hasMoreElements())
   ((Spline)(e1.nextElement())).draw(g);
 }

 /********************************************************************/
 /*               return vertex at position (x,y)                    */
 /********************************************************************/

 public Vertex vertexAt(int x,int y) {
  Enumeration e1=vertices.elements();
  while (e1.hasMoreElements()) {
   Vertex v=(Vertex)(e1.nextElement());
   if (v.contains(x,y)) return v;
  }
  return null;
 }

 /********************************************************************/
 /*       encode list of vertices (as array of vertice numbers)      */
 /********************************************************************/

 public Vector encode(Vector v) {
  Vector code=new Vector(10,10);
  Enumeration e1=v.elements();

  while (e1.hasMoreElements()) {
   Vertex vx=(Vertex)(e1.nextElement());
   if (vx.getNumber()>=0)
    code.addElement(Integer.valueOf(vx.getNumber()));
  }
  return code;
 }

 /********************************************************************/
 /*                      get vertex with number n                    */
 /********************************************************************/

 public Vertex getVertexByNum(int x) {
  Enumeration e1=vertices.elements();

  while (e1.hasMoreElements()) {
   Vertex vx=(Vertex)(e1.nextElement());
   if (vx.getNumber()==x) return vx;
  }
  return null;
 }

 /********************************************************************/
 /*                      decode list of vertices                     */
 /********************************************************************/

 public Vector decode(Vector code) {
  Enumeration e1=code.elements();
  Vector vec=new Vector(10,10);

  while (e1.hasMoreElements()) {
   int i=((Integer)(e1.nextElement())).intValue();
   //Vertex vx=getVertexByNum(i);
   //if (vx!=null) vec.addElement(vx);
   vec.addElement(vertices2[i]);
  }
  return vec;
 }

 /********************************************************************/
 /*                       collapse vertices                          */
 /********************************************************************/

 public void collapse(Vector vs,String name,Vector inflate) {
  Enumeration e1,e2,e3;
  boolean nonempty=false;
  Vertex vx3,vx2,vx1;
  
  e1=vertices.elements();

  vx1=new NormalVertex(name);
  vx1.setInflate(inflate);

  while (e1.hasMoreElements()) {
   vx2=(Vertex)(e1.nextElement());

   if (vs.indexOf(vx2)<0) {
    e2=vx2.getParents();
    while (e2.hasMoreElements()) {
     vx3=(Vertex)(e2.nextElement());
     if (vs.indexOf(vx3)>=0) {
      if (!vx1.isChild(vx2))
       vx1.addChild(vx2);
      vx3.removeChild(vx2);
     }
    }

    e2=vx2.getChildren();
    while (e2.hasMoreElements()) {
     vx3=(Vertex)(e2.nextElement());
     if (vs.indexOf(vx3)>=0) {
      if (!vx2.isChild(vx1))
       vx2.addChild(vx1);
      vx2.removeChild(vx3);
     }
    }
   } else { nonempty=true; }
  }

  e1=vs.elements();
  while (e1.hasMoreElements())
   try {
    removeVertex((Vertex)(e1.nextElement()));
   } catch (NoSuchElementException exn) {}

  if (nonempty) addVertex(vx1);
 }

 /********************************************************************/
 /*                      PostScript output                           */
 /********************************************************************/

 public void PS(String fname,boolean printable) throws IOException {
  FileOutputStream f = new FileOutputStream(fname);
  PrintWriter p = new PrintWriter(f, true);

  if (printable)
   p.println("%!PS-Adobe-2.0\n\n%%BeginProlog");
  else {
   p.println("%!PS-Adobe-2.0 EPSF-2.0\n%%Orientation: Portrait");
   p.println("%%BoundingBox: "+min_x+" "+min_y+" "+max_x+" "+max_y);
   p.println("%%EndComments\n\n%%BeginProlog");
  }
  p.println("/m { moveto } def /l { lineto } def /n { newpath } def");
  p.println("/s { stroke } def /c { curveto } def");
  p.println("/b { n 0 0 m dup true charpath pathbbox 1 index 4 index sub");
  p.println("7 index exch sub 2 div 9 index add 1 index 4 index sub 7 index exch sub");
  p.println("2 div 9 index add 2 index add m pop pop pop pop");
  p.println("1 -1 scale show 1 -1 scale n 3 index 3 index m 1 index 0 rlineto");
  p.println("0 exch rlineto neg 0 rlineto closepath s pop pop } def");
  p.println("%%EndProlog\n");
  if (printable) {
   int hsize=max_x-min_x;
   int vsize=max_y-min_y;
   if (hsize>vsize) {
    // Landscape output
    double scale=Math.min(1,Math.min(750.0/hsize,500.0/vsize));
    double trans_x=50+max_y*scale+(500-scale*vsize)/2.0;
    double trans_y=50+max_x*scale+(750-scale*hsize)/2.0;
    p.println(trans_x+" "+trans_y+" translate");
    p.println("-90 rotate");
    p.println(scale+" "+(-scale)+" scale");
   } else {
    // Portrait output
    double scale=Math.min(1,Math.min(500.0/hsize,750.0/vsize));
    double trans_x=50-min_x*scale+(500-scale*hsize)/2.0;
    double trans_y=50+max_y*scale+(750-scale*vsize)/2.0;
    p.println(trans_x+" "+trans_y+" translate");
    p.println(scale+" "+(-scale)+" scale");
   }
  } else
   p.println("0 "+(max_y+min_y)+" translate\n1 -1 scale");

  p.println("/Helvetica findfont 12 scalefont setfont");
  p.println("0.5 setlinewidth");

  Enumeration e1=vertices.elements();
  while (e1.hasMoreElements())
   ((Vertex)(e1.nextElement())).PS(p);

  e1=splines.elements();
  while (e1.hasMoreElements())
   ((Spline)(e1.nextElement())).PS(p);

  if (printable) p.println("showpage");

  f.close();
 }
}

/**** Return value of function calcPoint ****/

class Points {
 public Point p,q;

 public Points(Point p1,Point p2) {
  p=p1;q=p2;
 }
}

58%


¤ Dauer der Verarbeitung: 0.20 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland






Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.