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
checker    
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
checker    
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
checker    
Christian Müller committed
36
37
38
39
40
41
42
43
44

    s.add(toZ3.translate(f, ctx))

    // 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
checker    
Christian Müller committed
47
48
    }
    (c, s)
Christian Müller's avatar
Christian Müller committed
49
  }
Christian Müller's avatar
checker    
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
    
Christian Müller's avatar
Christian Müller committed
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}")
    }

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