src/Tools/Graphview/layout.scala
changeset 73606 d8a0e996614b
parent 73591 2dd1fd9112d9
equal deleted inserted replaced
73605:78aa7846e91f 73606:d8a0e996614b
   106                 val h2 = metrics.node_height2(lines.length)
   106                 val h2 = metrics.node_height2(lines.length)
   107                 ((Node(a), Info(0.0, 0.0, w2, h2, lines)), bs.toList.map(Node))
   107                 ((Node(a), Info(0.0, 0.0, w2, h2, lines)), bs.toList.map(Node))
   108             }).toList)
   108             }).toList)
   109 
   109 
   110       val initial_levels: Levels =
   110       val initial_levels: Levels =
   111         (empty_levels /: initial_graph.topological_order) {
   111         initial_graph.topological_order.foldLeft(empty_levels) {
   112           case (levels, vertex) =>
   112           case (levels, vertex) =>
   113             val level =
   113             val level =
   114               1 + (-1 /: initial_graph.imm_preds(vertex)) { case (m, v) => m max levels(v) }
   114               1 + initial_graph.imm_preds(vertex).foldLeft(-1) { case (m, v) => m max levels(v) }
   115             levels + (vertex -> level)
   115             levels + (vertex -> level)
   116         }
   116         }
   117 
   117 
   118 
   118 
   119       /* graph with dummies */
   119       /* graph with dummies */
   120 
   120 
   121       val dummy_info = Info(0.0, 0.0, metrics.dummy_size2, metrics.dummy_size2, Nil)
   121       val dummy_info = Info(0.0, 0.0, metrics.dummy_size2, metrics.dummy_size2, Nil)
   122 
   122 
   123       val (dummy_graph, dummy_levels) =
   123       val (dummy_graph, dummy_levels) =
   124         ((initial_graph, initial_levels) /: input_graph.edges_iterator) {
   124         input_graph.edges_iterator.foldLeft((initial_graph, initial_levels)) {
   125             case ((graph, levels), (node1, node2)) =>
   125           case ((graph, levels), (node1, node2)) =>
   126               val v1 = Node(node1); val l1 = levels(v1)
   126             val v1 = Node(node1); val l1 = levels(v1)
   127               val v2 = Node(node2); val l2 = levels(v2)
   127             val v2 = Node(node2); val l2 = levels(v2)
   128               if (l2 - l1 <= 1) (graph, levels)
   128             if (l2 - l1 <= 1) (graph, levels)
   129               else {
   129             else {
   130                 val dummies_levels =
   130               val dummies_levels =
   131                   (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex }
   131                 (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex }
   132                     yield (Dummy(node1, node2, i), l)).toList
   132                   yield (Dummy(node1, node2, i), l)).toList
   133                 val dummies = dummies_levels.map(_._1)
   133               val dummies = dummies_levels.map(_._1)
   134 
   134 
   135                 val levels1 = (levels /: dummies_levels)(_ + _)
   135               val levels1 = dummies_levels.foldLeft(levels)(_ + _)
   136                 val graph1 =
   136               val graph1 =
   137                   ((graph /: dummies)(_.new_node(_, dummy_info)).del_edge(v1, v2) /:
   137                 (v1 :: dummies ::: List(v2)).sliding(2).
   138                     (v1 :: dummies ::: List(v2)).sliding(2)) {
   138                   foldLeft(dummies.foldLeft(graph)(_.new_node(_, dummy_info)).del_edge(v1, v2)) {
   139                       case (g, List(a, b)) => g.add_edge(a, b) }
   139                     case (g, List(a, b)) => g.add_edge(a, b)
   140                 (graph1, levels1)
   140                   }
   141               }
   141               (graph1, levels1)
   142           }
   142             }
       
   143         }
   143 
   144 
   144 
   145 
   145       /* minimize edge crossings and initial coordinates */
   146       /* minimize edge crossings and initial coordinates */
   146 
   147 
   147       val levels = minimize_crossings(options, dummy_graph, level_list(dummy_levels))
   148       val levels = minimize_crossings(options, dummy_graph, level_list(dummy_levels))
   148 
   149 
   149       val levels_graph: Graph =
   150       val levels_graph: Graph =
   150         (((dummy_graph, 0.0) /: levels) {
   151         levels.foldLeft((dummy_graph, 0.0)) {
   151           case ((graph, y), level) =>
   152           case ((graph, y), level) =>
   152             val num_lines = (0 /: level) { case (n, v) => n max graph.get_node(v).lines.length }
   153             val num_lines = level.foldLeft(0) { case (n, v) => n max graph.get_node(v).lines.length }
   153             val num_edges = (0 /: level) { case (n, v) => n + graph.imm_succs(v).size }
   154             val num_edges = level.foldLeft(0) { case (n, v) => n + graph.imm_succs(v).size }
   154 
   155 
   155             val y1 = y + metrics.node_height2(num_lines)
   156             val y1 = y + metrics.node_height2(num_lines)
   156 
   157 
   157             val graph1 =
   158             val graph1 =
   158               (((graph, 0.0) /: level) { case ((g, x), v) =>
   159               level.foldLeft((graph, 0.0)) {
   159                 val info = g.get_node(v)
   160                 case ((g, x), v) =>
   160                 val g1 = g.map_node(v, _ => info.copy(x = x + info.width2, y = y1))
   161                   val info = g.get_node(v)
   161                 val x1 = x + info.width + metrics.gap
   162                   val g1 = g.map_node(v, _ => info.copy(x = x + info.width2, y = y1))
   162                 (g1, x1)
   163                   val x1 = x + info.width + metrics.gap
   163               })._1
   164                   (g1, x1)
       
   165               }._1
   164 
   166 
   165             val y2 = y1 + metrics.level_height2(num_lines, num_edges)
   167             val y2 = y1 + metrics.level_height2(num_lines, num_edges)
   166 
   168 
   167             (graph1, y2)
   169             (graph1, y2)
   168         })._1
   170         }._1
   169 
   171 
   170 
   172 
   171       /* pendulum/rubberband layout */
   173       /* pendulum/rubberband layout */
   172 
   174 
   173       val output_graph =
   175       val output_graph =
   186 
   188 
   187   private def minimize_crossings(
   189   private def minimize_crossings(
   188     options: Options, graph: Graph, levels: List[Level]): List[Level] =
   190     options: Options, graph: Graph, levels: List[Level]): List[Level] =
   189   {
   191   {
   190     def resort(parent: Level, child: Level, top_down: Boolean): Level =
   192     def resort(parent: Level, child: Level, top_down: Boolean): Level =
   191       child.map(v => {
   193       child.map(v =>
   192           val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v)
   194       {
   193           val weight =
   195         val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v)
   194             (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1)
   196         val weight =
   195           (v, weight)
   197           ps.foldLeft(0.0) { case (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1)
       
   198         (v, weight)
   196       }).sortBy(_._2).map(_._1)
   199       }).sortBy(_._2).map(_._1)
   197 
   200 
   198     ((levels, count_crossings(graph, levels)) /:
   201     (1 to (2 * options.int("graphview_iterations_minimize_crossings"))).
   199       (1 to (2 * options.int("graphview_iterations_minimize_crossings")))) {
   202       foldLeft((levels, count_crossings(graph, levels))) {
   200       case ((old_levels, old_crossings), iteration) =>
   203         case ((old_levels, old_crossings), iteration) =>
   201         val top_down = (iteration % 2 == 1)
   204           val top_down = (iteration % 2 == 1)
   202         val new_levels =
   205           val new_levels =
   203           if (top_down)
   206             if (top_down) {
   204             (List(old_levels.head) /: old_levels.tail)((tops, bot) =>
   207               old_levels.tail.foldLeft(List(old_levels.head)) {
   205               resort(tops.head, bot, top_down) :: tops).reverse
   208                 case (tops, bot) => resort(tops.head, bot, top_down) :: tops
   206           else {
   209               }.reverse
   207             val rev_old_levels = old_levels.reverse
   210             }
   208             (List(rev_old_levels.head) /: rev_old_levels.tail)((bots, top) =>
   211             else {
   209               resort(bots.head, top, top_down) :: bots)
   212               val rev_old_levels = old_levels.reverse
   210           }
   213               rev_old_levels.tail.foldLeft(List(rev_old_levels.head)) {
   211         val new_crossings = count_crossings(graph, new_levels)
   214                 case (bots, top) => resort(bots.head, top, top_down) :: bots
   212         if (new_crossings < old_crossings)
   215               }
   213           (new_levels, new_crossings)
   216             }
   214         else
   217           val new_crossings = count_crossings(graph, new_levels)
   215           (old_levels, old_crossings)
   218           if (new_crossings < old_crossings)
   216     }._1
   219             (new_levels, new_crossings)
       
   220           else
       
   221             (old_levels, old_crossings)
       
   222       }._1
   217   }
   223   }
   218 
   224 
   219   private def level_list(levels: Levels): List[Level] =
   225   private def level_list(levels: Levels): List[Level] =
   220   {
   226   {
   221     val max_lev = (-1 /: levels) { case (m, (_, l)) => m max l }
   227     val max_lev = levels.foldLeft(-1) { case (m, (_, l)) => m max l }
   222     val buckets = new Array[Level](max_lev + 1)
   228     val buckets = new Array[Level](max_lev + 1)
   223     for (l <- 0 to max_lev) { buckets(l) = Nil }
   229     for (l <- 0 to max_lev) { buckets(l) = Nil }
   224     for ((v, l) <- levels) { buckets(l) = v :: buckets(l) }
   230     for ((v, l) <- levels) { buckets(l) = v :: buckets(l) }
   225     buckets.iterator.map(_.sorted(Vertex.Ordering)).toList
   231     buckets.iterator.map(_.sorted(Vertex.Ordering)).toList
   226   }
   232   }
   258         val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a)
   264         val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a)
   259         bs.iterator.map(graph.get_node(_).x - x).sum / (bs.size max 1)
   265         bs.iterator.map(graph.get_node(_).x - x).sum / (bs.size max 1)
   260       }).sum / content.length).round.toDouble
   266       }).sum / content.length).round.toDouble
   261 
   267 
   262     def move(graph: Graph, dx: Double): Graph =
   268     def move(graph: Graph, dx: Double): Graph =
   263       if (dx == 0.0) graph else (graph /: content)(move_vertex(_, _, dx))
   269       if (dx == 0.0) graph else content.foldLeft(graph)(move_vertex(_, _, dx))
   264 
   270 
   265     def combine(that: Region): Region = new Region(content ::: that.content)
   271     def combine(that: Region): Region = new Region(content ::: that.content)
   266   }
   272   }
   267 
   273 
   268   private def pendulum(
   274   private def pendulum(
   287         case _ => level
   293         case _ => level
   288       }
   294       }
   289 
   295 
   290     def deflect(level: List[Region], top_down: Boolean, graph: Graph): (Graph, Boolean) =
   296     def deflect(level: List[Region], top_down: Boolean, graph: Graph): (Graph, Boolean) =
   291     {
   297     {
   292       ((graph, false) /: level.indices) {
   298       level.indices.foldLeft((graph, false)) {
   293         case ((graph, moved), i) =>
   299         case ((graph, moved), i) =>
   294           val r = level(i)
   300           val r = level(i)
   295           val d = r.deflection(graph, top_down)
   301           val d = r.deflection(graph, top_down)
   296           val dx =
   302           val dx =
   297             if (d < 0.0 && i > 0) {
   303             if (d < 0.0 && i > 0) {
   305       }
   311       }
   306     }
   312     }
   307 
   313 
   308     val initial_regions = levels.map(level => level.map(l => new Region(List(l))))
   314     val initial_regions = levels.map(level => level.map(l => new Region(List(l))))
   309 
   315 
   310     ((levels_graph, initial_regions, true) /:
   316     (1 to (2 * options.int("graphview_iterations_pendulum"))).
   311       (1 to (2 * options.int("graphview_iterations_pendulum")))) {
   317       foldLeft((levels_graph, initial_regions, true)) {
   312       case ((graph, regions, moved), iteration) =>
   318         case ((graph, regions, moved), iteration) =>
   313         val top_down = (iteration % 2 == 1)
   319           val top_down = (iteration % 2 == 1)
   314         if (moved) {
   320           if (moved) {
   315           val (graph1, regions1, moved1) =
   321             val (graph1, regions1, moved1) =
   316             ((graph, List.empty[List[Region]], false) /:
   322               (if (top_down) regions else regions.reverse).
   317               (if (top_down) regions else regions.reverse)) { case ((graph, tops, moved), bot) =>
   323                 foldLeft((graph, List.empty[List[Region]], false)) {
   318                 val bot1 = combine_regions(graph, top_down, bot)
   324                   case ((graph, tops, moved), bot) =>
   319                 val (graph1, moved1) = deflect(bot1, top_down, graph)
   325                     val bot1 = combine_regions(graph, top_down, bot)
   320                 (graph1, bot1 :: tops, moved || moved1)
   326                     val (graph1, moved1) = deflect(bot1, top_down, graph)
   321             }
   327                     (graph1, bot1 :: tops, moved || moved1)
   322           (graph1, regions1.reverse, moved1)
   328                 }
   323         }
   329             (graph1, regions1.reverse, moved1)
   324         else (graph, regions, moved)
   330           }
   325     }._1
   331           else (graph, regions, moved)
       
   332       }._1
   326   }
   333   }
   327 
   334 
   328 
   335 
   329 
   336 
   330   /** rubberband method **/
   337   /** rubberband method **/
   344   private def rubberband(
   351   private def rubberband(
   345     options: Options, metrics: Metrics, levels: List[Level], graph: Graph): Graph =
   352     options: Options, metrics: Metrics, levels: List[Level], graph: Graph): Graph =
   346   {
   353   {
   347     val gap = metrics.gap
   354     val gap = metrics.gap
   348 
   355 
   349     (graph /: (1 to (2 * options.int("graphview_iterations_rubberband")))) { case (graph, _) =>
   356     (1 to (2 * options.int("graphview_iterations_rubberband"))).foldLeft(graph) {
   350       (graph /: levels) { case (graph, level) =>
   357       case (graph, _) =>
   351         val m = level.length - 1
   358         levels.foldLeft(graph) { case (graph, level) =>
   352         (graph /: level.iterator.zipWithIndex) {
   359           val m = level.length - 1
   353           case (g, (v, i)) =>
   360           level.iterator.zipWithIndex.foldLeft(graph) {
   354             val d = force_weight(g, v)
   361             case (g, (v, i)) =>
   355             if (d < 0.0 && (i == 0 || vertex_right(g, level(i - 1)) + gap < vertex_left(g, v) + d) ||
   362               val d = force_weight(g, v)
   356                 d > 0.0 && (i == m || vertex_left(g, level(i + 1)) - gap > vertex_right(g, v) + d))
   363               if (d < 0.0 && (i == 0 || vertex_right(g, level(i - 1)) + gap < vertex_left(g, v) + d) ||
   357               move_vertex(g, v, d.round.toDouble)
   364                   d > 0.0 && (i == m || vertex_left(g, level(i + 1)) - gap > vertex_right(g, v) + d))
   358             else g
   365                 move_vertex(g, v, d.round.toDouble)
       
   366               else g
       
   367           }
   359         }
   368         }
   360       }
       
   361     }
   369     }
   362   }
   370   }
   363 }
   371 }
   364 
   372 
   365 final class Layout private(
   373 final class Layout private(