Preconditions.scala 6.97 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
2
3
4
package de.tum.workflows

import com.typesafe.scalalogging._
import blocks._
Christian Müller's avatar
Christian Müller committed
5
import de.tum.workflows.foltl.{FOLTL, FOTransformers, FormulaFunctions, Properties}
Christian Müller's avatar
Christian Müller committed
6
import de.tum.workflows.foltl.FOLTL._
Christian Müller's avatar
Christian Müller committed
7
import de.tum.workflows.foltl.Properties._
Christian Müller's avatar
Christian Müller committed
8
import de.tum.workflows.toz3.{InvProperties, Z3BSFO}
Christian Müller's avatar
Christian Müller committed
9
10

object Preconditions extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
11

Christian Müller's avatar
Christian Müller committed
12
  private def elaborateSteps(b: SimpleBlock, s: Spec): List[SimpleBlock] = {
13
14
15
16
    val newsteps = for (
        stmt <- b.steps
        if s.causals.map(_.typ).contains(stmt.tuple.head.typ) ||
          stmt.tuple.head.typ == s.target.params.head.typ) yield {
Christian Müller's avatar
Christian Müller committed
17
18
19
20
      val fun = Fun(stmt.fun, stmt.tuple)
      // TODO
      val guard = Neg(Eq(fun.in(T1), fun.in(T2)))
      ForallBlock(stmt.tuple, List(Add(guard, INFNAME, List(stmt.tuple.head))))
Christian Müller's avatar
Christian Müller committed
21
    }
Christian Müller's avatar
Christian Müller committed
22
    b :: newsteps
23
  }
Christian Müller's avatar
Christian Müller committed
24

Christian Müller's avatar
Christian Müller committed
25
  // For oracly blocks, remove O from guard and add to ForallMay choice predicate
26
  private def elaborateOraclyBlock(b: SimpleBlock, s: Spec) = {
Christian Müller's avatar
Christian Müller committed
27
28
    if (b.isoracly) {
      val stmt = b.steps.head // can only be one
Christian Müller's avatar
Christian Müller committed
29
      def fixguard(f: Formula) = {
Christian Müller's avatar
Christian Müller committed
30
        f.everywhere {
Christian Müller's avatar
Christian Müller committed
31
          case f: Fun if f.isOracle() => True
Christian Müller's avatar
Christian Müller committed
32
33
        }
      }
Christian Müller's avatar
Christian Müller committed
34
35

      def findOracle(f: Formula) = {
Christian Müller's avatar
Christian Müller committed
36
        f.collect {
Christian Müller's avatar
Christian Müller committed
37
          case f: Fun if (f.isOracle()) => List(f.name)
Christian Müller's avatar
Christian Müller committed
38
39
40
        }
      }
      val name = findOracle(stmt.guard).head
Christian Müller's avatar
Christian Müller committed
41

Christian Müller's avatar
Christian Müller committed
42
      val newstmt = stmt match {
Christian Müller's avatar
Christian Müller committed
43
44
        case Add(guard, fun, tuple)    => Add(fixguard(guard).simplify, fun, tuple)
        case Remove(guard, fun, tuple) => Remove(fixguard(guard).simplify, fun, tuple)
Christian Müller's avatar
Christian Müller committed
45
46
47
48
      }
      ForallMayBlock(b.agents, name, List(newstmt))
    } else b
  }
Christian Müller's avatar
Christian Müller committed
49
50
51

  def subst(f: Formula, updates: List[(String, (List[FOLTL.Var], FOLTL.Formula))], b: SimpleBlock) = {

52
53
54
55
56
    updates.foldRight(f)((update, f) => {
      val (repname, (vars, form)) = update
      f everywhere {
        case Fun(name, ind, params) if name == repname => {
          val renamed = form.parallelRename(vars, params)
Christian Müller's avatar
Christian Müller committed
57

58
59
60
61
62
63
64
65
66
67
          // Annotate the precondition with the index
          if (ind.isDefined) {
            FormulaFunctions.annotate(renamed, ind.get)
          } else {
            renamed
          }
        }
      }
    })
  }
68
69

  // TODO: make this a transformation instead of a logics block
