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

fix equality

parent cb281ad8
......@@ -84,6 +84,13 @@ object FOLTL {
val qname = "∀"
val qmake = Forall.apply _
}
case class ForallOtherThan(vars: List[Var], otherthan:List[Var], t: Term) extends Quantifier {
val qname = "∀"
val qmake = ForallOtherThan.apply(_:List[Var], otherthan, _:Term)
override def toString() = {
s"$qname ${vars.map(_.withType()).mkString(",")} ∉ {${otherthan.map(_.withType()).mkString(",")}}. ${t.bracketed()}"
}
}
trait TemporalTerm extends Term
......
......@@ -98,7 +98,7 @@ object TermFunctions extends LazyLogging {
case x => 1
}
}
def collect[T](combine: (T*) => T, empty: T)(coll: PartialFunction[Term, T], t: Term): T = {
if (coll.isDefinedAt(t))
coll(t)
......
......@@ -10,7 +10,7 @@ import Properties._
object Stubborn {
def apply(agent: Var, choices: Set[Fun]) = {
And.make(for (c <- choices toList) yield {
And.make(for (c <- choices.toList if c.params(0).typ == agent.typ) yield {
val f = c.updatedParams(0, agent)
Globally(
Forall(c.params.drop(1), Eq(f.in(T1), f.in(T2)))
......@@ -20,18 +20,19 @@ object Stubborn {
}
object Causal {
def apply(agent: Var, inputs: Set[Fun], outputs: Set[Fun]) = {
def apply(agent: Var, others:List[Var], inputs: Set[Fun], outputs: Set[Fun]) = {
val equalchoices = for (c <- inputs toList) yield {
val equalchoices = for (c <- inputs.toList if c.params(0).typ == agent.typ) yield {
val newc = c.updatedParams(0, agent)
Forall(c.params.drop(1), Eq(newc.in(T1), newc.in(T2)))
}
// FIXME
// bind maximum # per type
val types = outputs.flatMap(_.params.map(_.typ))
val noutputs = outputs.filter(_.params(0).typ == agent.typ)
val types = noutputs.flatMap(_.params.map(_.typ))
val tobind = (for (t <- types) yield {
val count = outputs.map(_.params.drop(1).count(_.typ == t)).max
val count = noutputs.map(_.params.drop(1).count(_.typ == t)).max
val list = for (num <- 1 to count) yield {
Var(s"causal$agent$t$num", t)
......@@ -42,10 +43,7 @@ object Causal {
val vexist = tobind.flatMap(_._2) toList
val violations = for (o <- outputs toList) yield {
if (o.params.isEmpty || o.params.head.typ != agent.typ) {
False
} else {
val violations = for (o <- noutputs toList) yield {
var counters:Map[String, Int] = Map().withDefault(_ => 0)
// drop the first, since it is agent
......@@ -54,17 +52,46 @@ object Causal {
counters.updated(t, counters(t) + 1)
variable
}
val newo = o.updatedParams(agent :: agents)
Neg(Eq(newo.in(T1), newo.in(T2)))
}
val t = Neg(Eq(newo.in(T1), newo.in(T2)))
Noninterference.buildViolations(agents, t, others)
}
WUntil(And.make(equalchoices), Exists(vexist, Or.make(violations)))
val viol = violations.flatten
WUntil(And.make(equalchoices), Exists(vexist, Or.make(viol)))
}
}
object Noninterference extends LazyLogging {
def buildViolations(vars:List[Var], t:Term, causals:List[Var]) = {
val univ = causals.groupBy(_.typ).withDefault(_ => List())
def build(agents:List[Var], t:Term):List[Term] = {
agents match {
case x::xs => {
val terms = build(xs, t)
val replacements = for (tt <- terms; a <- univ(x.typ)) yield {
tt.everywhere({
case f:Fun => f.updatedParams(f.params.map(p => if (p == x) a else p))
})
}
replacements ++ terms
}
case List() => List(t)
}
}
// equality with causals
val viol = build(vars, t)
Or.make(viol)
}
def apply(choices: Set[Fun], spec:Spec) = {
val agent = spec.target.params(0)
......@@ -73,8 +100,9 @@ object Noninterference extends LazyLogging {
val decl = Declassification(spec)
val difference = Neg(Eq(spec.target.in(T1), spec.target.in(T2)))
Exists(agent, And.make(samechoices, decl, Finally(Exists(spec.target.params.drop(1), difference))))
val diff = buildViolations(spec.target.params.drop(1), difference, spec.causals)
Exists(agent, And.make(samechoices, decl, Finally(Exists(spec.target.params.drop(1), diff))))
}
}
......@@ -131,11 +159,19 @@ object Properties {
val noninter = Noninterference(choices, spec)
val causal = And.make(for (a <- spec.causals) yield {
Exists(a, Causal(a, choices, spec.w.sig.preds))
val types = spec.w.sig.preds.flatMap(_.params).map(_.typ)
val stubs = And.make(for (t <- types.toList) yield {
val stuba = Var(s"typvar$t", t)
ForallOtherThan(stuba, spec.causals, Stubborn(stuba, choices))
})
val causals = And.make(for (a <- spec.causals) yield {
val others = spec.causals.filterNot(_ == a)
Causal(a, others, choices, spec.w.sig.preds)
})
val agentmodel = Exists(spec.causals, And.make(stubs, causals, noninter))
// maybe add exists t1, t2. phi?
And.make(cfg, sem.in(t1, nodes), sem.in(t2, nodes), noninter, causal)
And.make(cfg, sem.in(t1, nodes), sem.in(t2, nodes), agentmodel)
}
}
......@@ -4,6 +4,7 @@ import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.FOLTL
object LTL extends LazyLogging {
......@@ -30,6 +31,7 @@ object LTL extends LazyLogging {
case Exists(a, term) => a ++ term.collect(coll)
// don't go over Foralls
case Forall(_, _) => List.empty
case t:ForallOtherThan => List.empty
// don't go over Globally
case Globally(_) => List.empty
}
......@@ -39,6 +41,7 @@ object LTL extends LazyLogging {
case Exists(a, term) => term.everywhere(elim)
// don't go over Foralls
case term:Forall => term
case term:ForallOtherThan => term
// don't go over Globally
case term:Globally => term
}
......@@ -48,32 +51,41 @@ object LTL extends LazyLogging {
(agents, res)
}
// TODO: does not work for nested foralls
def eliminateUniversals(t: Term, agents: List[Var]) = {
def eliminateUniversals(t: Term, agents: List[Var]):Term = {
if (agents.isEmpty) {
logger.error("Agent list should never be empty")
}
val universe = agents.groupBy(_.typ)
def instantiate(tup:List[Var],t:Term,universe:Map[String,List[FOLTL.Var]]) = {
if(!tup.forall(v => universe.contains(v.typ))) {
// everything is valid for quantifiers over empty sets
logger.warn(s"Ignored ${Forall(tup, t)} (empty universe for at least one type)")
True
} else {
val replacements = comb(tup.map(_.typ), universe)
val terms = for (repl <- replacements) yield {
val mapping = tup.zip(repl) toMap
t.everywhere({
// do replacement
case Fun(f, id, tup) => Fun(f, id, tup.map(a => mapping.getOrElse(a, a)))
})
}
eliminateUniversals(And.make(terms), agents)
}
}
t.everywhere({
case Forall(tup, term) => {
if(!tup.forall(v => universe.contains(v.typ))) {
// everything is valid for quantifiers over empty sets
logger.warn(s"Ignored ${Forall(tup, term)} (empty universe for at least one type)")
True
} else {
val replacements = comb(tup.map(_.typ), universe)
val terms = for (repl <- replacements) yield {
val mapping = tup.zip(repl) toMap
term.everywhere({
// do replacement
case Fun(f, id, tup) => Fun(f, id, tup.map(a => mapping.getOrElse(a, a)))
})
}
And.make(terms)
}
instantiate(tup, term, universe)
}
case ForallOtherThan(tup, otherthan, term) => {
val smalleruniverse = universe.map(t => {
(t._1, t._2.filterNot(otherthan.contains(_)))
})
instantiate(tup, term, smalleruniverse)
}
})
}
......
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.FOLTL
object Test extends App {
val agents = List("a", "b", "c")
println(agents.combinations(2).toList)
val a = Var("a", "A")
val a2 = Var("a", "A")
val test = List(a)
println(test.contains(a2))
}
\ 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