TSConverter.scala 6.04 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
package de.tum.niwo.blocks
Christian Müller's avatar
Christian Müller committed
2 3 4 5 6

import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.Properties.{INFNAME, T1, T2}
Christian Müller's avatar
Christian Müller committed
7
import de.tum.niwo.invariants.{InvProperties, InvariantGenerator}
Christian Müller's avatar
Christian Müller committed
8 9 10

object TSConverter extends LazyLogging {

11
  // TODO: introduce more than one informedness depending on type?
Christian Müller's avatar
Christian Müller committed
12 13 14 15 16 17
  // TODO: move stubbornness flag out of properties
  def toInvariantSpec(spec:NISpec,
                      properties:InvProperties,
                      invgen:NISpec => Formula
                     ):InvariantSpec = {
    val w = spec.w
Christian Müller's avatar
Christian Müller committed
18 19

    // Elaborate all statements to Hyperproperty updates with informedness depending on stubbornness
Christian Müller's avatar
Christian Müller committed
20 21
    val elaboratefun = (b:SimpleWFBlock[_]) => elaborate(b, spec, properties)
    val elaborated = everywhere(w.steps, elaboratefun)
Christian Müller's avatar
Christian Müller committed
22

23 24

    // Add causals to constants, add informedness for causal agents
25 26 27
    val newsig = if (!properties.stubborn) {
      w.sig.copy(
        preds = w.sig.preds + Fun(INFNAME, List(spec.target.params.head)),
28
        constants = spec.causals.toSet union spec.constants union w.sig.constants
29 30
      )
    } else {
31 32 33
      w.sig.copy (
        constants = spec.constants union w.sig.constants
      )
34
    }
Christian Müller's avatar
Christian Müller committed
35

Christian Müller's avatar
Christian Müller committed
36 37 38 39 40
    // Map WFLoop/Nondet to TSLoop/TSNondet
    // Map Add/Remove statements to SetStmt
    val steps = elaborated.map(s => toTSBlock(s)(newsig, properties))


Christian Müller's avatar
Christian Müller committed
41
    val ts = TransitionSystem(newsig, steps)
Christian Müller's avatar
Christian Müller committed
42

Christian Müller's avatar
Christian Müller committed
43
    InvariantSpec(ts, spec.axioms, invgen(spec), spec.universe)
Christian Müller's avatar
Christian Müller committed
44
  }
Christian Müller's avatar
Christian Müller committed
45

Christian Müller's avatar
Christian Müller committed
46
  def everywhere(list: List[WFBlock],
Christian Müller's avatar
Christian Müller committed
47 48 49 50 51 52 53 54 55 56
                         update: SimpleWFBlock[_] => List[SimpleWFBlock[_]]):List[WFBlock] = {
    list match {
      case (l:WFLoop) :: xs => l.update(everywhere(l.steps, update)) :: everywhere(xs, update)
      case (nd:WFNondetChoice) :: xs => nd.update(
        everywhere(nd.left, update),
        everywhere(nd.right, update)
      ) :: everywhere(xs, update)
      case (s:SimpleWFBlock[_]) :: xs => update(s) ++ everywhere(xs, update)
      case Nil => Nil
    }
Christian Müller's avatar
Christian Müller committed
57 58
  }

Christian Müller's avatar
Christian Müller committed
59 60 61 62 63 64 65 66 67 68
  private def toTSBlock(b:WFBlock)(implicit sig:Signature, properties:InvProperties):TSBlock = {
    b match {
      case WFLoop(steps) =>
        TSLoop(steps.map(toTSBlock))
      case WFNondetChoice(left, right) =>
        TSNondetChoice(left.map(toTSBlock), right.map(toTSBlock))
      case s:SimpleWFBlock[_] =>
        SimpleTSBlock(s.steps.map(s => toSetStmt(s, sig, properties)))
    }
  }
Christian Müller's avatar
Christian Müller committed
69

Christian Müller's avatar
Christian Müller committed
70
  def toSetStmt(s:Statement[_], sig:Signature, properties:InvProperties): SetStmt = {
Christian Müller's avatar
Christian Müller committed
71

Christian Müller's avatar
Christian Müller committed
72
    val frees = (s.guard.freeVars -- s.tuple.toSet) -- sig.constants
Christian Müller's avatar
Christian Müller committed
73

Christian Müller's avatar
Christian Müller committed
74 75
    // Quantify free, non-const variables
    val guard = s match {
Christian Müller's avatar
Christian Müller committed
76 77 78 79 80 81
      case Add(_, _, _) => {
        Or(Fun(s.fun, s.tuple), Exists(frees.toList, s.guard)).simplify
      }
      case Remove(_, _, _) => {
        And(Fun(s.fun, s.tuple), Forall(frees.toList, Neg(s.guard))).simplify
      }
Christian Müller's avatar
Christian Müller committed
82
      case st:SetStmt => Exists(frees.toList, s.guard).simplify
Christian Müller's avatar
Christian Müller committed
83
    }
Christian Müller's avatar
Christian Müller committed
84
    SetStmt(guard, s.fun, s.tuple)
Christian Müller's avatar
Christian Müller committed
85 86 87 88 89 90 91 92 93 94 95
  }