Christian Müller's avatar
Christian Müller committed
70
  def getUpdate(s:Statement, b:SimpleBlock, choice:Option[Fun], spec:Spec, properties:InvProperties) = {
Christian Müller's avatar
Christian Müller committed
71
72
73
74
75
76

      //        val list = List(s.guard) ++ choice.toList
      //        val guard = And.make(list)
      val first = s.tuple.head

      // Trace related substitution for informedness
Christian Müller's avatar
Christian Müller committed
77
      val con = if (b.isoracly) {
Christian Müller's avatar
Christian Müller committed
78
79
80
81
82
83
84
85
86
87
        val decl = spec.declass.getOrElse(b.pred.get, (List(), False))._2
        // FIXME: substitutions?
        // FIXME: decl in T2?
        Or(And(decl.in(T1), choice.get.in(T1)), And(Neg(decl.in(T1)), choice.get))
      } else if (choice.isDefined) {
        // is "normal" may block
        val inner = if (first.typ == spec.target.params.head.typ) {
          val inf = Fun(INFNAME, List(b.agents.head))
          if (properties.stubborn) {
            choice.get.in(T1)
88
          } else {
Christian Müller's avatar
Christian Müller committed
89
            Or(And(Neg(inf.in(T1)), choice.get.in(T1)), And(inf.in(T1), choice.get))
90
91
          }
        } else {
Christian Müller's avatar
Christian Müller committed
92
          choice.get
93
        }
Christian Müller's avatar
Christian Müller committed
94
95
96
97
        inner
      } else {
        True
      }
Christian Müller's avatar
Christian Müller committed
98

Christian Müller's avatar
Christian Müller committed
99
      val guard = And(s.guard, con).simplify
Christian Müller's avatar
Christian Müller committed
100
      //        val guard = True
Christian Müller's avatar
Christian Müller committed
101
102

      val frees = guard.freeVars -- s.tuple.toSet -- spec.constants
Christian Müller's avatar
Christian Müller committed
103
104
105

      val form = s match {
        case Add(_, _, _) => {
Christian Müller's avatar
Christian Müller committed
106
          Or(Fun(s.fun, s.tuple), Exists(frees.toList, guard)).simplify
Christian Müller's avatar
Christian Müller committed
107
        }
Christian Müller's avatar
Christian Müller committed
108
        case Remove(_, _, _) => {
Christian Müller's avatar
Christian Müller committed
109
          And(Fun(s.fun, s.tuple), Forall(frees.toList, Neg(guard))).simplify
Christian Müller's avatar
Christian Müller committed
110
111
112
113
114
        }
      }
      form
  }

Christian Müller's avatar
Christian Müller committed
115
116
117
118
119
  def elaborate(block: SimpleBlock, spec:Spec, properties:InvProperties) = {
    val stepOne = if (!properties.stubborn) elaborateSteps(block, spec) else List(block)
    stepOne map { b =>  elaborateOraclyBlock(b, spec) }
  }

Christian Müller's avatar
Christian Müller committed
120
  def weakestPrecondition(post: Formula, outerb: SimpleBlock, spec: Spec, properties: InvProperties) = {
Christian Müller's avatar
Christian Müller committed
121

Christian Müller's avatar
cleanup    
Christian Müller committed
122
    // TODO: Make 2-trace elaboration optional
Christian Müller's avatar
Christian Müller committed
123

Christian Müller's avatar
cleanup    
Christian Müller committed
124
    val steps = elaborate(outerb, spec, properties)
Christian Müller's avatar
Christian Müller committed
125
126

    val precond = steps.foldRight(post)((b, f) => {
Christian Müller's avatar
Christian Müller committed
127
      val innerprecond = weakestPreconditionSingle(f, b, spec, properties)
Christian Müller's avatar
Christian Müller committed
128
      innerprecond
129
    })
Christian Müller's avatar
Christian Müller committed
130
131
132
    precond
  }

Christian Müller's avatar
Christian Müller committed
133
  private def weakestPreconditionSingle(f: Formula, b: SimpleBlock, spec: Spec, properties: InvProperties) = {
Christian Müller's avatar
Christian Müller committed
134
135
136
137
138

    val choice = b.pred.map(n => Fun(n, b.agents))

    val updates = for (s <- b.steps) yield {
      s.fun -> (s.tuple, {
Christian Müller's avatar
Christian Müller committed
139
        getUpdate(s, b, choice, spec, properties)
Christian Müller's avatar
Christian Müller committed
140
141
142
      })
    }

Christian Müller's avatar
Christian Müller committed
143
    // Replace literals with their precondition
144
    val replaced = subst(f, updates, b)
Christian Müller's avatar
Christian Müller committed
145

Christian Müller's avatar
Christian Müller committed
146
147
    // TODO: have we proven this correct?
    val removed = FOTransformers.eliminateDoubleQuantifiers(replaced)
Christian Müller's avatar
Christian Müller committed
148
149
    if (Utils.DEBUG_MODE) {
      if (FormulaFunctions.collectQuantifiers(removed) != FormulaFunctions.collectQuantifiers(replaced)) {
150
        logger.warn(s"Removed a quantifier:\nBefore: ${replaced}\nAfter:$removed")
Christian Müller's avatar
Christian Müller committed
151
152
      }
    }
Christian Müller's avatar
Christian Müller committed
153

Christian Müller's avatar
Christian Müller committed
154
    removed
Christian Müller's avatar
Christian Müller committed
155
  }
