author | wenzelm |
Tue, 30 Dec 2014 14:11:06 +0100 | |
changeset 59202 | 711c2446dc9d |
parent 56372 | src/Tools/Graphview/src/layout_pendulum.scala@fadb0fef09d7 |
permissions | -rw-r--r-- |
59202 | 1 |
/* Title: Tools/Graphview/layout_pendulum.scala |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Markus Kaiser, TU Muenchen |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
3 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
4 |
Pendulum DAG layout algorithm. |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
5 |
*/ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
6 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
7 |
package isabelle.graphview |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
8 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
9 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
10 |
import isabelle._ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
11 |
|
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
12 |
|
49744 | 13 |
object Layout_Pendulum |
14 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
15 |
type Key = String |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
16 |
type Point = (Double, Double) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
17 |
type Coordinates = Map[Key, Point] |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
18 |
type Level = List[Key] |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
19 |
type Levels = List[Level] |
49565
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49557
diff
changeset
|
20 |
type Dummies = (Model.Graph, List[Key], Map[Key, Int]) |
50469 | 21 |
|
50470 | 22 |
case class Layout(nodes: Coordinates, dummies: Map[(Key, Key), List[Point]]) |
23 |
val empty_layout = Layout(Map.empty, Map.empty) |
|
24 |
||
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
25 |
val pendulum_iterations = 10 |
49737
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
26 |
val minimize_crossings_iterations = 40 |
50469 | 27 |
|
50474
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
28 |
def apply(graph: Model.Graph, box_distance: Double, box_height: Int => Double): Layout = |
49737
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
29 |
{ |
50470 | 30 |
if (graph.is_empty) empty_layout |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
31 |
else { |
49744 | 32 |
val initial_levels = level_map(graph) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
33 |
|
49744 | 34 |
val (dummy_graph, dummies, dummy_levels) = |
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
50474
diff
changeset
|
35 |
((graph, Map.empty[(Key, Key), List[Key]], initial_levels) /: graph.keys_iterator) { |
49744 | 36 |
case ((graph, dummies, levels), from) => |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
37 |
((graph, dummies, levels) /: graph.imm_succs(from)) { |
49744 | 38 |
case ((graph, dummies, levels), to) => |
39 |
if (levels(to) - levels(from) <= 1) (graph, dummies, levels) |
|
50469 | 40 |
else { |
41 |
val (next, ds, ls) = add_dummies(graph, from, to, levels) |
|
42 |
(next, dummies + ((from, to) -> ds), ls) |
|
43 |
} |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
44 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
45 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
46 |
|
50469 | 47 |
val levels = minimize_crossings(dummy_graph, level_list(dummy_levels)) |
48 |
||
50474
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
49 |
val initial_coordinates: Coordinates = |
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
50 |
(((Map.empty[Key, Point], 0.0) /: levels) { |
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
51 |
case ((coords1, y), level) => |
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
52 |
((((coords1, 0.0) /: level) { |
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
53 |
case ((coords2, x), key) => |
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
54 |
val s = if (graph.defined(key)) graph.get_node(key).name else "X" |
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
55 |
(coords2 + (key -> (x, y)), x + box_distance) |
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
56 |
})._1, y + box_height(level.length)) |
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
57 |
})._1 |
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
58 |
|
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
59 |
val coords = pendulum(dummy_graph, box_distance, levels, initial_coordinates) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
60 |
|
49737
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
61 |
val dummy_coords = |
50467 | 62 |
(Map.empty[(Key, Key), List[Point]] /: dummies.keys) { |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
63 |
case (map, key) => map + (key -> dummies(key).map(coords(_))) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
64 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
65 |
|
50470 | 66 |
Layout(coords, dummy_coords) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
67 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
68 |
} |
49737
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
69 |
|
49744 | 70 |
|
71 |
def add_dummies(graph: Model.Graph, from: Key, to: Key, levels: Map[Key, Int]): Dummies = |
|
72 |
{ |
|
73 |
val ds = |
|
74 |
((levels(from) + 1) until levels(to)) |
|
75 |
.map("%s$%s$%d" format (from, to, _)).toList |
|
76 |
||
77 |
val ls = |
|
78 |
(levels /: ((levels(from) + 1) until levels(to)).zip(ds)) { |
|
79 |
case (ls, (l, d)) => ls + (d -> l) |
|
80 |
} |
|
81 |
||
82 |
val graph1 = (graph /: ds)(_.new_node(_, Model.empty_info)) |
|
83 |
val graph2 = |
|
84 |
(graph1.del_edge(from, to) /: (from :: ds ::: List(to)).sliding(2)) { |
|
85 |
case (g, List(x, y)) => g.add_edge(x, y) |
|
86 |
} |
|
87 |
(graph2, ds, ls) |
|
88 |
} |
|
89 |
||
50469 | 90 |
def level_map(graph: Model.Graph): Map[Key, Int] = |
50467 | 91 |
(Map.empty[Key, Int] /: graph.topological_order) { |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
92 |
(levels, key) => { |
49737
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
93 |
val lev = 1 + (-1 /: graph.imm_preds(key)) { case (m, key) => m max levels(key) } |
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
94 |
levels + (key -> lev) |
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
95 |
} |
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
96 |
} |
50469 | 97 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
98 |
def level_list(map: Map[Key, Int]): Levels = |
49737
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
99 |
{ |
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
100 |
val max_lev = (-1 /: map) { case (m, (_, l)) => m max l } |
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
101 |
val buckets = new Array[Level](max_lev + 1) |
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
102 |
for (l <- 0 to max_lev) { buckets(l) = Nil } |
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
103 |
for ((key, l) <- map) { buckets(l) = key :: buckets(l) } |
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
104 |
buckets.iterator.map(_.sorted).toList |
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
105 |
} |
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
106 |
|
49746 | 107 |
def count_crossings(graph: Model.Graph, levels: Levels): Int = |
108 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
109 |
def in_level(ls: Levels): Int = ls match { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
110 |
case List(top, bot) => |
49746 | 111 |
top.iterator.zipWithIndex.map { |
112 |
case (outer_parent, outer_parent_index) => |
|
113 |
graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)) |
|
114 |
.map(outer_child => |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
115 |
(0 until outer_parent_index) |
49746 | 116 |
.map(inner_parent => |
117 |
graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_)) |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
118 |
.filter(inner_child => outer_child < inner_child) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
119 |
.size |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
120 |
).sum |
49746 | 121 |
).sum |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
122 |
}.sum |
49746 | 123 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
124 |
case _ => 0 |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
125 |
} |
49746 | 126 |
|
127 |
levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
128 |
} |
50469 | 129 |
|
49745 | 130 |
def minimize_crossings(graph: Model.Graph, levels: Levels): Levels = |
131 |
{ |
|
50469 | 132 |
def resort_level(parent: Level, child: Level, top_down: Boolean): Level = |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
133 |
child.map(k => { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
134 |
val ps = if (top_down) graph.imm_preds(k) else graph.imm_succs(k) |
50469 | 135 |
val weight = |
50468 | 136 |
(0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
137 |
(k, weight) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
138 |
}).sortBy(_._2).map(_._1) |
50469 | 139 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
140 |
def resort(levels: Levels, top_down: Boolean) = top_down match { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
141 |
case true => |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
142 |
(List[Level](levels.head) /: levels.tail) { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
143 |
(tops, bot) => resort_level(tops.head, bot, top_down) :: tops |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
144 |
}.reverse |
50469 | 145 |
|
146 |
case false => |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
147 |
(List[Level](levels.reverse.head) /: levels.reverse.tail) { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
148 |
(bots, top) => resort_level(bots.head, top, top_down) :: bots |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
149 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
150 |
} |
50469 | 151 |
|
49737
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
152 |
((levels, count_crossings(graph, levels), true) /: (1 to minimize_crossings_iterations)) { |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
153 |
case ((old_levels, old_crossings, top_down), _) => { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
154 |
val new_levels = resort(old_levels, top_down) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
155 |
val new_crossings = count_crossings(graph, new_levels) |
49737
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
156 |
if (new_crossings < old_crossings) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
157 |
(new_levels, new_crossings, !top_down) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
158 |
else |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
159 |
(old_levels, old_crossings, !top_down) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
160 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
161 |
}._1 |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
162 |
} |
50469 | 163 |
|
50474
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
164 |
def pendulum(graph: Model.Graph, box_distance: Double, |
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
165 |
levels: Levels, coords: Map[Key, Point]): Coordinates = |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
166 |
{ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
167 |
type Regions = List[List[Region]] |
50469 | 168 |
|
169 |
def iteration(regions: Regions, coords: Coordinates, top_down: Boolean) |
|
170 |
: (Regions, Coordinates, Boolean) = |
|
171 |
{ |
|
172 |
val (nextr, nextc, moved) = |
|
50467 | 173 |
((List.empty[List[Region]], coords, false) /: |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
174 |
(if (top_down) regions else regions.reverse)) { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
175 |
case ((tops, coords, prev_moved), bot) => { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
176 |
val nextb = collapse(coords, bot, top_down) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
177 |
val (nextc, this_moved) = deflect(coords, nextb, top_down) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
178 |
(nextb :: tops, nextc, prev_moved || this_moved) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
179 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
180 |
} |
50469 | 181 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
182 |
(nextr.reverse, nextc, moved) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
183 |
} |
50469 | 184 |
|
185 |
def collapse(coords: Coordinates, level: List[Region], top_down: Boolean): List[Region] = |
|
186 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
187 |
if (level.size <= 1) level |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
188 |
else { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
189 |
var next = level |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
190 |
var regions_changed = true |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
191 |
while (regions_changed) { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
192 |
regions_changed = false |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
193 |
for (i <- (next.length to 1)) { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
194 |
val (r1, r2) = (next(i-1), next(i)) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
195 |
val d1 = r1.deflection(coords, top_down) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
196 |
val d2 = r2.deflection(coords, top_down) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
197 |
|
50469 | 198 |
if (// Do regions touch? |
50474
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
199 |
r1.distance(coords, r2) <= box_distance && |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
200 |
// Do they influence each other? |
50469 | 201 |
(d1 <= 0 && d2 < d1 || d2 > 0 && d1 > d2 || d1 > 0 && d2 < 0)) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
202 |
{ |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
203 |
regions_changed = true |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
204 |
r1.nodes = r1.nodes ::: r2.nodes |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
205 |
next = next.filter(next.indexOf(_) != i) |
50469 | 206 |
} |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
207 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
208 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
209 |
next |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
210 |
} |
50469 | 211 |
} |
212 |
||
213 |
def deflect(coords: Coordinates, level: List[Region], top_down: Boolean) |
|
214 |
: (Coordinates, Boolean) = |
|
215 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
216 |
((coords, false) /: (0 until level.length)) { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
217 |
case ((coords, moved), i) => { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
218 |
val r = level(i) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
219 |
val d = r.deflection(coords, top_down) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
220 |
val offset = { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
221 |
if (i == 0 && d <= 0) d |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
222 |
else if (i == level.length - 1 && d >= 0) d |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
223 |
else if (d < 0) { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
224 |
val prev = level(i-1) |
50474
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
225 |
(-(r.distance(coords, prev) - box_distance)) max d |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
226 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
227 |
else { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
228 |
val next = level(i+1) |
50474
6ee044e2d1a7
initial layout coordinates more like old browser;
wenzelm
parents:
50470
diff
changeset
|
229 |
(r.distance(coords, next) - box_distance) min d |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
230 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
231 |
} |
50469 | 232 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
233 |
(r.move(coords, offset), moved || (d != 0)) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
234 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
235 |
} |
50469 | 236 |
} |
237 |
||
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
238 |
val regions = levels.map(level => level.map(new Region(graph, _))) |
50469 | 239 |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
240 |
((regions, coords, true, true) /: (1 to pendulum_iterations)) { |
49746 | 241 |
case ((regions, coords, top_down, moved), _) => |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
242 |
if (moved) { |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
243 |
val (nextr, nextc, m) = iteration(regions, coords, top_down) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
244 |
(nextr, nextc, !top_down, m) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
245 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
246 |
else (regions, coords, !top_down, moved) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
247 |
}._2 |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
248 |
} |
50469 | 249 |
|
250 |
private class Region(val graph: Model.Graph, node: Key) |
|
251 |
{ |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
252 |
var nodes: List[Key] = List(node) |
50469 | 253 |
|
254 |
def left(coords: Coordinates): Double = nodes.map(coords(_)._1).min |
|
255 |
def right(coords: Coordinates): Double = nodes.map(coords(_)._1).max |
|
256 |
||
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
257 |
def distance(coords: Coordinates, to: Region): Double = |
50468 | 258 |
math.abs(left(coords) - to.left(coords)) min |
259 |
math.abs(right(coords) - to.right(coords)) |
|
50469 | 260 |
|
261 |
def deflection(coords: Coordinates, use_preds: Boolean) = |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
262 |
nodes.map(k => (coords(k)._1, |
49737
dd6fc7c9504a
avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient;
wenzelm
parents:
49565
diff
changeset
|
263 |
if (use_preds) graph.imm_preds(k).toList // FIXME iterator |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
264 |
else graph.imm_succs(k).toList)) |
50468 | 265 |
.map({ case (x, as) => as.map(coords(_)._1 - x).sum / (as.length max 1) }) |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
266 |
.sum / nodes.length |
50469 | 267 |
|
268 |
def move(coords: Coordinates, by: Double): Coordinates = |
|
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
269 |
(coords /: nodes) { |
50469 | 270 |
case (cs, node) => |
49557
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
271 |
val (x, y) = cs(node) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
272 |
cs + (node -> (x + by, y)) |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
273 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
274 |
} |
61988f9df94d
added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff
changeset
|
275 |
} |