InvariantChecker.scala 6.9 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2
package de.tum.workflows.toz3

Christian Müller's avatar
Christian Müller committed
3
import scala.annotation.tailrec
Christian Müller's avatar
Christian Müller committed
4
import com.microsoft.z3.Status
Christian Müller's avatar
Christian Müller committed
5
import com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
6 7 8 9 10
import de.tum.workflows.Encoding
import de.tum.workflows.Implicits._
import de.tum.workflows.Preconditions
import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._
Christian Müller's avatar
Christian Müller committed
11
import de.tum.workflows.foltl.FormulaFunctions
Christian Müller's avatar
Christian Müller committed
12
import de.tum.workflows.Utils
Christian Müller's avatar
Christian Müller committed
13
import de.tum.workflows.foltl.Properties
Christian Müller's avatar
Christian Müller committed
14

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

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


23 24
  def checkBlockInvariant(spec:Spec, b: SimpleBlock, pre: Formula, post: Formula, properties:InvProperties, untouched:Set[String]) = {
    val precond = Preconditions.abstractedPrecondition(post, b, spec, properties, untouched)
25

26
    val f = Implies(pre, precond)
27 28 29

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

30
    (Z3BSFO.checkAE(f.simplify), precond)
31
  }
32

Christian Müller's avatar
Christian Müller committed
33
  def checkInvariantFPLabelling(spec: Spec, inv: Formula, properties:InvProperties) = {
34
    val graph = Encoding.toGraph(spec.w)
35 36 37
    type Node = graph.NodeT
    type Edge = graph.EdgeT

38
    val untouched = Encoding.untouchedMap(graph, spec.w.sig, properties)
Christian Müller's avatar
Christian Müller committed
39

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

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

        // take one edge to prove
53 54 55 56
//        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
57
        val nextEdge = toProve.maxBy(edge => edge.source.value)
58
        
59
        // try to prove
Christian Müller's avatar
Christian Müller committed
60 61
        val pre = labels(nextEdge.from)
        val post = labels(nextEdge.to)
62
        val ((status, solver), strengthened) = checkBlockInvariant(spec, nextEdge, pre, post, properties, untouched(nextEdge.from))
63 64 65

        if (status == Status.UNSATISFIABLE) {
          // Negation of implication unsat
Christian Müller's avatar
Christian Müller committed
66
          // --> safe, continue with larger proven set.
Christian Müller's avatar
Christian Müller committed
67 68
          logger.info(s"Proven inductiveness for (${nextEdge._1} -> ${nextEdge.to}).")
          checkInvariantRec(labels :: labellist, (proven + nextEdge) :: provenlist)
69 70 71 72
        } 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
73
          // never relabel initial node
74
          logger.info(s"Invariant not inductive, strengthening.")
Christian Müller's avatar
Christian Müller committed
75

Christian Müller's avatar
Christian Müller committed
76
          val newinv = And(labels(nextEdge._1), strengthened).simplify
Christian Müller's avatar
Christian Müller committed
77 78 79 80 81 82 83

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

Christian Müller's avatar
Christian Müller committed
84
          val newlabels = labels.updated(nextEdge._1, newinv)
Christian Müller's avatar
Christian Müller committed
85

86
          val isfirst = !nextEdge.from.hasPredecessors
Christian Müller's avatar
Christian Müller committed
87
          if (!isfirst) {
Christian Müller's avatar
Christian Müller committed
88
            val invalidated = proven.filter(_.to == nextEdge.from)
Christian Müller's avatar
Christian Müller committed
89
            val newproven = (proven -- invalidated) + nextEdge
Christian Müller's avatar
Christian Müller committed
90

Christian Müller's avatar
src  
Christian Müller committed
91
            val (status2, solver2) = Z3BSFO.checkAE(Implies(newinv, False))
Christian Müller's avatar
Christian Müller committed
92
            if (status2 == Status.SATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
93
              // Negation of newinv still sat, newinv does not imply false)
Christian Müller's avatar
Christian Müller committed
94
              logger.info(s"Relabeling ${nextEdge._1}. New size: ${newinv.opsize}. Continuing.")
95
              checkInvariantRec(newlabels :: labellist, newproven :: provenlist)
Christian Müller's avatar
Christian Müller committed
96
            } else {
Christian Müller's avatar
Christian Müller committed
97
              logger.info(s"New invariant for ${nextEdge._1} not satisfiable. Terminating.")
98
              (false, newlabels :: labellist, newproven :: provenlist)
Christian Müller's avatar
Christian Müller committed
99
            }
100
          } else {
Christian Müller's avatar
Christian Müller committed
101 102
            logger.info("Relabelled initial node. Terminating.")
            // logger.info(s"Model: ${Z3.printModel(solver.getModel())}")
Christian Müller's avatar
Christian Müller committed
103
            (false, newlabels :: labellist, (proven + nextEdge) :: provenlist)
104 105 106
          }
        }
      }
