WorkflowParser.scala 5.95 KB
Newer Older
1 2 3 4 5 6
package de.tum.workflows

import scala.util.parsing.combinator._
import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.blocks.Workflow._
7
import com.typesafe.scalalogging.LazyLogging
8

9
object WorkflowParser extends RegexParsers with LazyLogging {
10 11
  
  def addChoicePredicates(blocks: List[Block]) = {
Christian Müller's avatar
Christian Müller committed
12 13 14 15 16 17
    def addChoice(blocks: List[Block], next:Int):List[Block] = {
      blocks match {
        case ForallMayBlock(v, _, stmts) :: xs => ForallMayBlock(v, s"choice$next", stmts) :: addChoice(xs, next + 1)
        case Loop(blocks) :: xs => Loop(addChoice(blocks, next)) :: addChoice(xs, next + blocks.size)
        case x :: xs => x :: addChoice(xs, next)
        case Nil => Nil
18 19
      }
    }
Christian Müller's avatar
Christian Müller committed
20
    addChoice(blocks, 0)
21 22
  }
  
23
  def allpredicates(list: List[Block]) = {
24 25 26 27 28
    def predicatesStmt(s: Statement):Set[Fun] = {
      // collect from guard
      val inguard = s.guard.collect({
        case f:Fun => List(f)
      })
29
      // changing function
30 31 32 33
      val ch = Fun(s.fun, s.tuple)
      inguard :+ ch toSet
    }
    
34
    def predicates(b: Block): Set[Fun] = {
35 36 37
      b match {
        case Loop(blocks) => blocks flatMap(predicates _) toSet
        case b:SimpleBlock => b.steps.flatMap(predicatesStmt _) toSet
38
        case NondetChoice(l,r) => (l.flatMap(predicates) ++ r.flatMap(predicates)) toSet
39 40 41
      }
    }
    
42 43 44 45 46
    list flatMap predicates
  }
  
  def checkSig(list: List[Block]) = {
    val preds = allpredicates(list)
47 48
    
    // Filter to just the first
49
    val grouped = preds groupBy (_.name)
50
    
51 52 53 54 55 56 57 58 59 60 61 62
    // Check arities
    val checks = for ((k, list) <- grouped) yield {
      val sizes = list map (_.params.size)
      // all equal
      (k, sizes.distinct.size == 1)
    }
    
    for ((k, valid) <- checks) {
      if (!valid) {
        logger.error(s"Predicate $k appears with conflicting arities")
      }
    }
63
    
64 65 66 67 68 69 70 71 72 73
    // all valid?
    checks.forall(x => x._2)
  }
  
