Commit 1d95e01f authored by Christian Müller's avatar Christian Müller

Merge branch 'master' of versioncontrolseidl.in.tum.de:mueller/loopingworkflows

parents bed072b8 79a55c21
......@@ -22,7 +22,7 @@ Workflow
# a workflow
# If types are omitted, everything is of type T, types can be given while binding the variables with the forall x:X
# Please use forallmay x:X,y:Y instead of forall x,y may (because of easier parsing)
# Please use forallmay x:X,y:Y instead of forall x:X,y:Y may (because of easier parsing)
Target
......@@ -36,8 +36,8 @@ Causality
## Testing
``de.tum.workflows.Main`` will use any ``.spec`` files in ``/examples/`` and logs the resulting LTL formulas for the example workflows to results/.
To get a feel for the code, see the tests in ``src/test/scala``
To run the unit tests, you can run ``sbt test``. You can find all the unit tests in ``src/test/scala``.
To test your own examples, run ``de.tum.workflows.Main`` by using ``sbt run``. This will parse all ``.spec`` files in ``/examples/`` and will log the resulting LTL formulas to ``results/``.
### Aalta
The resulting LTL formulas can be tested for satisfiability.
......
p cnf 3 2
3 0
-3 -1 -2 0
p cnf 35 44
7 0
-7 8 0
-7 9 0
-8 -1 -2 0
-9 10 0
-9 11 0
-10 -3 -4 0
-11 12 0
-11 13 0
-12 -3 -5 0
-13 14 0
-13 15 0
-14 -3 -2 0
-15 16 0
-15 17 0
-16 -6 -1 0
-17 18 0
-17 19 0
-18 -6 -3 0
-19 20 0
-19 21 0
-20 -6 -4 0
-21 22 0
-21 23 0
-22 -6 -2 0
-23 24 0
-23 25 0
-24 -6 -5 0
-25 26 0
-25 27 0
-26 -1 -3 0
-27 28 0
-27 29 0
-28 -1 -4 0
-29 30 0
-29 31 0
-30 -1 -5 0
-31 32 0
-31 33 0
-32 -4 -2 0
-33 34 0
-33 35 0
-34 -4 -5 0
-35 -2 -5 0
Workflow
forallmay a
True -> T1 += (a)
forallmay a
¬ T1(a) -> T2 += (a)
forallmay a
(¬ T1(a) ∧ ¬ T2(a)) -> T3 += (a)
forall a
(O(a) ∧ T1(a)) -> R += (a)
forallmay a,b
(T1(a) ∧ T2(b)) -> S += (b, a)
forallmay a,b
(T2(a) ∧ T3(b)) -> S += (b, a)
Declassify
O(x): F (T1(x) ∨ T2(x))
Target
S(a1, a2)
Causality
ca, cb
Workflow
forallmay a
True -> T1 += (a)
forallmay a
¬ T1(a) -> T2 += (a)
forallmay a
(¬ T1(a) ∧ ¬ T2(a)) -> T3 += (a)
forall a
(O(a) ∧ T1(a)) -> R += (a)
forallmay a,b
(T1(a) ∧ T2(b)) -> S += (b, a)
forallmay a,b
(T2(a) ∧ T3(b)) -> S += (b, a)
Declassify
O(x): F (T1(x) ∨ T2(x))
Target
S(a1, a2)
Causality
ca
package de.tum.workflows
import pqltl.PQLTL._
object Implicits {
implicit def toList[A](v: A): List[A] = List(v)
// Logic
implicit def nameToVar(name: String) = Var(name)
}
package de.tum.workflows
import pqltl.PQLTL._
import blocks.WorkFlow._
import Implicits._
object Main extends App {
// val post = Historically(Forall(List("x", "p"), Neg(And(Fun("Conf", List("x", "p")), Fun("Know", List("x", "p"))))))
//
// val workflow = Workflow(List(
// ForallMayBlock(List("a1", "p1"), Add(True, "Conf", List("a1", "p1"))),
// ForallMayBlock(List("a2", "b2", "p2"), Add(Fun("Conf", List("b2", "p2")), "Know", List("a2", "p2")))
// ))
// println(Neg(post).simplify())
// println(workflow)
}
\ No newline at end of file
package de.tum.workflows.blocks
import de.tum.workflows.pqltl.PQLTL._
import de.tum.workflows.blocks.WorkFlow._
import com.typesafe.scalalogging.LazyLogging
object Precondition extends LazyLogging {
// Generates new name everytime
def auxname = "Aux"
def apply(w: Workflow, t: Term): Term = {
val simp = t.simplify()
val result = foldblocks(simp, w.steps)
val notemporals = result.removeTemporals()
notemporals.simplify()
}
def foldblocks(t: Term, steps: List[Block]): Term = {
steps.zipWithIndex.foldRight(t)((b, t) => b match {
case (ForallBlock(agents, stmts),_) => foldstmts(t, stmts)
case (ForallMayBlock(agents, stmts), i) => foldmaystmts(t, auxname + i, stmts)
})
}
def foldstmts(t: Term, steps: List[Statement]): Term = {
// No aux calls
steps.foldRight(t)(wp(xs => True) _).simplify()
}
def foldmaystmts(t: Term, auxname:String, steps: List[Statement]): Term = {
steps.foldRight(t)(wp(xs => Fun(auxname, None, xs)) _).simplify()
}
def wp(mkaux: List[Var] => Term)(step:Statement, t:Term): Term = {
// Resolve temporals
val unwrapped = t.everywhere({
case Since(u, v) => Or(v, And(u, Since(u,v)))
case Once(t) => Or(t, Once(t))
case Historically(t) => And(t, Historically(t))
})
val simp = unwrapped.simplify()
val replaced = (step match {
case Add(guard, fun, tuple) => simp.everywhere({
// Ignore temporals
case _:TemporalTerm => t
case Fun(name, Some(ind), xs) if fun == name =>
Or(
Fun(name, Some(ind), xs),
Exists((guard.freeVars() -- xs).toList, And(guard.annotate(ind), mkaux(xs).annotate(ind)))
)
case Fun(name, None, xs) => {
println("FAIL")
False
}
})
case Remove(guard, fun, tuple) => simp.everywhere({
// Ignore temporals
case _:TemporalTerm => t
case Fun(name, Some(ind), xs) if fun == name =>
And(
Fun(name, Some(ind), xs),
Forall((guard.freeVars() -- xs).toList, Or(Neg(guard.annotate(ind)), Neg(mkaux(xs).annotate(ind))))
)
case Fun(name, None, xs) => {
println("FAIL")
False
}
})
})
val pre = replaced.simplify()
// Unwrap prev
val result = pre.everywhere({
case Previously(t) => t
})
logger.debug(s"Precondition of $t under $step is $result")
result
}
}
package de.tum.workflows.blocks
import de.tum.workflows.pqltl.PQLTL._
object WorkFlow {
case class Workflow(steps: List[Block]) {
override def toString() = steps.mkString("\n")
}
abstract sealed class Block
abstract class Statement
case class Add(guard: Term, fun: String, tuple: List[Var]) extends Statement {
override def toString() = guard + " → " + fun + " += " + tuple.mkString("(", ",", ")")
}
case class Remove(guard: Term, fun: String, tuple: List[Var]) extends Statement {
override def toString() = guard + " → " + fun + " -= " + tuple.mkString("(", ",", ")")
}
case class ForallBlock(agents: List[Var], steps: List[Statement]) extends Block {
override def toString() = "forall " + agents.mkString(",") + steps.mkString("\n ", ";\n ", "")
}
case class ForallMayBlock(agents: List[Var], steps: List[Statement]) extends Block {
override def toString() = "forall " + agents.mkString(",") + " may" + steps.mkString("\n ", ";\n ", "")
}
}
\ No newline at end of file
package de.tum.workflows.pqltl
object PQLTL {
abstract class Term {
def simplify() = TermFunctions.simplify(this)
def freeVars() = TermFunctions.freeVars(this)
def removeTemporals() = TermFunctions.removeTemporals(this)
def everywhere(trans: PartialFunction[Term, Term]) = TermFunctions.everywhere(trans, this)
def assumeEmpty(name: String) = TermFunctions.assumeEmpty(this, name)
def annotate(name:String) = TermFunctions.annotate(this, name)
def bracketed():String = this match {
case _:BinOp => "(" + this + ")"
case _ => this.toString()
}
}
case object True extends Term
case object False extends Term
case class Var(name: String) extends Term {
override def toString() = 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 + ind.mkString("(",",",")") + params.mkString("(", ",", ")")
}
trait Quantifier extends Term {
def qmake: (List[Var], Term) => Quantifier
def qname: String
def vars: List[Var]
def t: Term
override def toString() = {
qname + " " + vars.mkString(",") + ". " + t.bracketed()
}
}
object Quantifier {
def unapply(q: Quantifier) = Some((q.qmake, q.vars, q.t))
}
case class Exists(vars: List[Var], t: Term) extends Quantifier {
val qname = "∃"
val qmake = Exists.apply _
}
case class Forall(vars: List[Var], t: Term) extends Quantifier {
val qname = "∀"
val qmake = Forall.apply _
}
trait TemporalTerm extends Term
case class Previously(t:Term) extends TemporalTerm {
override def toString() = {
"Prev " + t.bracketed()
}
}
case class Historically(t: Term) extends TemporalTerm {
override def toString() = {
"A " + t.bracketed()
}
}
case class Since(t1: Term, t2: Term) extends TemporalTerm {
override def toString() = {
t1.bracketed() + " S " + t2.bracketed()
}
}
case class Once(t: Term) extends TemporalTerm
trait BinOp extends Term {
def make:(Term, Term) => BinOp
def opname: String
def t1: Term
def t2: Term
override def toString() = {
(t1, t2) match {
case (t1: BinOp, t2:BinOp) if (opname == t1.opname == t2.opname) => t1 + " " + opname + " " + t2
case (t1: BinOp, _) if (opname == t1.opname) => t1 + " " + opname + " " + t2.bracketed()
case (_, t2:BinOp) if (opname == t2.opname) => t1.bracketed() + " " + opname + " " + t2
case _ => t1.bracketed() + " " + opname + " " + t2.bracketed()
}
}
}
object BinOp {
def unapply(binop: BinOp) = {
Some((binop.make, binop.t1, binop.t2))
}
}
case class Or(t1: Term, t2: Term) extends BinOp {
val opname = "∨"
val make = Or.apply _
}
case class And(t1: Term, t2: Term) extends BinOp {
val opname = "∧"
val make = And.apply _
}
case class Eq(t1: Term, t2:Term) extends BinOp {
val opname = "↔"
val make = Eq.apply _
}
trait UnOp extends Term {
def opname: String
def t: Term
override def toString() = opname + t.bracketed
}
case class Neg(t: Term) extends UnOp {
val opname = "¬"
}
}
\ No newline at end of file
package de.tum.workflows.pqltl
import PQLTL._
object TermFunctions {
def freeVars(t: Term) = {
def free(t: Term, bound: Set[Var]): Set[Var] = {
t match {
// Extractors
// Exists, Forall
case Quantifier(_, ps, t) => free(t, bound ++ ps)
case Since(t1, t2) => free(t1, bound) ++ free(t2, bound)
case Once(t1) => free(t1, bound)
case Historically(t1) => free(t1, bound)
// And, Or, Eq
case BinOp(_, t1, t2) => free(t1, bound) ++ free(t2, bound)
case Neg(t1) => free(t1, bound)
case Fun(_, Some(ind), ps) => (ps.toSet -- bound) + Var(ind)
case Fun(_, _, ps) => (ps.toSet -- bound)
case v: Var if !bound(v) => Set(v)
case x => Set()
}
}
free(t, Set())
}
def simplify(t: Term): Term = {
val simp: PartialFunction[Term, Term] = {
// Push negation inward
case Neg(Or(t1, t2)) => And(Neg(t1), Neg(t2))
case Neg(And(t1, t2)) => Or(Neg(t1), Neg(t2))
case Neg(Historically(t)) => Once(Neg(t))
case Neg(Once(t)) => Historically(Neg(t))
case Neg(Previously(t)) => Previously(Neg(t))
case Neg(Forall(vars, t)) => Exists(vars, Neg(t))
case Neg(Exists(vars, t)) => Forall(vars, Neg(t))
// Simple laws
case Neg(True) => False
case Neg(False) => True
case Or(True, t) => True
case Or(t, True) => True
case Or(False, t) => t
case Or(t, False) => t
case And(False, t) => False
case And(t, False) => False
case And(True, t) => t
case And(t, True) => t
case Eq(False, False) => True
case Neg(Neg(t)) => t
// TODO: Since
// Remove quantifiers if empty
case Quantifier(qmake, xs, t) if xs.isEmpty => t
case Quantifier(qmake, xs, True) => True
case Quantifier(qmake, xs, False) => False
// Remove variables from quantifiers if not used in the body
// case Quantifier(qmake, xs, t) if !(xs.toSet -- t.freeVars()).isEmpty =>
// qmake((xs.toSet.intersect(t.freeVars())).toList, t)
//
// // Split off binops from quantifiers
// case Quantifier(qmake, xs, BinOp(make, t1, t2)) if (t1.freeVars().intersect(xs.toSet)).isEmpty =>
// make(t1, qmake(xs, t2))
// case Quantifier(qmake, xs, BinOp(make, t1, t2)) if (t2.freeVars().intersect(xs.toSet)).isEmpty =>
// make(qmake(xs, t1), t2)
}
val t1 = everywhere(simp, t)
if (t == t1) t1 else simplify(t1)
}
def everywhere(trans: PartialFunction[Term, Term], t: Term): Term = {
if (trans.isDefinedAt(t))
trans(t)
else
t match {
// Extractors
case Quantifier(make, ps, t) => make(ps, everywhere(trans, t))
case Since(t1, t2) => Since(everywhere(trans, t1), everywhere(trans, t2))
case Once(t1) => Once(everywhere(trans, t1))
case Historically(t1) => Historically(everywhere(trans, t1))
case Previously(t1) => Previously(everywhere(trans, t1))
case BinOp(make, t1, t2) => make(everywhere(trans, t1), everywhere(trans, t2))
case Neg(t1) => Neg(everywhere(trans, t1))
case x => x
}
}
def removeTemporals(t: Term): Term = {
t.everywhere({
case Historically(u) => u
case Since(u, v) => v
case Once(u) => u
case _: TemporalTerm => False
})
}
def assumeEmpty(t: Term, name: String) = {
t.everywhere({
case Fun(f, _, _) if f == name => False
})
}
def annotate(t: Term, name: String) = {
t.everywhere({
case Fun(f, None, xs) => Fun(f, Some(name), xs)
})
}
}
\ No newline at end of file
......@@ -16,7 +16,7 @@ import de.tum.workflows.foltl.TermFunctions
object Main extends App with LazyLogging {
val MAXAGENTS = 5
val MAXAGENTS = 8
val FOLDER = "results"
def generateExample(name: String) {
......
......@@ -9,11 +9,12 @@ object Utils {
if (string.isEmpty) "" else string.mkString(start, mid, end)
}
def collectChoices(w: Block):List[Fun] = {
def collectChoices(w: Block): List[Fun] = {
w match {
case Loop(steps) => steps.flatMap(collectChoices _)
case ForallMayBlock(agents, pred, _) => List(Fun(pred, agents))
case b:ForallBlock => List()
case NondetChoice(l,r) => l.flatMap(collectChoices) ++ r.flatMap(collectChoices)
}
}
......
......@@ -31,10 +31,11 @@ object WorkflowParser extends RegexParsers with LazyLogging {
inguard :+ ch toSet
}
def predicates(b: Block):Set[Fun] = {
def predicates(b: Block): Set[Fun] = {
b match {
case Loop(blocks) => blocks flatMap(predicates _) toSet
case b:SimpleBlock => b.steps.flatMap(predicatesStmt _) toSet
case NondetChoice(l,r) => (l.flatMap(predicates) ++ r.flatMap(predicates)) toSet
}
}
......@@ -115,8 +116,8 @@ object WorkflowParser extends RegexParsers with LazyLogging {
// logics
def tt = "True" ^^^ True
def ff = "False" ^^^ False
def AND = "(" ~> repsep(TERM, "∧") <~ ")" ^^ { case ts => And.make(ts) }
def OR = "(" ~> repsep(TERM, "∨") <~ ")" ^^ { case ts => Or.make(ts) }
def AND = "(" ~> (repsep(TERM, "∧") | repsep(TERM, "&&")) <~ ")" ^^ { case ts => And.make(ts) }
def OR = "(" ~> (repsep(TERM, "∨") | repsep(TERM, "||")) <~ ")" ^^ { case ts => Or.make(ts) }
def NEG = ("¬" | "!") ~ SIMPLETERM ^^ { case _ ~ t => Neg(t) }
// temporals
......@@ -134,7 +135,6 @@ object WorkflowParser extends RegexParsers with LazyLogging {
def STMT = ADD | REM
// TODO: There could be several - one per Oracle
def DECLASS = (FUN <~ ":") ~ TERM ^^ { case f ~ t => (f,t) }
def BLOCK = "forall" ~> ("may"?) ~ repsep(TYPEDVAR, ",") ~ (STMT+) ^? ({
......@@ -151,6 +151,7 @@ object WorkflowParser extends RegexParsers with LazyLogging {
}, t => s"$t is not a valid block (check free variables, duplicate variables, ...)" )
def LOOP = "loop" ~> "{" ~> (BLOCK+) <~ "}" ^^ { case bs => Loop(bs) }
def NDCHOICE = "choose" ~> "{" ~> ((BLOCK+) <~ "}" <~ "{")~ (BLOCK+) <~ "}" ^^ { case l ~ r => NondetChoice(l,r) }
def WORKFLOW = rep(BLOCK | LOOP) ^? {
case blocks if checkSig(blocks) => {
......@@ -159,6 +160,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 =
"Workflow" ~! WORKFLOW ~
(("Declassify" ~> DECLASS)?) ~
......
......@@ -83,5 +83,9 @@ case class Loop(steps: List[Block]) extends Block {
"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