FOLTLTermFunctions.scala 10.3 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
2
3
package de.tum.workflows.foltl

import FOLTL._
Christian Müller's avatar
Christian Müller committed
4
import com.typesafe.scalalogging.LazyLogging
5
import de.tum.workflows.blocks.Workflow
Christian Müller's avatar
Christian Müller committed
6

7
object FormulaFunctions extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
8

9
10
  def freeVars(t: Formula) = {
    def free(t: Formula, bound: Set[Var]): Set[Var] = {
Christian Müller's avatar
Christian Müller committed
11
12
13
      t match {
        // Extractors
        // Exists, Forall
Christian Müller's avatar
Christian Müller committed
14
15
        case Quantifier(_, ps, t) => free(t, bound ++ ps)
        case UnOp(make, t)        => free(t, bound)
Christian Müller's avatar
Christian Müller committed
16
        // And, Or, Eq, Implies
Christian Müller's avatar
Christian Müller committed
17
        case BinOp(_, t1, t2)     => free(t1, bound) ++ free(t2, bound)
Christian Müller's avatar
Christian Müller committed
18

Christian Müller's avatar
Christian Müller committed
19
20
21
22
23
        //      TODO: path is not a free variable anymore
        //        case Fun(_, Some(ind), ps) => (ps.toSet -- bound) + Var(ind)
        case Fun(_, _, ps)        => (ps.toSet -- bound)
        case v: Var if !bound(v)  => Set(v)
        case x                    => Set()
Christian Müller's avatar
Christian Müller committed
24
25
26
27
28
      }
    }
    free(t, Set())
  }

29
30
  def simplify(t: Formula): Formula = {
    val simp: PartialFunction[Formula, Formula] = {
Christian Müller's avatar
Christian Müller committed
31
      // Push negation inward
Christian Müller's avatar
Christian Müller committed
32
33
34
35
36
37
38
39
      case Neg(Or(t1, t2))                    => And(Neg(t1), Neg(t2))
      case Neg(And(t1, t2))                   => Or(Neg(t1), Neg(t2))
      case Neg(Globally(t))                   => Finally(Neg(t))
      case Neg(Finally(t))                    => Globally(Neg(t))
      case Neg(Next(t))                       => Next(Neg(t))
      case Neg(Forall(vars, t))               => Exists(vars, Neg(t))
      case Neg(Exists(vars, t))               => Forall(vars, Neg(t))
      case Neg(Implies(t1, t2))               => And(t1, Neg(t2))
Christian Müller's avatar
Christian Müller committed
40
41

      // Simple laws
Christian Müller's avatar
Christian Müller committed
42
43
44
45
46
47
48
49
50
51
52
      case Neg(True)                          => False
      case Neg(False)                         => True
      case Neg(Neg(t))                        => t
      case Or(True, t)                        => True
      case Or(t, True)                        => True
      case Or(False, t)                       => t
      case Or(t, False)                       => t
      case And(False, t)                      => False
      case And(t, False)                      => False
      case And(True, t)                       => t
      case And(t, True)                       => t
Christian Müller's avatar
Christian Müller committed
53

54
      // Equivalence
Christian Müller's avatar
Christian Müller committed
55
      case Eq(t1, t2) if t1 == t2             => True
Christian Müller's avatar
Christian Müller committed
56

57
      // Double Temporals
Christian Müller's avatar
Christian Müller committed
58
59
      case Finally(Finally(t))                => Finally(t)
      case Globally(Globally(t))              => Globally(t)
Christian Müller's avatar
Christian Müller committed
60
61

      // Remove quantifiers if empty
62
      case Quantifier(_, xs, t) if xs.isEmpty => t
Christian Müller's avatar
Christian Müller committed
63
64
      case Quantifier(_, _, True)             => True
      case Quantifier(_, _, False)            => False
65

Christian Müller's avatar
Christian Müller committed
66
      // TODO: Double quantifiers
67

Christian Müller's avatar
Christian Müller committed
68
69
70
71
72
73
74
75
76
77
78
79
80
81
      // Remove variables from quantifiers if not used in the body
      //      case Quantifier(qmake, xs, t) if !(xs.toSet -- t.freeVars()).isEmpty =>
      //        qmake((xs.toSet.intersect(t.freeVars())).toList, t)
      //
      //      // Split off binops from quantifiers
      //      case Quantifier(qmake, xs, BinOp(make, t1, t2)) if (t1.freeVars().intersect(xs.toSet)).isEmpty =>
      //        make(t1, qmake(xs, t2))
      //      case Quantifier(qmake, xs, BinOp(make, t1, t2)) if (t2.freeVars().intersect(xs.toSet)).isEmpty =>
      //        make(qmake(xs, t1), t2)
    }

    val t1 = everywhere(simp, t)
    if (t == t1) t1 else simplify(t1)
  }
