products/sources/formale sprachen/Isabelle/Tools/Graphview/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: layout.scala   Sprache: Scala

Original von: Isabelle©
/*  Title:      Tools/Graphview/layout.scala
    Author:     Markus Kaiser, TU Muenchen
    Author:     Makarius

DAG layout according to:

  Georg Sander, "Graph Layout through the VCG Tool", in: Graph Drawing,
  DIMACS International Workshop (GD'94), Springer LNCS 894, 1995.

  https://doi.org/10.1007/3-540-58950-3_371
  ftp://ftp.cs.uni-sb.de/pub/graphics/vcg/doc/tr-A03-94.ps.gz
*/

package isabelle.graphview


import isabelle._


object Layout
{
  /* graph structure */

  object Vertex
  {
    object Ordering extends scala.math.Ordering[Vertex]
    {
      def compare(v1: Vertex, v2: Vertex): Int =
        (v1, v2) match {
          case (Node(a), Node(b)) => Graph_Display.Node.Ordering.compare(a, b)
          case (Dummy(a1, a2, i), Dummy(b1, b2, j)) =>
            Graph_Display.Node.Ordering.compare(a1, b1) match {
              case 0 =>
                Graph_Display.Node.Ordering.compare(a2, b2) match {
                  case 0 => i compare j
                  case ord => ord
                }
              case ord => ord
            }
          case (Node(a), Dummy(b, _, _)) =>
            Graph_Display.Node.Ordering.compare(a, b) match {
              case 0 => -1
              case ord => ord
            }
          case (Dummy(a, _, _), Node(b)) =>
            Graph_Display.Node.Ordering.compare(a, b) match {
              case 0 => 1
              case ord => ord
            }
        }
    }
  }

  sealed abstract class Vertex
  case class Node(node: Graph_Display.Node) extends Vertex
  case class Dummy(node1: Graph_Display.Node, node2: Graph_Display.Node, index: Int) extends Vertex

  sealed case class Info(
    x: Double, y: Double, width2: Double, height2: Double, lines: List[String])
  {
    def left: Double = x - width2
    def right: Double = x + width2
    def width: Double = 2 * width2
    def height: Double = 2 * height2
  }

  type Graph = isabelle.Graph[Vertex, Info]

  def make_graph(entries: List[((Vertex, Info), List[Vertex])]): Graph =
    isabelle.Graph.make(entries)(Vertex.Ordering)

  val empty_graph: Graph = make_graph(Nil)


  /* vertex x coordinate */

  private def vertex_left(graph: Graph, v: Vertex) = graph.get_node(v).left
  private def vertex_right(graph: Graph, v: Vertex) = graph.get_node(v).right

  private def move_vertex(graph: Graph, v: Vertex, dx: Double): Graph =
    if (dx == 0.0) graph else graph.map_node(v, info => info.copy(x = info.x + dx))


  /* layout */

  val empty: Layout = new Layout(Metrics.default, Graph_Display.empty_graph, empty_graph)


  private type Levels = Map[Vertex, Int]
  private val empty_levels: Levels = Map.empty

