Properties.scala 752 Bytes
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29
package de.tum.workflows.foltl

import de.tum.workflows.Implicits._
import de.tum.workflows.Encoding._
import de.tum.workflows.blocks.Workflow._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.Utils._

object Properties {
  
  def noninterStubborn(w: Workflow, target: Fun) = {
    
    val t1 = "t1"
    val t2 = "t2"
    
    val cfg = sanecfg(w)
    val sem = exec(w)
    
    val agents = target.params.map(s => Var("a" + s.name))
    val newtarget = Fun(target.name, agents) 
    
    val choices = allchoices(w)
    
    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))
  }
}