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

Christian Müller's avatar
Christian Müller committed
3
import scalax.collection.Graph
Christian Müller's avatar
Christian Müller committed
4
5
import scalax.collection.GraphPredef._
import scalax.collection.GraphEdge._
Christian Müller's avatar
Christian Müller committed
6
7
import scalax.collection.edge.LDiEdge
import scalax.collection.edge.Implicits._
8
import blocks._
Christian Müller's avatar
Christian Müller committed
9
10
import de.tum.workflows.foltl.FOLTL
import de.tum.workflows.foltl.FOLTL._
11
import de.tum.workflows.foltl.FormulaFunctions._
Christian Müller's avatar
Christian Müller committed
12
import com.typesafe.scalalogging._
Christian Müller's avatar
Christian Müller committed
13
import scalax.collection.edge.LBase.LEdgeImplicits
14
15
import scalax.collection.io.dot._
import implicits._
Christian Müller's avatar
Christian Müller committed
16
import Implicits._
17
import de.tum.workflows.toz3.InvProperties
Christian Müller's avatar
Christian Müller committed
18
import scalax.collection.GraphTraversal.{BreadthFirst, DepthFirst}
Christian Müller's avatar
Christian Müller committed
19

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

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

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

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

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

Christian Müller's avatar
Christian Müller committed
37
38
39
      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
40
41
          case _: Loop  => steps :+ makeId()
          case _: Block => steps
Christian Müller's avatar
Christian Müller committed
42
43
        }
        // looping with n-1 nodes around n1
Christian Müller's avatar
Christian Müller committed
44
        val newnodes = n1 +: (0 until adjsteps.size - 1).toList.map(_ => makeNode()) :+ n1
Christian Müller's avatar
Christian Müller committed
45
46
47

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

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

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

  def toGraph(w: Workflow): WorkflowGraph = {

Christian Müller's avatar
Christian Müller committed
77
78
    var n1 = 0

Christian Müller's avatar
Christian Müller committed
79
80
81
82
83
    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
      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
Christian Müller's avatar
Christian Müller committed
95
    val 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 = 800
199

200
  def toDot(g: WorkflowGraph, elaboration:Option[(InvProperties, Spec)] = None)(labels:Map[Int, 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
          val color = List(DotAttr("color", if (green) "green" else "red"))
210
211
212
213
214
215
216
217

          val elaborated = (elaboration map {
            case (prop, spec) => Preconditions.elaborate(label, spec, prop)
          }).getOrElse(List(label))
          val strlabel = elaborated.mkString("\n")

          val labelled = DotAttr("label", strlabel) :: color

218
219
220
221
222
          Some((
            root,
            DotEdgeStmt(
              source.toString,
              target.toString,
Christian Müller's avatar
Christian Müller committed
223
              labelled
224
            )
Christian Müller's avatar
Christian Müller committed
225
226
          ))
        }
227
228
      }
    }
229

230
    def nodeTransformer(innerNode: WorkflowGraph#NodeT): Option[(DotGraph, DotNodeStmt)] = {
231
      val str = labels.withDefault(d => s"$d").apply(innerNode.value)
Christian Müller's avatar
Christian Müller committed
232
      val label = if (str.length() > MAXINVLENGTH) str.substring(0, MAXINVLENGTH) + "..." + s"(${str.length()} characters)" else str
233
234
      Some((root, DotNodeStmt(innerNode.toString, List(DotAttr("label", "Node " + innerNode + ":\n" + label)))))
    }
235
236
237

    g.toDot(root, edgeTransformer, None, Some(nodeTransformer))
  }
Christian Müller's avatar
Christian Müller committed
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267

  /**
    * 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): Map[g.NodeT, Set[String]] = {

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

    // FIXME: 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
    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
  }

Christian Müller's avatar
Christian Müller committed
268
}