Commit 18857293 authored by Christian Müller's avatar Christian Müller

add types to parser and variables

parent 23439d04
......@@ -7,7 +7,7 @@ forallmay x,p
forallmay x,p,r
(Ass(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
loop {
forall xa,xb,p,r (A(x1,p) ∧ Review(xb,p,r)) -> Read += (xa,xb,p,r)
forall xa,xb,p,r (A(xa,p) ∧ Review(xb,p,r)) -> Read += (xa,xb,p,r)
forallmay x,p,r (A(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
}
......
......@@ -24,7 +24,7 @@ object Main extends App with LazyLogging {
generate(name, spec)
}
def write(name: String, prop:Term) {
def write(name: String, prop:String) {
val file = new File(name)
val writer = new PrintWriter(file)
writer.print(prop)
......@@ -46,14 +46,14 @@ object Main extends App with LazyLogging {
val quantfree = LTL.eliminateUniversals(res, agents)
val ltlprop = LTL.eliminatePredicates(quantfree)
write(s"${name}_${agents.size}agents.ltl", ltlprop)
write(s"${name}_${agents.size}agents.ltl", ltlprop.toString())
write(s"${name}_${agents.size}agents.ppltl", ltlprop.pretty())
logger.info(s"Written all files for $name")
}
def generate(name: String, spec:Spec) {
logger.info(s"Encoding Workflow:\n$spec.w")
logger.info(s"Encoding Spec:\n$spec")
val t1 = "pi1"
val t2 = "pi2"
......
......@@ -75,8 +75,44 @@ object WorkflowParser extends RegexParsers with LazyLogging {
Signature(oracles toSet, rels toSet)
}
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)
val unbound = stmts.flatMap(_.freeVars()).filterNot(v => names.contains(v.name))
if (!unbound.isEmpty) {
logger.error(s"Variables $unbound appear unbound.")
}
distinct && unbound.isEmpty
}
def VAR = "[a-zA-Z][a-zA-Z0-9]*".r ^^ { str => Var(str) }
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) }
def tt = "True" ^^^ True
def ff = "False" ^^^ False
......@@ -95,19 +131,29 @@ object WorkflowParser extends RegexParsers with LazyLogging {
def STMT = ADD | REM
def BLOCK = "forall" ~> repsep(VAR, ",") ~ (STMT+) ^^ { case vars ~ stmts => ForallBlock(vars, stmts) }
def MAYBLOCK = "forallmay" ~> repsep(VAR, ",") ~ (STMT+) ^^ { case vars ~ stmts => ForallMayBlock(vars, "", stmts) }
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, ...)" )
def LOOP = "loop" ~> "{" ~> ((MAYBLOCK | BLOCK)+) <~ "}" ^^ { case bs => Loop(bs) }
def LOOP = "loop" ~> "{" ~> (BLOCK+) <~ "}" ^^ { case bs => Loop(bs) }
def WORKFLOW = rep(BLOCK | MAYBLOCK | LOOP) ^? {
def WORKFLOW = rep(BLOCK | LOOP) ^? {
case blocks if checkSig(blocks) => {
val choiceblocks = addChoicePredicates(blocks)
Workflow(buildSig(choiceblocks), choiceblocks)
}
}
def SPEC = "Workflow" ~> WORKFLOW ~ (("Declassify" ~> TERM)?) ~ ("Target" ~> FUN) ^^ { case w ~ decl ~ tar => Spec(w, decl.getOrElse(True), tar) }
def SPEC = "Workflow" ~! WORKFLOW ~ (("Declassify" ~> TERM)?) ~ ("Target" ~> FUN) ^^ { case _ ~ w ~ decl ~ tar => Spec(w, decl.getOrElse(True), tar) }
def parseWorkflow(s: String) = parseAll(WORKFLOW, s)
def parseSpec(s: String) = parseAll(SPEC, s)
......
......@@ -14,7 +14,11 @@ object Workflow {
val EMPTY = Workflow(Signature.EMPTY, List())
}
case class Spec(w: Workflow, declass: Term, target: Fun)
case class Spec(w: Workflow, declass: Term, target: Fun) {
override def toString = {
s"Spec\nWorkflow:\n$w\nDeclass:$declass\nTarget:$target"
}
}
object Spec {
val EMPTY = Spec(Workflow.EMPTY, True, Fun("NOTHING", List()))
}
......@@ -31,6 +35,8 @@ abstract class Statement {
def guard: Term
def fun: String
def tuple: List[Var]
def freeVars() = guard.freeVars() ++ tuple
}
case class Add(guard: Term, fun: String, tuple: List[Var]) extends Statement {
......
......@@ -42,15 +42,18 @@ object FOLTL {
case object True extends Term
case object False extends Term
case class Var(name: String) extends Term {
override def toString() = name
object Var {
val DEFAULT_TYPE = "T"
}
case class Var(name: String, typ:String = Var.DEFAULT_TYPE) extends Term {
override def toString() = s"$name"
}
object Fun {
def apply(name: String, params: List[Var]): Fun = Fun(name, None, params)
}
case class Fun(name: String, ind: Option[String], params: List[Var]) extends Term {
override def toString() = name + Utils.mkString(ind, "(", "", ")") + params.mkString("(", ",", ")")
override def toString() = name + Utils.mkString(ind, "(", "", ")") + params.map(_.name).mkString("(", ",", ")")
def updatedParams(index: Int, p:Var) = Fun(name, ind, params.updated(index, p))
def updatedParams(list: List[Var]) = Fun(name, ind, list)
}
......@@ -62,7 +65,8 @@ object FOLTL {
def t: Term
override def toString() = {
qname + " " + vars.mkString(",") + ". " + t.bracketed()
// show types only in quantifiers
qname + " " + vars.map(v => s"${v.name}:${v.typ}").mkString(",") + ". " + t.bracketed()
}
}
......
......@@ -145,6 +145,26 @@ class ParserTest extends FlatSpec {
"""
WorkflowParser.parseWorkflow(s).successful should be (false)
}
it should "parse typed variables" in {
val st = """
forallmay x:Agent,s:Paper
O(x) -> R += (x,s)
"""
val x = Var("x","Agent")
val s = Var("s","Paper")
val typedsig = Signature(Set(Fun("O", List(x))), Set(Fun("R", List(x, s))))
val w = Workflow(
typedsig,
List(
ForallMayBlock(List(x, s), "choice0",
Add(Fun("O", x), "R", List(x,s)))))
testResult(st, w)
}
"Spec Parser" should "parse simpleNochoice" in {
val s = """
......
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