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

import com.typesafe.scalalogging._
import blocks._
Christian Müller's avatar
Christian Müller committed
5
6
7
8
import de.tum.niwo.foltl.{FOLTL, FOTransformers, FormulaFunctions, Properties}
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.Properties._
import de.tum.niwo.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
  def subst(f: Formula, updates: List[(String, (List[FOLTL.Var], FOLTL.Formula))], b: SimpleTSBlock): Formula = {
Christian Müller's avatar
Christian Müller committed
13
14
    // TODO: should this contain f.freeVars?
    val boundvars = f.boundVars
15
16
    updates.foldRight(f)((update, f) => {
      val (repname, (vars, form)) = update
Christian Müller's avatar
Christian Müller committed
17
18
      val fixupdate = FormulaFunctions.fixBinding(form, boundvars -- vars)

Christian Müller's avatar
example    
Christian Müller committed
19
      val res = f everywhere {
20
        case Fun(name, ind, params) if name == repname => {
Christian Müller's avatar
Christian Müller committed
21
          val renamed = fixupdate.parallelRename(vars, params)
Christian Müller's avatar
Christian Müller committed
22

23
24
25
26
27
28
29
30
          // Annotate the precondition with the index
          if (ind.isDefined) {
            FormulaFunctions.annotate(renamed, ind.get)
          } else {
            renamed
          }
        }
      }
Christian Müller's avatar
example    
Christian Müller committed
31
      res
32
33
    })
  }
34

Christian Müller's avatar
Christian Müller committed
35
36
37
  def getUpdate(s:SetStmt, spec:InvariantSpec, properties:InvProperties): Formula = {
    val frees = s.guard.freeVars -- s.tuple.toSet -- spec.ts.sig.constants
    Exists(frees.toList, s.guard).simplify
Christian Müller's avatar
Christian Müller committed
38
39
  }

Christian Müller's avatar
Christian Müller committed
40
41
42
43
44
45
46
47
  // FIXME: is this still needed?
//  def weakestPrecondition(post: Formula, outerb: SimpleTSBlock, spec: InvariantSpec, properties: InvProperties): Formula = {
//    val precond = outerb.steps.foldRight(post)((b, f) => {
//      val innerprecond = weakestPreconditionSingle(f, b, spec, properties)
//      innerprecond
//    })
//    precond
//  }
Christian Müller's avatar
Christian Müller committed
48

Christian Müller's avatar
Christian Müller committed
49
  private def weakestPrecondition(f: Formula, b:SimpleTSBlock, spec: InvariantSpec, properties: InvProperties) = {
Christian Müller's avatar
Christian Müller committed
50
51
52

    val updates = for (s <- b.steps) yield {
      s.fun -> (s.tuple, {
Christian Müller's avatar
leaders    
Christian Müller committed
53
        getUpdate(s, spec, properties)
Christian Müller's avatar
Christian Müller committed
54
55
56
      })
    }

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

Christian Müller's avatar
Christian Müller committed
60
61
    // TODO: have we proven this correct?
    val removed = FOTransformers.eliminateDoubleQuantifiers(replaced)
Christian Müller's avatar
Christian Müller committed
62
    if (Utils.DEBUG_MODE) {
Christian Müller's avatar
leaders    
Christian Müller committed
63
64
65
      val neg1 = replaced.toNegNf
      val neg2 = removed.toNegNf
      if (FormulaFunctions.collectQuantifiers(neg1) != FormulaFunctions.collectQuantifiers(neg2)) {
Christian Müller's avatar
Christian Müller committed
66
        logger.error(s"Would have removed a quantifier:\nBefore: ${neg1}\nAfter:  $neg2")
Christian Müller's avatar
Christian Müller committed
67
68
      }
    }
Christian Müller's avatar
Christian Müller committed
69

Christian Müller's avatar
Christian Müller committed
70
71
    replaced
//    removed
Christian Müller's avatar
Christian Müller committed
72
  }
Christian Müller's avatar
Christian Müller committed
73

