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

import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL.Fun
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 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
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
    */
  def untouchedMap(g:WorkflowGraph, sig:Signature, props:InvProperties): Map[g.NodeT, Set[String]] = {

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

    // this could 1. be more functional, 2. not just give up for loops
    var map:Map[g.NodeT, Set[String]] = Map().withDefault(_ => Set())

    // initially all untouched
    // TODO: maybe introduce informedness as sig.pred?
    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
  }
}