Encoding.scala 7.42 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
2
3
4
5
package de.tum.workflows

import scalax.collection.Graph // or scalax.collection.mutable.Graph
import scalax.collection.GraphPredef._
import scalax.collection.GraphEdge._
Christian Müller's avatar
Christian Müller committed
6
import scalax.collection.edge.LDiEdge // labeled directed edge
Christian Müller's avatar
Christian Müller committed
7
8
import scalax.collection.edge.Implicits._ // shortcuts

9
import blocks._
Christian Müller's avatar
Christian Müller committed
10
11
import de.tum.workflows.foltl.FOLTL
import de.tum.workflows.foltl.FOLTL._
12
import de.tum.workflows.foltl.FormulaFunctions._
Christian Müller's avatar
Christian Müller committed
13

Christian Müller's avatar
Christian Müller committed
14
15
import com.typesafe.scalalogging._

Christian Müller's avatar
Christian Müller committed
16
import scalax.collection.edge.LBase.LEdgeImplicits
17
18
import scalax.collection.io.dot._
import implicits._
Christian Müller's avatar
Christian Müller committed
19
import Implicits._
Christian Müller's avatar
Christian Müller committed
20

Christian Müller's avatar
Christian Müller committed
21
object Encoding extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
22

23
  type WorkflowGraph = Graph[Int, LDiEdge]
Christian Müller's avatar
Christian Müller committed
24

Christian Müller's avatar
Christian Müller committed
25
26
  // Naming
  // TODO: make sure there are no clashes
Christian Müller's avatar
Christian Müller committed
27
  def nodeVar(n: Any) = Fun("n" + n, List())
Christian Müller's avatar
Christian Müller committed
28
  def choiceVar(n: Any) = "choice" + n
