WFGraphEncoding.scala 2.17 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4 5 6 7 8 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 61 62 63 64 65 66 67 68 69 70 71
package de.tum.niwo.graphs

import com.typesafe.scalalogging._
import de.tum.niwo.Preconditions
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.Properties
import de.tum.niwo.toz3.InvProperties
import scalax.collection.Graph
import scalax.collection.GraphTraversal.BreadthFirst
import scalax.collection.edge.LDiEdge
import de.tum.niwo.Implicits._
import scalax.collection.edge.LBase.LEdgeImplicits

object WFGraphEncoding extends GraphBuilder with LazyLogging {

  type WorkflowGraph = Graph[Int, LDiEdge]

  object EdgeImplicits extends LEdgeImplicits[SimpleWFBlock[_]]
  import EdgeImplicits._

  // Naming
  // TODO: make sure there are no clashes
  def nodeVar(n: Any) = Fun("n" + n, List())
//  def choiceVar(n: Any) = "choice" + n

  def toBlock(e:WorkflowGraph#EdgeT):SimpleWFBlock[_] = e.label
  def toNumber(n:WorkflowGraph#NodeT):Int = n.toOuter


//  type TSGraph = Graph[Int, LDiEdge]

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

  def toGraph(w:Workflow): WorkflowGraph = {
    def makeid() = ForallWFBlock(List(), List())
    toGraph(w.steps, makeid)
  }


  // FIXME: remove this when conversion is done
  /**
    * 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) ++ Some(Properties.INFNAME) )

    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
  }
}