InvariantChecker.scala 6.58 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 java.util.HashMap
Christian Müller's avatar
Christian Müller committed
4

Christian Müller's avatar
Christian Müller committed
5 6 7
import scala.annotation.tailrec

// labeled directed edge
Christian Müller's avatar
Christian Müller committed
8 9 10
import com.microsoft.z3.Context
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
11 12 13 14 15 16

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
17
import de.tum.workflows.foltl.FormulaFunctions
Christian Müller's avatar
Christian Müller committed
18
import de.tum.workflows.ltl.LTL
Christian Müller's avatar
Christian Müller committed
19 20

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

Christian Müller's avatar
Christian Müller committed
22
  val TIMEOUT = 60000 // in milliseconds
Christian Müller's avatar
Christian Müller committed
23 24 25 26 27 28

  def checkOnZ3(f: Formula) = {
    // Set up Z3
    val cfg = new HashMap[String, String]()
    cfg.put("timeout", TIMEOUT.toString())
    val ctx = new Context(cfg)
29

30 31 32 33
    //    val qe = ctx.mkTactic("qe")
    //    val default = ctx.mkTactic("smt")
    //    val t = ctx.andThen(qe, default)
    //    val s = ctx.mkSolver(t)
34

Christian Müller's avatar
Christian Müller committed
35
    val s = ctx.mkSolver()
Christian Müller's avatar
Christian Müller committed
36 37 38
    
    // Can only check universal things
    val neg = Neg(f).simplify()
39 40

    // univfree is now in E*, so can be solved as SAT Problem
Christian Müller's avatar
Christian Müller committed
41
    val stripped = FormulaFunctions.stripQuantifiers(neg)
42 43 44 45

    // val prefix = FormulaFunctions.collectQuantifiersSub(univfree)
    val satform = LTL.eliminatePredicates(stripped)

Christian Müller's avatar
Christian Müller committed
46
    // Checking QFree
47
    s.add(Z3QFree.translate(satform, ctx))
Christian Müller's avatar
Christian Müller committed
48 49 50 51 52 53 54

    // Send to z3
    val c = s.check()
    if (c == Status.UNKNOWN) {
      logger.info(s"Z3 status unknown: ${s.getReasonUnknown()}")
    }
    if (c == Status.SATISFIABLE) {
55
      logger.info(s"Z3 status satisfiable")
56
      //      logger.info(s"${s.getModel()}")
Christian Müller's avatar
Christian Müller committed
57 58
    }
    (c, s)
Christian Müller's avatar
Christian Müller committed
59
  }
Christian Müller's avatar
Christian Müller committed
60

61
  def checkBlockInvariant(sig: Signature, b: SimpleBlock, pre: Formula, post: Formula, stubborn: Boolean, isfirst: Boolean) = {
62 63 64 65 66 67 68 69
    val precond = Preconditions.weakestPrecondition(post, b)

    // Stubborn agents -> remove trace variable from choice predicate
    val stubprecond = if (stubborn) {
      precond.everywhere {
        case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
      }
    } else precond
70

71
    // TODO: do we do this here?
72 73 74 75 76 77 78 79 80 81 82
    val firstprecond = if (isfirst) {
      stubprecond.assumeEmpty(sig.preds.map(_.name).toList)
    } else { stubprecond }

    //      val test1 = inv.toPrenex()
    //      val test2 = stubprecond.toPrenex()

    val f = Implies(pre, firstprecond)

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

83 84
    checkOnZ3(f.simplify())
  }
85

