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(