TSGraphEncoding.scala 3.03 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4
package de.tum.niwo.graphs

import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.blocks._
5
import de.tum.niwo.foltl.FOLTL.{Fun, True}
Christian Müller's avatar
Christian Müller committed
6 7
import de.tum.niwo.foltl.Properties
import de.tum.niwo.graphs.WFGraphEncoding.WorkflowGraph
Christian Müller's avatar
Christian Müller committed
8
import de.tum.niwo.invariants.InvProperties
Christian Müller's avatar
Christian Müller committed
9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
import scalax.collection.Graph
import scalax.collection.GraphTraversal.BreadthFirst
import scalax.collection.edge.LBase.LEdgeImplicits
import scalax.collection.edge.LDiEdge

object TSGraphEncoding extends GraphBuilder with LazyLogging {
  type TSGraph = Graph[Int, LDiEdge]

  object EdgeImplicits extends LEdgeImplicits[SimpleTSBlock]
  import EdgeImplicits._

  def nodeVar(n: Any) = Fun("n" + n, List())

  def toBlock(e:TSGraph#EdgeT):SimpleTSBlock = e.label
  def toNumber(n:TSGraph#NodeT):Int = n.toOuter

  def toGraph(w:TransitionSystem): TSGraph = {
    def makeid() = SimpleTSBlock(List())
    toGraph(w.steps, makeid)
  }



  /**
    * Get an underapproximation of relation symbols that are sure to be untouched, i.e. empty
    *
    * @param w the graph
    */
37
  def untouchedMap(g:TSGraph, sig:Signature, props:InvProperties): Map[g.NodeT, Set[String]] = {
Christian Müller's avatar
Christian Müller committed
38 39 40 41 42

    val sourceid = 0
    val sourcenode = g.get(sourceid)
    val nodes = sourcenode.withKind(BreadthFirst).filterNot(_ == sourcenode)

Christian Müller's avatar
Christian Müller committed
43
    // TODO: this could 1. be more functional, 2. not just give up for loops
Christian Müller's avatar
Christian Müller committed
44 45 46 47 48 49 50 51 52 53 54 55 56 57 58
    var map:Map[g.NodeT, Set[String]] = Map().withDefault(_ => Set())

    // initially all untouched
    map = map.updated(g.get(sourceid), sig.preds.map(_.name))

    for (elem <- nodes) {
      // If all predecessors are known
      if (elem.diPredecessors.forall(map.contains(_))) {
        val union = elem.diPredecessors.flatMap(map(_))
        val touched = elem.incoming.flatMap(_.updating)
        map = map.updated(elem, union -- touched)
      }
    }
    map
  }
59 60 61 62 63 64 65 66

  /**
    * Get an underapproximation of the nodes where all traces are sure to be equal
    *
    * @param w the graph
    */
  def divergedMap(g:TSGraph, sig:Signature, props:InvProperties): Map[g.NodeT, Boolean] = {

Christian Müller's avatar
Christian Müller committed
67
    val anames = sig.as.map(_.name)
68

Christian Müller's avatar
Christian Müller committed
69 70 71 72 73 74
    // Node diverges locally if it has an incoming edge that touches an A that might differ
    def divergeslocally(node:g.NodeT) = {
      node.incoming.exists(stmt =>
        stmt.steps.exists(_.guard.hasSubFormula{
          // FIXME: this would be the TS correct version
          // case Fun(name, None, _) if anames.contains(name) => true
75

Christian Müller's avatar
Christian Müller committed
76 77 78 79
          // This is the WF correct version
          case f:Fun if f.isOracle => true
        }))
    }
80

Christian Müller's avatar
Christian Müller committed
81 82 83 84 85 86 87 88 89 90 91 92 93 94

    // find all nodes where divergence could happen locally
    val divergenodes = (for (node <- g.nodes
                            if divergeslocally(node)) yield {
      node
    }).toSet

    // diverge all nodes that can be reached from a local divergence
    // This is O(n^2), could be improved
    val reachablenodes = for (
      node <- divergenodes;
      reachnode <- node.withKind(BreadthFirst)
    ) yield {
      reachnode
95
    }
Christian Müller's avatar
Christian Müller committed
96 97 98

    val map = (for (node <- reachablenodes) yield node -> true).toMap
    map.withDefault(_ => false)
99
  }
Christian Müller's avatar
Christian Müller committed
100
}