  def buildSig(list: List[Block]) = {
    val preds = allpredicates(list)
    
    // Filter to just the first
    val filtered = preds groupBy (_.name) map (_._2.head)
    val (oracles, rels) = filtered.partition(_.name.startsWith("O"))
Christian Müller's avatar
Christian Müller committed
74
    Signature(oracles toSet, rels toSet)
75 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
  def typeMap(typedvars: List[Var]) = {
    typedvars.map(v => v.name -> v.typ) toMap
  }
  
  def inferType(typemap: Map[String, String], v:Var) = {
    Var(v.name, typemap(v.name))
  }
  
  def inferTypes(typemap: Map[String, String], stmt: Statement) = {
    
    val newguard = stmt.guard.everywhere({
      case Fun(n, tr, params) => Fun(n, tr, params map (inferType(typemap, _))) 
    })
    val newtup = stmt.tuple.map (inferType(typemap, _))
    
    // TODO this could be improved
    stmt match {
      case s:Add => Add(newguard, stmt.fun, newtup)
      case s:Remove => Remove(newguard, stmt.fun, newtup)
    }
  }
  
  def validblock(bound: List[Var], stmts:List[Statement]) = {
    // no duplicate variables
    val distinct = bound.distinct.size == bound.size
    
    // all variable names contained in bound
    val names = bound.map(_.name)
    val unbound = stmts.flatMap(_.freeVars()).filterNot(v => names.contains(v.name))
    if (!unbound.isEmpty) {
      logger.error(s"Variables $unbound appear unbound.")
    }
    distinct && unbound.isEmpty
  }
111

112 113 114
  def IDENT = "[a-zA-Z][a-zA-Z0-9]*".r
  def VAR =  IDENT ^^ { str => Var(str) }
  def TYPEDVAR = IDENT ~ ((":" ~> IDENT)?) ^^ { case str ~ typ => if (typ.isDefined) Var(str, typ.get) else Var(str) } 
115
  
Christian Müller's avatar
Christian Müller committed
116
  // logics
117 118
  def tt = "True" ^^^ True
  def ff = "False" ^^^ False
Christian Müller's avatar
Christian Müller committed
119 120 121
  def AND = repsep(SIMPLETERM, "∧") ^^ { case ts => And.make(ts) } 
  def OR = repsep(SIMPLETERM, "∨") ^^ { case ts => Or.make(ts) } 
  def NEG = ("¬" | "!") ~ SIMPLETERM ^^ { case _ ~ t => Neg(t) } 
122
  
Christian Müller's avatar
Christian Müller committed
123 124 125 126
  // temporals
  def GLOBALLY = ("G" | "☐") ~> TERM ^^ { case t => Globally(t) }
  def FINALLY = ("F" | "♢") ~> TERM ^^ { case t => Finally(t) }
  
Christian Müller's avatar
Christian Müller committed
127
  def TUPLE = "(" ~> repsep(TYPEDVAR, ",") <~ ")" 
128 129
  def FUN = VAR ~ TUPLE ^^ { case f ~ tup => Fun(f.name, tup) }
  
Christian Müller's avatar
Christian Müller committed
130
  def SIMPLETERM = (tt | ff | FUN )
Christian Müller's avatar
Christian Müller committed
131
  def TERM:Parser[Term] = (SIMPLETERM | GLOBALLY | FINALLY | "(" ~> AND <~ ")" | "(" ~> OR <~ ")" | NEG )
132 133 134 135 136 137
  
  def ADD = TERM ~ ("→" | "->") ~ VAR ~ "+=" ~ TUPLE ^^ { case guard ~ _ ~ fun ~ _ ~ tup => Add(guard, fun.name, tup) }
  def REM = TERM ~ ("→" | "->") ~ VAR ~ "-=" ~ TUPLE ^^ { case guard ~ _ ~ fun ~ _ ~ tup => Remove(guard, fun.name, tup) }
  
  def STMT = ADD | REM
  
Christian Müller's avatar
Christian Müller committed
138 139 140
  // TODO: There could be several - one per Oracle
  def DECLASS = (FUN <~ ":") ~ TERM ^^ { case f ~ t => (f,t) } 
  
141 142 143 144 145 146 147 148 149 150 151 152
  def BLOCK = "forall" ~> ("may"?) ~ repsep(TYPEDVAR, ",") ~ (STMT+) ^? ({ 
    // all free variables contained
    case may ~ vars ~ stmts if validblock(vars, stmts) => {
      val typemap = typeMap(vars)
      val typedstmts = stmts map (inferTypes(typemap, _))
      if (may.isEmpty) {
        ForallBlock(vars, typedstmts)
      } else {
        ForallMayBlock(vars, "", typedstmts)
      }
    }
  }, t => s"$t is not a valid block (check free variables, duplicate variables, ...)" )
153
  
154
  def LOOP = "loop" ~> "{" ~> (BLOCK+) <~ "}" ^^ { case bs => Loop(bs) }
155
  def NDCHOICE = "choose" ~> "{" ~> (BLOCK+) ~ "}" ~ "{" ~ (BLOCK+) ~ "}" ^^  { case l ~ _ ~ _~ r ~ _ => NondetChoice(l,r) }
156
  
157
  def WORKFLOW = rep(BLOCK | LOOP) ^? { 
158 159 160 161 162
    case blocks if checkSig(blocks) => {
      val choiceblocks = addChoicePredicates(blocks)
      Workflow(buildSig(choiceblocks), choiceblocks) 
    }
  }
163
  
164 165 166 167 168
//  def WORKFLOW = BLOCK | (BLOCK ~ WORKFLOW) ^? { 
//    case block => { Workflow(Signature.EMPTY, List(block)) }
//    case block ~ workflow => { Workflow(Signature.EMPTY, workflow.steps) }
//  }
  
Christian Müller's avatar
Christian Müller committed
169 170
  def SPEC = 
    "Workflow" ~! WORKFLOW ~ 
Christian Müller's avatar
Christian Müller committed
171
    (("Declassify" ~> DECLASS)?) ~ 
Christian Müller's avatar
Christian Müller committed
172 173
    ("Target" ~> FUN) ~ 
    (("Causality" ~> repsep(TYPEDVAR, ","))?) ^^ { 
Christian Müller's avatar
Christian Müller committed
174
      case _ ~ w ~ decl ~ tar ~ causals => Spec(w, decl.toList, tar, causals.getOrElse(List())) 
Christian Müller's avatar
Christian Müller committed
175
    }
Christian Müller's avatar
Christian Müller committed
176
  
177
  def parseWorkflow(s: String) = parseAll(WORKFLOW, s)
Christian Müller's avatar
Christian Müller committed
178
  def parseSpec(s: String) = parseAll(SPEC, s)
179
  def parseTerm(s:String) = parseAll(TERM, s)
180
}