107 108
    }

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

112
    // update initial labels with untouched map
Christian Müller's avatar
Christian Müller committed
113 114 115 116
    val untouchedlabels = for ((n, inv) <- labels) yield {
      n -> inv.assumeEmpty(untouched(graph.get(n)).toList)
    }

Christian Müller's avatar
Christian Müller committed
117
    val (time, (result, labellings, proven)) = Utils.time { checkInvariantRec(List(untouchedlabels), List(Set())) }
118
    
Christian Müller's avatar
Christian Müller committed
119
    val dot1 = labellings.zip(proven).reverse
Christian Müller's avatar
Christian Müller committed
120
    val dot2 = dot1.map(tup => Encoding.toDot(graph)(tup._1.map(t => (t._1, {
Christian Müller's avatar
Christian Müller committed
121
      t._2.pretty
Christian Müller's avatar
Christian Müller committed
122
    })), tup._2))
Christian Müller's avatar
Christian Müller committed
123

Christian Müller's avatar
Christian Müller committed
124
    (result, graph, labellings.reverse, proven.reverse, dot2, time)
Christian Müller's avatar
Christian Müller committed
125 126
  }
  
Christian Müller's avatar
Christian Müller committed
127
  def checkInvariantFPDot(spec: Spec, inv: Formula, properties:InvProperties = InvProperties.DEFAULT) = {
Christian Müller's avatar
Christian Müller committed
128
    val (result, graph, afterlabels, proven, dot, time) = checkInvariantFPLabelling(spec, inv, properties)
Christian Müller's avatar
Christian Müller committed
129 130 131 132
    (result, dot, time)
  }

  def checkInvariantFPHeadLabel(spec: Spec, inv: Formula, properties:InvProperties = InvProperties.DEFAULT) = {
Christian Müller's avatar
Christian Müller committed
133 134
    val (result, graph, afterlabels, proven, dot, time) = checkInvariantFPLabelling(spec, inv, properties)
    (result, graph, afterlabels.last, time)
135
  }
Christian Müller's avatar
Christian Müller committed
136
  
Christian Müller's avatar
Christian Müller committed
137
  def checkInvariantOnce(spec: Spec, inv: Formula, properties: InvProperties) = {
Christian Müller's avatar
Christian Müller committed
138

Christian Müller's avatar
Christian Müller committed
139
    // Build graph
140
    val graph = Encoding.toGraph(spec.w)
141
    val untouched = Encoding.untouchedMap(graph, spec.w.sig, properties)
Christian Müller's avatar
Christian Müller committed
142

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

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

Christian Müller's avatar
Christian Müller committed
149
      // Check I -> WP[w](inv)
Christian Müller's avatar
Christian Müller committed
150
      val b: SimpleBlock = e
151

152
      val ((res, solver), strengthened) = checkBlockInvariant(spec, b, inv, inv, properties, untouched(e.from))
153

Christian Müller's avatar
Christian Müller committed
154
      if (res != Status.UNSATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
155 156 157
        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
158
          msg ++= Z3FOEncoding.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
Christian Müller's avatar
Christian Müller committed
159 160
        } else if (res == Status.UNKNOWN) {
          msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
Christian Müller's avatar
Christian Müller committed
161 162
        }
        msg ++= "\n"
Christian Müller's avatar
Christian Müller committed
163 164 165 166 167 168
        logger.info(s"Could not prove invariant $inv")
        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
169

Christian Müller's avatar
Christian Müller committed
170 171
    val safe = list.reduceLeft(_ && _)
    if (safe) {
172
      msg ++= s"Proven safe.\n"
Christian Müller's avatar
Christian Müller committed
173
      logger.info(s"Workflow ${spec.w}\n proven safe for invariant:\n${inv.pretty}")
Christian Müller's avatar
Christian Müller committed
174
    }
Christian Müller's avatar
Christian Müller committed
175
    (safe, msg)
Christian Müller's avatar
Christian Müller committed
176 177
  }
}