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
testing    
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
checker    
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
checker    
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
testing    
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
testing    
Christian Müller committed
46
    // Checking QFree
47
    s.add(Z3QFree.translate(satform, ctx))
Christian Müller's avatar
checker    
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
checker    
Christian Müller committed
57
58
    }
    (c, s)
Christian Müller's avatar
Christian Müller committed
59
  }
Christian Müller's avatar
checker    
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

Christian Müller's avatar
Christian Müller committed
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
checker    
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
checker    
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
checker    
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
checker    
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
checker    
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
checker    
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
  }
}