Preconditions.scala 5.75 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}
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
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
        case Add(guard, fun, tuple)    => Add(fixguard(guard).simplify(), fun, tuple)
Christian Müller's avatar
Christian Müller committed
44
45
46
47
48
        case Remove(guard, fun, tuple) => Remove(fixguard(guard).simplify(), fun, tuple)
      }
      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
100
      val guard = And(s.guard, con).simplify()
      //        val guard = True
Christian Müller's avatar
Christian Müller committed
101
      val frees = guard.freeVars -- s.tuple.toSet
Christian Müller's avatar
Christian Müller committed
102
103
104
105

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

Christian Müller's avatar
Christian Müller committed
114
115
116
117
118
  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
119
  def weakestPrecondition(post: Formula, outerb: SimpleBlock, spec: Spec, properties: InvProperties) = {
Christian Müller's avatar
Christian Müller committed
120
121
122

    val steps = elaborate(outerb, spec, properties)

Christian Müller's avatar
Christian Müller committed
123
    // elaborate only if non-stubborn
Christian Müller's avatar
Christian Müller committed
124
//    val steps = if (!properties.stubborn) elaborateSteps(outerb, spec) else List(outerb)
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
128
129
130
131
132
//      val innerb = if (b.isoracly) {
//        elaborateOraclyBlock(b, spec)
//      } else {
//        b
//      }
      val innerprecond = weakestPreconditionSingle(f, b, spec, properties)
Christian Müller's avatar
Christian Müller committed
133
      innerprecond
134
    })
Christian Müller's avatar
Christian Müller committed
135
136
137
    precond
  }

Christian Müller's avatar
Christian Müller committed
138
  private def weakestPreconditionSingle(f: Formula, b: SimpleBlock, spec: Spec, properties: InvProperties) = {
Christian Müller's avatar
Christian Müller committed
139
140
141
142
143

    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
144
        getUpdate(s, b, choice, spec, properties)
Christian Müller's avatar
Christian Müller committed
145
146
147
      })
    }

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

Christian Müller's avatar
Christian Müller committed
151
152
    // TODO: have we proven this correct?
    val removed = FOTransformers.eliminateDoubleQuantifiers(replaced)
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

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

Christian Müller's avatar
Christian Müller committed
160
    // Stubborn agents -> remove trace variable from choice predicate
161
    // Not neccessary anymore
Christian Müller's avatar
Christian Müller committed
162
163
164
165
166
167
168
169
170
    //    val stubprecond = if (stubborn) {
    //      precond.everywhere {
    //        case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
    //      }
    //    } else precond

    // Abstract away inner existentials - always if causal agents
    val universalinv = if (!properties.stubborn || b.isomitting) {
      FOTransformers.abstractExistentials(precond)
Christian Müller's avatar
Christian Müller committed
171
    } else {
172
      precond
Christian Müller's avatar
Christian Müller committed
173
    }
Christian Müller's avatar
Christian Müller committed
174

Christian Müller's avatar
Christian Müller committed
175
    // Abstract away auxilliaries
Christian Müller's avatar
Christian Müller committed
176
177
    val auxless = if (b.pred.isDefined && properties.eliminateAux) {
      FOTransformers.eliminateAuxiliaryPredicate(universalinv, b.pred.get)
Christian Müller's avatar
Christian Müller committed
178
179
180
    } else {
      universalinv
    }
Christian Müller's avatar
Christian Müller committed
181
    auxless.simplify()
Christian Müller's avatar
Christian Müller committed
182
183
  }
}