InvariantChecker.scala 7.47 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4 5 6 7 8 9
package de.tum.workflows.toz3

import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.ltl.LTL
import de.tum.workflows.Implicits._
import de.tum.workflows.WorkflowParser
import de.tum.workflows.Encoding
import de.tum.workflows.Preconditions
Christian Müller's avatar
Christian Müller committed
10 11
import de.tum.workflows.foltl.Properties.T1
import de.tum.workflows.foltl.Properties.T2
Christian Müller's avatar
Christian Müller committed
12 13 14 15 16 17 18

import scalax.collection.edge.LDiEdge // labeled directed edge
import com.microsoft.z3.Context
import java.util.HashMap
import org.omg.CORBA.TIMEOUT
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
19
import de.tum.workflows.foltl.Properties
Christian Müller's avatar
Christian Müller committed
20
import de.tum.workflows.foltl.FormulaFunctions
21 22 23
import scalax.collection.Graph
import de.tum.workflows.Encoding.WorkflowGraph
import scala.annotation.tailrec
Christian Müller's avatar
Christian Müller committed
24 25

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

Christian Müller's avatar
Christian Müller committed
27
  val TIMEOUT = 60000 // in milliseconds
Christian Müller's avatar
Christian Müller committed
28 29 30 31 32 33

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

35 36 37 38
    //    val qe = ctx.mkTactic("qe")
    //    val default = ctx.mkTactic("smt")
    //    val t = ctx.andThen(qe, default)
    //    val s = ctx.mkSolver(t)
39

Christian Müller's avatar
Christian Müller committed
40
    val s = ctx.mkSolver()
Christian Müller's avatar
Christian Müller committed
41

42 43 44 45 46 47 48 49 50 51 52 53 54
    // Make QFree - will work for any A* or A*E* formula
    val tocheck = Neg(f).simplify()
    if (!tocheck.isBS()) {
      logger.error(s"Not in BS: ${tocheck.pretty}")
    }
    val univfree = LTL.instantiateUniversals(tocheck)

    // univfree is now in E*, so can be solved as SAT Problem
    val stripped = FormulaFunctions.stripQuantifiers(univfree)

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

Christian Müller's avatar
Christian Müller committed
55
    // Checking QFree
56
    s.add(Z3QFree.translate(satform, ctx))
Christian Müller's avatar
Christian Müller committed
57 58 59 60 61 62 63

    // Send to z3
    val c = s.check()
    if (c == Status.UNKNOWN) {
      logger.info(s"Z3 status unknown: ${s.getReasonUnknown()}")
    }
    if (c == Status.SATISFIABLE) {
64
      logger.info(s"Z3 status satisfiable")
65
      //      logger.info(s"${s.getModel()}")
Christian Müller's avatar
Christian Müller committed
66 67
    }
    (c, s)
Christian Müller's avatar
Christian Müller committed
68
  }
Christian Müller's avatar
Christian Müller committed
69

70
  def checkBlockInvariant(sig: Signature, b: SimpleBlock, pre: Formula, post: Formula, stubborn: Boolean, isfirst: Boolean) = {
71 72 73 74 75 76 77 78
    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
79

80
    // TODO: do we do this here?
81 82 83 84 85 86 87 88 89 90 91
    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")

92 93
    checkOnZ3(f.simplify())
  }
94

95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138
  def checkInvariantFP(w: Workflow, inv: Formula, stubborn: Boolean) = {
    val graph = Encoding.toGraph(w)
    type Node = graph.NodeT
    type Edge = graph.EdgeT

    @tailrec
    def checkInvariantRec(labels: Map[Node, Formula], proven: Set[Edge]): Option[Map[Node, Formula]] = {

      // check if done, i.e. all edges proven
      val toProve = (graph.edges -- proven)
      if (toProve.isEmpty) {
        Some(labels)
      } else {

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

        // try to prove
        val pre = labels(next._1)
        val post = labels(next._2)
        val (status, solver) = checkBlockInvariant(w.sig, next, pre, post, stubborn, next._1.hasPredecessors)

        if (status == Status.UNSATISFIABLE) {
          // Negation of implication unsat
          // --> safe, continue with larger proven set
          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
          val newinv = And(labels(next._1), Preconditions.weakestPrecondition(post, next))
          val (status2, solver2) = checkOnZ3(newinv)

          val newlabels = labels.updated(next._1, newinv)
          val newproven = proven.filterNot(_._1 == next._1)

          if (status2 == Status.UNSATISFIABLE) {
            // Negation of newinv still unsat, newinv still sat
            checkInvariantRec(newlabels, newproven)
          } else {
            None
          }
        }
      }
139 140
    }

141 142 143
    // create labelling
    val labels = (for (n <- graph.nodes) yield { n -> inv }) toMap
    val result = checkInvariantRec(labels, Set())
144

145
    val dot = Encoding.toDot(graph, labels.map(t => (t._1, t._2.pretty())))
146

147
    (result, dot)
148 149
  }