82
83

  def eliminateImplication(f: Formula) = {
Christian Müller's avatar
Christian Müller committed
84
85
86
87
    f everywhere {
      case Implies(f1, f2) => Or(Neg(f1), f2)
    }
  }
Christian Müller's avatar
Christian Müller committed
88

89
  def everywhere(trans: PartialFunction[Formula, Formula], t: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
90
91
92
93
94
95
    if (trans.isDefinedAt(t))
      trans(t)
    else
      t match {
        // Extractors
        case Quantifier(make, ps, t) => make(ps, everywhere(trans, t))
Christian Müller's avatar
Christian Müller committed
96
        case UnOp(make, t1)          => make(everywhere(trans, t1))
Christian Müller's avatar
Christian Müller committed
97
98
99
100
        case BinOp(make, t1, t2)     => make(everywhere(trans, t1), everywhere(trans, t2))
        case x                       => x
      }
  }
101

102
  def opsize(t: Formula): Int = {
103
104
105
106
107
108
109
110
    t match {
      // Extractors
      case Quantifier(_, ps, t) => 1 + t.opsize()
      case UnOp(_, t)           => 1 + t.opsize()
      case BinOp(_, t1, t2)     => 1 + t1.opsize() + t2.opsize()
      case x                    => 1
    }
  }
Christian Müller's avatar
Christian Müller committed
111

112
  def collect[T](combine: (T*) => T, empty: T)(coll: PartialFunction[Formula, T], t: Formula): T = {
Christian Müller's avatar
Christian Müller committed
113
114
115
116
117
118
119
120
    if (coll.isDefinedAt(t))
      coll(t)
    else
      t match {
        // Extractors
        case Quantifier(make, ps, t) => collect(combine, empty)(coll, t)
        case UnOp(make, t)           => collect(combine, empty)(coll, t)
        case BinOp(make, t1, t2)     => combine(collect(combine, empty)(coll, t1), collect(combine, empty)(coll, t2))
121
122
123
        case x                       => empty
      }
  }
124

125
  def collect[T](coll: PartialFunction[Formula, List[T]], t: Formula): List[T] = {
126
127
128
129
130
131
132
133
134
    if (coll.isDefinedAt(t))
      coll(t)
    else
      t match {
        // Extractors
        case Quantifier(make, ps, t) => collect(coll, t)
        case UnOp(make, t)           => collect(coll, t)
        case BinOp(make, t1, t2)     => List.concat(collect(coll, t1), collect(coll, t2))
        case x                       => List.empty
Christian Müller's avatar
Christian Müller committed
135
136
      }
  }
137

138
  def assumeEmpty(t: Formula, name: String) = {
Christian Müller's avatar
Christian Müller committed
139
140
141
142
    t.everywhere({
      case Fun(f, _, _) if f == name => False
    })
  }
143
144
145
146
147
148
149
  
  def assumeAllEmpty(f:Formula, names:List[String]) = {
    // Assume all workflow relations empty
    val assumers = names.map(p => (f: Formula) => assumeEmpty(f,p))
    val allempty = assumers.reduce(_ andThen _)(f)
    allempty.simplify()
  }
