GraphBuilder.scala 4.46 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
package de.tum.niwo.graphs
Christian Müller's avatar
Christian Müller committed
2

Christian Müller's avatar
Christian Müller committed
3 4 5
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.blocks._
import de.tum.niwo.graphs.WFGraphEncoding.MAXINVLENGTH
Christian Müller's avatar
Christian Müller committed
6
import scalax.collection.Graph
Christian Müller's avatar
Christian Müller committed
7
import de.tum.niwo.Implicits._
Christian Müller's avatar
Christian Müller committed
8 9
import scalax.collection.edge.LDiEdge
import scalax.collection.edge.Implicits._
10
import scalax.collection.io.dot._
Christian Müller's avatar
Christian Müller committed
11
import scalax.collection.io.dot.implicits._
Christian Müller's avatar
Christian Müller committed
12

Christian Müller's avatar
Christian Müller committed
13
trait GraphBuilder extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
14

Christian Müller's avatar
Christian Müller committed
15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52
  val MAXINVLENGTH = 800


  def toGraph[BL <: Block](steps:List[_ <: Block], makeid: () => BL): Graph[Int, LDiEdge] = {

    var n1 = 0

    def newnode() = {
      n1 = n1 + 1
      n1
    }

    val edges = (for ((step, i) <- steps.zipWithIndex) yield {
      if (i == 0 && step.isInstanceOf[Loop[_, _]]) {
        logger.info("Found loop in the initial step")
        val n = n1
        val n2 = newnode()
        val n3 = newnode()
        val edges = makeblock(step, n2, n3, newnode, makeid)
        val e2 = edges :+ (n ~+> n2)(makeid())

        val e3 = if (i == steps.size - 1) {
          e2 :+ (n3 ~+> n3)(makeid())
        } else e2
        e3
      } else if (i == steps.size - 1) {
        val n = n1
        val n2 = newnode()
        val edges = makeblock(step, n, n2, newnode, makeid)
        edges :+ (n2 ~+> n2)(makeid())
      } else {
        makeblock(step, n1, newnode(), newnode, makeid)
      }
    }).flatten
    val nodes = (0 until n1).toList

    Graph.from(nodes, edges)
  }
Christian Müller's avatar
Christian Müller committed
53 54


55 56

  def makeblock[BL <: Block](b: BL, n1: Int, n2: Int, makeNode: () => Int, makeId: () => BL): List[LDiEdge[Int]] = {
Christian Müller's avatar
Christian Müller committed
57

Christian Müller's avatar
Christian Müller committed
58
    b match {
ezal's avatar
ezal committed
59
      // single edge
60
      case b: SimpleBlock[_, _] => {
ezal's avatar
ezal committed
61 62
        List((n1 ~+> n2)(b))
      }
Christian Müller's avatar
Christian Müller committed
63

64
      case l:Loop[_, _] => {
Christian Müller's avatar
Christian Müller committed
65
        // add empty statement if loop ends with loop
66 67 68
        val adjsteps = l.steps.last match {
          case _: Loop[_, _]  => l.steps :+ makeId()
          case _ => l.steps
Christian Müller's avatar
Christian Müller committed
69 70
        }
        // looping with n-1 nodes around n1
Christian Müller's avatar
Christian Müller committed
71
        val newnodes = n1 +: (0 until adjsteps.size - 1).toList.map(_ => makeNode()) :+ n1
Christian Müller's avatar
Christian Müller committed
72 73 74

        // n1 -> n2, n2 -> n3, ...
        val edgenodes = newnodes.sliding(2).toList
Christian Müller's avatar
Christian Müller committed
75
        val edges = for ((step, List(start, end)) <- adjsteps.zip(edgenodes)) yield {
Christian Müller's avatar
Christian Müller committed
76 77 78 79
          makeblock(step, start, end, makeNode, makeId)
        }
        edges.flatten :+ (n1 ~+> n2)(makeId())
      }
Christian Müller's avatar
Christian Müller committed
80

81 82 83
      case nd:NondetChoice[_, _] => {
        val l1 = nd.left
        val l2 = nd.right
Christian Müller's avatar
Christian Müller committed
84 85 86 87
        // make sure that at least one of the two branches has one node, so they will never build 2 edges between the same node
        val newl1 = if (l1.length == l2.length && l1.length == 1) {
          l1 :+ makeId()
        } else l1
Christian Müller's avatar
Christian Müller committed
88

Christian Müller's avatar
Christian Müller committed
89
        val newnodes1 = n1 +: (0 until newl1.size - 1).toList.map(_ => makeNode()) :+ n2
ezal's avatar
ezal committed
90
        val edgenodes1 = newnodes1.sliding(2).toList
Christian Müller's avatar
Christian Müller committed
91
        val edges1 = for ((step, List(start, end)) <- newl1.zip(edgenodes1)) yield {
ezal's avatar
ezal committed
92 93 94 95 96 97 98 99
          makeblock(step, start, end, makeNode, makeId)
        }
        val newnodes2 = n1 +: (0 until l2.size - 1).toList.map(_ => makeNode()) :+ n2
        val edgenodes2 = newnodes2.sliding(2).toList
        val edges2 = for ((step, List(start, end)) <- l2.zip(edgenodes2)) yield {
          makeblock(step, start, end, makeNode, makeId)
        }
        edges1.flatten ++ edges2.flatten
Christian Müller's avatar
Christian Müller committed
100 101 102
      }
    }
  }
Christian Müller's avatar
Christian Müller committed
103

Christian Müller's avatar
Christian Müller committed
104
  def toDot(g: Graph[Int, LDiEdge])(labels:Map[Int, String], edges:Set[g.EdgeT]) = {
105 106
    val root = DotRootGraph(
      directed = true,
107 108
      id = Some("Invariant Labelling")
    )
109

Christian Müller's avatar
Christian Müller committed
110
    def edgeTransformer(innerEdge: Graph[Int, LDiEdge]#EdgeT): Option[(DotGraph, DotEdgeStmt)] = innerEdge.edge match {
111
      case LDiEdge(source, target, label) => label match {
Christian Müller's avatar
Christian Müller committed
112
        case label: SimpleBlock[_, _] => {
113
          val green = edges.exists(_ == innerEdge)
Christian Müller's avatar
Christian Müller committed
114
          val color = List(DotAttr("color", if (green) "green" else "red"))
115

Christian Müller's avatar
Christian Müller committed
116
          val labelled = DotAttr("label", label.toString) :: color
117

118 119 120 121 122
          Some((
            root,
            DotEdgeStmt(
              source.toString,
              target.toString,
Christian Müller's avatar
Christian Müller committed
123
              labelled
124
            )
Christian Müller's avatar
Christian Müller committed
125 126
          ))
        }
127 128
      }
    }
129

Christian Müller's avatar
Christian Müller committed
130
    def nodeTransformer(innerNode: Graph[Int, LDiEdge]#NodeT): Option[(DotGraph, DotNodeStmt)] = {
131
      val str = labels.withDefault(d => s"$d").apply(innerNode.value)
Christian Müller's avatar
Christian Müller committed
132
      val label = if (str.length() > MAXINVLENGTH) str.substring(0, MAXINVLENGTH) + "..." + s"(${str.length()} characters)" else str
133 134
      Some((root, DotNodeStmt(innerNode.toString, List(DotAttr("label", "Node " + innerNode + ":\n" + label)))))
    }
135 136 137

    g.toDot(root, edgeTransformer, None, Some(nodeTransformer))
  }
Christian Müller's avatar
Christian Müller committed
138
}