InvariantChecker.scala 7.46 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
package de.tum.niwo.invariants
Christian Müller's avatar
Christian Müller committed
2

Christian Müller's avatar
Christian Müller committed
3
import com.microsoft.z3.{Solver, Status}
Christian Müller's avatar
Christian Müller committed
4
import com.typesafe.scalalogging.LazyLogging
5 6 7
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.FormulaFunctions
Christian Müller's avatar
Christian Müller committed
8
import de.tum.niwo.graphs.WFGraphEncoding.WorkflowGraph
Christian Müller's avatar
Christian Müller committed
9 10 11 12 13
import de.tum.niwo.graphs.{TSGraphEncoding, WFGraphEncoding}
import de.tum.niwo.toz3.{Z3BSFO, Z3FOEncoding}
import de.tum.niwo.{Preconditions, Utils}

import scala.annotation.tailrec
Christian Müller's avatar
Christian Müller committed
14

Christian Müller's avatar
Christian Müller committed
15
case class InvProperties(stubborn:Boolean, eliminateA:Boolean, eliminateB:Boolean = false) { }
Christian Müller's avatar
Christian Müller committed
16
object InvProperties {
Christian Müller's avatar
Christian Müller committed
17 18 19 20 21
  val DEFAULT = InvProperties(
    stubborn = true,
    eliminateA = true,
    eliminateB = true
  )
Christian Müller's avatar
Christian Müller committed
22 23
}

Christian Müller's avatar
Christian Müller committed
24
object InvariantChecker extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
25 26


Christian Müller's avatar
Christian Müller committed
27
  def checkBlockInvariant(spec: InvariantSpec, b: SimpleTSBlock, pre: Formula, post: Formula, properties:InvProperties, untouched:Set[String]): ((Status, Solver), Formula) = {
28
    val precond = Preconditions.abstractedPrecondition(post, b, spec, properties, untouched)
29

Christian Müller's avatar
Christian Müller committed
30
    // pre is universal, spec.always is AE
31
    val f = Implies(And(pre, spec.axioms), precond)
32 33 34

    logger.info(s"Checking invariant implication for $b")

35
    (Z3BSFO.checkAE(f.simplify), precond)
36
  }
37