86 87 88 89 90 91
  def checkInvariantFP(w: Workflow, inv: Formula, stubborn: Boolean) = {
    val graph = Encoding.toGraph(w)
    type Node = graph.NodeT
    type Edge = graph.EdgeT

    @tailrec
Christian Müller's avatar
Christian Müller committed
92
    def checkInvariantRec(labels: Map[Node, Formula], proven: Set[Edge]): (Boolean, Map[Node, Formula], Set[Edge]) = {
93 94 95 96

      // check if done, i.e. all edges proven
      val toProve = (graph.edges -- proven)
      if (toProve.isEmpty) {
Christian Müller's avatar
Christian Müller committed
97
        logger.info("Everything proven. Terminating.")
Christian Müller's avatar
Christian Müller committed
98
        (true, labels, proven)
99 100 101 102 103 104 105 106
      } else {

        // take one edge to prove
        val next = toProve.head

        // try to prove
        val pre = labels(next._1)
        val post = labels(next._2)
Christian Müller's avatar
Christian Müller committed
107 108
        val isfirst = !next._1.hasPredecessors
        val (status, solver) = checkBlockInvariant(w.sig, next, pre, post, stubborn, isfirst)
109 110 111

        if (status == Status.UNSATISFIABLE) {
          // Negation of implication unsat
Christian Müller's avatar
Christian Müller committed
112 113
          // --> safe, continue with larger proven set.
          logger.info(s"Proven inductiveness for (${next._1} -> ${next._2}).")
114 115 116 117 118
          checkInvariantRec(labels, proven + next)
        } 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
119 120
          // never relabel initial node
          if (!isfirst) {
Christian Müller's avatar
Christian Müller committed
121 122 123 124 125 126 127 128
            val newinv = And(labels(next._1), Preconditions.weakestPrecondition(post, next)).simplify()
            
            // Abstract away inner existentials
            val universalinv = LTL.instantiateExistentials(newinv).simplify()
            
            // TODO: Abstract away auxilliaries
            
            val (status2, solver2) = checkOnZ3(Implies(universalinv, False))
Christian Müller's avatar
Christian Müller committed
129
  
Christian Müller's avatar
Christian Müller committed
130
            // FIXME breaks if universalinv is used
Christian Müller's avatar
Christian Müller committed
131 132 133 134 135 136 137 138 139 140 141 142 143
            val newlabels = labels.updated(next._1, newinv)
            val invalidated = proven.filter(_._2 == next._1)
            
            val newproven = (proven -- invalidated) + next
  
            if (status2 == Status.SATISFIABLE) {
              // Negation of newinv still sat, newinv does not imply false
              logger.info(s"Relabeling ${next._1}. Continuing.")
              checkInvariantRec(newlabels, newproven)
            } else {
              logger.info(s"New invariant for ${next._1} not satisfiable. Terminating.")
              (false, newlabels, newproven)
            }
144
          } else {
Christian Müller's avatar
Christian Müller committed
145 146
            logger.info("Would have to relabel initial node. Terminating.")
            (false, labels, proven)
147 148 149
          }
        }
      }
150 151
    }

Christian Müller's avatar
Christian Müller committed
152 153
    // create labelling - FIXME: maybe use inv only for last
    val labels = (for (n <- graph.nodes) yield { n -> inv }).toMap
Christian Müller's avatar
Christian Müller committed
154
    val (result, afterlabels, proven) = checkInvariantRec(labels, Set())
155

Christian Müller's avatar
Christian Müller committed
156
    val dot = Encoding.toDot(graph)(afterlabels.map(t => (t._1, t._2.pretty())), proven)
157
    (result, dot)
158
  }
Christian Müller's avatar
Christian Müller committed
159
  
160
  def checkInvariantOnce(w: Workflow, inv: Formula, stubborn: Boolean) = {
Christian Müller's avatar
Christian Müller committed
161

Christian Müller's avatar
Christian Müller committed
162 163
    // Build graph
    val graph = Encoding.toGraph(w)
Christian Müller's avatar
Christian Müller committed
164

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

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

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

174 175 176
      // Special handling for first block
      // TODO: Replace by iteration
      val isfirst = !e.from.hasPredecessors
177

178
      val (res, solver) = checkBlockInvariant(w.sig, b, inv, inv, stubborn, isfirst)
179

Christian Müller's avatar
Christian Müller committed
180
      if (res != Status.UNSATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
181 182 183
        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
184
          msg ++= Z3.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
Christian Müller's avatar
Christian Müller committed
185 186
        } else if (res == Status.UNKNOWN) {
          msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
Christian Müller's avatar
Christian Müller committed
187 188
        }
        msg ++= "\n"
Christian Müller's avatar
Christian Müller committed
189 190 191 192 193 194
        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
195

Christian Müller's avatar
Christian Müller committed
196 197
    val safe = list.reduceLeft(_ && _)
    if (safe) {
198
      msg ++= s"Proven safe.\n"
Christian Müller's avatar
Christian Müller committed
199
      logger.info(s"Workflow $w\n proven safe for invariant:\n${inv.pretty()}")
Christian Müller's avatar
Christian Müller committed
200
    }
Christian Müller's avatar
Christian Müller committed
201
    (safe, msg)
Christian Müller's avatar
Christian Müller committed
202 203
  }
}