Commit be0c687b authored by ezal's avatar ezal

adding nondeterministic choice; incompelte

parent 24497f1d
...@@ -9,11 +9,12 @@ object Utils { ...@@ -9,11 +9,12 @@ object Utils {
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)
} }
} }
......
...@@ -31,10 +31,11 @@ object WorkflowParser extends RegexParsers with LazyLogging { ...@@ -31,10 +31,11 @@ object WorkflowParser extends RegexParsers with LazyLogging {
inguard :+ ch toSet inguard :+ ch toSet
} }
def predicates(b: Block):Set[Fun] = { def predicates(b: Block): Set[Fun] = {
b match { b match {
case Loop(blocks) => blocks flatMap(predicates _) toSet case Loop(blocks) => blocks flatMap(predicates _) toSet
case b:SimpleBlock => b.steps.flatMap(predicatesStmt _) toSet case b:SimpleBlock => b.steps.flatMap(predicatesStmt _) toSet
case NondetChoice(l,r) => (l.flatMap(predicates) ++ r.flatMap(predicates)) toSet
} }
} }
...@@ -151,6 +152,7 @@ object WorkflowParser extends RegexParsers with LazyLogging { ...@@ -151,6 +152,7 @@ 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" ~> "{" ~> (BLOCK+) <~ "}" ^^ { case bs => Loop(bs) }
def NDCHOICE = "choose" ~> "{" ~> (BLOCK+) ~ "}" ~ "{" ~ (BLOCK+) ~ "}" ^^ { case l ~ _ ~ _~ r ~ _ => NondetChoice(l,r) }
def WORKFLOW = rep(BLOCK | LOOP) ^? { def WORKFLOW = rep(BLOCK | LOOP) ^? {
case blocks if checkSig(blocks) => { case blocks if checkSig(blocks) => {
...@@ -159,6 +161,11 @@ object WorkflowParser extends RegexParsers with LazyLogging { ...@@ -159,6 +161,11 @@ object WorkflowParser extends RegexParsers with LazyLogging {
} }
} }
// def WORKFLOW = BLOCK | (BLOCK ~ WORKFLOW) ^? {
// case block => { Workflow(Signature.EMPTY, List(block)) }
// case block ~ workflow => { Workflow(Signature.EMPTY, workflow.steps) }
// }
def SPEC = def SPEC =
"Workflow" ~! WORKFLOW ~ "Workflow" ~! WORKFLOW ~
(("Declassify" ~> DECLASS)?) ~ (("Declassify" ~> DECLASS)?) ~
......
...@@ -73,10 +73,16 @@ case class ForallMayBlock(agents: List[Var], pred: String, steps: List[Statement ...@@ -73,10 +73,16 @@ case class ForallMayBlock(agents: List[Var], pred: String, steps: List[Statement
} }
case class Loop(steps: List[Block]) extends Block { case class Loop(steps: List[Block]) extends Block {
val agents = List()
override def toString() = { override def toString() = {
// indentation // indentation
val s = steps.map(_.toString().lines.mkString(" ", "\n ", "")) val s = steps.map(_.toString().lines.mkString(" ", "\n ", ""))
"loop(*)\n" + s.mkString(";\n") "loop(*)\n" + s.mkString(";\n")
} }
} }
case class NondetChoice(left: List[Block], right: List[Block]) extends Block {
override def toString() = {
// TODO: indentation
"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