Christian Müller's avatar
Christian Müller committed
29
30
31

  def makeblock(b: Block, n1: Int, n2: Int, makeNode: (() => Int), makeId: (() => Block)): (List[LDiEdge[Int]]) = {

Christian Müller's avatar
Christian Müller committed
32
    b match {
ezal's avatar
ezal committed
33
34
35
36
      // single edge
      case b: SimpleBlock => {
        List((n1 ~+> n2)(b))
      }
Christian Müller's avatar
Christian Müller committed
37

Christian Müller's avatar
Christian Müller committed
38
39
40
      case Loop(steps) => {
        // add empty statement if loop ends with loop
        val adjsteps = steps.last match {
Christian Müller's avatar
Christian Müller committed
41
42
          case _: Loop  => steps :+ makeId()
          case _: Block => steps
Christian Müller's avatar
Christian Müller committed
43
44
        }
        // looping with n-1 nodes around n1
Christian Müller's avatar
Christian Müller committed
45
        val newnodes = n1 +: (0 until adjsteps.size - 1).toList.map(_ => makeNode()) :+ n1
Christian Müller's avatar
Christian Müller committed
46
47
48

        // n1 -> n2, n2 -> n3, ...
        val edgenodes = newnodes.sliding(2).toList
Christian Müller's avatar
Christian Müller committed
49
        val edges = for ((step, List(start, end)) <- adjsteps.zip(edgenodes)) yield {
Christian Müller's avatar
Christian Müller committed
50
51
52
53
          makeblock(step, start, end, makeNode, makeId)
        }
        edges.flatten :+ (n1 ~+> n2)(makeId())
      }
Christian Müller's avatar
Christian Müller committed
54

ezal's avatar
ezal committed
55
      case NondetChoice(l1, l2) => {
Christian Müller's avatar
Christian Müller committed
56
57
58
59
        // 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
60

Christian Müller's avatar
Christian Müller committed
61
        val newnodes1 = n1 +: (0 until newl1.size - 1).toList.map(_ => makeNode()) :+ n2
ezal's avatar
ezal committed
62
        val edgenodes1 = newnodes1.sliding(2).toList
Christian Müller's avatar
Christian Müller committed
63
        val edges1 = for ((step, List(start, end)) <- newl1.zip(edgenodes1)) yield {
ezal's avatar
ezal committed
64
65
66
67
68
69
70
71
          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
72
73
74
      }
    }
  }
Christian Müller's avatar
Christian Müller committed
75
76
77

  def toGraph(w: Workflow): WorkflowGraph = {

Christian Müller's avatar
Christian Müller committed
78
79
80
81
82
83
    var n1 = 0;
    def newnode() = {
      n1 = n1 + 1
      n1
    }
    def makeid() = ForallBlock(List(), List())
Christian Müller's avatar
Christian Müller committed
84
85

    val edges = (for ((step, i) <- w.steps.zipWithIndex) yield {
Christian Müller's avatar
Christian Müller committed
86
87
88
89
90
91
92
93
94
95
      if (i == w.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
    var nodes = (0 until n1).toList
Christian Müller's avatar
Christian Müller committed
96

Christian Müller's avatar
Christian Müller committed
97
98
    Graph.from(nodes, edges)
  }
Christian Müller's avatar
Christian Müller committed
99

100
  def encodeGraph(g: WorkflowGraph) = {
Christian Müller's avatar
Christian Müller committed
101
    val allnodes = for (n <- g.nodes.toList) yield {
Christian Müller's avatar
Christian Müller committed
102
103
      val list = n.outgoing.toList.map(e => nodeVar(e.to))
      Implies(nodeVar(n), Next(Or.make(list: _*)))
Christian Müller's avatar
Christian Müller committed
104
    }
105
    Globally(And.make(allnodes))
Christian Müller's avatar
Christian Müller committed
106
  }
Christian Müller's avatar
Christian Müller committed
107

108
  def encodeSanity(g: WorkflowGraph) = {
Christian Müller's avatar
Christian Müller committed
109
110
111
    val negs = for (n <- g.nodes.toList; n2 <- g.nodes.toList if n < n2) yield {
      Neg(And(nodeVar(n), nodeVar(n2)))
    }
Christian Müller's avatar
Christian Müller committed
112
113
114
115
    val nodes = for (n <- g.nodes.toList if !(n == 0)) yield {
      Neg(nodeVar(n))
    }
    And.make(nodeVar(0), And.make(nodes), Globally(And.make(negs)))
Christian Müller's avatar
Christian Müller committed
116
  }
Christian Müller's avatar
Christian Müller committed
117

118
  def encodeStmt(s: Statement, pred: Option[Formula], bind: List[Var]): (Formula, String) = {
Christian Müller's avatar
Christian Müller committed
119
120
121
122
    //    var guard = s.guard
    //    for (p <- pred) { // if pred defined
    //      guard = And(guard, p)
    //    }
123
124
    val list = List(s.guard) ++ pred.toList
    val guard = And.make(list)
Christian Müller's avatar
Christian Müller committed
125
126
127
128

    // omitted variables
    val omitted = (bind toSet) -- (s.tuple toSet)

Christian Müller's avatar
Christian Müller committed
129
    val t = s match {
Christian Müller's avatar
Christian Müller committed
130
131
132
133
      case Add(_, f, tup) if omitted.isEmpty    => Or(Fun(f, tup), guard)
      case Add(_, f, tup)                       => Or(Fun(f, tup), Exists(omitted toList, guard))
      case Remove(_, f, tup) if omitted.isEmpty => And(Fun(f, tup), Neg(guard))
      case Remove(_, f, tup)                    => And(Fun(f, tup), Exists(omitted toList, Neg(guard)))
Christian Müller's avatar
Christian Müller committed
134
    }
Christian Müller's avatar
Christian Müller committed
135

Christian Müller's avatar
Christian Müller committed
136
137
    (Forall(s.tuple, Eq(Next(Fun(s.fun, s.tuple)), t)), s.fun)
  }
Christian Müller's avatar
Christian Müller committed
138

Christian Müller's avatar
Christian Müller committed
139
140
  def encodeStaying(target: Fun) = {
    Forall(target.params, Eq(Next(target), target))
Christian Müller's avatar
Christian Müller committed
141
  }
Christian Müller's avatar
Christian Müller committed
142

Christian Müller's avatar
Christian Müller committed
143
  def encodeSem(sig: Signature, g: Graph[Int, LDiEdge]) = {
Christian Müller's avatar
Christian Müller committed
144
    val impls = for (e <- g.edges.toList) yield {
145
      val choice = e.pred.map(n => Fun(n, e.agents))
Christian Müller's avatar
Christian Müller committed
146
147
      val bound = e.agents

Christian Müller's avatar
Christian Müller committed
148
      val res = for (s <- e.steps) yield {
Christian Müller's avatar
Christian Müller committed
149
        encodeStmt(s, choice, e.agents)
Christian Müller's avatar
Christian Müller committed
150
      }
Christian Müller's avatar
Christian Müller committed
151
      val updates = res.map(_._2)
Christian Müller's avatar
Christian Müller committed
152
153
      val staying = for (f <- sig.preds if !updates.contains(f.name)) yield {
        encodeStaying(f)
Christian Müller's avatar
Christian Müller committed
154
      }
Christian Müller's avatar
Christian Müller committed
155

Christian Müller's avatar
Christian Müller committed
156
      val terms = res.map(_._1) ++ staying
157
      Implies(And(nodeVar(e.from), Next(nodeVar(e.to))), And.make(terms))
Christian Müller's avatar
Christian Müller committed
158
    }
159
    Globally(And.make(impls))
Christian Müller's avatar
Christian Müller committed
160
  }
Christian Müller's avatar
Christian Müller committed
161

Christian Müller's avatar
Christian Müller committed
162
  def encodeInitial(sig: Signature, g: Graph[Int, LDiEdge]) = {
Christian Müller's avatar
Christian Müller committed
163
    val empties = for (f <- sig.preds toList) yield {
Christian Müller's avatar
Christian Müller committed
164
      Forall(f.params, Neg(f))
Christian Müller's avatar
Christian Müller committed
165
    }
Christian Müller's avatar
Christian Müller committed
166
167
    And.make(empties)
  }
Christian Müller's avatar
Christian Müller committed
168

169
  def sanecfg(g: Graph[Int, LDiEdge]) = {
Christian Müller's avatar
Christian Müller committed
170
171
    And(encodeGraph(g), encodeSanity(g))
  }
Christian Müller's avatar
Christian Müller committed
172

173
174
  def exec(sig: Signature, g: Graph[Int, LDiEdge]) = {
    And(encodeInitial(sig, g), encodeSem(sig, g))
Christian Müller's avatar
Christian Müller committed
175
  }
Christian Müller's avatar
Christian Müller committed
176

177
178
179
  def nodepredicates(g: Graph[Int, LDiEdge]) = {
    // toSet because the initial set is mutable
    g.nodes map nodeVar toSet
Christian Müller's avatar
Christian Müller committed
180
  }
Christian Müller's avatar
Christian Müller committed
181
182
183
184

  //  def toFOLTL(w: Workflow) = {
  //    val g = toGraph(w)
  //		logger.info("Graph of w:\n" + g)
185
  //
Christian Müller's avatar
Christian Müller committed
186
187
188
189
190
191
192
193
  //    val cfg = encodeGraph(g)
  //    logger.info(s"cfg(w): $cfg")
  //    val sanity = encodeSanity(g)
  //    logger.info(s"sanity(w): $sanity")
  //    val sem = encodeSem(w.sig, g)
  //    logger.info(s"sem(w): $sem")
  //    val init = encodeInitial(w.sig, g)
  //    logger.info(s"init(w): $init")
194
  //
Christian Müller's avatar
Christian Müller committed
195
196
  //    And.make(List(cfg, sanity, sem, init))
  //  }
Christian Müller's avatar
Christian Müller committed
197
198
  
  val MAXINVLENGTH = 1200
199

Christian Müller's avatar
Christian Müller committed
200
  def toDot(g: WorkflowGraph)(labels:Map[Encoding.WorkflowGraph#NodeT, String], edges:Set[g.EdgeT]) = {
201
202
203
204
205
206
    val root = DotRootGraph(
      directed = true,
      id = Some("Invariant Labelling"))

    def edgeTransformer(innerEdge: WorkflowGraph#EdgeT): Option[(DotGraph, DotEdgeStmt)] = innerEdge.edge match {
      case LDiEdge(source, target, label) => label match {
Christian Müller's avatar
Christian Müller committed
207
        case label: SimpleBlock => {
208
          val green = edges.exists(_ == innerEdge)
Christian Müller's avatar
Christian Müller committed
209
210
211
212
213
214
          val color = List(DotAttr("color", if (green) "green" else "red"))
          
          val labelled = if (label.nonEmpty) {
            DotAttr("label", label.toString) :: color
          } else { color } 
          
215
216
217
218
219
          Some((
            root,
            DotEdgeStmt(
              source.toString,
              target.toString,
Christian Müller's avatar
Christian Müller committed
220
221
222
223
              labelled
              )
          ))
        }
224
225
      }
    }
226
227
    def nodeTransformer(innerNode: WorkflowGraph#NodeT): Option[(DotGraph, DotNodeStmt)] = {
      val str = labels(innerNode)
Christian Müller's avatar
Christian Müller committed
228
      val label = if (str.length() > MAXINVLENGTH) str.substring(0, MAXINVLENGTH) + "..." + s"(${str.length()} characters)" else str
229
230
      Some((root, DotNodeStmt(innerNode.toString, List(DotAttr("label", "Node " + innerNode + ":\n" + label)))))
    }
231
232
233

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