WorkflowParser.scala 4.37 KB
Newer Older
1 2 3 4 5
package de.tum.niwo.parser

import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._
Christian Müller's avatar
Christian Müller committed
6
import ParserUtils._
7 8 9

import scala.util.parsing.combinator._

10
object WorkflowParser extends RegexParsers with PackratParsers with FormulaParser with LazyLogging {
11
  
Christian Müller's avatar
Christian Müller committed
12
  private def addChoicePredicates(blocks: List[WFBlock]): (List[WFBlock], Set[Fun]) = {
13 14 15 16 17
    var i = -1; // start at 0
    def next() = {
      i = i + 1
      i
    }
Christian Müller's avatar
Christian Müller committed
18
    var list:List[Fun] = Nil
19 20 21 22

    def addChoice(blocks: List[WFBlock], next:() => Int):List[WFBlock] = {
      blocks match {
        case ForallMayWFBlock(v, _, stmts) :: xs =>
Christian Müller's avatar
Christian Müller committed
23 24 25 26 27
          val name = s"choice${next()}"
          list = Fun(name, v) :: list
          ForallMayWFBlock(v, name, stmts) :: addChoice(xs, next)
        case WFLoop(bl) :: xs =>
          WFLoop(addChoice(bl, next)) :: addChoice(xs, next)
28 29 30 31 32 33
        case WFNondetChoice(left, right) :: xs =>
          WFNondetChoice(addChoice(left, next), addChoice(right, next)) :: addChoice(xs, next)
        case x :: xs => x :: addChoice(xs, next)
        case Nil => Nil
      }
    }
Christian Müller's avatar
Christian Müller committed
34
    (addChoice(blocks, next), list.toSet)
35 36
  }

37
  private def validblock(bound: List[Var], stmts:List[Statement[_]]): Boolean = {
38 39 40 41 42 43 44 45 46 47 48 49
    // 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.nonEmpty) {
      logger.error(s"Variables $unbound appear unbound.")
    }
    distinct && unbound.isEmpty
  }

Christian Müller's avatar
Christian Müller committed
50 51 52 53
  private def ADD: Parser[Add] = TERM ~ ("→" | "->") ~ VAR ~ "+=" ~ TUPLE ^^ {
    case guard ~ _ ~ fun ~ _ ~ tup => Add(guard, fun.name, tup) }
  private def REM: Parser[Remove] = TERM ~ ("→" | "->") ~ VAR ~ "-=" ~ TUPLE ^^ {
    case guard ~ _ ~ fun ~ _ ~ tup => Remove(guard, fun.name, tup) }
54

55
  private def STMT: Parser[Statement[_]] = ADD | REM
56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78

  private def DECLASS: Parser[(Fun, Formula)] = (FUN <~ ":") ~ TERM ^^ { case f ~ t => (f,t) }

  private def BLOCK: Parser[WFBlock] = "forall" ~> ("may"?) ~ repsep(TYPEDVAR, ",") ~ (STMT+) ^? ({
    // all free variables contained
    case may ~ vars ~ stmts if validblock(vars, stmts) => {
      // add quantified variables to typemap
      val typemap = typeMap(vars ++ stmts.flatMap(_.guard.boundVars))
      val typedstmts = stmts map (inferTypes(typemap, _))
      if (may.isEmpty) {
        ForallWFBlock(vars, typedstmts)
      } else {
        ForallMayWFBlock(vars, "", typedstmts)
      }
    }
  }, t => s"$t is not a valid block (check free variables, duplicate variables, ...)" )

  private def LOOP: Parser[WFLoop] = "loop" ~> "{" ~> BLOCKLIST <~ "}" ^^ (bs => WFLoop(bs))
  private def NDCHOICE: Parser[WFNondetChoice] = "choose" ~> "{" ~> (BLOCKLIST <~ "}" <~ "{")~ (BLOCK+) <~ "}" ^^  { case l ~ r => WFNondetChoice(l,r) }

  private def BLOCKLIST: Parser[List[WFBlock]] = (BLOCK | LOOP | NDCHOICE)+

  private def WORKFLOW: Parser[Workflow] = BLOCKLIST ^? {
Christian Müller's avatar
Christian Müller committed
79
    case blocks if {
Christian Müller's avatar
Christian Müller committed
80
      val (choiceblocks, choicepredicates) = addChoicePredicates(blocks)
Christian Müller's avatar
Christian Müller committed
81
      val predicates = allpredicates(choiceblocks)
Christian Müller's avatar
Christian Müller committed
82
      val sig = buildSig(predicates ++ choicepredicates)
Christian Müller's avatar
Christian Müller committed
83 84
      checkSig(sig, predicates)
    } => {
Christian Müller's avatar
Christian Müller committed
85
      val (choiceblocks, choicepredicates) = addChoicePredicates(blocks)
Christian Müller's avatar
Christian Müller committed
86
      val predicates = allpredicates(choiceblocks)
Christian Müller's avatar
Christian Müller committed
87
      val sig = buildSig(predicates ++ choicepredicates)
Christian Müller's avatar
Christian Müller committed
88
      Workflow(sig, choiceblocks)
89 90 91 92 93
    }
  }

  private def SPEC: Parser[NISpec] =
    "Workflow" ~! WORKFLOW ~ 
Christian Müller's avatar
Christian Müller committed
94 95 96
    (("Declassify" ~> DECLASS)?) ~
    (("Invariant" ~> repsep(TERM, ","))?) ~
    ("Target" ~> FUN) ~
97
    (("Causality" ~> repsep(TYPEDVAR, ","))?) ^^ { 
Christian Müller's avatar
Christian Müller committed
98 99 100 101 102 103 104 105 106
      case _ ~ w ~ decl ~ inv ~ tar ~ causals => {
        // temporary typing sig
        val sig = w.sig.copy(w.sig.as,
          w.sig.constas,
          w.sig.bs,
          w.sig.preds,
          w.sig.constants ++ tar.params ++ causals.toList.flatten)
        NISpec(w, toMap(decl.toList), True, tar, causals.getOrElse(List()), inv.map(list => And.make(list.map(inferFormulaTypes(sig, _)))))
      }
107 108 109 110 111
    }

  private def toMap(list:List[(Fun, Formula)]):Map[String, (List[Var], Formula)] = {
    list.map { l =>
      l._1.name -> (l._1.params, l._2)
112
    }.toMap
113 114 115 116 117
  }
  
  def parseWorkflow(s: String): ParseResult[Workflow] = parseAll(WORKFLOW, s)
  def parseSpec(s: String): ParseResult[NISpec] = parseAll(SPEC, s)
}