Workflow.scala 5.25 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
package de.tum.niwo.blocks

import de.tum.niwo.foltl.FOLTL._
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.Utils
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)
      case s: SimpleWFBlock => s.steps.exists(stmt => s.agents.exists(a => !stmt.tuple.contains(a)))
      }
    }
    steps.exists(omitting)
  }
}
object Workflow {
  val EMPTY = Workflow(Signature.EMPTY, List())
}

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?
  }

  def checkSanity(): Boolean = {
    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
    }

    def saneoraclestmt(stmt:Statement, frees:List[Var]) = {
      // 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 {
        case b: SimpleWFBlock => {
          // 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

Christian Müller's avatar
stuff  
Christian Müller committed
107
trait SimpleWFBlock extends SimpleBlock with WFBlock {
108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136
  def agents: List[Var]
  def may: Boolean
  def pred: Option[String]

  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
  }
}

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

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