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

add encodings for stubborn, noninterference and tests

parent 49d1c9ef
G (
(n0 → X n1) ∧ (n1 → X (n3 ∨ n2)) ∧ (n2 → X n2) ∧ (n3 → X n1)
) ∧ G (
¬(n0 ∧ n1) ∧ ¬(n0 ∧ n2) ∧ ¬(n0 ∧ n3) ∧ ¬(n1 ∧ n2) ∧ ¬(n1 ∧ n3) ∧ ¬(n2 ∧ n3)
) ∧ G (
((n0 ∧ X n1) → (
(X Q_a_a ↔ (Q_a_a ∨ (O_a ∧ choice0_a_a))) ∧
(X O_a ↔ O_a) ∧
(X R_a_a ↔ R_a_a) ∧
(X S_a_a_a ↔ S_a_a_a)
)) ∧
((n1 ∧ X n3) → (
(X S_a_a_a ↔ (S_a_a_a ∨ (R_a_a ∧ choice1_a_a_a))) ∧
(X O_a ↔ O_a) ∧
(X Q_a_a ↔ Q_a_a) ∧
(X R_a_a ↔ R_a_a)
)) ∧
((n1 ∧ X n2) → (
(X O_a ↔ O_a) ∧ (X Q_a_a ↔ Q_a_a) ∧
(X R_a_a ↔ R_a_a) ∧
(X S_a_a_a ↔ S_a_a_a)
)) ∧
((n2 ∧ X n2) → (
(X O_a ↔ O_a) ∧
(X Q_a_a ↔ Q_a_a) ∧
(X R_a_a ↔ R_a_a) ∧
(X S_a_a_a ↔ S_a_a_a)
)) ∧
((n3 ∧ X n1) → (
(X R_a_a ↔ (R_a_a ∨ Q_a_a)) ∧
(X O_a ↔ O_a) ∧
(X Q_a_a ↔ Q_a_a) ∧
(X S_a_a_a ↔ S_a_a_a)
))
) ∧ n0 ∧ ¬n1 ∧ ¬n2 ∧ ¬n3 ∧ ¬Q_a_a ∧ ¬R_a_a ∧ ¬S_a_a_a
G (
n0
)
\ No newline at end of file
G (
(n0 → X n1) ∧ (n1 → X (n3 ∨ n2)) ∧ (n2 → X n2) ∧ (n3 → X n1)
) ∧ G (
¬(n0 ∧ n1) ∧ ¬(n0 ∧ n2) ∧ ¬(n0 ∧ n3) ∧ ¬(n1 ∧ n2) ∧ ¬(n1 ∧ n3) ∧ ¬(n2 ∧ n3)
) ∧ G (
((n0 ∧ X n1) → (
(X Q_a_a ↔ (Q_a_a ∨ (O_a ∧ choice0_a_a))) ∧
(X O_a ↔ O_a) ∧
(X R_a_a ↔ R_a_a) ∧
(X S_a_a_a ↔ S_a_a_a)
)) ∧
((n1 ∧ X n3) → (
(X S_a_a_a ↔ (S_a_a_a ∨ (R_a_a ∧ choice1_a_a_a))) ∧
(X O_a ↔ O_a) ∧
(X Q_a_a ↔ Q_a_a) ∧
(X R_a_a ↔ R_a_a)
)) ∧
((n1 ∧ X n2) → (
(X O_a ↔ O_a) ∧ (X Q_a_a ↔ Q_a_a) ∧
(X R_a_a ↔ R_a_a) ∧
(X S_a_a_a ↔ S_a_a_a)
)) ∧
((n2 ∧ X n2) → (
(X O_a ↔ O_a) ∧
(X Q_a_a ↔ Q_a_a) ∧
(X R_a_a ↔ R_a_a) ∧
(X S_a_a_a ↔ S_a_a_a)
)) ∧
((n3 ∧ X n1) → (
(X R_a_a ↔ (R_a_a ∨ Q_a_a)) ∧
(X O_a ↔ O_a) ∧
(X Q_a_a ↔ Q_a_a) ∧
(X S_a_a_a ↔ S_a_a_a)
))
) ∧ n0 ∧ ¬n1 ∧ ¬n2 ∧ ¬n3 ∧ ¬Q_a_a ∧ ¬R_a_a ∧ ¬S_a_a_a
G((n0→Xn1)∧(n1→X(n3∨n2))∧(n2→Xn2)∧(n3→Xn1))∧G(¬(n0∧n1)∧¬(n0∧n2)∧¬(n0∧n3)∧¬(n1∧n2)∧¬(n1∧n3)∧¬(n2∧n3))∧G(((n0∧Xn1)→((XQ_a_a↔(Q_a_a∨(O_a∧choice0_a_a)))∧(XO_a↔O_a)∧(XR_a_a↔R_a_a)∧(XS_a_a_a↔S_a_a_a)))∧((n1∧Xn3)→((XS_a_a_a↔(S_a_a_a∨(R_a_a∧choice1_a_a_a)))∧(XO_a↔O_a)∧(XQ_a_a↔Q_a_a)∧(XR_a_a↔R_a_a)))∧((n1∧Xn2)→((XO_a↔O_a)∧(XQ_a_a↔Q_a_a)∧(XR_a_a↔R_a_a)∧(XS_a_a_a↔S_a_a_a)))∧((n2∧Xn2)→((XO_a↔O_a)∧(XQ_a_a↔Q_a_a)∧(XR_a_a↔R_a_a)∧(XS_a_a_a↔S_a_a_a)))∧((n3∧Xn1)→((XR_a_a↔(R_a_a∨Q_a_a))∧(XO_a↔O_a)∧(XQ_a_a↔Q_a_a)∧(XS_a_a_a↔S_a_a_a))))∧n0∧¬n1∧¬n2∧¬n3∧¬Q_a_a∧¬R_a_a∧¬S_a_a_a
\ No newline at end of file
......@@ -82,16 +82,16 @@ object Encoding extends LazyLogging {
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(BinOp.makeL(Or.apply, list)))
Implies(nodeVar(n), Next(Or.make(list)))
}
Globally(BinOp.makeL(And.apply, allnodes))
Globally(And.make(allnodes))
}
def encodeSanity(g: Graph[Int, LDiEdge]) = {
val negs = for (n <- g.nodes.toList; n2 <- g.nodes.toList if n < n2) yield {
Neg(And(nodeVar(n), nodeVar(n2)))
}
Globally(BinOp.makeL(And.apply, negs))
Globally(And.make(negs))
}
def encodeStmt(s: Statement, pred: Option[Term]):(Term, String) = {
......@@ -126,9 +126,9 @@ object Encoding extends LazyLogging {
}
val terms = res.map(_._1) ++ staying
Implies(And(nodeVar(e.from), Next(nodeVar(e.to))), BinOp.makeL(And.apply, terms))
Implies(And(nodeVar(e.from), Next(nodeVar(e.to))), And.make(terms))
}
Globally(BinOp.makeL(And.apply, impls))
Globally(And.make(impls))
}
def encodeInitial(sig: Signature, g: Graph[Int, LDiEdge]) = {
......@@ -138,7 +138,7 @@ object Encoding extends LazyLogging {
val nodes = for (n <- g.nodes.toList if !(n == 0)) yield {
Neg(nodeVar(n))
}
BinOp.makeL(And.apply, nodeVar(0) +: (nodes ++ empties))
And.make(nodeVar(0) +: (nodes ++ empties))
}
def toFOLTL(w: Workflow) = {
......@@ -154,6 +154,6 @@ object Encoding extends LazyLogging {
val init = encodeInitial(w.sig, g)
logger.info(s"init(w): $init")
BinOp.makeL(And.apply, List(cfg, sanity, sem, init))
And.make(List(cfg, sanity, sem, init))
}
}
\ No newline at end of file
......@@ -21,7 +21,7 @@ object Main extends App with LazyLogging {
Add(Fun("O","s"),"Q", List("x","s"))
),
Loop(List(
ForallMayBlock(List("x","y","s"),
ForallBlock(List("x","y","s"),
Add(Fun("R", List("y","s")), "S", List("x","y","s"))
),
ForallBlock(List("x","s"),
......@@ -35,7 +35,7 @@ object Main extends App with LazyLogging {
val res = Encoding.toFOLTL(w)
// agent list to execute the workflow for (should not clash with variables in the workflow)
val agents:List[Var] = List("a")
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.foltl
import de.tum.workflows.Implicits._
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)))
)
})
}
}
\ No newline at end of file
......@@ -9,7 +9,7 @@ object FOLTL {
def freeVars() = TermFunctions.freeVars(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 in(name:String) = TermFunctions.annotate(this, name)
def bracketed():String = this match {
case _:BinOp => "(" + this + ")"
......@@ -99,19 +99,28 @@ object FOLTL {
Some((binop.make, binop.t1, binop.t2))
}
def makeL(make:(Term, Term) => BinOp, l: List[Term]):Term = {
def makeL(make:(Term, Term) => BinOp, l: List[Term], empty: Term):Term = {
l match {
case List(x) => x
case x :: xs => make(x, makeL(make, xs))
case x :: xs => make(x, makeL(make, xs, empty))
case List() => empty
}
}
}
object Or {
def make(terms: List[Term]) = {
BinOp.makeL(Or.apply _, terms, False)
}
}
case class Or(t1: Term, t2: Term) extends BinOp {
val opname = "∨"
val make = Or.apply _
}
object And {
def make(terms: List[Term]) = {
BinOp.makeL(And.apply _, terms, True)
}
}
case class And(t1: Term, t2: Term) extends BinOp {
val opname = "∧"
val make = And.apply _
......
......@@ -42,6 +42,7 @@ object TermFunctions {
// Simple laws
case Neg(True) => False
case Neg(False) => True
case Neg(Neg(t)) => t
case Or(True, t) => True
case Or(t, True) => True
case Or(False, t) => t
......@@ -51,10 +52,13 @@ object TermFunctions {
case And(True, t) => t
case And(t, True) => t
case Eq(False, False) => True
// Equivalence
case Eq(t1, t2) if t1 == t2 => True
case Neg(Neg(t)) => t
// TODO: Since
// Double Temporals
case Finally(Finally(t)) => Finally(t)
case Globally(Globally(t)) => Globally(t)
// Remove quantifiers if empty
case Quantifier(qmake, xs, t) if xs.isEmpty => t
......
package de.tum.workflows.foltl
import de.tum.workflows.Implicits._
import FOLTL._
object Noninterference {
def apply(agent:Var, choices: List[Fun], target: Fun, t1: String, t2:String) = {
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 difference = Exists(cetarget.params.drop(1), Neg(Eq(cetarget.in(t1), cetarget.in(t2))))
Exists(agent, And(Globally(And.make(samechoices)), Finally(difference)))
}
}
\ No newline at end of file
......@@ -42,7 +42,7 @@ object LTL extends LazyLogging {
}
newterm
}
BinOp.makeL(And.apply, terms)
And.make(terms)
}
})
}
......
package de.tum.workflows.ltl.tests
import org.scalatest._
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
import de.tum.workflows.Implicits._
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._
class EncodingTest extends FlatSpec {
val w = Workflow(
Signature(Map(
// first one is oracle
("O" -> List("s")),
("R" -> List("x", "s")))),
List(
ForallMayBlock(List("x", "s"),
Add(Fun("O", "s"), "R", List("x", "s")))))
// shorthands
val n0 = Fun("n0", List())
val n1 = Fun("n1", List())
val aux0xs = Fun("choice0", List("x", "s"))
val Os = Fun("O", List("s"))
val Rxs = Fun("R", List("x", "s"))
"Workflow encoding" should "work" in {
val g = Encoding.toGraph(w)
val cfg = Encoding.encodeGraph(g)
val sanity = Encoding.encodeSanity(g)
val sem = Encoding.encodeSem(w.sig, g)
val init = Encoding.encodeInitial(w.sig, g)
cfg should be(
Globally(
And(Implies(n0, Next(n1)), Implies(n1, Next(n1)))
)
)
sanity should be(
Globally(Neg(And(n0, n1)))
)
val rstays = Forall(List("x", "s"), Eq(Next(Rxs), Rxs))
val ostays = Forall(List("s"), Eq(Next(Os), Os))
sem should be(
Globally(
And(
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))
)
)
)
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)))
)
)
}
"Stubbornness encoding" should "work" in {
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")))
)
)
}
"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 aux0ay = Fun("choice0", List("a", "y"))
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")))))
))
)
}
}
\ 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