TSConverter.scala 5.58 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

Christian Müller's avatar
Christian Müller committed
26 27 28 29 30
    // Add causals to constants?
    val newsig = w.sig.copy(
      preds = w.sig.preds + Fun(INFNAME, List(spec.target.params.head)),
      constants = spec.causals.toSet ++ w.sig.constants
    )
Christian Müller's avatar
Christian Müller committed
31

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

Christian Müller's avatar
Christian Müller committed
34 35
    InvariantSpec(ts, spec.axioms, invgen(spec))
  }
Christian Müller's avatar
Christian Müller committed
36

Christian Müller's avatar
Christian Müller committed
37 38 39 40 41 42 43 44 45 46 47
  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
48 49
  }

Christian Müller's avatar
Christian Müller committed
50 51 52 53 54 55 56 57 58 59
  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
60

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

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

Christian Müller's avatar
Christian Müller committed
65 66
    // Quantify free, non-const variables
    val guard = s match {
Christian Müller's avatar
Christian Müller committed
67 68 69 70 71 72
      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
73
      case st:SetStmt => Exists(frees.toList, s.guard).simplify
Christian Müller's avatar
Christian Müller committed
74
    }
Christian Müller's avatar
Christian Müller committed
75
    SetStmt(guard, s.fun, s.tuple)
Christian Müller's avatar
Christian Müller committed
76 77 78 79 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 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129
  }

  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
    }

    // FIXME: wät? why do I have to cast this? this should be an inference error
    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
130 131 132 133 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
  // 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
168
}