WorkflowParser.scala 6.74 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

Christian Müller's avatar
Christian Müller committed
9
object WorkflowParser extends RegexParsers with PackratParsers with LazyLogging {
10 11
  
  def addChoicePredicates(blocks: List[Block]) = {
Christian Müller's avatar
Christian Müller committed
12 13 14 15 16 17 18
    var i = -1; // start at 0
    def next() = {
      i = i + 1
      i
    }
    
    def addChoice(blocks: List[Block], next:() => Int):List[Block] = {
Christian Müller's avatar
Christian Müller committed
19
      blocks match {
Christian Müller's avatar
Christian Müller committed
20 21 22
        case ForallMayBlock(v, _, stmts) :: xs => ForallMayBlock(v, s"choice${next()}", stmts) :: addChoice(xs, next)
        case Loop(blocks) :: xs => Loop(addChoice(blocks, next)) :: addChoice(xs, next)
        case NondetChoice(left, right) :: xs => NondetChoice(addChoice(left, next), addChoice(right, next)) :: addChoice(xs, next)
Christian Müller's avatar
Christian Müller committed
23 24
        case x :: xs => x :: addChoice(xs, next)
        case Nil => Nil
25 26
      }
    }
Christian Müller's avatar
Christian Müller committed
27
    addChoice(blocks, next)
28 29
  }
  
30
  def allpredicates(list: List[Block]) = {
31 32 33 34 35
    def predicatesStmt(s: Statement):Set[Fun] = {
      // collect from guard
      val inguard = s.guard.collect({
        case f:Fun => List(f)
      })
36
      // changing function
37 38 39 40
      val ch = Fun(s.fun, s.tuple)
      inguard :+ ch toSet
    }
    
41
    def predicates(b: Block): Set[Fun] = {
42
      b match {
Christian Müller's avatar
Christian Müller committed
43 44
        case Loop(blocks) => blocks flatMap predicates toSet
        case b:SimpleBlock => b.steps.flatMap(predicatesStmt) toSet
45
        case NondetChoice(l,r) => (l.flatMap(predicates) ++ r.flatMap(predicates)) toSet
46 47 48
      }
    }
    
49 50 51 52 53
    list flatMap predicates
  }
  
  def checkSig(list: List[Block]) = {
    val preds = allpredicates(list)
54 55
    
    // Filter to just the first
56
    val grouped = preds groupBy (_.name)
57
    
58 59 60 61 62 63 64 65 66 67 68 69
    // 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")
      }
    }
70
    
71 72 73 74 75 76 77 78
    // all valid?
    checks.forall(x => x._2)
  }
  
  def buildSig(list: List[Block]) = {
    val preds = allpredicates(list)
    
    // Filter to just the first
79 80 81 82
    val filtered = preds groupBy (_.name) map (_._2.head) toSet
    val oracles = filtered.filter(_.isOracle())
    val bs = filtered.filter(_.isB())
    val rels = filtered -- oracles -- bs
Christian Müller's avatar
ineq  
Christian Müller committed
83
    Signature(oracles, bs, rels)
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
  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)
Christian Müller's avatar
Christian Müller committed
114
    val unbound = stmts.flatMap(_.freeVars).filterNot(v => names.contains(v.name))
Christian Müller's avatar
Christian Müller committed
115
    if (unbound.nonEmpty) {
116 117 118 119
      logger.error(s"Variables $unbound appear unbound.")
    }
    distinct && unbound.isEmpty
  }
120

121 122 123
  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) } 
124
  
Christian Müller's avatar
Christian Müller committed
125
  // logics
126 127
  def tt = "True" ^^^ True
  def ff = "False" ^^^ False
Christian Müller's avatar
Christian Müller committed
128 129
  def AND = "(" ~> (repsep(TERM, "∧") | repsep(TERM, "&&")) <~ ")" ^^ (ts => And.make(ts))
  def OR = "(" ~> (repsep(TERM, "∨") | repsep(TERM, "||")) <~ ")" ^^ (ts => Or.make(ts))
