Workflow.scala 5.46 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13
package de.tum.niwo.blocks

import de.tum.niwo.foltl.FOLTL._
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.foltl.Properties

case class Workflow(sig: Signature, steps: List[WFBlock]) {
  override def toString: String = steps.mkString("\n")
  lazy val isomitting: Boolean = {

    def omitting(b:Block):Boolean = { b match {
      case l: WFLoop => l.steps.exists(omitting)
      case c: WFNondetChoice => c.left.exists(omitting) || c.right.exists(omitting)
14
      case s: SimpleWFBlock[_] => s.steps.exists(stmt => s.agents.exists(a => !stmt.tuple.contains(a)))
15 16 17 18 19 20 21 22 23
      }
    }
    steps.exists(omitting)
  }
}
object Workflow {
  val EMPTY = Workflow(Signature.EMPTY, List())
}

Christian Müller's avatar
Christian Müller committed
24
// TODO: make causals a set
25 26 27 28 29 30 31 32 33 34 35 36 37
case class NISpec(w: Workflow, declass: Map[String, (List[Var], Formula)], axioms: Formula, target: Fun, causals:List[Var]) extends Spec with LazyLogging {
  override def toString: String = {
    s"NISpec\nWorkflow:\n$w\nDeclass:$declass\nTarget:$target"
  }

  lazy val constants:Set[Var] = {
    // Treat free variables in the declassification as constants
    declass.values.flatMap {
      case (params, f) => f.freeVars -- params
    }.toSet
    // TODO: How to check for more constants?
  }

Christian Müller's avatar
Christian Müller committed
38
  def isSane(): Boolean = {
39 40 41 42 43 44 45 46 47 48 49 50 51
    var sane = true

    // TODO: check all types
    // TODO: check target types
    // TODO: check declass arities and types (o should be an Oracle relation etc)

    val ta = target.params.head
    // check declass bindings
    for ((o, (f, t)) <- declass if !t.freeVars.forall(v => f.contains(v) || (v == ta))) {
    	logger.error(s"Not all variables of the declassification condition for $o bound by the oracle")
    	sane = false
    }

52
    def saneoraclestmt(stmt:Statement[_], frees:List[Var]) = {
53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72
      // Oracle only positive
      val f = stmt.guard.toNegNf
      val noneg = !f.hasSubFormula {
        case Neg(f:Fun) if f.isOracle => true
      }
      if (!noneg) {
        logger.error(s"Found negated oracle in guard for statement $stmt")
      }
//      val allvars = !(f hasSubFormula {
//        case f:Fun if f.isOracle && f.params != frees => true
//      })
//      if (!allvars) {
//        logger.error(s"Found oracle with wrong parameters in statement $stmt")
//      }
      noneg // && allvars
    }

    // check same relation only updated once per block
    def isSane(steps:List[Block]):Boolean = {
      val sanes = steps map {
73
        case b: SimpleWFBlock[_] => {
74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
          // all predicates should only appear at most once
          val pred = w.sig.preds.find(p => b.steps.count(s => s.fun == p.name) > 1)
          pred.foreach(p =>
            logger.error(s"Predicate $p updated more than once in $b")
          )
          // if using oracle, only single stmt
          val saneoracly = if (b.isoracly) {
            b.pred.isEmpty && b.steps.size == 1 && saneoraclestmt(b.steps.head, b.agents)
          } else true
          if (!saneoracly) { logger.warn(s"Oracles used wrongly in $b") }
          pred.isEmpty && saneoracly
        }
        case WFLoop(blocks) => isSane(blocks)
        case WFNondetChoice(left, right) => isSane(left) && isSane(right)
      }
      sanes reduce (_ && _)
    }

    sane &&= isSane(w.steps)
    sane
  }

  def addKnowledge(k:Formula) = {
Christian Müller's avatar
stuff  
Christian Müller committed
97
    NISpec(w, declass, And.make(axioms, k), target, causals)
98 99 100 101 102 103 104 105 106
  }
}
object NISpec {
  val EMPTY = NISpec(Workflow.EMPTY, Map(), True, Fun("NOTHING", List()), List())
}


trait WFBlock extends Block

107
trait SimpleWFBlock[T <: SimpleWFBlock[T]] extends SimpleBlock[SimpleWFBlock[T], Statement[_]] with WFBlock {
108 109 110 111
  def agents: List[Var]
  def may: Boolean
  def pred: Option[String]

112 113
  override def update(steps: List[Statement[_]]): SimpleWFBlock[T]

114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137
  override def updating:Set[String] = {
    // This works because of the way the untouchedmap is computed.
    // As soon as that changes, fix here.
    if (isoracly) {
      super.updating + Properties.INFNAME
    } else {
      super.updating
    }
  }

  def isoracly: Boolean = {
    // before transformation
    val before = steps.exists(s => {
      s.guard.hasSubFormula {
        case f:Fun => f.isOracle
      }
    })
    // after transformation
    val after = pred.exists(name => Fun(name, agents).isOracle)

    before || after
  }
}

138
case class ForallWFBlock(agents: List[Var], steps: List[Statement[_]]) extends SimpleWFBlock[ForallWFBlock] {
139
  val may = false
Christian Müller's avatar
stuff  
Christian Müller committed
140
  override def pred:None.type = None
141
  override def toString: String = "forall " + agents.map(_.withType).mkString(",") + steps.mkString("\n  ", "\n  ", "")
142
  override def update(newsteps: List[Statement[_]]): ForallWFBlock = copy(agents, newsteps)
143
}
144 145
case class ForallMayWFBlock(agents: List[Var], choice: String, steps: List[Statement[_]]) extends SimpleWFBlock[ForallMayWFBlock] {
  type SType = Statement[_]
146 147 148
  val may = true
  override def pred:Some[String] = Some(choice)
  override def toString: String = "forall " + agents.map(_.withType).mkString(",") + " may (" + pred + ")" + steps.mkString("\n  ", "\n  ", "")
149
  override def update(newsteps: List[Statement[_]]): ForallMayWFBlock = copy(agents, choice, newsteps)
150 151
}

152
case class WFLoop(steps:List[WFBlock]) extends Loop[WFLoop, WFBlock] with WFBlock {
Christian Müller's avatar
stuff  
Christian Müller committed
153 154 155 156 157
  type B = WFBlock
  override def update(steps:List[WFBlock] = steps):WFLoop = {
    WFLoop(steps)
  }
}
158
case class WFNondetChoice(left:List[WFBlock], right:List[WFBlock]) extends NondetChoice[WFNondetChoice, WFBlock] with WFBlock {
Christian Müller's avatar
stuff  
Christian Müller committed
159 160 161 162 163
  type B = WFBlock
  override def update(left:List[WFBlock] = left, right:List[WFBlock] = right):WFNondetChoice = {
    WFNondetChoice(left, right)
  }
}