Commit 08c66638 authored by Christian Müller's avatar Christian Müller

fix stubborn noninterference, add existential elimination

parent 1b0cf6da
......@@ -95,10 +95,12 @@ object Encoding extends LazyLogging {
}
def encodeStmt(s: Statement, pred: Option[Term]):(Term, String) = {
var guard = s.guard
for (p <- pred) { // if pred defined
guard = And(guard, p)
}
// var guard = s.guard
// for (p <- pred) { // if pred defined
// guard = And(guard, p)
// }
val list = List(s.guard) ++ pred.toList
val guard = And.make(list)
val t = s match {
case Add(_, f, tup) => Or(Fun(f, tup), guard)
......
......@@ -10,6 +10,7 @@ object FOLTL {
def everywhere(trans: PartialFunction[Term, Term]) = TermFunctions.everywhere(trans, this)
def assumeEmpty(name: String) = TermFunctions.assumeEmpty(this, name)
def in(name:String) = TermFunctions.annotate(this, name)
def collect[T](coll: PartialFunction[Term, List[T]]) = TermFunctions.collect(coll, this)
def bracketed():String = this match {
case _:BinOp => "(" + this + ")"
......
......@@ -89,7 +89,7 @@ object TermFunctions {
}
}
def collect[T](combine:(T,T) => T, empty:() =>T)(coll: PartialFunction[Term, T], t: Term): T = {
def collect[T](combine:(T*) => T, empty:T)(coll: PartialFunction[Term, T], t: Term): T = {
if (coll.isDefinedAt(t))
coll(t)
else
......@@ -98,7 +98,20 @@ object TermFunctions {
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()
case x => empty
}
}
def collect[T](coll: PartialFunction[Term, List[T]], t: Term): List[T] = {
if (coll.isDefinedAt(t))
coll(t)
else
t match {
// Extractors
case Quantifier(make, ps, t) => collect(coll, t)
case UnOp(make, t) => collect(coll, t)
case BinOp(make, t1, t2) => List.concat(collect(coll, t1), collect(coll, t2))
case x => List.empty
}
}
......
......@@ -13,9 +13,9 @@ object Noninterference {
}
val samechoices = Stubborn(agent, choices, t1, t2)
val difference = Neg(Eq(target.in(t1), target.in(t2)))
val difference = Exists(target.params.drop(1), Neg(Eq(target.in(t1), target.in(t2))))
Exists(agent, And(Globally(samechoices), Finally(difference)))
Exists(agent, And(samechoices, Finally(difference)))
}
}
\ No newline at end of file
......@@ -24,6 +24,7 @@ object Properties {
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))
// maybe add exists t1, t2. phi?
And.make(cfg, sem.in(t1), sem.in(t2), stubb, noninter)
}
}
......@@ -21,6 +21,32 @@ object LTL extends LazyLogging {
}
}
def eliminateExistentials(t:Term) = {
// TODO: can't we improve this syntax?
def coll:PartialFunction[Term, List[Term]] = {
case Exists(a, term) => List.concat(a, term.collect(coll))
// don't go over Foralls
case Forall(_, _) => List.empty
// don't go over Globally
case Globally(_) => List.empty
}
val agents = t.collect(coll)
def elim:PartialFunction[Term, Term] = {
case Exists(a, term) => term.everywhere(elim)
// don't go over Foralls
case term:Forall => term
// don't go over Globally
case term:Globally => term
}
val res = t.everywhere(elim)
(agents, res)
}
// agents need to be distince names in t
def eliminateUniversals(t: Term, agents: List[Var]) = {
......
......@@ -11,6 +11,8 @@ import de.tum.workflows.foltl.Noninterference
import de.tum.workflows.foltl.Stubborn
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.Utils._
import de.tum.workflows.foltl.Properties
import de.tum.workflows.ltl.LTL
class EncodingTest extends FlatSpec {
......@@ -41,25 +43,29 @@ class EncodingTest extends FlatSpec {
And(Implies(n0, Next(n1)), Implies(n1, Next(n1)))))
sanity should be(
Globally(Neg(And(n0, n1))))
And.make(n0, Neg(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))
// if O stays
// 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)))))
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)))))
Implies(And(n0, Next(n1)),
Forall(List("x", "s"), Eq(Next(Rxs), Or(Rxs, And(Os, aux0xs))))),
Implies(And(n1, Next(n1)), 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 {
......@@ -68,7 +74,7 @@ class EncodingTest extends FlatSpec {
val stubness = Stubborn("a1", choices, "t1", "t2")
val auxa1 = Fun("choice0", List("a1", "y"))
stubness should be(
stubness should be (
Globally(
Forall(List("y"), Eq(auxa1.in("t1"), auxa1.in("t2")))))
}
......@@ -87,18 +93,27 @@ class EncodingTest extends FlatSpec {
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", "s"))))
val ce = Fun("R", List("ax", "as"))
val noninter = Noninterference(choices, ce, t1, t2)
noninter should be (
Exists("ax", And(
Stubborn("ax", choices, t1, t2),
Finally(Exists("as", Neg(Eq(ce.in(t1), ce.in(t2))))))))
val prop = Properties.noninterStubborn(w, Fun("R", List("x", "s")))
val (agents, res) = LTL.eliminateExistentials(prop)
choices should be (List(Fun("choice0", List("x", "y"))))
agents should be (List(Var("ax"), Var("as")))
}
}
\ No newline at end of file
......@@ -10,16 +10,22 @@ import de.tum.workflows.Implicits._
class LTLSpec extends FlatSpec {
"A FOLTL formula" should "simplify double negation" in {
Neg(Neg(True)).simplify() should be (True)
"FOLTL simplification" should "simplify double negation" in {
Neg(Neg(True)).simplify() should be(True)
}
"The universal replacement" should "work" in {
"universal elimination" should "work" in {
val f = Globally(Forall(List("x", "y"), Fun("f", List("x", "y"))))
LTL.eliminateUniversals(f, List("a")) should be (Globally(Fun("f", List("a", "a"))))
LTL.eliminateUniversals(f, List("a")) should be(Globally(Fun("f", List("a", "a"))))
val f2 = Exists("x", Forall(List("y"), Fun("f", List("x", "y"))))
LTL.eliminateUniversals(f2, List("a")) should be (Exists("x", Fun("f", List("x", "a"))))
LTL.eliminateUniversals(f2, List("a")) should be(Exists("x", Fun("f", List("x", "a"))))
}
"Existential elimination" should "work" in {
val test = Exists("a", And(Globally(Exists("b", True)), Exists("c", Forall("d", Exists("e", False)))))
LTL.eliminateExistentials(test) should be(
(List(Var("a"), Var("c")), And(Globally(Exists("b", True)), Forall("d", Exists("e", False)))))
}
}
\ 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