TSConverter.scala 5.7 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 {

Christian Müller's avatar
Christian Müller committed
11 12 13 14 15 16
  // 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
17 18

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

    // Map WFLoop/Nondet to TSLoop/TSNondet
    // Map Add/Remove statements to SetStmt
Christian Müller's avatar
Christian Müller committed
24
    val steps = elaborated.map(s => toTSBlock(s)(w.sig, properties))
Christian Müller's avatar
Christian Müller committed
25

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

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

Christian Müller's avatar
Christian Müller committed
38 39
    InvariantSpec(ts, spec.axioms, invgen(spec))
  }
Christian Müller's avatar
Christian Müller committed
40

Christian Müller's avatar
Christian Müller committed
41 42 43 44 45 46 47 48 49 50 51
  private def everywhere(list: List[WFBlock],
                         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
52 53
  }

Christian Müller's avatar
Christian Müller committed
54 55 56 57 58 59 60 61 62 63
  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
64

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

Christian Müller's avatar
Christian Müller committed
67
    val frees = s.guard.freeVars -- s.tuple.toSet -- sig.constants
Christian Müller's avatar
Christian Müller committed
68

Christian Müller's avatar
Christian Müller committed
69 70
    // Quantify free, non-const variables
    val guard = s match {
Christian Müller's avatar
Christian Müller committed
71 72 73 74 75 76
      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
77
      case st:SetStmt => Exists(frees.toList, s.guard).simplify
Christian Müller's avatar
Christian Müller committed
78
    }
Christian Müller's avatar
Christian Müller committed
79
    SetStmt(guard, s.fun, s.tuple)
Christian Müller's avatar
Christian Müller committed
80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
  }

  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
      val choice = Fun(b.pred.get, b.agents)

      val fixed = for (s <- b.steps) yield {
        val first = s.tuple.head
        val inner = if (first.typ == spec.target.params.head.typ) {
          if (properties.stubborn) {
            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))
          }
        } else {
          choice
        }
        val newguard = And(s.guard, inner)
        s.update(guard = newguard)
      }
      fixed
    } else {
      b.steps
    }

113
    // 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
114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133
    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
134 135 136 137 138 139 140 141 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
  // 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
172
}