  def make(options: Options, metrics: Metrics,
    node_text: (Graph_Display.Node, XML.Body) => String,
    input_graph: Graph_Display.Graph): Layout =
  {
    if (input_graph.is_empty) empty
    else {
      /* initial graph */

      val initial_graph =
        make_graph(
          input_graph.iterator.map(
            { case (a, (content, (_, bs))) =>
                val lines = split_lines(node_text(a, content))
                val w2 = metrics.node_width2(lines)
                val h2 = metrics.node_height2(lines.length)
                ((Node(a), Info(0.0, 0.0, w2, h2, lines)), bs.toList.map(Node))
            }).toList)

      val initial_levels: Levels =
        (empty_levels /: initial_graph.topological_order) {
          case (levels, vertex) =>
            val level =
              1 + (-1 /: initial_graph.imm_preds(vertex)) { case (m, v) => m max levels(v) }
            levels + (vertex -> level)
        }


      /* graph with dummies */

      val dummy_info = Info(0.0, 0.0, metrics.dummy_size2, metrics.dummy_size2, Nil)

      val (dummy_graph, dummy_levels) =
        ((initial_graph, initial_levels) /: input_graph.edges_iterator) {
            case ((graph, levels), (node1, node2)) =>
              val v1 = Node(node1); val l1 = levels(v1)
              val v2 = Node(node2); val l2 = levels(v2)
              if (l2 - l1 <= 1) (graph, levels)
              else {
                val dummies_levels =
                  (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex }
                    yield (Dummy(node1, node2, i), l)).toList
                val dummies = dummies_levels.map(_._1)

                val levels1 = (levels /: dummies_levels)(_ + _)
                val graph1 =
                  ((graph /: dummies)(_.new_node(_, dummy_info)).del_edge(v1, v2) /:
                    (v1 :: dummies ::: List(v2)).sliding(2)) {
                      case (g, List(a, b)) => g.add_edge(a, b) }
                (graph1, levels1)
              }
          }


      /* minimize edge crossings and initial coordinates */

      val levels = minimize_crossings(options, dummy_graph, level_list(dummy_levels))

      val levels_graph: Graph =
        (((dummy_graph, 0.0) /: levels) {
          case ((graph, y), level) =>
            val num_lines = (0 /: level) { case (n, v) => n max graph.get_node(v).lines.length }
            val num_edges = (0 /: level) { case (n, v) => n + graph.imm_succs(v).size }

            val y1 = y + metrics.node_height2(num_lines)

            val graph1 =
              (((graph, 0.0) /: level) { case ((g, x), v) =>
                val info = g.get_node(v)
                val g1 = g.map_node(v, _ => info.copy(x = x + info.width2, y = y1))
                val x1 = x + info.width + metrics.gap
                (g1, x1)
              })._1

            val y2 = y1 + metrics.level_height2(num_lines, num_edges)

            (graph1, y2)
        })._1


      /* pendulum/rubberband layout */

      val output_graph =
        rubberband(options, metrics, levels,
          pendulum(options, metrics, levels, levels_graph))

      new Layout(metrics, input_graph, output_graph)
    }
  }



  /** edge crossings **/

  private type Level = List[Vertex]

  private def minimize_crossings(
    options: Options, graph: Graph, levels: List[Level]): List[Level] =
  {
    def resort(parent: Level, child: Level, top_down: Boolean): Level =
      child.map(v => {
          val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v)
          val weight =
            (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1)
          (v, weight)
      }).sortBy(_._2).map(_._1)

    ((levels, count_crossings(graph, levels)) /:
      (1 to (2 * options.int("graphview_iterations_minimize_crossings")))) {
      case ((old_levels, old_crossings), iteration) =>
        val top_down = (iteration % 2 == 1)
        val new_levels =
          if (top_down)
            (List(old_levels.head) /: old_levels.tail)((tops, bot) =>
              resort(tops.head, bot, top_down) :: tops).reverse
          else {
            val rev_old_levels = old_levels.reverse
            (List(rev_old_levels.head) /: rev_old_levels.tail)((bots, top) =>
              resort(bots.head, top, top_down) :: bots)
          }
        val new_crossings = count_crossings(graph, new_levels)
        if (new_crossings < old_crossings)
          (new_levels, new_crossings)
        else
          (old_levels, old_crossings)
    }._1
  }

  private def level_list(levels: Levels): List[Level] =
  {
    val max_lev = (-1 /: levels) { case (m, (_, l)) => m max l }
    val buckets = new Array[Level](max_lev + 1)
    for (l <- 0 to max_lev) { buckets(l) = Nil }
    for ((v, l) <- levels) { buckets(l) = v :: buckets(l) }
    buckets.iterator.map(_.sorted(Vertex.Ordering)).toList
  }

  private def count_crossings(graph: Graph, levels: List[Level]): Int =
    levels.iterator.sliding(2).map {
      case List(top, bot) =>
        top.iterator.zipWithIndex.map {
          case (outer_parent, outer_parent_index) =>
            graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)).map(outer_child =>
              (0 until outer_parent_index).iterator.map(inner_parent =>
                graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_))
                  .count(inner_child => outer_child < inner_child)).sum).sum
        }.sum
      case _ => 0
    }.sum



  /** pendulum method **/

  /*This is an auxiliary class which is used by the layout algorithm when
    calculating coordinates with the "pendulum method". A "region" is a
    group of vertices which "stick together".*/
  private class Region(val content: List[Vertex])
  {
    def distance(metrics: Metrics, graph: Graph, that: Region): Double =
      vertex_left(graph, that.content.head) -
      vertex_right(graph, this.content.last) -
      metrics.gap

    def deflection(graph: Graph, top_down: Boolean): Double =
      ((for (a <- content.iterator) yield {
        val x = graph.get_node(a).x
        val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a)
        bs.iterator.map(graph.get_node(_).x - x).sum / (bs.size max 1)
      }).sum / content.length).round.toDouble

    def move(graph: Graph, dx: Double): Graph =
      if (dx == 0.0) graph else (graph /: content)(move_vertex(_, _, dx))

    def combine(that: Region): Region = new Region(content ::: that.content)
  }

  private def pendulum(
    options: Options, metrics: Metrics, levels: List[Level], levels_graph: Graph): Graph =
  {
    def combine_regions(graph: Graph, top_down: Boolean, level: List[Region]): List[Region] =
      level match {
        case r1 :: rest =>
          val rest1 = combine_regions(graph, top_down, rest)
          rest1 match {
            case r2 :: rest2 =>
              val d1 = r1.deflection(graph, top_down)
              val d2 = r2.deflection(graph, top_down)
              if (// Do regions touch?
                  r1.distance(metrics, graph, r2) <= 0.0 &&
                  // Do they influence each other?
                  (d1 <= 0.0 && d2 < d1 || d2 > 0.0 && d1 > d2 || d1 > 0.0 && d2 < 0.0))
                r1.combine(r2) :: rest2
              else r1 :: rest1
            case _ => r1 :: rest1
          }
        case _ => level
      }

    def deflect(level: List[Region], top_down: Boolean, graph: Graph): (Graph, Boolean) =
    {
      ((graph, false) /: level.indices) {
        case ((graph, moved), i) =>
          val r = level(i)
          val d = r.deflection(graph, top_down)
          val dx =
            if (d < 0.0 && i > 0)
              - (level(i - 1).distance(metrics, graph, r) min (- d))
            else if (d >= 0.0 && i < level.length - 1)
              r.distance(metrics, graph, level(i + 1)) min d
            else d
          (r.move(graph, dx), moved || d != 0.0)
      }
    }

    val initial_regions = levels.map(level => level.map(l => new Region(List(l))))

    ((levels_graph, initial_regions, true) /:
      (1 to (2 * options.int("graphview_iterations_pendulum")))) {
      case ((graph, regions, moved), iteration) =>
        val top_down = (iteration % 2 == 1)
        if (moved) {
          val (graph1, regions1, moved1) =
            ((graph, List.empty[List[Region]], false) /:
              (if (top_down) regions else regions.reverse)) { case ((graph, tops, moved), bot) =>
                val bot1 = combine_regions(graph, top_down, bot)
                val (graph1, moved1) = deflect(bot1, top_down, graph)
                (graph1, bot1 :: tops, moved || moved1)
            }
          (graph1, regions1.reverse, moved1)
        }
        else (graph, regions, moved)
    }._1
  }



  /** rubberband method **/

  private def force_weight(graph: Graph, v: Vertex): Double =
  {
    val preds = graph.imm_preds(v)
    val succs = graph.imm_succs(v)
    val n = preds.size + succs.size
    if (n == 0) 0.0
    else {
      val x = graph.get_node(v).x
      ((preds.iterator ++ succs.iterator).map(w => graph.get_node(w).x - x)).sum / n
    }
  }

  private def rubberband(
    options: Options, metrics: Metrics, levels: List[Level], graph: Graph): Graph =
  {
    val gap = metrics.gap

    (graph /: (1 to (2 * options.int("graphview_iterations_rubberband")))) { case (graph, _) =>
      (graph /: levels) { case (graph, level) =>
        val m = level.length - 1
        (graph /: level.iterator.zipWithIndex) {
          case (g, (v, i)) =>
            val d = force_weight(g, v)
            if (d < 0.0 && (i == 0 || vertex_right(g, level(i - 1)) + gap < vertex_left(g, v) + d) ||
                d > 0.0 && (i == m || vertex_left(g, level(i + 1)) - gap > vertex_right(g, v) + d))
              move_vertex(g, v, d.round.toDouble)
            else g
        }
      }
    }
  }
}

