Properties.scala 1.62 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4
package de.tum.workflows.foltl

import de.tum.workflows.Implicits._
import de.tum.workflows.Encoding._
5
import de.tum.workflows.blocks._
Christian Müller's avatar
Christian Müller committed
6 7 8
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.Utils._

9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
object Stubborn {
  def apply(agent: Var, choices: Set[Fun], t1: String, t2: String) = {
    And.make(for (c <- choices toList) yield {
      val f = Fun(c.name, c.params.updated(0, agent))
    	Globally(
    	  Forall(c.params.drop(1), Eq(f.in(t1), f.in(t2)))    
   		)
    })
  }
}

object Noninterference {
  def apply(choices: Set[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 = Stubborn(agent, choices, t1, t2)
    
    val difference = Exists(target.params.drop(1), Neg(Eq(target.in(t1), target.in(t2))))
    
    Exists(agent, And(samechoices, Finally(difference)))
    
  }
}

Christian Müller's avatar
Christian Müller committed
37 38
object Properties {
  
39
  // include optimizations for choices
40
  def noninterStubborn(w: Workflow, target: Term) = {
Christian Müller's avatar
Christian Müller committed
41 42 43 44
    
    val t1 = "t1"
    val t2 = "t2"
    
45 46 47
    val graph = toGraph(w)
    val cfg = sanecfg(graph)
    val sem = exec(w.sig, graph)
48 49

    val agents = target freeVars() toList
Christian Müller's avatar
Christian Müller committed
50
    
51 52 53 54
    // choice and node predicates are equal in both runs (stubborn)
    val nodes = nodepredicates(graph) map (_.name)
    val choices = allchoices(w) map (_.name)
    val equals = nodes ++ choices
Christian Müller's avatar
Christian Müller committed
55
    
56
    val noninter = Exists(agents, Finally(Neg(Eq(target.in(t1), target.in(t2)))))
Christian Müller's avatar
Christian Müller committed
57
    
58
    // maybe add exists t1, t2. phi?
59
    And.make(cfg, sem.in(t1, equals), sem.in(t2, equals), noninter)
Christian Müller's avatar
Christian Müller committed
60 61
  }
}