InvariantChecker.scala 5.65 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
Christian Müller's avatar
Christian Müller committed
21 22

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

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

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

Christian Müller's avatar
Christian Müller committed
32 33 34 35
//    val qe = ctx.mkTactic("qe")
//    val default = ctx.mkTactic("smt")
//    val t = ctx.andThen(qe, default)
//    val s = ctx.mkSolver(t)
36

Christian Müller's avatar
Christian Müller committed
37
    val s = ctx.mkSolver()
Christian Müller's avatar
Christian Müller committed
38

Christian Müller's avatar
Christian Müller committed
39 40
    // Checking QFree
    s.add(Z3QFree.translate(f, ctx))
Christian Müller's avatar
Christian Müller committed
41 42 43 44 45 46 47

    // Send to z3
    val c = s.check()
    if (c == Status.UNKNOWN) {
      logger.info(s"Z3 status unknown: ${s.getReasonUnknown()}")
    }
    if (c == Status.SATISFIABLE) {
48 49
      logger.info(s"Z3 status satisfiable")
//      logger.info(s"${s.getModel()}")
Christian Müller's avatar
Christian Müller committed
50 51
    }
    (c, s)
Christian Müller's avatar
Christian Müller committed
52
  }
Christian Müller's avatar
Christian Müller committed
53

54 55 56 57 58 59 60 61 62 63
  def checkBlockInvariant(sig:Signature, b: SimpleBlock, pre: Formula, post: Formula, stubborn: Boolean, isfirst: Boolean) = {
    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
    
64
    // TODO: do we do this here?
65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83
    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")
    val tocheck = Neg(f).simplify()

    //      val test3 = tocheck.toPrenex()

    // Transform to existential
    if (!tocheck.isBS()) {
      logger.error(s"Not in BS: Invariant implication ${tocheck.pretty}")
    }

84
    val univfree = LTL.instantiateUniversals(tocheck)
Christian Müller's avatar
Christian Müller committed
85 86 87 88 89 90 91
    
    // 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)
92

Christian Müller's avatar
Christian Müller committed
93 94
//    val test3 = stripped.pretty()
//    println(test3)
95

Christian Müller's avatar
Christian Müller committed
96
    checkOnZ3(satform.simplify())
97 98
  }

Christian Müller's avatar
Christian Müller committed
99 100
  def checkInvariant(w: Workflow, inv: Formula, stubborn: Boolean) = {

Christian Müller's avatar
Christian Müller committed
101 102
    // Build graph
    val graph = Encoding.toGraph(w)
Christian Müller's avatar
Christian Müller committed
103

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

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

Christian Müller's avatar
Christian Müller committed
110
      // Check I -> WP[w](inv)
Christian Müller's avatar
Christian Müller committed
111
      val b: SimpleBlock = e
112
      
113 114 115
      // Special handling for first block
      // TODO: Replace by iteration
      val isfirst = !e.from.hasPredecessors
116
      
117
      val (res, solver) = checkBlockInvariant(w.sig, b, inv, inv, stubborn, isfirst)
118

Christian Müller's avatar
Christian Müller committed
119
      if (res != Status.UNSATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
120 121 122
        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
123
          msg ++= Z3.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
Christian Müller's avatar
Christian Müller committed
124 125
        } else if (res == Status.UNKNOWN) {
          msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
Christian Müller's avatar
Christian Müller committed
126 127
        }
        msg ++= "\n"
Christian Müller's avatar
Christian Müller committed
128 129 130 131 132 133
        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
134

Christian Müller's avatar
Christian Müller committed
135 136
    val safe = list.reduceLeft(_ && _)
    if (safe) {
137
      msg ++= s"Proven safe.\n"
Christian Müller's avatar
Christian Müller committed
138
      logger.info(s"Workflow $w\n proven safe for invariant:\n${inv.pretty()}")
Christian Müller's avatar
Christian Müller committed
139
    }
Christian Müller's avatar
Christian Müller committed
140
    (safe, msg)
Christian Müller's avatar
Christian Müller committed
141
  }
Christian Müller's avatar
Christian Müller committed
142 143

  def genEq(f: Fun, p: List[Var]) = {
Christian Müller's avatar
Christian Müller committed
144 145 146
    val newf = f.parallelRename(f.params, p)
    Eq(newf.in(T1), newf.in(T2))
  }
Christian Müller's avatar
Christian Müller committed
147 148

  def invariantNoninterStubborn(spec: Spec) = {
Christian Müller's avatar
Christian Müller committed
149
    val agent = spec.target.params(0)
Christian Müller's avatar
Christian Müller committed
150 151

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

Christian Müller's avatar
Christian Müller committed
156 157
    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
158
      Forall(quant, genEq(r, agent :: quant))
Christian Müller's avatar
Christian Müller committed
159
    })
Christian Müller's avatar
Christian Müller committed
160

Christian Müller's avatar
Christian Müller committed
161
    Forall(agent, premise  conclusion).simplify()
Christian Müller's avatar
Christian Müller committed
162
  }
Christian Müller's avatar
Christian Müller committed
163

164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180
  def invariantNoninterStubbornBS(spec: Spec) = {
    val agent = spec.target.params(0)

    val premise = for ((o, t) <- spec.declass) yield {
      // Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2) 
      (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
181 182 183 184 185 186
  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
187
}