Christian Müller's avatar
Christian Müller committed
156

157
158
  def abstractedPrecondition(f: Formula, b: SimpleBlock, spec: Spec, properties: InvProperties, untouched: Set[String]) = {
    val precond = weakestPrecondition(f, b, spec, properties)
Christian Müller's avatar
Christian Müller committed
159

Christian Müller's avatar
Christian Müller committed
160
161
162
163
164
    // Assume untoucheds empty
    val untouchedprecond = precond.assumeEmpty(untouched.toList)

    val z3simpednewinv = Z3BSFO.simplifyBS(untouchedprecond)

165
166
167
168
169
170
171
172
173
174
    // if informedness untouched T1 and T2 are equal anyway, so remove annotations
    // TODO: better recognition for necessarily equal
    val removedannotations = if (untouched.contains(Properties.INFNAME)) {
      val rels = spec.w.sig.preds.map(_.name)
      rels.foldRight(z3simpednewinv)((r, f) => Z3BSFO.simplifyBS(FormulaFunctions.removeAnnotation(f, r)))
    } else {
      z3simpednewinv
    }


Christian Müller's avatar
Christian Müller committed
175
    // Abstract away inner existentials
176
    val universalinv = if (removedannotations.toNegNf.hasSubFormula {
Christian Müller's avatar
Christian Müller committed
177
178
      case e:Exists => true
    }) {
179
      FOTransformers.abstractExistentials(removedannotations)
Christian Müller's avatar
Christian Müller committed
180
    } else {
181
      removedannotations
Christian Müller's avatar
Christian Müller committed
182
    }
Christian Müller's avatar
Christian Müller committed
183

Christian Müller's avatar
Christian Müller committed
184
    // Eliminate Choices
Christian Müller's avatar
Christian Müller committed
185
186
    val auxless = if (b.pred.isDefined && properties.eliminateAux) {
      FOTransformers.eliminateAuxiliaryPredicate(universalinv, b.pred.get)
Christian Müller's avatar
Christian Müller committed
187
188
189
    } else {
      universalinv
    }
Christian Müller's avatar
src    
Christian Müller committed
190

Christian Müller's avatar
Christian Müller committed
191
192
    // Eliminate Oracles
    val oless = if (properties.eliminateAux) {
193
      val oracles = spec.w.sig.oracles.map(_.name)
Christian Müller's avatar
Christian Müller committed
194
195
196
197
198
      oracles.foldRight(auxless)((b, inv) => FOTransformers.eliminateAuxiliaryPredicate(inv, b))
    } else {
      auxless
    }

Christian Müller's avatar
src    
Christian Müller committed
199
200
    // Win game
    val bless = if (properties.eliminateB) {
Christian Müller's avatar
Christian Müller committed
201
      val bs = oless.collect {
Christian Müller's avatar
cleanup    
Christian Müller committed
202
203
        case f:Fun if f.isB() => List(f.name)
      }.toSet
204
205
206
207
      if (bs.nonEmpty && !untouched.contains(Properties.INFNAME)) {
        logger.error("Trying to compute strategies for B with B,B' not necessarily equal")
      }

Christian Müller's avatar
Christian Müller committed
208
      bs.foldRight(oless)((b, inv) => FOTransformers.eliminateBPredicate(inv, b)._1)
Christian Müller's avatar
src    
Christian Müller committed
209
    } else {
Christian Müller's avatar
Christian Müller committed
210
      oless
Christian Müller's avatar
src    
Christian Müller committed
211
212
    }

213
214
215
216
217
218

    if (Utils.DEBUG_MODE) {
      val possibleAttack = Z3BSFO.debugmodelBS(Neg(bless))
      logger.trace(s"Possible attack: $possibleAttack")
    }

Christian Müller's avatar
Christian Müller committed
219
    Z3BSFO.simplifyBS(bless.simplify)
Christian Müller's avatar
Christian Müller committed
220
221
  }
}