InvariantChecker.scala 5.3 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 21

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

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

  def checkOnZ3(f: Formula) = {
    // Set up Z3
    val cfg = new HashMap[String, String]()
    cfg.put("timeout", TIMEOUT.toString())
    val ctx = new Context(cfg)
30 31 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)
Christian Müller's avatar
Christian Müller committed
36

Christian Müller's avatar
Christian Müller committed
37
    s.add(Z3.translate(f, ctx))
Christian Müller's avatar
Christian Müller committed
38 39 40 41 42 43 44

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

51 52 53 54 55 56 57 58 59 60
  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
    
61
    // TODO: do we do this here?
62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80
    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}")
    }

81
    val univfree = LTL.instantiateUniversals(tocheck)
82 83 84 85 86 87 88

    //      val test3 = univfree.pretty()
    //      println(test3)

    checkOnZ3(univfree.simplify())
  }

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

Christian Müller's avatar
Christian Müller committed
91 92
    // Build graph
    val graph = Encoding.toGraph(w)
Christian Müller's avatar
Christian Müller committed
93

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

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

Christian Müller's avatar
Christian Müller committed
100
      // Check I -> WP[w](inv)
Christian Müller's avatar
Christian Müller committed
101
      val b: SimpleBlock = e
102
      
103 104 105
      // Special handling for first block
      // TODO: Replace by iteration
      val isfirst = !e.from.hasPredecessors
106
      
107
      val (res, solver) = checkBlockInvariant(w.sig, b, inv, inv, stubborn, isfirst)
108

Christian Müller's avatar
Christian Müller committed
109
      if (res != Status.UNSATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
110 111 112
        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
113
          msg ++= Z3.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
Christian Müller's avatar
Christian Müller committed
114 115
        } else if (res == Status.UNKNOWN) {
          msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
Christian Müller's avatar
Christian Müller committed
116 117
        }
        msg ++= "\n"
Christian Müller's avatar
Christian Müller committed
118 119 120 121 122 123
        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
124

Christian Müller's avatar
Christian Müller committed
125 126
    val safe = list.reduceLeft(_ && _)
    if (safe) {
127
      msg ++= s"Proven safe.\n"
Christian Müller's avatar
Christian Müller committed
128
      logger.info(s"Workflow $w\n proven safe for invariant:\n${inv.pretty()}")
Christian Müller's avatar
Christian Müller committed
129
    }
Christian Müller's avatar
Christian Müller committed
130
    (safe, msg)
Christian Müller's avatar
Christian Müller committed
131
  }
Christian Müller's avatar
Christian Müller committed
132 133

  def genEq(f: Fun, p: List[Var]) = {
Christian Müller's avatar
Christian Müller committed
134 135 136
    val newf = f.parallelRename(f.params, p)
    Eq(newf.in(T1), newf.in(T2))
  }
Christian Müller's avatar
Christian Müller committed
137 138

  def invariantNoninterStubborn(spec: Spec) = {
Christian Müller's avatar
Christian Müller committed
139
    val agent = spec.target.params(0)
Christian Müller's avatar
Christian Müller committed
140 141

    val premise = And.make(for ((o, t) <- spec.declass) yield {
Christian Müller's avatar
Christian Müller committed
142 143
      // 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
144
    })
Christian Müller's avatar
Christian Müller committed
145

Christian Müller's avatar
Christian Müller committed
146 147
    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
148
      Forall(quant, genEq(r, agent :: quant))
Christian Müller's avatar
Christian Müller committed
149
    })
Christian Müller's avatar
Christian Müller committed
150

Christian Müller's avatar
Christian Müller committed
151
    Forall(agent, premise  conclusion).simplify()
Christian Müller's avatar
Christian Müller committed
152
  }
Christian Müller's avatar
Christian Müller committed
153

154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170
  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
171 172 173 174 175 176
  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
177
}