src/Tools/Graphview/layout.scala
 changeset 59307 b5d1b8175b8e parent 59306 cd2a0c14fe66 child 59310 7cdabe4cec33
```     1.1 --- a/src/Tools/Graphview/layout.scala	Tue Jan 06 20:12:46 2015 +0100
1.2 +++ b/src/Tools/Graphview/layout.scala	Tue Jan 06 22:34:26 2015 +0100
1.3 @@ -2,7 +2,7 @@
1.4      Author:     Markus Kaiser, TU Muenchen
1.5      Author:     Makarius
1.6
1.7 -DAG layout algorithm, according to:
1.8 +DAG layout according to:
1.9
1.10    Georg Sander, "Graph Layout through the VCG Tool", in: Graph Drawing,
1.11    DIMACS International Workshop (GD'94), Springer LNCS 894, 1995.
1.12 @@ -58,12 +58,25 @@
1.13    val empty_graph: Graph = make_graph(Nil)
1.14
1.15
1.16 +  /* vertex x coordinate */
1.17 +
1.18 +  private def vertex_left(metrics: Metrics, graph: Graph, v: Vertex): Double =
1.19 +    graph.get_node(v).x - metrics.box_width2(v)
1.20 +
1.21 +  private def vertex_right(metrics: Metrics, graph: Graph, v: Vertex): Double =
1.22 +    graph.get_node(v).x + metrics.box_width2(v)
1.23 +
1.24 +  private def move_vertex(graph: Graph, v: Vertex, dx: Double): Graph =
1.25 +    if (dx == 0.0) graph else graph.map_node(v, p => Point(p.x + dx, p.y))
1.26 +
1.27 +
1.28    /* layout */
1.29
1.30    val empty: Layout = new Layout(Metrics.default, Graph_Display.empty_graph, empty_graph)
1.31
1.32 +  val minimize_crossings_iterations = 40
1.33    val pendulum_iterations = 10
1.34 -  val minimize_crossings_iterations = 40
1.35 +  val rubberband_iterations = 10
1.36
1.37
1.38    private type Levels = Map[Vertex, Int]
1.39 @@ -128,9 +141,11 @@
1.40          })._1
1.41
1.42
1.43 -      /* pendulum layout */
1.44 +      /* pendulum/rubberband layout */
1.45
1.46 -      val output_graph = pendulum(metrics, levels_graph, levels)
1.47 +      val output_graph =
1.48 +        rubberband(metrics, levels,
1.49 +          pendulum(metrics, levels, levels_graph))
1.50
1.51        new Layout(metrics, input_graph, output_graph)
1.52      }
1.53 @@ -142,7 +157,7 @@
1.54
1.55    private type Level = List[Vertex]
1.56
1.57 -  def minimize_crossings(graph: Graph, levels: List[Level]): List[Level] =
1.58 +  private def minimize_crossings(graph: Graph, levels: List[Level]): List[Level] =
1.59    {
1.60      def resort(parent: Level, child: Level, top_down: Boolean): Level =
1.61        child.map(v => {
1.62 @@ -171,7 +186,7 @@
1.63      }._1
1.64    }
1.65
1.66 -  def level_list(levels: Levels): List[Level] =
1.67 +  private def level_list(levels: Levels): List[Level] =
1.68    {
1.69      val max_lev = (-1 /: levels) { case (m, (_, l)) => m max l }
1.70      val buckets = new Array[Level](max_lev + 1)
1.71 @@ -180,7 +195,7 @@
1.72      buckets.iterator.map(_.sorted(Vertex.Ordering)).toList
1.73    }
1.74
1.75 -  def count_crossings(graph: Graph, levels: List[Level]): Int =
1.76 +  private def count_crossings(graph: Graph, levels: List[Level]): Int =
1.77    {
1.78      def in_level(ls: List[Level]): Int = ls match {
1.79        case List(top, bot) =>
1.80 @@ -215,11 +230,9 @@
1.81      var content: List[Vertex] = List(init)
1.82
1.83      def distance(metrics: Metrics, graph: Graph, that: Region): Double =
1.84 -    {
1.85 -      val v1 = this.content.last; val x1 = graph.get_node(v1).x + metrics.box_width2(v1)
1.86 -      val v2 = that.content.head; val x2 = graph.get_node(v2).x - metrics.box_width2(v2)
1.87 -      x2 - x1 - metrics.box_gap
1.88 -    }
1.89 +      vertex_left(metrics, graph, that.content.head) -
1.90 +      vertex_right(metrics, graph, this.content.last) -
1.91 +      metrics.box_gap
1.92
1.93      def deflection(graph: Graph, top_down: Boolean): Double =
1.94        ((for (a <- content.iterator) yield {
1.95 @@ -229,13 +242,12 @@
1.96        }).sum / content.length).round.toDouble
1.97
1.98      def move(graph: Graph, dx: Double): Graph =
1.99 -      if (dx == 0.0) graph
1.100 -      else (graph /: content) { case (g, v) => g.map_node(v, p => Point(p.x + dx, p.y)) }
1.101 +      if (dx == 0.0) graph else (graph /: content)(move_vertex(_, _, dx))
1.102    }
1.103
1.104    private type Regions = List[List[Region]]
1.105
1.106 -  def pendulum(metrics: Metrics, levels_graph: Graph, levels: List[Level]): Graph =
1.107 +  private def pendulum(metrics: Metrics, levels: List[Level], levels_graph: Graph): Graph =
1.108    {
1.109      def iteration(graph: Graph, regions: Regions, top_down: Boolean): (Graph, Regions, Boolean) =
1.110      {
1.111 @@ -304,6 +316,43 @@
1.112          else (graph, regions, !top_down, moved)
1.113      }._1
1.114    }
1.115 +
1.116 +
1.117 +
1.118 +  /** rubberband method **/
1.119 +
1.120 +  private def force_weight(graph: Graph, v: Vertex): Double =
1.121 +  {
1.122 +    val preds = graph.imm_preds(v)
1.123 +    val succs = graph.imm_succs(v)
1.124 +    val n = preds.size + succs.size
1.125 +    if (n == 0) 0.0
1.126 +    else {
1.127 +      val x = graph.get_node(v).x
1.128 +      ((preds.iterator ++ succs.iterator).map(w => graph.get_node(w).x - x)).sum / n
1.129 +    }
1.130 +  }
1.131 +
1.132 +  private def rubberband(metrics: Metrics, levels: List[Level], graph: Graph): Graph =
1.133 +  {
1.134 +    val gap = metrics.box_gap
1.135 +    def left(g: Graph, v: Vertex) = vertex_left(metrics, g, v)
1.136 +    def right(g: Graph, v: Vertex) = vertex_right(metrics, g, v)
1.137 +
1.138 +    (graph /: (1 to rubberband_iterations)) { case (graph, _) =>
1.139 +      (graph /: levels) { case (graph, level) =>
1.140 +        val m = level.length - 1
1.141 +        (graph /: level.iterator.zipWithIndex) {
1.142 +          case (g, (v, i)) =>
1.143 +            val d = force_weight(g, v)
1.144 +            if (d < 0.0 && (i == 0 || right(g, level(i - 1)) + gap < left(g, v) + d) ||
1.145 +                d > 0.0 && (i == m || left(g, level(i + 1)) - gap > right(g, v) + d))
1.146 +              move_vertex(g, v, d.round.toDouble)
1.147 +            else g
1.148 +        }
1.149 +      }
1.150 +    }
1.151 +  }
1.152  }
1.153
1.154  final class Layout private(
```