Properties.scala

package de.tum.workflows.foltl

import de.tum.workflows.Implicits._
import de.tum.workflows.Encoding._
import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.Utils._
import com.typesafe.scalalogging.LazyLogging
import Properties._

object Stubborn {
  def apply(agent: Var, choices: Set[Fun]) = {
    And.make(for (c <- choices.toList if c.params.head.typ == agent.typ) yield {
      val f = c.updatedParams(0, agent)
    	Globally(
    	  Forall(c.params.drop(1), Eq(f.in(T1), f.in(T2)))    
   		)
    })
  }
}

object Causal {

  def apply(agent: Var, others:List[Var], inputs: Set[Fun], outputs: Set[Fun]) = {
    
    val equalchoices = for (c <- inputs.toList if c.params.head.typ == agent.typ) yield {
      val newc = c.updatedParams(0, agent)
      Forall(c.params.drop(1), Eq(newc.in(T1), newc.in(T2)))                    
    }
    
    val noutputs = outputs.filter(_.params.head.typ == agent.typ)
    
    val types = noutputs.flatMap(_.params.map(_.typ))
    val tobind = (for (t <- types) yield {
      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) 
      }
      
      (t -> list) 
    }) toMap
    
    val vexist = tobind.flatMap(_._2) toList
    
    val violations = for (o <- noutputs toList) yield {
      val counters: Map[String, Int] = Map().withDefault(_ => 0)
        
        // drop the first, since it is agent
        val agents = for (p <- o.params.drop(1); t = p.typ) yield {
          val variable = tobind(t)(counters(t))
          counters.updated(t, counters(t) + 1)
          variable
        }
        val newo = o.updatedParams(agent :: agents)
        val t = Neg(Eq(newo.in(T1), newo.in(T2)))
        
        Noninterference.buildViolations(agents, t, others)
    }
    
    val viol = violations.flatten
    
    WUntil(And.make(equalchoices), Exists(vexist, Or.make(viol)))    
  }
}

object Noninterference extends LazyLogging {
  
    
  def buildViolations(vars:List[Var], t:Formula, causals:List[Var]) = {
    val univ = causals.groupBy(_.typ).withDefault(_ => List())
    
    def build(agents:List[Var], t:Formula):List[Formula] = {
      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.head
    val samechoices = Stubborn(agent, choices)
    
    val decl = Declassification(spec)
    
    val difference = Neg(Eq(spec.target.in(T1), spec.target.in(T2)))
    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))))
  }
}

object Declassification extends {
  def apply(spec: Spec) = {
    val sameoracles = for ((o,(p,t)) <- spec.declass) yield {
      val fun = Fun(o, None, p)
      // Forall fv(o). (t_T1 and t_t2) -> G (o_T1 <-> o_T2) 
      Globally(Forall(p, Implies(Or(t.in(T1), t.in(T2)), Eq(fun.in(T1), fun.in(T2)))))
    }
    And.make(sameoracles.toList)
  }
}

object Properties {
  
  val T1 = "t1"
  val T2 = "t2"
  val INFNAME = "informed"
  
  // include optimizations for choices
  def noninterStubborn(spec: Spec) = {
    
    val graph = toGraph(spec.w)
    val cfg = sanecfg(graph)
    val sem = exec(spec.w.sig, graph)

    val agents = spec.target.freeVars.toList
    
    // choice and node predicates are equal in both runs (stubborn)
    val nodes = nodepredicates(graph) map (_.name)
    val choices = allchoices(spec.w) map (_.name)
    val equals = nodes ++ choices
    
    val decl = Declassification(spec)
    
    val noninter = Exists(agents, And(decl, Finally(Neg(Eq(spec.target.in(T1), spec.target.in(T2))))))
    
    // maybe add exists t1, t2. phi?
    And.make(cfg, sem.in(T1, equals), sem.in(T2, equals), noninter)
  }
  
  def noninterCausal(spec:Spec) = {
    
    val graph = toGraph(spec.w)
    val cfg = sanecfg(graph)
    val sem = exec(spec.w.sig, graph)

    val agents = spec.target.freeVars.toList
    
    val nodes = nodepredicates(graph) map (_.name)
    val choices = allchoices(spec.w)
    
    val noninter = Noninterference(choices, spec)
    
    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), agentmodel)
  }
}