Commit 639dfaf0 authored by Christian Müller's avatar Christian Müller

start of encoding

parent fbefa70c
......@@ -6,7 +6,7 @@ import scalax.collection.GraphEdge._
import scalax.collection.edge.LDiEdge // labeled directed edge
import scalax.collection.edge.Implicits._ // shortcuts
import blocks.WorkFlow._
import blocks.Workflow._
import de.tum.workflows.foltl.FOLTL
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.TermFunctions._
......@@ -19,8 +19,6 @@ object BlockImplicit extends LEdgeImplicits[SimpleBlock]; import BlockImplicit._
object Encoding extends LazyLogging {
val ORACLE = "O"
// Naming
// TODO: make sure there are no clashes
def nodeVar(n: Any) = Fun("n" + n, List())
......@@ -80,9 +78,8 @@ object Encoding extends LazyLogging {
def encodeGraph(g:Graph[Int, LDiEdge]) = {
val allnodes = for (n <- g.nodes.toList) yield {
// TODO: better syntax
val list = n.outgoing.toList.map(e => nodeVar(e.to))
Implies(nodeVar(n), Next(Or.make(list)))
Implies(nodeVar(n), Next(Or.make(list:_*)))
}
Globally(And.make(allnodes))
}
......@@ -91,7 +88,10 @@ object Encoding extends LazyLogging {
val negs = for (n <- g.nodes.toList; n2 <- g.nodes.toList if n < n2) yield {
Neg(And(nodeVar(n), nodeVar(n2)))
}
Globally(And.make(negs))
val nodes = for (n <- g.nodes.toList if !(n == 0)) yield {
Neg(nodeVar(n))
}
And.make(nodeVar(0), And.make(nodes), Globally(And.make(negs)))
}
def encodeStmt(s: Statement, pred: Option[Term]):(Term, String) = {
......@@ -107,9 +107,8 @@ object Encoding extends LazyLogging {
(Forall(s.tuple, Eq(Next(Fun(s.fun, s.tuple)), t)), s.fun)
}
def encodeStaying(sig: Signature, u:String) = {
val tup = sig.preds(u)
Forall(tup, Eq(Next(Fun(u, tup)), Fun(u, tup)))
def encodeStaying(target: Fun) = {
Forall(target.params, Eq(Next(target), target))
}
def encodeSem(sig: Signature, g: Graph[Int, LDiEdge]) = {
......@@ -121,8 +120,8 @@ object Encoding extends LazyLogging {
encodeStmt(s, choice)
}
val updates = res.map(_._2)
val staying = for (u <- sig.preds.map(_._1) if !updates.contains(u)) yield {
encodeStaying(sig, u)
val staying = for (f <- sig.preds if !updates.contains(f.name)) yield {
encodeStaying(f)
}
val terms = res.map(_._1) ++ staying
......@@ -132,13 +131,19 @@ object Encoding extends LazyLogging {
}
def encodeInitial(sig: Signature, g: Graph[Int, LDiEdge]) = {
val empties = for ((p, tup) <- sig.preds if !(p == ORACLE)) yield {
Forall(tup, Neg(Fun(p, tup)))
}
val nodes = for (n <- g.nodes.toList if !(n == 0)) yield {
Neg(nodeVar(n))
val empties = for (f <- sig.preds) yield {
Forall(f.params, Neg(f))
}
And.make(nodeVar(0) +: (nodes ++ empties))
And.make(empties)
}
def sanecfg(w: Workflow) = {
val g = toGraph(w)
And(encodeGraph(g), encodeSanity(g))
}
def exec(w: Workflow) = {
val g = toGraph(w)
And(encodeInitial(w.sig, g), encodeSem(w.sig, g))
}
def toFOLTL(w: Workflow) = {
......
package de.tum.workflows
import foltl.FOLTL._
import blocks.WorkFlow._
import blocks.Workflow._
import Implicits._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.ltl.LTL
import de.tum.workflows.Utils._
import de.tum.workflows.foltl.Stubborn
object Main extends App with LazyLogging {
val w = Workflow(
Signature(Map(
// first one is oracle
("O" -> List("s")),
("Q" -> List("x","s")),
("R" -> List("y","s")),
("S" -> List("x","y","s"))
)),
Signature(
List(Fun("O", List("s"))),
List(
ForallMayBlock(List("x","s"),
Add(Fun("O","s"),"Q", List("x","s"))
),
Fun("Q", List("x", "s")),
Fun("R", List("y", "s")),
Fun("S", List("x", "y", "s")))),
List(
ForallMayBlock(List("x", "s"), "choice0",
Add(Fun("O", "s"), "Q", List("x", "s"))),
Loop(List(
ForallBlock(List("x","y","s"),
Add(Fun("R", List("y","s")), "S", List("x","y","s"))
),
ForallBlock(List("x","s"),
Add(Fun("Q",List("x","s")), "R", List("x","s"))
)
))
))
ForallBlock(List("x", "y", "s"),
Add(Fun("R", List("y", "s")), "S", List("x", "y", "s"))),
ForallBlock(List("x", "s"),
Add(Fun("Q", List("x", "s")), "R", List("x", "s")))))))
logger.info(s"Workflow:\n$w")
val res = Encoding.toFOLTL(w)
val choices = allchoices(w)
// agent list to execute the workflow for (should not clash with variables in the workflow)
val agents:List[Var] = List("a","b")
val agents: List[Var] = List("a", "b")
val res2 = LTL.eliminateUniversals(res, agents)
val res3 = LTL.eliminatePredicates(res2)
logger.info(s"Complete formula: $res3")
......
package de.tum.workflows
import de.tum.workflows.blocks.Workflow._
import de.tum.workflows.foltl.FOLTL._
object Utils {
def mkString[T](string: Iterable[T], start: String, mid: String, end:String) = {
if (string.isEmpty) "" else string.mkString(start, mid, end)
}
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()
}
}
def allchoices(w: Workflow):List[Fun] = {
w.steps.flatMap(collectChoices _)
}
}
\ No newline at end of file
......@@ -2,8 +2,8 @@ package de.tum.workflows.blocks
import de.tum.workflows.foltl.FOLTL._
object WorkFlow {
case class Signature(preds: Map[String, List[Var]])
object Workflow {
case class Signature(oracles: List[Fun], preds: List[Fun])
case class Workflow(sig: Signature, steps: List[Block]) {
override def toString() = steps.mkString("\n")
......@@ -34,7 +34,7 @@ object WorkFlow {
val may = false
override def toString() = "forall " + agents.mkString(",") + steps.mkString("\n ", ";\n ", "")
}
case class ForallMayBlock(agents: List[Var], steps: List[Statement]) extends SimpleBlock {
case class ForallMayBlock(agents: List[Var], pred: String, steps: List[Statement]) extends SimpleBlock {
val may = true
override def toString() = "forall " + agents.mkString(",") + " may" + steps.mkString("\n ", ";\n ", "")
}
......
......@@ -7,10 +7,8 @@ import de.tum.workflows.foltl.FOLTL._
object Stubborn {
def apply(agent: Var, choices: List[Fun], t1: String, t2: String) = {
And.make(for (c <- choices) yield {
val f = Fun(c.name, c.params.updated(0, agent))
Globally(
Forall(c.params.drop(1), Eq(f.in(t1), f.in(t2)))
)
......
......@@ -57,24 +57,36 @@ object FOLTL {
trait TemporalTerm extends Term
case class Next(t:Term) extends TemporalTerm {
override def toString() = {
"X " + t.bracketed()
}
case class Next(t:Term) extends TemporalTerm with UnOp {
val make = Next.apply _
val opname = "X"
}
case class Globally(t: Term) extends TemporalTerm {
override def toString() = {
"G " + t.bracketed()
}
case class Globally(t: Term) extends TemporalTerm with UnOp {
val make = Globally.apply _
val opname = "G"
}
case class Until(t1: Term, t2: Term) extends TemporalTerm {
override def toString() = {
t1.bracketed() + " U " + t2.bracketed()
}
case class Finally(t: Term) extends TemporalTerm with UnOp {
val make = Finally.apply _
val opname = "F"
}
case class Finally(t: Term) extends TemporalTerm {
override def toString() = {
"F " + t.bracketed()
case class Until(t1: Term, t2: Term) extends TemporalTerm with BinOp {
val make = Until.apply _
val opname = "U"
}
trait UnOp extends Term {
def make:Term => UnOp
def opname: String
def t: Term
override def toString() = opname + " " + t.bracketed()
}
object UnOp {
def unapply(unop: UnOp) = {
Some((unop.make, unop.t))
}
}
......@@ -99,8 +111,8 @@ object FOLTL {
Some((binop.make, binop.t1, binop.t2))
}
def makeL(make:(Term, Term) => BinOp, l: List[Term], empty: Term):Term = {
l match {
def makeL(make:(Term, Term) => Term, l: Seq[Term], empty: Term):Term = {
l.toList match {
case List(x) => x
case x :: xs => make(x, makeL(make, xs, empty))
case List() => empty
......@@ -109,6 +121,9 @@ object FOLTL {
}
object Or {
def make(terms: List[Term]) = {
BinOp.makeL(Or.apply _, terms, True)
}
def make(terms: Term*) = {
BinOp.makeL(Or.apply _, terms, False)
}
}
......@@ -120,6 +135,9 @@ object FOLTL {
def make(terms: List[Term]) = {
BinOp.makeL(And.apply _, terms, True)
}
def make(terms: Term*) = {
BinOp.makeL(And.apply _, terms, True)
}
}
case class And(t1: Term, t2: Term) extends BinOp {
val opname = "∧"
......@@ -134,14 +152,8 @@ object FOLTL {
val make = Implies.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 make = Neg.apply _
val opname = "¬"
}
......
......@@ -10,13 +10,9 @@ object TermFunctions {
// Extractors
// Exists, Forall
case Quantifier(_, ps, t) => free(t, bound ++ ps)
case Until(t1, t2) => free(t1, bound) ++ free(t2, bound)
case Next(t1) => free(t1, bound)
case Globally(t1) => free(t1, bound)
case Finally(t1) => free(t1, bound)
case UnOp(make, t) => free(t, bound)
// And, Or, Eq, Implies
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)
......@@ -87,17 +83,25 @@ object TermFunctions {
t match {
// Extractors
case Quantifier(make, ps, t) => make(ps, everywhere(trans, t))
case Until(t1, t2) => Until(everywhere(trans, t1), everywhere(trans, t2))
case Finally(t1) => Finally(everywhere(trans, t1))
case Globally(t1) => Globally(everywhere(trans, t1))
case Next(t1) => Next(everywhere(trans, t1))
case UnOp(make, t1) => make(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 collect[T](combine:(T,T) => T, empty:() =>T)(coll: PartialFunction[Term, T], t: Term): T = {
if (coll.isDefinedAt(t))
coll(t)
else
t match {
// Extractors
case Quantifier(make, ps, t) => collect(combine, empty)(coll, t)
case UnOp(make, t) => collect(combine, empty)(coll, t)
case BinOp(make, t1, t2) => combine(collect(combine, empty)(coll, t1), collect(combine, empty)(coll, t2))
case x => empty()
}
}
def assumeEmpty(t: Term, name: String) = {
t.everywhere({
case Fun(f, _, _) if f == name => False
......
......@@ -4,20 +4,18 @@ import de.tum.workflows.Implicits._
import FOLTL._
object Noninterference {
def apply(agent:Var, choices: List[Fun], target: Fun, t1: String, t2:String) = {
def apply(choices: List[Fun], target: Fun, t1: String, t2:String) = {
val agent = target.params(0)
val cechoices = for (f <- choices) yield {
Fun(f.name, f.params.updated(0, agent))
}
val samechoices = for (f <- cechoices) yield {
Forall(f.params.drop(1), Eq(f.in(t1), f.in(t2)))
}
val cetarget = Fun(target.name, target.params.updated(0, agent))
val samechoices = Stubborn(agent, choices, t1, t2)
val difference = Exists(cetarget.params.drop(1), Neg(Eq(cetarget.in(t1), cetarget.in(t2))))
val difference = Neg(Eq(target.in(t1), target.in(t2)))
Exists(agent, And(Globally(And.make(samechoices)), Finally(difference)))
Exists(agent, And(Globally(samechoices), Finally(difference)))
}
}
\ No newline at end of file
package de.tum.workflows.foltl
import de.tum.workflows.Implicits._
import de.tum.workflows.Encoding._
import de.tum.workflows.blocks.Workflow._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.Utils._
object Properties {
def noninterStubborn(w: Workflow, target: Fun) = {
val t1 = "t1"
val t2 = "t2"
val cfg = sanecfg(w)
val sem = exec(w)
val agents = target.params.map(s => Var("a" + s.name))
val newtarget = Fun(target.name, agents)
val choices = allchoices(w)
val noninter = Noninterference(choices, newtarget, t1, t2)
val stubb = Forall("a", Stubborn("a", choices, t1, t2))
Exists(List(t1, t2), And.make(cfg, sem.in(t1), sem.in(t2), stubb, noninter))
}
}
......@@ -5,21 +5,21 @@ import org.scalatest.Matchers._
import org.scalatest.Inspectors._
import de.tum.workflows.Implicits._
import de.tum.workflows.blocks.WorkFlow._
import de.tum.workflows.blocks.Workflow._
import de.tum.workflows.Encoding
import de.tum.workflows.foltl.Noninterference
import de.tum.workflows.foltl.Stubborn
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.Utils._
class EncodingTest extends FlatSpec {
val w = Workflow(
Signature(Map(
// first one is oracle
("O" -> List("s")),
("R" -> List("x", "s")))),
Signature(
List(Fun("O", List("s"))),
List(Fun("R", List("x", "s")))),
List(
ForallMayBlock(List("x", "s"),
ForallMayBlock(List("x", "s"), "choice0",
Add(Fun("O", "s"), "R", List("x", "s")))))
// shorthands
......@@ -38,13 +38,10 @@ class EncodingTest extends FlatSpec {
cfg should be(
Globally(
And(Implies(n0, Next(n1)), Implies(n1, Next(n1)))
)
)
And(Implies(n0, Next(n1)), Implies(n1, Next(n1)))))
sanity should be(
Globally(Neg(And(n0, n1)))
)
Globally(Neg(And(n0, n1))))
val rstays = Forall(List("x", "s"), Eq(Next(Rxs), Rxs))
val ostays = Forall(List("s"), Eq(Next(Os), Os))
......@@ -55,47 +52,53 @@ class EncodingTest extends FlatSpec {
Implies(And(n0, Next(n1)), And(
Forall(List("x", "s"), Eq(Next(Rxs), Or(Rxs, And(Os, aux0xs)))),
ostays)),
Implies(And(n1, Next(n1)), And(ostays, rstays))
)
)
)
Implies(And(n1, Next(n1)), And(ostays, rstays)))))
init should be(
And.make(List(
// n0 and n1 and forall x,s. not R(x,s)
n0,
Neg(n1),
Forall(List("x", "s"), Neg(Rxs)))
)
)
Forall(List("x", "s"), Neg(Rxs)))))
}
"Stubbornness encoding" should "work" in {
val choices = List(Fun("choice0", List("x","y")))
val choices = List(Fun("choice0", List("x", "y")))
val stubness = Stubborn("a1", choices, "t1", "t2")
val auxa1 = Fun("choice0", List("a1", "y"))
stubness should be (
Globally(
Forall(List("y"), Eq(auxa1.in("t1"), auxa1.in("t2")))
)
)
stubness should be(
Globally(
Forall(List("y"), Eq(auxa1.in("t1"), auxa1.in("t2")))))
}
"Noninterference encoding" should "work" in {
val choices = List(Fun("choice0", List("x","y")))
val nonint = Noninterference("a", choices, Rxs, "t1", "t2")
val Ras = Fun("R", List("a", "s"))
val choices = List(Fun("choice0", List("x", "y")))
val Rab = Fun("R", List("a", "b"))
val nonint = Noninterference(choices, Rab, "t1", "t2")
val aux0ay = Fun("choice0", List("a", "y"))
nonint should be (
nonint should be(
Exists(List("a"), And(
Globally(Forall("y", Eq(aux0ay.in("t1"),aux0ay.in("t2")))),
Finally(Exists("s", Neg(Eq(Ras.in("t1"), Ras.in("t2")))))
))
)
Globally(Forall("y", Eq(aux0ay.in("t1"), aux0ay.in("t2")))),
Finally(Exists("b", Neg(Eq(Rab.in("t1"), Rab.in("t2"))))))))
}
"Property encoding" should "work" in {
val t1 = "t1"
val t2 = "t2"
val choices = allchoices(w)
choices should be (List(Fun("choice0", List("x", "y"))))
}
}
\ No newline at end of file
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