Christian Müller's avatar
Christian Müller committed
130 131 132
  def NEG = ("¬" | "!") ~ SIMPLETERM ^^ { case _ ~ t => Neg(t) }
  def IMPLIES = "(" ~> TERM ~ "⟹" ~ (TERM <~ ")") ^^ { case t1 ~ _ ~ t2 => Implies(t1, t2) }

Christian Müller's avatar
Christian Müller committed
133
  // temporals
Christian Müller's avatar
Christian Müller committed
134 135
  def GLOBALLY = ("G" | "☐") ~> TERM ^^ (t => Globally(t))
  def FINALLY = ("F" | "♢") ~> TERM ^^ (t => Finally(t))
Christian Müller's avatar
Christian Müller committed
136
  
Christian Müller's avatar
Christian Müller committed
137
  def TUPLE = "(" ~> repsep(TYPEDVAR, ",") <~ ")" 
138
  def FUN = VAR ~ TUPLE ^^ { case f ~ tup => Fun(f.name, tup) }
Christian Müller's avatar
Christian Müller committed
139 140 141 142 143 144 145

  def EXISTS = "∃" ~> (repsep(TYPEDVAR, ",") <~ ("."?)) ~ TERM ^^ { case vs ~ t => Exists(vs, t) }
  def FORALL = "∀" ~> (repsep(TYPEDVAR, ",") <~ ("."?)) ~ TERM ^^ { case vs ~ t => Forall(vs, t) }
  def QUANTIFIER = EXISTS | FORALL

  def SIMPLETERM = (tt | ff | FUN)
  lazy val TERM:PackratParser[Formula] = (AND | OR | IMPLIES | NEG | SIMPLETERM | GLOBALLY | FINALLY | QUANTIFIER)
146 147 148 149 150 151
  
  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
152 153
  def DECLASS = (FUN <~ ":") ~ TERM ^^ { case f ~ t => (f,t) } 
  
154 155 156 157 158 159 160 161 162 163 164 165
  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, ...)" )
166
  
Christian Müller's avatar
Christian Müller committed
167
  def LOOP = "loop" ~> "{" ~> BLOCKLIST <~ "}" ^^ (bs => Loop(bs))
168
  def NDCHOICE = "choose" ~> "{" ~> (BLOCKLIST <~ "}" <~ "{")~ (BLOCK+) <~ "}" ^^  { case l ~ r => NondetChoice(l,r) }
169
  
170 171 172
  def BLOCKLIST:Parser[List[Block]] = (BLOCK | LOOP | NDCHOICE)+
  
  def WORKFLOW = BLOCKLIST ^? { 
173 174 175 176 177
    case blocks if checkSig(blocks) => {
      val choiceblocks = addChoicePredicates(blocks)
      Workflow(buildSig(choiceblocks), choiceblocks) 
    }
  }
178
  
179 180 181 182 183
//  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
184 185
  def SPEC = 
    "Workflow" ~! WORKFLOW ~ 
Christian Müller's avatar
Christian Müller committed
186
    (("Declassify" ~> DECLASS)?) ~ 
Christian Müller's avatar
Christian Müller committed
187 188
    ("Target" ~> FUN) ~ 
    (("Causality" ~> repsep(TYPEDVAR, ","))?) ^^ { 
Christian Müller's avatar
Christian Müller committed
189
      case _ ~ w ~ decl ~ tar ~ causals => NISpec(w, toMap(decl.toList), tar, causals.getOrElse(List()))
Christian Müller's avatar
Christian Müller committed
190
    }
191
  
Christian Müller's avatar
Christian Müller committed
192 193 194 195 196 197
  def toMap(list:List[(Fun, Formula)]):Map[String, (List[Var], Formula)] = {
    list.map { l =>
      l._1.name -> (l._1.params, l._2)
    } toMap
  }
  
198
  def parseWorkflow(s: String) = parseAll(WORKFLOW, s)
199
  def parseSpec(s: String) = parseAll(SPEC, s)
200
  def parseTerm(s:String) = parseAll(TERM, s)
201
}