WorkflowParser.scala 6.31 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
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
79
80
    // 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
81
    Signature(oracles toSet, rels toSet)
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
  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
112
    val unbound = stmts.flatMap(_.freeVars).filterNot(v => names.contains(v.name))
Christian Müller's avatar
Christian Müller committed
113
    if (unbound.nonEmpty) {
114
115
116
117
      logger.error(s"Variables $unbound appear unbound.")
    }
    distinct && unbound.isEmpty
  }
118

119
120
121
  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) } 
122
  
Christian Müller's avatar
Christian Müller committed
123
  // logics
124
125
  def tt = "True" ^^^ True
  def ff = "False" ^^^ False
Christian Müller's avatar
Christian Müller committed
126
127
  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
128
  def NEG = ("¬" | "!") ~ SIMPLETERM ^^ { case _ ~ t => Neg(t) } 
129
  
Christian Müller's avatar
Christian Müller committed
130
  // temporals
Christian Müller's avatar
Christian Müller committed
131
132
  def GLOBALLY = ("G" | "☐") ~> TERM ^^ (t => Globally(t))
  def FINALLY = ("F" | "♢") ~> TERM ^^ (t => Finally(t))
Christian Müller's avatar
Christian Müller committed
133
  
Christian Müller's avatar
Christian Müller committed
134
  def TUPLE = "(" ~> repsep(TYPEDVAR, ",") <~ ")" 
135
136
  def FUN = VAR ~ TUPLE ^^ { case f ~ tup => Fun(f.name, tup) }
  
Christian Müller's avatar
Christian Müller committed
137
  def SIMPLETERM = (tt | ff | FUN )
138
  def TERM:Parser[Formula] = (SIMPLETERM | GLOBALLY | FINALLY | AND | OR | NEG )
139
140
141
142
143
144
  
  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
145
146
  def DECLASS = (FUN <~ ":") ~ TERM ^^ { case f ~ t => (f,t) } 
  
147
148
149
150
151
152
153
154
155
156
157
158
  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, ...)" )
159
  
Christian Müller's avatar
Christian Müller committed
160
  def LOOP = "loop" ~> "{" ~> BLOCKLIST <~ "}" ^^ (bs => Loop(bs))
161
  def NDCHOICE = "choose" ~> "{" ~> (BLOCKLIST <~ "}" <~ "{")~ (BLOCK+) <~ "}" ^^  { case l ~ r => NondetChoice(l,r) }
162
  
163
164
165
  def BLOCKLIST:Parser[List[Block]] = (BLOCK | LOOP | NDCHOICE)+
  
  def WORKFLOW = BLOCKLIST ^? { 
166
167
168
169
170
    case blocks if checkSig(blocks) => {
      val choiceblocks = addChoicePredicates(blocks)
      Workflow(buildSig(choiceblocks), choiceblocks) 
    }
  }
171
  
172
173
174
175
176
//  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
177
178
  def SPEC = 
    "Workflow" ~! WORKFLOW ~ 
Christian Müller's avatar
Christian Müller committed
179
    (("Declassify" ~> DECLASS)?) ~ 
Christian Müller's avatar
Christian Müller committed
180
181
    ("Target" ~> FUN) ~ 
    (("Causality" ~> repsep(TYPEDVAR, ","))?) ^^ { 
Christian Müller's avatar
Christian Müller committed
182
      case _ ~ w ~ decl ~ tar ~ causals => Spec(w, toMap(decl.toList), tar, causals.getOrElse(List())) 
Christian Müller's avatar
Christian Müller committed
183
    }
Christian Müller's avatar
Christian Müller committed
184
  
Christian Müller's avatar
Christian Müller committed
185
186
187
188
189
190
  def toMap(list:List[(Fun, Formula)]):Map[String, (List[Var], Formula)] = {
    list.map { l =>
      l._1.name -> (l._1.params, l._2)
    } toMap
  }
  
191
  def parseWorkflow(s: String) = parseAll(WORKFLOW, s)
Christian Müller's avatar
Christian Müller committed
192
  def parseSpec(s: String) = parseAll(SPEC, s)
193
  def parseTerm(s:String) = parseAll(TERM, s)
194
}