Christian Müller's avatar
Christian Müller committed
150

151
  def annotate(t: Formula, name: String) = {
Christian Müller's avatar
Christian Müller committed
152
153
154
155
    t.everywhere({
      case Fun(f, None, xs) => Fun(f, Some(name), xs)
    })
  }
156

157
  def annotate(t: Formula, name: String, ignore: Set[String]) = {
158
159
160
161
    t.everywhere({
      case Fun(f, None, xs) if (!(ignore contains f)) => Fun(f, Some(name), xs)
    })
  }
162

163
  def checkSanity(t: Formula) = {
Christian Müller's avatar
Christian Müller committed
164
165
166
167
168
169
    // TODO add more things, f.e. existentials
    // T1, T2 can appear freely
    val frees = t.freeVars() -- Set(Var(Properties.T1), Var(Properties.T2))
    if (!frees.isEmpty) {
      logger.warn(s"Sanity check failed: $frees appear free in the property.")
    }
170

Christian Müller's avatar
Christian Müller committed
171
172
    frees.isEmpty
  }
Christian Müller's avatar
Christian Müller committed
173
174

  def removeOTQuantifiers(f: Formula): Formula = {
Christian Müller's avatar
Christian Müller committed
175
176
177
    f.everywhere({
      case ForallOtherThan(vars, otherthan, fp) => {
        val eqs = for (x <- vars; y <- otherthan) yield {
Christian Müller's avatar
Christian Müller committed
178
          Neg(Eq(x, y))
Christian Müller's avatar
Christian Müller committed
179
        }
Christian Müller's avatar
Christian Müller committed
180
        Forall(vars, Implies(And.make(eqs), fp.removeOTQuantifiers()))
Christian Müller's avatar
Christian Müller committed
181
182
183
      }
    })
  }
Christian Müller's avatar
Christian Müller committed
184
185

  // f[newvars/vars]
Christian Müller's avatar
Christian Müller committed
186
  def parallelRename(f: Formula, vars: List[Var], newvars: List[Var]): Formula = {
Christian Müller's avatar
Christian Müller committed
187
    val repls = vars zip newvars toMap
Christian Müller's avatar
Christian Müller committed
188

Christian Müller's avatar
Christian Müller committed
189
190
    parallelRename(f, repls)
  }
Christian Müller's avatar
Christian Müller committed
191
192
193

  def parallelRename(f: Formula, repls: Map[Var, Var]): Formula = {
    f everywhere {
Christian Müller's avatar
Christian Müller committed
194
      case v: Var if repls.contains(v) => repls(v)
Christian Müller's avatar
Christian Müller committed
195
      case Fun(f, ind, params)         => Fun(f, ind, params map (p => repls.getOrElse(p, p)))
Christian Müller's avatar
Christian Müller committed
196
197
198
199
200
201
      case Quantifier(make, xs, f) => {
        val rep = repls -- (xs)
        make(xs, parallelRename(f, rep))
      }
    }
  }
Christian Müller's avatar
Christian Müller committed
202
203
204
205
206
207
208
209
210
211
212
213
214

  /**
   * Check if there exist quantifiers binding the same variable more than once
   */
  def hasDuplicateBindings(f: Formula) = {
    def boundNames(f: Formula): List[Var] = {
      f collect {
        case Quantifier(make, xs, sub) => xs ++: boundNames(sub)
      }
    }
    boundNames(f).groupBy(n => n).exists(_._2.length > 1)
  }