Christian Müller's avatar
Christian Müller committed
38
  def checkInvariantFPLabelling(spec: InvariantSpec, properties:InvProperties) = {
Christian Müller's avatar
Christian Müller committed
39
    val graph = TSGraphEncoding.toGraph(spec.ts)
40 41 42
    type Node = graph.NodeT
    type Edge = graph.EdgeT

Christian Müller's avatar
fix  
Christian Müller committed
43
    val untouched = TSGraphEncoding.untouchedMap(graph, spec.ts.sig, properties)
Christian Müller's avatar
Christian Müller committed
44

45
    @tailrec
Christian Müller's avatar
Christian Müller committed
46
    def checkInvariantRec(labellist: List[Map[Int, Formula]], provenlist: List[Set[Edge]]): (Boolean, List[Map[Int, Formula]], List[Set[Edge]]) = {
47

48 49
      val labels = labellist.head
      val proven = provenlist.head
50
      // check if done, i.e. all edges proven
Christian Müller's avatar
Christian Müller committed
51
      val toProve = graph.edges -- proven
52
      if (toProve.isEmpty) {
Christian Müller's avatar
Christian Müller committed
53
        logger.info("Everything proven. Terminating.")
54
        (true, labellist, provenlist)
55 56 57
      } else {

        // take one edge to prove
58 59 60 61
//        val next = toProve.head
        // take the edge with a minimum of following unproven edges excluding selfloops
//        val next = toProve.minBy(edge => ((edge.target.outgoing.filter(t => t.target != t.source) -- proven).size))
        // take the edge with maximum source node first
Christian Müller's avatar
Christian Müller committed
62
        val nextEdge = toProve.maxBy(edge => edge.source.value)
63
        
64
        // try to prove
Christian Müller's avatar
Christian Müller committed
65 66
        val pre = labels(nextEdge.from)
        val post = labels(nextEdge.to)
Christian Müller's avatar
Christian Müller committed
67 68 69 70 71 72 73 74
        val ((status, solver), strengthened) =
          checkBlockInvariant(
            spec,
            TSGraphEncoding.toBlock(nextEdge),
            pre,
            post,
            properties,
            untouched(nextEdge.from))
75

Christian Müller's avatar
Christian Müller committed
76 77
        val from = TSGraphEncoding.toNumber(nextEdge._1)
        val to = TSGraphEncoding.toNumber(nextEdge._2)
78 79 80

        if (status == Status.UNSATISFIABLE) {
          // Negation of implication unsat
Christian Müller's avatar
Christian Müller committed
81
          // --> safe, continue with larger proven set.
82 83

          logger.info(s"Proven inductiveness for ($from -> $to).")
Christian Müller's avatar
Christian Müller committed
84
          checkInvariantRec(labels :: labellist, (proven + nextEdge) :: provenlist)
85 86 87 88
        } else {
          // Negation of implication sat
          // --> unsafe, relabel incoming node, invalidate all proven guarantees for that node
          // check if relabelled invariant still satisfiable
Christian Müller's avatar
Christian Müller committed
89
          // never relabel initial node
90
          logger.info(s"Invariant not inductive, strengthening.")
Christian Müller's avatar
Christian Müller committed
91

92
          val newinv = And(labels(from), strengthened).simplify
Christian Müller's avatar
Christian Müller committed
93 94 95 96 97 98 99

          val nostrangebindings = FormulaFunctions.checkBindings(newinv)
          if (!nostrangebindings) {
            logger.error("New invariant binds variables more than once")
            logger.error(s"Invariant would be $newinv")
          }

100
          val newlabels = labels.updated(from, newinv)
Christian Müller's avatar
Christian Müller committed
101

102
          val isfirst = !nextEdge.from.hasPredecessors
Christian Müller's avatar
Christian Müller committed
103
          if (!isfirst) {
Christian Müller's avatar
Christian Müller committed
104
            val invalidated = proven.filter(_.to == nextEdge.from)
Christian Müller's avatar
Christian Müller committed
105
            val newproven = (proven -- invalidated) + nextEdge
Christian Müller's avatar
Christian Müller committed
106

Christian Müller's avatar
src  
Christian Müller committed
107
            val (status2, solver2) = Z3BSFO.checkAE(Implies(newinv, False))
Christian Müller's avatar
Christian Müller committed
108
            if (status2 == Status.SATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
109
              // Negation of newinv still sat, newinv does not imply false)
110
              logger.info(s"Relabeling $from. New size: ${newinv.opsize}. Continuing.")
111
              checkInvariantRec(newlabels :: labellist, newproven :: provenlist)
Christian Müller's avatar
Christian Müller committed
112
            } else {
113
              logger.info(s"New invariant for $from not satisfiable. Terminating.")
114
              (false, newlabels :: labellist, newproven :: provenlist)
Christian Müller's avatar
Christian Müller committed
115
            }
116
          } else {
Christian Müller's avatar
Christian Müller committed
117 118
            logger.info("Relabelled initial node. Terminating.")
            // logger.info(s"Model: ${Z3.printModel(solver.getModel())}")
Christian Müller's avatar
Christian Müller committed
119
            (false, newlabels :: labellist, (proven + nextEdge) :: provenlist)
120 121 122
          }
        }
      }
123 124
    }

Christian Müller's avatar
Christian Müller committed
125
    // create labelling
Christian Müller's avatar
Christian Müller committed
126
    val labels = (for (n <- graph.nodes) yield { n.value -> spec.inv }).toMap
Christian Müller's avatar
Christian Müller committed
127

128
    // update initial labels with untouched map
Christian Müller's avatar
Christian Müller committed
129 130 131 132
    val untouchedlabels = for ((n, inv) <- labels) yield {
      n -> inv.assumeEmpty(untouched(graph.get(n)).toList)
    }

Christian Müller's avatar
Christian Müller committed
133
    val (time, (result, labellings, proven)) = Utils.time { checkInvariantRec(List(untouchedlabels), List(Set())) }
134
    
Christian Müller's avatar
Christian Müller committed
135
    val dot1 = labellings.zip(proven).reverse
Christian Müller's avatar
Christian Müller committed
136
    val dot2 = dot1.map(tup => WFGraphEncoding.toDot(graph)(tup._1.map(t => (t._1, {
Christian Müller's avatar
Christian Müller committed
137
      t._2.pretty
Christian Müller's avatar
Christian Müller committed
138
    })), tup._2))
Christian Müller's avatar
Christian Müller committed
139

Christian Müller's avatar
Christian Müller committed
140
    (result, graph, labellings.reverse, proven.reverse, dot2, time)
Christian Müller's avatar
Christian Müller committed
141 142
  }
  
