lib/browser/GraphBrowser/Region.java
author blanchet
Wed, 04 Aug 2010 23:27:27 +0200
changeset 38195 a8cef06e0480
parent 37738 7bf3ec9e7b0c
child 50473 ca4088bf8365
permissions -rw-r--r--
Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again; the effect of removing the constraint varies on problem to problem, but it tends to be overwhelmingly negative in conjuction with the new datatype sym breaking stuff at high cardinalities
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     1
/***************************************************************************
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     2
  Title:      GraphBrowser/Region.java
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     3
  Author:     Stefan Berghofer, TU Muenchen
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     4
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     5
  This is an auxiliary class which is used by the layout algorithm when
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     6
  calculating coordinates with the "pendulum method". A "region" is a
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     7
  group of nodes which "stick together".
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     8
***************************************************************************/
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
     9
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    10
package GraphBrowser;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    11
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    12
import java.util.*;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    13
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    14
class Region {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    15
	Vector vertices=new Vector(10,10);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    16
	Graph gra;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    17
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    18
	public Region(Graph g) { gra=g; }
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    19
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    20
	public void addVertex(Vertex v) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    21
		vertices.addElement(v);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    22
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    23
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    24
	public Enumeration getVertices() {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    25
		return vertices.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    26
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    27
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    28
	public int pred_deflection() {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    29
		float d1=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    30
		int n=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    31
		Enumeration e1=vertices.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    32
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    33
			float d2=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    34
			int p=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    35
			n++;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    36
			Vertex v=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    37
			Enumeration e2=v.getParents();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    38
			while (e2.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    39
				p++;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    40
				d2+=((Vertex)(e2.nextElement())).getX()-v.getX();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    41
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    42
			if (p>0) d1+=d2/p;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    43
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    44
		return (int)(Math.round(d1/n));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    45
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    46
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    47
	public int succ_deflection() {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    48
		float d1=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    49
		int n=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    50
		Enumeration e1=vertices.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    51
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    52
			float d2=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    53
			int p=0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    54
			n++;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    55
			Vertex v=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    56
			Enumeration e2=v.getChildren();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    57
			while (e2.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    58
				p++;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    59
				d2+=((Vertex)(e2.nextElement())).getX()-v.getX();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    60
			}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    61
			if (p>0) d1+=d2/p;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    62
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    63
		return (int)(Math.round(d1/n));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    64
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    65
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    66
	public void move(int x) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    67
		Enumeration e1=vertices.elements();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    68
		while (e1.hasMoreElements()) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    69
			Vertex v=(Vertex)(e1.nextElement());
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    70
			v.setX(v.getX()+x);
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    71
		}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    72
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    73
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    74
	public void combine(Region r2) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    75
		Enumeration e1=r2.getVertices();
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    76
		while (e1.hasMoreElements()) addVertex((Vertex)(e1.nextElement()));
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    77
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    78
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    79
	public int spaceBetween(Region r2) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    80
		return ((Vertex)(r2.getVertices().nextElement())).leftX()-
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    81
			((Vertex)(vertices.lastElement())).rightX()-
37738
7bf3ec9e7b0c Boxes may now have different widths.
berghofe
parents: 33686
diff changeset
    82
			20;
3599
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    83
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    84
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    85
	public boolean touching(Region r2) {
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    86
		return spaceBetween(r2)==0;
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    87
	}
89cbba12863d Source files for Isabelle theory graph browser.
berghofe
parents:
diff changeset
    88
}