215
216
217
  def stripQuantifiers(f: Formula): Formula = {
    f everywhere {
      case Quantifier(_, _, fsub) => stripQuantifiers(fsub)
Christian Müller's avatar
Christian Müller committed
218
    }
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
  }
  
    def collectQuantifiersSub(f: Formula): List[(Boolean, Formula => Quantifier)] = {
    f collect {
      case Exists(xs, fsub) => List((true, (t: Formula) => (Exists(xs, t)))) ++ collectQuantifiersSub(fsub)
      case Forall(xs, fsub) => List((false, (t: Formula) => (Forall(xs, t)))) ++ collectQuantifiersSub(fsub)
      case BinOp(make, f1, f2) => {
        val q1 = collectQuantifiersSub(f1)
        val q2 = collectQuantifiersSub(f2)

        // Merge while trying to stay in BS, if possible 
        // TODO: could be improved to minimize quantifier alternations)
        // TODO: merge universals with same type by renaming 
        val ex1 = q1.takeWhile(_._1)
        val rest1 = q1.drop(ex1.size)

        val ex2 = q2.takeWhile(_._1)
        val rest2 = q2.drop(ex2.size)

        ex1 ++ ex2 ++ rest1 ++ rest2
Christian Müller's avatar
Christian Müller committed
239
240
      }
    }
241
242
243
244
245
246
247
248
  }

  def collectQuantifiers(f: Formula) = {
    collectQuantifiersSub(f).map(_._2)
  }
  
  def isBS(f:Formula) = {
    val quantprefix = collectQuantifiersSub(f.toNegNf())
249
250
    // has no forall exists in quantifier prefix
    !quantprefix.sliding(2).exists(list => !list(0)._1 && list(1)._1)
251
252
253
254
  }
  
  def toNegNf(f:Formula) = {
    val bound = if (hasDuplicateBindings(f)) {
255
//      logger.info(s"Formula binds variables more than once - renaming bindings: ${f.pretty}")
256
257
258
259
260
261
262
263
264
265
266
267
      FormulaFunctions.fixBinding(f, Set())._1
    } else f
    eliminateImplication(bound).simplify()
  }

  def generateName(base: Var, bound: Set[Var]) = {

    val chars = base.name.toCharArray()
    val (basename, start) = if (chars.last.isDigit) {
      (base.name.dropRight(1), chars.last.toInt + 1)
    } else {
      (base.name, 1)
Christian Müller's avatar
Christian Müller committed
268
    }
269
270
271
272
273
274
275
276
277
278
279
280
    val stream = Stream.from(start)

    val droppedstream = stream.dropWhile(i => bound.contains(Var(basename + i, base.typ)))

    Var(basename + droppedstream.head, base.typ)
  }

  def fixBinding(f: Formula, bound: Set[Var]): (Formula, Set[Var]) = {
    f match {
      case UnOp(make, f1) => {
        val (newf, newbounds) = fixBinding(f1, bound)
        (make(newf), newbounds)
Christian Müller's avatar
Christian Müller committed
281
      }
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
      case BinOp(make, f1, f2) => {
        val (newf1, newbound) = fixBinding(f1, bound)
        val (newf2, newbound2) = fixBinding(f2, newbound)
        (make(newf1, newf2), newbound2)
      }
      case Quantifier(make, vars, fsub) => {
        val alreadybounds = vars.filter(bound.contains(_))
        val newnames = alreadybounds.map(generateName(_, bound))
        val renamed = fsub.parallelRename(alreadybounds, newnames)
        val binding = (vars.toSet -- alreadybounds) ++ newnames

        val (fixedrename, newbound) = fixBinding(renamed, bound ++ binding)
        val newf = make(binding.toList, fixedrename)
        (newf, newbound)
      }
      // Functions, Variables
      case f => (f, bound)
Christian Müller's avatar
Christian Müller committed
299
    }
300
301
302
303
  }

  def toPrenex(f: Formula) = {
    val negnf = f.toNegNf()
Christian Müller's avatar
Christian Müller committed
304
    val (simp, boundVars) = fixBinding(negnf, Set())
305

Christian Müller's avatar
Christian Müller committed
306
307
308
    // Simplify first to push negation inward
    val quants = collectQuantifiers(simp)
    val stripped = stripQuantifiers(simp)
309

Christian Müller's avatar
Christian Müller committed
310
311
    quants.foldRight(stripped)((quant, inner) => quant(inner))
  }
Christian Müller's avatar
Christian Müller committed
312
}