Christian Müller's avatar
Christian Müller committed
143 144 145 146
  def checkInvariantFPDot(spec: InvariantSpec,
                          properties:InvProperties = InvProperties.DEFAULT
                         ): (Boolean, List[String], Long) = {
    val (result, graph, afterlabels, proven, dot, time) = checkInvariantFPLabelling(spec, properties)
Christian Müller's avatar
Christian Müller committed
147 148 149
    (result, dot, time)
  }

Christian Müller's avatar
Christian Müller committed
150 151 152 153
  def checkInvariantFPHeadLabel(spec: InvariantSpec,
                                properties:InvProperties = InvProperties.DEFAULT
                               ): (Boolean, WorkflowGraph, Map[Int, Formula], Long) = {
    val (result, graph, afterlabels, proven, dot, time) = checkInvariantFPLabelling(spec, properties)
Christian Müller's avatar
Christian Müller committed
154
    (result, graph, afterlabels.last, time)
155
  }
Christian Müller's avatar
Christian Müller committed
156
  
Christian Müller's avatar
Christian Müller committed
157
  def checkInvariantOnce(spec: InvariantSpec, properties: InvProperties): (Boolean, StringBuilder) = {
Christian Müller's avatar
Christian Müller committed
158

Christian Müller's avatar
Christian Müller committed
159
    // Build graph
Christian Müller's avatar
Christian Müller committed
160 161
    val graph = TSGraphEncoding.toGraph(spec.ts)
    val untouched = TSGraphEncoding.untouchedMap(graph, spec.ts.sig, properties)
Christian Müller's avatar
Christian Müller committed
162

Christian Müller's avatar
Christian Müller committed
163
    val msg = new StringBuilder()
Christian Müller's avatar
Christian Müller committed
164
    msg ++= s"Trying to prove safe with invariant:\n\n${spec.inv.pretty}\n\n"
Christian Müller's avatar
Christian Müller committed
165

166
    // Check all edges
Christian Müller's avatar
Christian Müller committed
167
    val list = for (e <- graph.edges) yield {
Christian Müller's avatar
Christian Müller committed
168

Christian Müller's avatar
Christian Müller committed
169
      // Check I -> WP[w](inv)
Christian Müller's avatar
Christian Müller committed
170
      val b = TSGraphEncoding.toBlock(e)
171

Christian Müller's avatar
Christian Müller committed
172
      val ((res, solver), _) = checkBlockInvariant(spec, b, spec.inv, spec.inv, properties, untouched(e.from))
173

Christian Müller's avatar
Christian Müller committed
174
      if (res != Status.UNSATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
175 176 177
        msg ++= s"Possibly unsafe: Block may not uphold invariant:\n\n${e.label}\n\n"
        if (res == Status.SATISFIABLE) {
          msg ++= "Satisfying model:\n"
Christian Müller's avatar
Christian Müller committed
178
          msg ++= Z3FOEncoding.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
Christian Müller's avatar
Christian Müller committed
179 180
        } else if (res == Status.UNKNOWN) {
          msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
Christian Müller's avatar
Christian Müller committed
181 182
        }
        msg ++= "\n"
Christian Müller's avatar
Christian Müller committed
183
        logger.info(s"Could not prove invariant ${spec.inv}")
Christian Müller's avatar
Christian Müller committed
184 185 186 187 188
        logger.info(s"Z3 status $res")
        logger.info(s"Block ${e.label} may not uphold it")
      }
      res == Status.UNSATISFIABLE
    }
Christian Müller's avatar
Christian Müller committed
189

Christian Müller's avatar
Christian Müller committed
190 191
    val safe = list.reduceLeft(_ && _)
    if (safe) {
192
      msg ++= s"Proven safe.\n"
Christian Müller's avatar
Christian Müller committed
193
      logger.info(s"Workflow ${spec.ts}\n proven safe for invariant:\n${spec.inv.pretty}")
Christian Müller's avatar
Christian Müller committed
194
    }
Christian Müller's avatar
Christian Müller committed
195
    (safe, msg)
Christian Müller's avatar
Christian Müller committed
196 197
  }
}