add negnf, fix incomplete quantifiers

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

@@ -42,22 +42,6 @@ object Main extends App with LazyLogging {
     writer.print(prop)
     writer.close()
   }
-  
-  def timeNoninter(spec:Spec) = {
-      val inv = InvariantChecker.invariantNoninterStubborn(spec)
-      val (t, (safe, msg)) = time {
-        InvariantChecker.checkInvariant(spec.w, inv, true)
-      }
-      s"Noninterference Invariant (took $t ms):\n$msg\n"
-  }
-  
-  def timeAllEqual(spec:Spec) = {
-      val inv = InvariantChecker.invariantAllEqual(spec)
-      val (t, (safe, msg)) = time {
-        InvariantChecker.checkInvariant(spec.w, inv, true)
-      }
-      s"All Equal Invariant (took $t ms):\n$msg\n"
-  }
 
   def writeExample(name: String, spec: Spec, prop: Formula) {
 
@@ -117,8 +101,9 @@ object Main extends App with LazyLogging {
     if (checkinvariants) {
       
       def invariants = List(
-          InvariantChecker.invariantNoninterStubborn _,
-          InvariantChecker.invariantAllEqual _
+          InvariantChecker.invariantNoninterStubbornBS _
+//          InvariantChecker.invariantNoninterStubborn _
+//          InvariantChecker.invariantAllEqual _
       )
 
       def msgs = for (inv <- invariants) yield {
@@ -152,7 +137,7 @@ object Main extends App with LazyLogging {
   }
 
   //  clear()
-    generateExample("omitting/conference")
+    generateExample("nonomitting/conference")
   //    generateExample("tests/declasstest")
 //  generateAllExamples()
 }
\ No newline at end of file

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

@@ -47,5 +47,6 @@ object Preconditions extends LazyLogging {
       }
     }
   }
-
+  
+  // TODO: Replace oracles and choices by fresh predicates?
 }
\ No newline at end of file

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