final class Layout private(
  val metrics: Metrics,
  val input_graph: Graph_Display.Graph,
  val output_graph: Layout.Graph)
{
  /* vertex coordinates */

  def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Layout =
  {
    if ((dx == 0.0 && dy == 0.0) || !output_graph.defined(v)) this
    else {
      val output_graph1 =
        output_graph.map_node(v, info => info.copy(x = info.x + dx, y = info.y + dy))
      new Layout(metrics, input_graph, output_graph1)
    }
  }


  /* regular nodes */

  def get_node(node: Graph_Display.Node): Layout.Info =
    output_graph.get_node(Layout.Node(node))

  def nodes_iterator: Iterator[Layout.Info] =
    for ((_: Layout.Node, (info, _)) <- output_graph.iterator) yield info


  /* dummies */

  def dummies_iterator: Iterator[Layout.Info] =
    for ((_: Layout.Dummy, (info, _)) <- output_graph.iterator) yield info

  def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Info] =
    new Iterator[Layout.Info] {
      private var index = 0
      def hasNext: Boolean = output_graph.defined(Layout.Dummy(edge._1, edge._2, index))
      def next: Layout.Info =
      {
        val info = output_graph.get_node(Layout.Dummy(edge._1, edge._2, index))
        index += 1
        info
      }
    }
}


¤ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ¤



Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff