Preconditions.scala 1.92 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
package de.tum.workflows

import com.typesafe.scalalogging._

import blocks._
import de.tum.workflows.foltl.FOLTL
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.FormulaFunctions._
import de.tum.workflows.foltl.FormulaFunctions

object Preconditions extends LazyLogging {

  def weakestPrecondition(f: Formula, b: SimpleBlock) = {
    // TODO: f can't be temporal yet
    val choice = b.pred.map(n => Fun(n, b.agents))

    val updates = b.steps.map(s => {
      s.fun -> (s.tuple, {
        val frees = s.guard.freeVars() -- s.tuple.toSet
Christian Müller's avatar
Christian Müller committed
20

Christian Müller's avatar
Christian Müller committed
21
22
        val list = List(s.guard) ++ choice.toList
        val guard = And.make(list)
Christian Müller's avatar
Christian Müller committed
23

Christian Müller's avatar
Christian Müller committed
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
        s match {
          case Add(_, _, _) => {
            Or(Fun(s.fun, s.tuple), Exists(frees.toList, guard)).simplify()
          }
          case Remove(_, _, _) => {
            And(Fun(s.fun, s.tuple), Forall(frees.toList, Neg(guard))).simplify()
          }
        }
      })
    }) toMap

    // Replace literals with their precondition
    f everywhere {
      case Fun(name, ind, params) if b.steps.exists(s => s.fun == name) => {
        val up = updates(name)
        val renamed = up._2.parallelRename(up._1, params)
Christian Müller's avatar
Christian Müller committed
40

Christian Müller's avatar
Christian Müller committed
41
42
        // Annotate the precondition with the index
        if (ind.isDefined) {
Christian Müller's avatar
Christian Müller committed
43
          FormulaFunctions.annotate(renamed, ind.get)
Christian Müller's avatar
Christian Müller committed
44
45
46
47
48
49
        } else {
          renamed
        }
      }
    }
  }
Christian Müller's avatar
Christian Müller committed
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

  def weakestPreconditionWithInformedness(f: Formula, b: SimpleBlock) = {

    val wp = weakestPrecondition(f, b)

    val PRED = "__inf__"
    val agent = "_i_"

    if (b.may) {

      val updates = b.steps.map(s => {
        val frees = s.guard.freeVars() -- Set(s.tuple.head)

        s match {
          case Add(_, _, _) => {
            Or(Fun(s.fun, s.tuple), Exists(frees.toList, guard)).simplify()
          }
          case Remove(_, _, _) => {
            And(Fun(s.fun, s.tuple), Forall(frees.toList, Neg(guard))).simplify()
          }
        }
      })
    }

  }
Christian Müller's avatar
Christian Müller committed
75
}