Christian Müller's avatar
Christian Müller committed
74
  def abstractedPrecondition(f: Formula, b: SimpleTSBlock, spec: InvariantSpec, properties: InvProperties, untouched: Set[String]): Formula = {
75
    val precond = weakestPrecondition(f, b, spec, properties)
Christian Müller's avatar
Christian Müller committed
76

Christian Müller's avatar
leaders    
Christian Müller committed
77
    // Assume untouched predicates empty
Christian Müller's avatar
Christian Müller committed
78
79
80
81
    val untouchedprecond = precond.assumeEmpty(untouched.toList)

    val z3simpednewinv = Z3BSFO.simplifyBS(untouchedprecond)

Christian Müller's avatar
Christian Müller committed
82
83
    // if informedness untouched then T1 and T2 are equal anyway, so remove annotations
    // TODO: better recognition for necessarily equal, this does not work for general cases (also, this is hyperprop-specific)
84
    val removedannotations = if (untouched.contains(Properties.INFNAME)) {
Christian Müller's avatar
Christian Müller committed
85
      val rels = spec.ts.sig.preds.map(_.name)
86
87
88
89
90
      rels.foldRight(z3simpednewinv)((r, f) => Z3BSFO.simplifyBS(FormulaFunctions.removeAnnotation(f, r)))
    } else {
      z3simpednewinv
    }

Christian Müller's avatar
Christian Müller committed
91
    // Abstract away inner existentials
92
    val universalinv = if (removedannotations.toNegNf.hasSubFormula {
Christian Müller's avatar
leaders    
Christian Müller committed
93
      case _:Exists => true
Christian Müller's avatar
Christian Müller committed
94
    }) {
95
      FOTransformers.abstractExistentials(removedannotations)
Christian Müller's avatar
Christian Müller committed
96
    } else {
97
      removedannotations
Christian Müller's avatar
Christian Müller committed
98
    }
Christian Müller's avatar
Christian Müller committed
99

Christian Müller's avatar
Christian Müller committed
100
    // Eliminate As (choices/oracles)
Christian Müller's avatar
Christian Müller committed
101
    val oless = if (properties.eliminateA) {
Christian Müller's avatar
Christian Müller committed
102
103
104
105
106
107
108
109
110
      val oracles = spec.ts.sig.as.map(_.name)

      val occuringAs = oracles.filter(AUX =>
        universalinv.hasSubFormula { case Fun(AUX, _, _) => true }
      )

      occuringAs.foldRight(universalinv)((AUX, inv) =>
        FOTransformers.eliminateAuxiliaryPredicate(inv, AUX)
      )
Christian Müller's avatar
Christian Müller committed
111
    } else {
Christian Müller's avatar
Christian Müller committed
112
      universalinv
Christian Müller's avatar
Christian Müller committed
113
114
    }

Christian Müller's avatar
Christian Müller committed
115
    // Eliminate Bs (Win game)
Christian Müller's avatar
src    
Christian Müller committed
116
    val bless = if (properties.eliminateB) {
Christian Müller's avatar
Christian Müller committed
117
      val bs = spec.ts.sig.bs
Christian Müller's avatar
ineq    
Christian Müller committed
118
119

      val occuringBs = bs.filter(b =>
Christian Müller's avatar
Christian Müller committed
120
        oless.hasSubFormula { case Fun(b.name, _, _) => true }
Christian Müller's avatar
ineq    
Christian Müller committed
121
122
123
      )

      if (occuringBs.nonEmpty && !untouched.contains(Properties.INFNAME)) {
124
125
126
        logger.error("Trying to compute strategies for B with B,B' not necessarily equal")
      }

Christian Müller's avatar
ineq    
Christian Müller committed
127
      occuringBs.foldRight(oless)((b, inv) => FOTransformers.eliminateBPredicate(inv, b)._1)
Christian Müller's avatar
src    
Christian Müller committed
128
    } else {
Christian Müller's avatar
Christian Müller committed
129
      oless
Christian Müller's avatar
src    
Christian Müller committed
130
131
    }

132
133
134
135
136
137

    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
138
    Z3BSFO.simplifyBS(bless.simplify)
Christian Müller's avatar
Christian Müller committed
139
140
  }
}