@@ -17,9 +17,12 @@ object FOLTL {
     def opsize() = FormulaFunctions.opsize(this)
     
     def toPrenex() = FormulaFunctions.toPrenex(this)
+    def toNegNf() = FormulaFunctions.toNegNf(this)
+    def isBS() = FormulaFunctions.isBS(this)
     
     def removeOTQuantifiers() = FormulaFunctions.removeOTQuantifiers(this)
     def parallelRename(vars:List[Var], newvars:List[Var]) = FormulaFunctions.parallelRename(this, vars, newvars)
+    
 
     def bracketed(): String = this match {
       case _: BinOp => "(" + this + ")"

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

@@ -61,9 +61,9 @@ object FormulaFunctions extends LazyLogging {
       case Quantifier(_, xs, t) if xs.isEmpty => t
       case Quantifier(_, _, True)             => True
       case Quantifier(_, _, False)            => False
-      
+
       // TODO: Double quantifiers
-      
+
       // Remove variables from quantifiers if not used in the body
       //      case Quantifier(qmake, xs, t) if !(xs.toSet -- t.freeVars()).isEmpty =>
       //        qmake((xs.toSet.intersect(t.freeVars())).toList, t)
@@ -78,8 +78,8 @@ object FormulaFunctions extends LazyLogging {
     val t1 = everywhere(simp, t)
     if (t == t1) t1 else simplify(t1)
   }
-  
-  def eliminateImplication(f:Formula) = {
+
+  def eliminateImplication(f: Formula) = {
     f everywhere {
       case Implies(f1, f2) => Or(Neg(f1), f2)
     }
@@ -204,90 +204,101 @@ object FormulaFunctions extends LazyLogging {
     boundNames(f).groupBy(n => n).exists(_._2.length > 1)
   }
 
-  def toPrenex(f: Formula) = {
-    def stripQuantifiers(f:Formula):Formula = {
-      f everywhere {
-        case Quantifier(_, _, fsub) => stripQuantifiers(fsub)
-      }
+  def stripQuantifiers(f: Formula): Formula = {
+    f everywhere {
+      case Quantifier(_, _, fsub) => stripQuantifiers(fsub)
     }
-    
-    def collectQuantifiers(f:Formula) = {    
-      def collectQuantifiersSub(f:Formula):List[(Boolean, Formula => Quantifier)] = {
-        f collect {
-          case Exists(xs, fsub) => List((true, (t:Formula) => (Exists(xs,t)))) ++ collectQuantifiersSub(fsub)
-          case Forall(xs, fsub) => List((false, (t:Formula) => (Forall(xs,t)))) ++ collectQuantifiersSub(fsub)
-          case BinOp(make, f1, f2) => {
-            val q1 = collectQuantifiersSub(f1)
-            val q2 = collectQuantifiersSub(f2)
-            
-            // Merge while trying to stay in BS, if possible 
-            // TODO: could be improved to minimize quantifier alternations)
-            // TODO: merge universals with same type by renaming 
-            val ex1 = q1.takeWhile(_._1)
-            val rest1 = q1.drop(ex1.size)
-            
-            val ex2 = q2.takeWhile(_._1)
-            val rest2 = q2.drop(ex2.size)
-            
-            ex1 ++ ex2 ++ rest1 ++ rest2
-          }
-        }
+  }
+  
+    def collectQuantifiersSub(f: Formula): List[(Boolean, Formula => Quantifier)] = {
+    f collect {
+      case Exists(xs, fsub) => List((true, (t: Formula) => (Exists(xs, t)))) ++ collectQuantifiersSub(fsub)
+      case Forall(xs, fsub) => List((false, (t: Formula) => (Forall(xs, t)))) ++ collectQuantifiersSub(fsub)
+      case BinOp(make, f1, f2) => {
+        val q1 = collectQuantifiersSub(f1)
+        val q2 = collectQuantifiersSub(f2)
+
+        // Merge while trying to stay in BS, if possible 
+        // TODO: could be improved to minimize quantifier alternations)
+        // TODO: merge universals with same type by renaming 
+        val ex1 = q1.takeWhile(_._1)
+        val rest1 = q1.drop(ex1.size)
+
+        val ex2 = q2.takeWhile(_._1)
+        val rest2 = q2.drop(ex2.size)
+
+        ex1 ++ ex2 ++ rest1 ++ rest2
       }
-      collectQuantifiersSub(f).map(_._2)
     }
-    
-    def generateName(base:Var, bound:Set[Var]) = {
-
-      val chars = base.name.toCharArray()
-      val (basename, start) = if (chars.last.isDigit) {
-        (base.name.dropRight(1), chars.last.toInt + 1) 
-      } else {
-        (base.name, 1)
-      }
-      val stream = Stream.from(start)
-      
-      val droppedstream = stream.dropWhile(i => bound.contains(Var(basename + i, base.typ)))
-      
-      Var(basename + droppedstream.head, base.typ)
+  }
+
+  def collectQuantifiers(f: Formula) = {
+    collectQuantifiersSub(f).map(_._2)
+  }
+  
+  def isBS(f:Formula) = {
+    val quantprefix = collectQuantifiersSub(f.toNegNf())
+    // has forall exists in quantifier prefix
+    quantprefix.sliding(2).exists(list => !list(0)._1 && list(1)._1)
+  }
+  
+  def toNegNf(f:Formula) = {
+    val bound = if (hasDuplicateBindings(f)) {
+      logger.info(s"Formula $f binds variables more than once - renaming bindings")
+      FormulaFunctions.fixBinding(f, Set())._1
+    } else f
+    eliminateImplication(bound).simplify()
+  }
+
+  def generateName(base: Var, bound: Set[Var]) = {
+
+    val chars = base.name.toCharArray()
+    val (basename, start) = if (chars.last.isDigit) {
+      (base.name.dropRight(1), chars.last.toInt + 1)
+    } else {
+      (base.name, 1)
     }
-    
-    def fixBinding(f:Formula, bound:Set[Var]):(Formula, Set[Var]) = {
-      f match {
-        case UnOp(make, f1) => {
-          val (newf, newbounds) = fixBinding(f1, bound)
-          (make(newf), newbounds)
-        }
-        case BinOp(make, f1, f2) => {
-          val (newf1, newbound) = fixBinding(f1, bound) 
-          val (newf2, newbound2) = fixBinding(f2, newbound)
-          (make(newf1, newf2), newbound2)
-        }
-        case Quantifier(make, vars, fsub) => {
-          val alreadybounds = vars.filter(bound.contains(_))
-          val newnames = alreadybounds.map(generateName(_, bound))
-          val renamed = fsub.parallelRename(alreadybounds, newnames)
-          val binding = (vars.toSet -- alreadybounds) ++ newnames
-          
-          val (fixedrename, newbound) = fixBinding(renamed, bound ++ binding)
-          val newf = make(binding.toList, fixedrename)
-          (newf, newbound)
-        }
-        // Functions, Variables
-        case f => (f, bound)
+    val stream = Stream.from(start)
+
+    val droppedstream = stream.dropWhile(i => bound.contains(Var(basename + i, base.typ)))
+
+    Var(basename + droppedstream.head, base.typ)
+  }
+
+  def fixBinding(f: Formula, bound: Set[Var]): (Formula, Set[Var]) = {
+    f match {
+      case UnOp(make, f1) => {
+        val (newf, newbounds) = fixBinding(f1, bound)
+        (make(newf), newbounds)
       }
+      case BinOp(make, f1, f2) => {
+        val (newf1, newbound) = fixBinding(f1, bound)
+        val (newf2, newbound2) = fixBinding(f2, newbound)
+        (make(newf1, newf2), newbound2)
+      }
+      case Quantifier(make, vars, fsub) => {
+        val alreadybounds = vars.filter(bound.contains(_))
+        val newnames = alreadybounds.map(generateName(_, bound))
+        val renamed = fsub.parallelRename(alreadybounds, newnames)
+        val binding = (vars.toSet -- alreadybounds) ++ newnames
+
+        val (fixedrename, newbound) = fixBinding(renamed, bound ++ binding)
+        val newf = make(binding.toList, fixedrename)
+        (newf, newbound)
+      }
+      // Functions, Variables
+      case f => (f, bound)
     }
-    
-    if (hasDuplicateBindings(f)) {
-      logger.info(s"Formula $f binds variables more than once - renaming bindings")
-    }
-    
-    val negnf = eliminateImplication(f).simplify()
+  }
+
+  def toPrenex(f: Formula) = {
+    val negnf = f.toNegNf()
     val (simp, boundVars) = fixBinding(negnf, Set())
-    
+
     // Simplify first to push negation inward
     val quants = collectQuantifiers(simp)
     val stripped = stripQuantifiers(simp)
-    
+
     quants.foldRight(stripped)((quant, inner) => quant(inner))
   }
 }
\ No newline at end of file

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

@@ -5,6 +5,7 @@ import com.typesafe.scalalogging.LazyLogging
 import de.tum.workflows.Utils
 import de.tum.workflows.foltl.FOLTL._
 import de.tum.workflows.foltl.FOLTL
+import de.tum.workflows.foltl.FormulaFunctions
 
 object LTL extends LazyLogging {
   

src/main/scala/de/tum/workflows/toz3/InvariantChecker.scala

@@ -27,7 +27,12 @@ object InvariantChecker extends LazyLogging {
     val cfg = new HashMap[String, String]()
     cfg.put("timeout", TIMEOUT.toString())
     val ctx = new Context(cfg)
-    val s = ctx.mkSolver()
+
+    val qe = ctx.mkTactic("qe")
+    val default = ctx.mkTactic("smt")
+    val t = ctx.andThen(qe, default)
+
+    val s = ctx.mkSolver(t)
 
     s.add(toZ3.translate(f, ctx))
 
@@ -63,16 +68,33 @@ object InvariantChecker extends LazyLogging {
           case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
         }
       } else precond
-      
-      val test1 = inv.toPrenex()
-      val test2 = stubprecond.toPrenex()
+
+      //      val test1 = inv.toPrenex()
+      //      val test2 = stubprecond.toPrenex()
 
       val f = Implies(inv, stubprecond)
 
       logger.info(s"Checking invariant implication for ${e.label}")
       val tocheck = Neg(f).simplify()
 
-      val (res, solver) = checkOnZ3(tocheck)
+      //      val test3 = tocheck.toPrenex()
+
+      // Transform to existential
+      if (!tocheck.isBS()) {
+        logger.error(s"Invariant implication $tocheck is not in BS fragment!")
+      }
+      
+      val negnf = tocheck.toNegNf()
+    
+      val (agents, inner) = LTL.eliminateExistentials(negnf)
+      val existbound = Exists(agents, inner)
+      val univfree = LTL.eliminateUniversals(existbound, agents)
+      
+//      val test3 = univfree.pretty()
+//      println(test3)
+
+      val (res, solver) = checkOnZ3(univfree)
+      
       if (res != Status.UNSATISFIABLE) {
         msg ++= s"Possibly unsafe: Block may not uphold invariant:\n\n${e.label}\n\n"
         if (res == Status.SATISFIABLE) {
@@ -118,6 +140,23 @@ object InvariantChecker extends LazyLogging {
     Forall(agent, premise → conclusion).simplify()
   }
 
+  def invariantNoninterStubbornBS(spec: Spec) = {
+    val agent = spec.target.params(0)
+
+    val premise = for ((o, t) <- spec.declass) yield {
+      // Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2) 
+      (o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
+    }
+    val quants = premise.flatMap(_._1).toSet.toList // eliminate doubles
+
+    val conclusion = And.make(for (r <- spec.w.sig.preds.toList if r.params.head.typ == agent.typ) yield {
+      val quant = r.params.drop(1)
+      Forall(quant, genEq(r, agent :: quant))
+    })
+
+    Forall(agent, Forall(quants, Implies(And.make(premise.map(_._2)), conclusion))).simplify()
+  }
+
   def invariantAllEqual(spec: Spec) = {
     And.make(for (r <- spec.w.sig.preds.toList) yield {
       Forall(r.params, genEq(r, r.params))