fix types

cnf.dimacs

-p cnf 3 2
-3 0
--3 -1 -2 0
+p cnf 107 116
+31 0
+-31 32 0
+-31 39 0
+-32 33 0
+-32 34 0
+-33 -1 2 0
+-34 35 0
+-34 36 0
+-35 -3 4 0
+-36 37 0
+-36 38 0
+-37 1 -2 0
+-38 3 -4 0
+-39 40 0
+-39 47 0
+-40 41 0
+-40 42 0
+-41 -5 6 0
+-42 43 0
+-42 44 0
+-43 -7 8 0
+-44 45 0
+-44 46 0
+-45 5 -6 0
+-46 7 -8 0
+-47 48 0
+-47 63 0
+-48 49 0
+-48 50 0
+-49 -9 10 0
+-50 51 0
+-50 52 0
+-51 -11 12 0
+-52 53 0
+-52 54 0
+-53 -13 14 0
+-54 55 0
+-54 56 0
+-55 -15 16 0
+-56 57 0
+-56 58 0
+-57 9 -10 0
+-58 59 0
+-58 60 0
+-59 13 -14 0
+-60 61 0
+-60 62 0
+-61 11 -12 0
+-62 15 -16 0
+-63 64 0
+-63 79 0
+-64 65 0
+-64 66 0
+-65 -17 18 0
+-66 67 0
+-66 68 0
+-67 -19 20 0
+-68 69 0
+-68 70 0
+-69 -21 22 0
+-70 71 0
+-70 72 0
+-71 -23 24 0
+-72 73 0
+-72 74 0
+-73 17 -18 0
+-74 75 0
+-74 76 0
+-75 21 -22 0
+-76 77 0
+-76 78 0
+-77 19 -20 0
+-78 23 -24 0
+-79 80 0
+-79 81 0
+-80 -25 -26 0
+-81 82 0
+-81 83 0
+-82 -25 -27 0
+-83 84 0
+-83 85 0
+-84 -28 -25 0
+-85 86 0
+-85 87 0
+-86 -28 -29 0
+-87 88 0
+-87 89 0
+-88 -28 -26 0
+-89 90 0
+-89 91 0
+-90 -28 -27 0
+-91 92 0
+-91 93 0
+-92 -25 -29 0
+-93 94 0
+-93 95 0
+-94 -26 -27 0
+-95 96 0
+-95 97 0
+-96 -30 -29 0
+-97 98 0
+-97 99 0
+-98 -30 -27 0
+-99 100 0
+-99 101 0
+-100 -29 -27 0
+-101 102 0
+-101 103 0
+-102 -30 -26 0
+-103 104 0
+-103 105 0
+-104 -29 -26 0
+-105 106 0
+-105 107 0
+-106 -30 -25 0
+-107 -30 -28 0

examples/easychair3.spec

@@ -2,14 +2,13 @@ Workflow
 
 forallmay x:A,p:P
 	True -> Conf += (x,p)
-}
 forallmay x:A,p:P
 	!Conf(x,p) -> Ass += (x,p)
 forallmay x:A,p:P
 	(Ass(x,p) ∧ O(x,p)) -> Acc += (x,p)
 loop {
-	forall xa:X,xb:X,p:P (A(xa,p) ∧ Acc(xb,p)) -> Read += (xa,xb,p)
-	forallmay x:X,p:P (A(x,p) ∧ O(x,p)) -> Acc += (x,p)
+	forall xa:A,xb:A,p:P (A(xa,p) ∧ Acc(xb,p)) -> Read += (xa,xb,p)
+	forallmay x:A,p:P (A(x,p) ∧ O(x,p)) -> Acc += (x,p)
 }
 
 Declassify
@@ -18,4 +17,4 @@ Declassify
 
 Target
 
-Read(xa:X,xb:X,p:P)
+Read(xa:A,xb:A,p:P)

examples/easychair_linear.spec

@@ -4,10 +4,9 @@ forallmay x:X,p:P
 	True -> Conf += (x,p)
 forallmay x:X,p:P
 	!Conf(x,p) -> Ass += (x,p)
-}
 forall x:X,p:P,r:R
 	(Ass(x,p) ∧ O(p,r)) -> Read += (x,p,r)
-forallmay y:Y,x:X,p:P 
+forallmay y:X,x:X,p:P 
 	(Ass(x,p) ∧ Ass(y,p)) -> Comm += (x,y,p)
 
 Declassify

src/main/scala/de/tum/workflows/Main.scala

@@ -12,6 +12,7 @@ import java.io.PrintWriter
 import java.io.File
 import de.tum.workflows.blocks.Workflow
 import de.tum.workflows.blocks.Spec