150
  def checkInvariantOnce(w: Workflow, inv: Formula, stubborn: Boolean) = {
Christian Müller's avatar
Christian Müller committed
151

Christian Müller's avatar
Christian Müller committed
152 153
    // Build graph
    val graph = Encoding.toGraph(w)
Christian Müller's avatar
Christian Müller committed
154

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

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

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

164 165 166
      // Special handling for first block
      // TODO: Replace by iteration
      val isfirst = !e.from.hasPredecessors
167

168
      val (res, solver) = checkBlockInvariant(w.sig, b, inv, inv, stubborn, isfirst)
169

Christian Müller's avatar
Christian Müller committed
170
      if (res != Status.UNSATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
171 172 173
        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
174
          msg ++= Z3.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
Christian Müller's avatar
Christian Müller committed
175 176
        } else if (res == Status.UNKNOWN) {
          msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
Christian Müller's avatar
Christian Müller committed
177 178
        }
        msg ++= "\n"
Christian Müller's avatar
Christian Müller committed
179 180 181 182 183 184
        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
185

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

  def genEq(f: Fun, p: List[Var]) = {
Christian Müller's avatar
Christian Müller committed
195 196 197
    val newf = f.parallelRename(f.params, p)
    Eq(newf.in(T1), newf.in(T2))
  }
Christian Müller's avatar
Christian Müller committed
198 199

  def invariantNoninterStubborn(spec: Spec) = {
Christian Müller's avatar
Christian Müller committed
200
    val agent = spec.target.params(0)
Christian Müller's avatar
Christian Müller committed
201 202

    val premise = And.make(for ((o, t) <- spec.declass) yield {
203
      // Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
Christian Müller's avatar
Christian Müller committed
204
      Forall(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
Christian Müller's avatar
Christian Müller committed
205
    })
Christian Müller's avatar
Christian Müller committed
206

Christian Müller's avatar
Christian Müller committed
207 208
    val conclusion = And.make(for (r <- spec.w.sig.preds.toList if r.params.head.typ == agent.typ) yield {
      val quant = r.params.drop(1)
Christian Müller's avatar
Christian Müller committed
209
      Forall(quant, genEq(r, agent :: quant))
Christian Müller's avatar
Christian Müller committed
210
    })
Christian Müller's avatar
Christian Müller committed
211

Christian Müller's avatar
Christian Müller committed
212
    Forall(agent, premise  conclusion).simplify()
Christian Müller's avatar
Christian Müller committed
213
  }
Christian Müller's avatar
Christian Müller committed
214

215 216 217 218
  def invariantNoninterStubbornBS(spec: Spec) = {
    val agent = spec.target.params(0)

    val premise = for ((o, t) <- spec.declass) yield {
219
      // Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
220 221 222 223 224 225 226 227 228 229 230 231
      (o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
    }
    val quants = premise.flatMap(_._1).toSet.toList // eliminate doubles

    val conclusion = And.make(for (r <- spec.w.sig.preds.toList if r.params.head.typ == agent.typ) yield {
      val quant = r.params.drop(1)
      Forall(quant, genEq(r, agent :: quant))
    })

    Forall(agent, Forall(quants, Implies(And.make(premise.map(_._2)), conclusion))).simplify()
  }

Christian Müller's avatar
Christian Müller committed
232 233 234 235 236 237
  def invariantAllEqual(spec: Spec) = {
    And.make(for (r <- spec.w.sig.preds.toList) yield {
      Forall(r.params, genEq(r, r.params))
    })
  }

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