  def elaborate(block: SimpleWFBlock[_], spec:NISpec, properties:InvProperties): List[SimpleWFBlock[_]] = {
    val stepOne = elaborateSteps(block, spec, properties)
    stepOne map { b =>  elaborateOraclyBlock(b, spec) }
  }

  private def elaborateSteps(b: SimpleWFBlock[_], spec: NISpec, properties: InvProperties):List[SimpleWFBlock[_]] = {

    val guardfix = if (!b.isoracly && b.pred.isDefined) {
      // is "normal" may block
Christian Müller's avatar
Christian Müller committed
96

Christian Müller's avatar
Christian Müller committed
97
      val choice = Fun(b.pred.get, b.agents)
Christian Müller's avatar
Christian Müller committed
98
      val first = b.agents.head
Christian Müller's avatar
Christian Müller committed
99

100 101 102
      val informableTypes = spec.target.params.head.typ :: spec.causals.map(_.typ)

      if (informableTypes.contains(first.typ)) {
Christian Müller's avatar
Christian Müller committed
103 104
        for (s <- b.steps) yield {
          val inner = if (properties.stubborn) {
Christian Müller's avatar
Christian Müller committed
105 106 107 108 109
            choice.in(T1)
          } else {
            val inf = Fun(INFNAME, List(b.agents.head))
            Or(And(Neg(inf.in(T1)), choice.in(T1)), And(inf.in(T1), choice))
          }
Christian Müller's avatar
Christian Müller committed
110 111
          val newguard = And(s.guard, inner)
          s.update(guard = newguard)
Christian Müller's avatar
Christian Müller committed
112
        }
Christian Müller's avatar
Christian Müller committed
113 114 115
      } else {
        logger.warn(s"First agent of tuple in block: $b can not be informed - skipping introduction of choice predicate")
        b.steps
Christian Müller's avatar
Christian Müller committed
116 117 118 119 120
      }
    } else {
      b.steps
    }

121
    // FIXME: wät? why do I have to cast this? this should be correctly inferred by the compiler
Christian Müller's avatar
Christian Müller committed
122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141
    val newb:Any = b.update(guardfix)

    // for causality, add informedness updates
    val list = if (properties.stubborn) {
      List(newb)
    } else {
      val newsteps = for (
        stmt <- b.steps
        if spec.causals.map(_.typ).contains(stmt.tuple.head.typ) ||
          stmt.tuple.head.typ == spec.target.params.head.typ) yield {
        val fun = Fun(stmt.fun, stmt.tuple)
        // TODO
        val guard = Neg(Equiv(fun.in(T1), fun.in(T2)))
        ForallWFBlock(stmt.tuple, List(Add(guard, INFNAME, List(stmt.tuple.head))))
      }
      newb :: newsteps
    }
    list.asInstanceOf[List[SimpleWFBlock[_]]]
  }

Christian Müller's avatar
Christian Müller committed
142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
  // For oracly blocks, remove O from guard and add to ForallMay choice predicate
  private def elaborateOraclyBlock(b: SimpleWFBlock[_], spec: NISpec) = {
    if (b.isoracly) {

      val stmt = b.steps.head // can only be one

      def findOracle(f: Formula) = {
        f.collect {
          case f: Fun if f.isOracle => List(f.name)
        }
      }
      val oracles = findOracle(stmt.guard)
      val name = oracles.head

      if (oracles.size != 1) {
        logger.error(s"Found oracly block $b with more than one oracle")
      }

      val choice = Fun(name, b.agents)

      def fixguard(f: Formula, choice:Fun) = {
        val nooracles = f.everywhere {
          case f: Fun if f.isOracle => True
        }

        val decl = spec.declass.getOrElse(name, (List(), False))._2
        // FIXME: substitutions?
        // FIXME: decl in T2?
        And(nooracles, Or(And(decl.in(T1), choice.in(T1)), And(Neg(decl.in(T1)), choice)))
      }

      val newstmt = stmt match {
        case Add(guard, fun, tuple)    => Add(fixguard(guard, choice).simplify, fun, tuple)
        case Remove(guard, fun, tuple) => Remove(fixguard(guard, choice).simplify, fun, tuple)
      }
      ForallMayWFBlock(b.agents, name, List(newstmt))
    } else b
  }
Christian Müller's avatar
Christian Müller committed
180
}