Commit a9050f9d authored by Christian Müller's avatar Christian Müller
Browse files

fix nondet choice parsing and tostrings

parent 083df74b
...@@ -4,21 +4,26 @@ import de.tum.workflows.blocks._ ...@@ -4,21 +4,26 @@ import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._ import de.tum.workflows.foltl.FOLTL._
object Utils { object Utils {
def mkString[T](string: Iterable[T], start: String, mid: String, end:String) = { def mkString[T](string: Iterable[T], start: String, mid: String, end: String) = {
if (string.isEmpty) "" else string.mkString(start, mid, end) if (string.isEmpty) "" else string.mkString(start, mid, end)
} }
def collectChoices(w: Block): List[Fun] = { def collectChoices(w: Block): List[Fun] = {
w match { w match {
case Loop(steps) => steps.flatMap(collectChoices _) case Loop(steps) => steps.flatMap(collectChoices _)
case ForallMayBlock(agents, pred, _) => List(Fun(pred, agents)) case ForallMayBlock(agents, pred, _) => List(Fun(pred, agents))
case b:ForallBlock => List() case b: ForallBlock => List()
case NondetChoice(l,r) => l.flatMap(collectChoices) ++ r.flatMap(collectChoices) case NondetChoice(l, r) => l.flatMap(collectChoices) ++ r.flatMap(collectChoices)
} }
} }
def allchoices(w: Workflow) = { def allchoices(w: Workflow) = {
w.steps flatMap (collectChoices _) toSet w.steps flatMap (collectChoices _) toSet
} }
def indentLines(s: String) = {
s.lines.map(" " + _).mkString("\n")
}
} }
\ No newline at end of file
...@@ -150,10 +150,12 @@ object WorkflowParser extends RegexParsers with LazyLogging { ...@@ -150,10 +150,12 @@ object WorkflowParser extends RegexParsers with LazyLogging {
} }
}, t => s"$t is not a valid block (check free variables, duplicate variables, ...)" ) }, t => s"$t is not a valid block (check free variables, duplicate variables, ...)" )
def LOOP = "loop" ~> "{" ~> (BLOCK+) <~ "}" ^^ { case bs => Loop(bs) } def LOOP = "loop" ~> "{" ~> BLOCKLIST <~ "}" ^^ { case bs => Loop(bs) }
def NDCHOICE = "choose" ~> "{" ~> ((BLOCK+) <~ "}" <~ "{")~ (BLOCK+) <~ "}" ^^ { case l ~ r => NondetChoice(l,r) } def NDCHOICE = "choose" ~> "{" ~> (BLOCKLIST <~ "}" <~ "{")~ (BLOCK+) <~ "}" ^^ { case l ~ r => NondetChoice(l,r) }
def WORKFLOW = rep(BLOCK | LOOP | NDCHOICE) ^? { def BLOCKLIST:Parser[List[Block]] = (BLOCK | LOOP | NDCHOICE)+
def WORKFLOW = BLOCKLIST ^? {
case blocks if checkSig(blocks) => { case blocks if checkSig(blocks) => {
val choiceblocks = addChoicePredicates(blocks) val choiceblocks = addChoicePredicates(blocks)
Workflow(buildSig(choiceblocks), choiceblocks) Workflow(buildSig(choiceblocks), choiceblocks)
......
...@@ -2,6 +2,7 @@ package de.tum.workflows.blocks ...@@ -2,6 +2,7 @@ package de.tum.workflows.blocks
import de.tum.workflows.foltl.FOLTL._ import de.tum.workflows.foltl.FOLTL._
import com.typesafe.scalalogging.LazyLogging import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils
case class Signature(oracles: Set[Fun], preds: Set[Fun]) case class Signature(oracles: Set[Fun], preds: Set[Fun])
object Signature { object Signature {
...@@ -59,33 +60,31 @@ abstract class Statement { ...@@ -59,33 +60,31 @@ abstract class Statement {
} }
case class Add(guard: Term, fun: String, tuple: List[Var]) extends Statement { case class Add(guard: Term, fun: String, tuple: List[Var]) extends Statement {
override def toString() = guard + " → " + fun + " += " + tuple.mkString("(", ",", ")") override def toString() = guard + " → " + fun + " += " + tuple.mkString("(", ",", ")") + ";"
} }
case class Remove(guard: Term, fun: String, tuple: List[Var]) extends Statement { case class Remove(guard: Term, fun: String, tuple: List[Var]) extends Statement {
override def toString() = guard + " → " + fun + " -= " + tuple.mkString("(", ",", ")") override def toString() = guard + " → " + fun + " -= " + tuple.mkString("(", ",", ")") + ";"
} }
case class ForallBlock(agents: List[Var], steps: List[Statement]) extends SimpleBlock { case class ForallBlock(agents: List[Var], steps: List[Statement]) extends SimpleBlock {
val may = false val may = false
override def toString() = "forall " + agents.map(_.withType).mkString(",") + steps.mkString("\n ", ";\n ", "") override def toString() = "forall " + agents.map(_.withType).mkString(",") + steps.mkString("\n ", "\n ", "")
override def pred() = None override def pred() = None
} }
case class ForallMayBlock(agents: List[Var], choice: String, steps: List[Statement]) extends SimpleBlock { case class ForallMayBlock(agents: List[Var], choice: String, steps: List[Statement]) extends SimpleBlock {
val may = true val may = true
override def toString() = "forall " + agents.map(_.withType).mkString(",") + " may (" + pred + ")" + steps.mkString("\n ", ";\n ", "") override def toString() = "forall " + agents.map(_.withType).mkString(",") + " may (" + pred + ")" + steps.mkString("\n ", "\n ", "")
override def pred() = Some(choice) override def pred() = Some(choice)
} }
case class Loop(steps: List[Block]) extends Block { case class Loop(steps: List[Block]) extends Block {
override def toString() = { override def toString() = {
// indentation // indentation
val s = steps.map(_.toString().lines.mkString(" ", "\n ", "")) "loop(*)\n" + Utils.indentLines(steps.mkString("\n"))
"loop(*)\n" + s.mkString(";\n")
} }
} }
case class NondetChoice(left: List[Block], right: List[Block]) extends Block { case class NondetChoice(left: List[Block], right: List[Block]) extends Block {
override def toString() = { override def toString() = {
// TODO: indentation "choose {\n" + Utils.indentLines(left.mkString("\n")) + "\n} {\n" + Utils.indentLines(right.mkString("\n")) + "\n}\n"
"or\n" + left.toString() + "\n" + right.toString() + "\n"
} }
} }
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment