InvariantChecker.scala 7.68 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
  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) {
Christian Müller's avatar
Christian Müller committed
106
        logger.info("Everything proven. Terminating.")
107 108 109 110 111 112 113 114 115 116 117 118 119
        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
Christian Müller's avatar
Christian Müller committed
120 121
          // --> safe, continue with larger proven set.
          logger.info(s"Proven inductiveness for (${next._1} -> ${next._2}).")
122 123 124 125 126 127 128 129 130 131 132 133 134 135 136
          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 {
Christian Müller's avatar
Christian Müller committed
137
            logger.info("New invariant not satisfiable. Terminating.")
138 139 140 141
            None
          }
        }
      }
142 143
    }

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

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

150
    (result, dot)
151 152
  }

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

Christian Müller's avatar
Christian Müller committed
155 156
    // Build graph
    val graph = Encoding.toGraph(w)
Christian Müller's avatar
Christian Müller committed
157

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

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

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

167 168 169
      // Special handling for first block
      // TODO: Replace by iteration
      val isfirst = !e.from.hasPredecessors
170

171
      val (res, solver) = checkBlockInvariant(w.sig, b, inv, inv, stubborn, isfirst)
172

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

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

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

  def invariantNoninterStubborn(spec: Spec) = {
Christian Müller's avatar
Christian Müller committed
203
    val agent = spec.target.params(0)
Christian Müller's avatar
Christian Müller committed
204 205

    val premise = And.make(for ((o, t) <- spec.declass) yield {
206
      // Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
Christian Müller's avatar
Christian Müller committed
207
      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
208
    })
Christian Müller's avatar
Christian Müller committed
209

Christian Müller's avatar
Christian Müller committed
210 211
    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
212
      Forall(quant, genEq(r, agent :: quant))
Christian Müller's avatar
Christian Müller committed
213
    })
Christian Müller's avatar
Christian Müller committed
214

Christian Müller's avatar
Christian Müller committed
215
    Forall(agent, premise  conclusion).simplify()
Christian Müller's avatar
Christian Müller committed
216
  }
Christian Müller's avatar
Christian Müller committed
217

218 219 220 221
  def invariantNoninterStubbornBS(spec: Spec) = {
    val agent = spec.target.params(0)

    val premise = for ((o, t) <- spec.declass) yield {
222
      // Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
223 224 225 226 227 228 229 230 231 232 233 234
      (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
235 236 237 238 239 240
  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
241
}