+import de.tum.workflows.foltl.TermFunctions
 
 object Main extends App with LazyLogging {
   
@@ -35,6 +36,11 @@ object Main extends App with LazyLogging {
   def writeExample(name: String, prop: Term) {
 
     write(s"${name}.foltl", prop.pretty())
+
+    if (!TermFunctions.checkSanity(prop)) {
+      logger.error("Property didn't pass sanity check")
+      return
+    }
     
     val (agents, res) = LTL.eliminateExistentials(prop)
     

src/main/scala/de/tum/workflows/WorkflowParser.scala

@@ -9,17 +9,15 @@ import com.typesafe.scalalogging.LazyLogging
 object WorkflowParser extends RegexParsers with LazyLogging {
   
   def addChoicePredicates(blocks: List[Block]) = {
-    var num = -1;
-    
-    for (b <- blocks) yield {
-      b match {
-        case ForallMayBlock(v, _, stmts) => {
-        	num += 1;
-          ForallMayBlock(v, "choice" + num, stmts)
-        }
-        case x => x
+    def addChoice(blocks: List[Block], next:Int):List[Block] = {
+      blocks match {
+        case ForallMayBlock(v, _, stmts) :: xs => ForallMayBlock(v, s"choice$next", stmts) :: addChoice(xs, next + 1)
+        case Loop(blocks) :: xs => Loop(addChoice(blocks, next)) :: addChoice(xs, next + blocks.size)
+        case x :: xs => x :: addChoice(xs, next)
+        case Nil => Nil
       }
     }
+    addChoice(blocks, 0)
   }
   
   def allpredicates(list: List[Block]) = {

src/main/scala/de/tum/workflows/foltl/FOLTLTermFunctions.scala

 package de.tum.workflows.foltl
 
 import FOLTL._
+import com.typesafe.scalalogging.LazyLogging
 
-object TermFunctions {
+object TermFunctions extends LazyLogging {
 
   def freeVars(t: Term) = {
     def free(t: Term, bound: Set[Var]): Set[Var] = {
@@ -132,4 +133,15 @@ object TermFunctions {
       case Fun(f, None, xs) if (!(ignore contains f)) => Fun(f, Some(name), xs)
     })
   }
+  
+  def checkSanity(t: Term) = {
+    // TODO add more things, f.e. existentials
+    // T1, T2 can appear freely
+    val frees = t.freeVars() -- Set(Var(Properties.T1), Var(Properties.T2))
+    if (!frees.isEmpty) {
+      logger.warn(s"Sanity check failed: $frees appear free in the property.")
+    }
+    
+    frees.isEmpty
+  }
 }
\ No newline at end of file

src/main/scala/de/tum/workflows/foltl/Properties.scala

@@ -6,40 +6,58 @@ 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], t1: String, t2: String) = {
+  def apply(agent: Var, choices: Set[Fun]) = {
     And.make(for (c <- choices toList) yield {
       val f = c.updatedParams(0, agent)
     	Globally(
-    	  Forall(c.params.drop(1), Eq(f.in(t1), f.in(t2)))    
+    	  Forall(c.params.drop(1), Eq(f.in(T1), f.in(T2)))    
    		)
     })
   }
 }
 
 object Causal {
-  def apply(agent: Var, inputs: Set[Fun], outputs: Set[Fun], t1: String, t2: String) = {
+  def apply(agent: Var, inputs: Set[Fun], outputs: Set[Fun]) = {
     
     val equalchoices = for (c <- inputs toList) yield {
       val newc = c.updatedParams(0, agent)
-      Forall(c.params.drop(1), Eq(newc.in(t1), newc.in(t2)))                    
+      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 tobind = for (t <- types) yield {
-      val count = outputs.map(_.params.count(_.typ == t)).max
-      (t -> count) 
-    }
-    
-    val vexist = (for ((t,count) <- tobind; num <- 1 until count) yield { Var(s"causal$agent$t$num", t) }) toList
-    val agents = agent :: vexist
+    val tobind = (for (t <- types) yield {
+      val count = outputs.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 <- outputs toList) yield {
-      val newo = o.updatedParams(agents.take(o.params.length))
-      Neg(Eq(newo.in(t1), newo.in(t2)))
+      if (o.params.isEmpty || o.params.head.typ != agent.typ) {
+        False
+      } else {
+        var 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)
+        Neg(Eq(newo.in(T1), newo.in(T2)))
+      }
     }
     
     WUntil(And.make(equalchoices), Exists(vexist, Or.make(violations)))    
@@ -47,14 +65,14 @@ object Causal {
 }
 
 object Noninterference extends LazyLogging {
-  def apply(choices: Set[Fun], spec:Spec, t1: String, t2:String) = {
+  def apply(choices: Set[Fun], spec:Spec) = {
         
     if (!spec.declass.freeVars().forall(spec.target.params.contains(_))) {
       logger.error("Not all variables of the declassification condition bound by the target")
     }
     
     val agent = spec.target.params(0)
-    val samechoices = Stubborn(agent, choices, t1, t2)
+    val samechoices = Stubborn(agent, choices)
     
     // TODO: declassification binding?
 //    val sameoracles = for (o <- oracles) yield {
@@ -62,7 +80,7 @@ object Noninterference extends LazyLogging {
 //    }
 //    val decl = Or(Neg(declass.in(t1)), And.make(sameoracles toList))
     
-    val difference = Neg(Eq(spec.target.in(t1), spec.target.in(t2)))
+    val difference = Neg(Eq(spec.target.in(T1), spec.target.in(T2)))
 
     Exists(agent, And(samechoices, Finally(Exists(spec.target.params.drop(1), difference))))
   }
@@ -70,12 +88,12 @@ object Noninterference extends LazyLogging {
 
 object Properties {
   
+  val T1 = "t1"
+  val T2 = "t2"
+  
   // include optimizations for choices
   def noninterStubborn(spec: Spec) = {
     
-    val t1 = "t1"
-    val t2 = "t2"
-    
     val graph = toGraph(spec.w)
     val cfg = sanecfg(graph)
     val sem = exec(spec.w.sig, graph)
@@ -87,10 +105,10 @@ object Properties {
     val choices = allchoices(spec.w) map (_.name)
     val equals = nodes ++ choices
     
-    val noninter = Exists(agents, Finally(Neg(Eq(spec.target.in(t1), spec.target.in(t2)))))
+    val noninter = Exists(agents, 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)
+    And.make(cfg, sem.in(T1, equals), sem.in(T2, equals), noninter)
   }
   
   def noninterCausal(spec:Spec) = {
@@ -108,10 +126,10 @@ object Properties {
     val nodes = nodepredicates(graph) map (_.name)
     val choices = allchoices(spec.w)
     
-    val noninter = Noninterference(choices, spec, t1, t2)
+    val noninter = Noninterference(choices, spec)
     
     val causal = And.make(for (a <- spec.causals) yield {
-      Exists(a, Causal(a, choices, spec.w.sig.preds, t1, t2))
+      Exists(a, Causal(a, choices, spec.w.sig.preds))
     })
     
     // maybe add exists t1, t2. phi?

src/main/scala/de/tum/workflows/ltl/LTL.scala

@@ -51,7 +51,6 @@ object LTL extends LazyLogging {
   // TODO: does not work for nested foralls
   def eliminateUniversals(t: Term, agents: List[Var]) = {
     
-    
     if (agents.isEmpty) {
       logger.error("Agent list should never be empty")
     }
@@ -59,16 +58,22 @@ object LTL extends LazyLogging {
     
     t.everywhere({
         case Forall(tup, term) => {
-          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)))
-            })
+          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)
           }
-          And.make(terms)
         }
     })
   }

src/test/scala/de/tum/workflows/ltl/tests/EncodingTest.scala

@@ -12,6 +12,7 @@ import de.tum.workflows.foltl.Stubborn
 import de.tum.workflows.foltl.FOLTL._
 import de.tum.workflows.Utils._
 import de.tum.workflows.foltl.Properties
+import Properties._
 import de.tum.workflows.ltl.LTL
 import de.tum.workflows.ExampleWorkflows
 import de.tum.workflows.blocks._
@@ -68,12 +69,12 @@ class EncodingTest extends FlatSpec {
   "Stubbornness encoding" should "work" in {
     val choices = Set(Fun("choice0", List("x", "y")))
 
-    val stubness = Stubborn("a1", choices, "t1", "t2")
+    val stubness = Stubborn("a1", choices)
     val auxa1 = Fun("choice0", List("a1", "y"))
 
     stubness should be (
       Globally(
-        Forall(List("y"), Eq(auxa1.in("t1"), auxa1.in("t2")))))
+        Forall(List("y"), Eq(auxa1.in(T1), auxa1.in(T2)))))
   }
 
   "Noninterference encoding" should "work" in {
@@ -81,9 +82,9 @@ class EncodingTest extends FlatSpec {
     val choices = Set(Fun("choice0", List("x", "y")))
     val Rab = Fun("R", List("a", "b"))
     
-    val s = Spec(Workflow.EMPTY, True, Rab)
+    val s = Spec(Workflow.EMPTY, True, Rab, List())
 
-    val nonint = Noninterference(choices, s, "t1", "t2")
+    val nonint = Noninterference(choices, s)
 
     val aux0ay = Fun("choice0", List("a", "y"))
 
@@ -94,22 +95,20 @@ class EncodingTest extends FlatSpec {
   }
 
   "Property encoding" should "work" in {
-    val t1 = "t1"
-    val t2 = "t2"
     val choices = allchoices(w)
 
     choices should be (Set(Fun("choice0", List("x", "s"))))
     val ce = Fun("R", List("ax", "as"))
     
-    val s = Spec(Workflow.EMPTY, True, ce)
+    val s = Spec(Workflow.EMPTY, True, ce, List())
 
-    val noninter = Noninterference(choices, s, t1, t2)
+    val noninter = Noninterference(choices, s)
     noninter should be (
       Exists("ax", And(
-        Stubborn("ax", choices, t1, t2),
-        Finally(Exists("as", Neg(Eq(ce.in(t1), ce.in(t2))))))))
+        Stubborn("ax", choices),
+        Finally(Exists("as", Neg(Eq(ce.in(T1), ce.in(T2))))))))
 
-    val s2 = Spec(w, True, Fun("R", List("ax", "as")))
+    val s2 = Spec(w, True, Fun("R", List("ax", "as")), List())
     val prop = Properties.noninterStubborn(s2)
 
     val (agents, res) = LTL.eliminateExistentials(prop)