fix a few things, add tests

examples/nonomitting/incarity5.spec

-IGNORE
-
 Workflow
 
 forallmay i True -> R += (i)

examples/nonomitting/notebook.spec

@@ -5,7 +5,7 @@ loop {
 		forallmay x:User, i:Info
 			Written(i, x) → Read += (x, i)
 	} {
-		forallmay x:User, i:Info
+		forall x:User, i:Info
 			Oracle(i, x) → Written += (i, x)
 	}
 }

examples/nonomitting/notebook_stubborn.spec

+Workflow
+
+loop {
+	choose {
+		forallmay x:User, i:Info
+			Written(i, x) → Read += (x, i)
+	} {
+		forall x:User, i:Info
+			Oracle(i, x) → Written += (i, x)
+	}
+}
+
+Declassify
+
+Oracle(i:Info,x:User): Written(i:Info, u:User)
+
+Target
+
+Read(u:User, info:Info)

examples/nonomitting/university.spec

 Workflow
 
-forallmay p:Prof,s:Student,g:Grade
+forall p:Prof,s:Student,g:Grade
     (O(p,s,g)) -> Grading += (p,s,g)
 forallmay p:Prof,t:TA
     True -> Talk1 += (t, p)
@@ -9,7 +9,7 @@ forallmay t:TA,s:Student
 
 Declassify
 
-O(p:Prof,s:Student,g:Grade): Grading(p:Prof,as:Student,g:Grade)
+O(p:Prof,s:Student,g:Grade): False
 
 Target
 

examples/omitting/conference.spec

@@ -7,7 +7,7 @@ forallmay x:A,p:P
 forall x:A,p:P,r:R
 	(Assign(x,p) ∧ O(x,p,r)) → Review += (x,p,r)
 loop {
-	forall x:A,y:A,p:P,r:R (Assign(x,p) ∧ Review(y,p,r)) → Read += (x,r)
+	forall x:A,y:A,p:P,r:R (Assign(x,p) ∧ Review(y,p,r)) → Read += (x,p,r)
 	forallmay x:A,p:P,r:R (Assign(x,p)) → Review += (x,p,r)
 }
 

examples/omitting/conference_fixed_stubborn.spec

+Workflow
+
+forallmay x:A,p:P
+	True → Conf += (x,p)
+forallmay x:A,p:P
+	!Conf(x,p) → Assign += (x,p)
+forall x:A,y:A,p:P,q:P
+	(Assign(x,p) ∧ Assign(y,p) ∧ Conf(x,q) ∧ !Conf(y,q)) → Assign -= (y,p)
+forall x:A,p:P,r:R
+	(Assign(x,p) ∧ O(x,p,r)) → Review += (x,p,r)
+loop {
+	forall x:A,y:A,p:P,r:R (Assign(x,p) ∧ Review(y,p,r)) → Read += (x,r)
+	forallmay x:A,p:P,r:R (Assign(x,p)) → Review += (x,p,r)
+}
+
+Declassify
+
+O(x:A,p:P,r:R): ¬ Conf(xt:A,p:P)
+
+Target
+
+Read(xt:A, rt:R)

examples/omitting/conference_linear_fixed_stubborn.spec

+Workflow
+
+forallmay x:X,p:P
+	True -> Conf += (x,p)
+forallmay x:X,p:P
+	!Conf(x,p) -> Assign += (x,p)
+forall x:X,y:X,p:P,q:P
+	(Conf(x,p) ∧ ¬ Conf(y,p) ∧ Assign(x,q) ∧ Assign(y,q)) -> Assign -= (y,q)
+forall x:X,p:P,r:R
+	(Assign(x,p) ∧ O(x,p,r)) -> Read += (x,p,r)
+forallmay y:X,x:X,p:P 
+	(Assign(x,p) ∧ Assign(y,p)) -> Comm += (x,y,p)
+
+Declassify
+
+O(x:X,p:P,r:R): ¬ Conf(xt:X,p:P)
+
+Target
+
+Comm(xt:X, yt:X, pt:P)

examples/omitting/conference_stubborn.spec

+Workflow
+
+forallmay x:A,p:P
+	True → Conf += (x,p)
+forallmay x:A,p:P
+	!Conf(x,p) → Assign += (x,p)
+forall x:A,p:P,r:R
+	(Assign(x,p) ∧ O(x,p,r)) → Review += (x,p,r)
+loop {
+	forall x:A,y:A,p:P,r:R (Assign(x,p) ∧ Review(y,p,r)) → Read += (x,p,r)
+	forallmay x:A,p:P,r:R (Assign(x,p)) → Review += (x,p,r)
+}
+
+Declassify
+
+O(x:A,p:P,r:R): ¬ Conf(xt:A,p:P)
+
+Target
+
+Read(xt:A, rt:R)

renderpngs.sh

 # /bin/bash
 shopt -s nullglob
+shopt -s globstar
 TIMEOUT=1m
 
 
@@ -8,20 +9,20 @@ echo "Gobbling up metrics"
 rm -f results/allmetrics.metrics
 touch results/allmetrics.metrics
 
-for FILE in results/*/*.metrics
+for FILE in results/**/*.metrics
 do
 	echo "${FILE}:" >> results/allmetrics.metrics
 	cat ${FILE} >> results/allmetrics.metrics
 	echo -e "\n\n" >> results/allmetrics.metrics
 done
 
-for FILE in results/*/*.png
+for FILE in results/**/*.png
 do
 	echo "Deleting ${FILE}"
 	rm $FILE
 done
 
-for FILE in results/*/*.dot
+for FILE in results/**/*.dot
 do
 	NAME=$(basename ${FILE} .dot)
 	DIR=$(dirname "${FILE}")

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

@@ -14,6 +14,7 @@ import scalax.collection.edge.LBase.LEdgeImplicits
 import scalax.collection.io.dot._
 import implicits._
 import Implicits._
+import de.tum.workflows.toz3.InvProperties
 import scalax.collection.GraphTraversal.{BreadthFirst, DepthFirst}
 
 object Encoding extends LazyLogging {
@@ -194,9 +195,9 @@ object Encoding extends LazyLogging {
   //    And.make(List(cfg, sanity, sem, init))
   //  }
   
-  val MAXINVLENGTH = 1200
+  val MAXINVLENGTH = 800
 
-  def toDot(g: WorkflowGraph)(labels:Map[Int, String], edges:Set[g.EdgeT]) = {
+  def toDot(g: WorkflowGraph, elaboration:Option[(InvProperties, Spec)] = None)(labels:Map[Int, String], edges:Set[g.EdgeT]) = {
     val root = DotRootGraph(
       directed = true,
       id = Some("Invariant Labelling"))
@@ -206,24 +207,28 @@ object Encoding extends LazyLogging {
         case label: SimpleBlock => {
           val green = edges.exists(_ == innerEdge)
           val color = List(DotAttr("color", if (green) "green" else "red"))
-          
-          val labelled = if (label.nonEmpty) {
-            DotAttr("label", label.toString) :: color
-          } else { color } 
-          
+
+          val elaborated = (elaboration map {
+            case (prop, spec) => Preconditions.elaborate(label, spec, prop)
+          }).getOrElse(List(label))
+          val strlabel = elaborated.mkString("\n")
+
+          val labelled = DotAttr("label", strlabel) :: color
+
           Some((
             root,
             DotEdgeStmt(
               source.toString,
               target.toString,
               labelled
-              )
+            )
           ))
         }
       }
     }
+
     def nodeTransformer(innerNode: WorkflowGraph#NodeT): Option[(DotGraph, DotNodeStmt)] = {
-      val str = labels(innerNode.value)
+      val str = labels.withDefault(d => s"$d").apply(innerNode.value)
       val label = if (str.length() > MAXINVLENGTH) str.substring(0, MAXINVLENGTH) + "..." + s"(${str.length()} characters)" else str
       Some((root, DotNodeStmt(innerNode.toString, List(DotAttr("label", "Node " + innerNode + ":\n" + label)))))
     }

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

@@ -27,9 +27,9 @@ object MainInvariants extends App with LazyLogging {
     val (res, dot, t) = InvariantChecker.checkInvariantFPDot(spec, invariant(spec))
     val msg = s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n"
 
-    write(s"$name.inv", msg)
+    write(name, s"$name.inv", msg)
     for ((s, i) <- dot.zipWithIndex) {
-      write(s"${name}_$i.dot", s)
+      write(name, s"${name}_$i.dot", s)
     }
   }
 

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

@@ -8,6 +8,7 @@ import de.tum.workflows.foltl.FOLTL._
 import de.tum.workflows.foltl.FOTransformers
 import de.tum.workflows.synth.Model
 import de.tum.workflows.toz3._
+import de.tum.workflows.foltl.Properties
 
 // Labelled Edge to Block
 import Implicits._
@@ -97,22 +98,24 @@ object MainInvariantsInference extends App with LazyLogging {
         val steeredinv = instinv.everywhere {
           case f:Fun if z3map.contains(f) => z3map(f)
         }
+        val steeredInfinv = steeredinv.assumeEmpty(Properties.INFNAME)
 
         // just for testing
-//        val tocheck = List("Conf")
-//
-//        val modelmap = for ((f, vs) <- newmodel.state; v <- vs if !tocheck.contains(f.name)) yield {
-//          v match {
-//            case Neg(f) => (f, False)
-//            case f:Fun => (f, True)
-//          }
-//        }
-//
-//        val modelinv = steeredinv.everywhere {
-//          case f:Fun if modelmap.contains(f) => modelmap(f)
-//        }
-
-        val easyinv = steeredinv.simplify()
+        val tocheck = List("Assign")
+
+        val modelmap = for ((f, vs) <- newmodel.state; v <- vs if !tocheck.contains(f.name)) yield {
+          v match {
+            case Neg(f) => (f, False)
+            case f:Fun => (f, True)
+          }
+        }
+
+        val modelinv = steeredInfinv.everywhere {
+          case f:Fun if modelmap.contains(f) => modelmap(f)
+        }
+
+//        val easyinv = modelinv.simplify()
+        val easyinv = steeredInfinv.simplify()
         logger.info(s"inv: $easyinv")
 
 

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

@@ -20,7 +20,7 @@ object MainLTL extends App with LazyLogging {
 
     var metrics = List[String]()
 
-    write(s"$name.foltl", prop.pretty())
+    write(name, s"$name.foltl", prop.pretty())
     metrics :+= s"$name.foltl: ${prop.opsize()}"
 
     if (!FormulaFunctions.checkSanity(prop)) {
@@ -44,8 +44,8 @@ object MainLTL extends App with LazyLogging {
     metrics :+= s"$name.ltl: ${ltlprop.opsize()}"
     metrics :+= s"Universe: $universe"
 
-    write(s"$name.ltl", ltlprop.toString())
-    write(s"$name.ppltl", ltlprop.pretty())
+    write(name, s"$name.ltl", ltlprop.toString())
+    write(name, s"$name.ppltl", ltlprop.pretty())
 
 
     val owlform = OwlTransformer.toOwl(ltlprop)
@@ -53,7 +53,7 @@ object MainLTL extends App with LazyLogging {
     val (t, sat) = time {
       // simplify owl
       val simped = SimplifierFactory.applyDefault(owlform.formula()).nnf()
-      write(s"$name.owlltl", simped.toString)
+      write(name, s"$name.owlltl",simped.toString)
       logger.info("Simplified owl formula")
       // check owl sat
       logger.info("Checking satisfiability")
@@ -65,7 +65,7 @@ object MainLTL extends App with LazyLogging {
     metrics :+= s"Satisfiable: $sat"
     metrics :+= s"Owl runtime: $t ms"
 
-    write(s"$name.metrics", metrics.mkString("", "\n", "\n"))
+    write(name, s"$name.metrics", metrics.mkString("", "\n", "\n"))
   }
 
   def generate(name: String, spec: Spec, onlystubborn:Boolean) {

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

@@ -10,7 +10,10 @@ import de.tum.workflows.toz3.InvProperties
 object Preconditions extends LazyLogging {
 
   private def elaborateSteps(b: SimpleBlock, s: Spec): List[SimpleBlock] = {
-    val newsteps = for (stmt <- b.steps if stmt.tuple.head.typ == s.target.params.head.typ) yield {
+    val newsteps = for (
+        stmt <- b.steps
+        if s.causals.map(_.typ).contains(stmt.tuple.head.typ) ||
+          stmt.tuple.head.typ == s.target.params.head.typ) yield {
       val fun = Fun(stmt.fun, stmt.tuple)
       // TODO
       val guard = Neg(Eq(fun.in(T1), fun.in(T2)))
@@ -20,7 +23,7 @@ object Preconditions extends LazyLogging {
   }
 
   // For oracly blocks, remove O from guard and add to ForallMay choice predicate
-  def elaborateOraclyBlock(b: SimpleBlock, s: Spec) = {
+  private def elaborateOraclyBlock(b: SimpleBlock, s: Spec) = {
     if (b.isoracly) {
       val stmt = b.steps.head // can only be one
       def fixguard(f: Formula) = {
@@ -62,7 +65,8 @@ object Preconditions extends LazyLogging {
       }
     })
   }
-  
+
+  // TODO: make this a transformation instead of a logics block
   def getUpdate(s:Statement, b:SimpleBlock, choice:Option[Fun], spec:Spec, properties:InvProperties) = {
 
       //        val list = List(s.guard) ++ choice.toList
@@ -109,7 +113,6 @@ object Preconditions extends LazyLogging {
 
   def elaborate(block: SimpleBlock, spec:Spec, properties:InvProperties) = {
     val stepOne = if (!properties.stubborn) elaborateSteps(block, spec) else List(block)
-
     stepOne map { b =>  elaborateOraclyBlock(b, spec) }
   }
 

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

@@ -53,8 +53,8 @@ object Utils extends LazyLogging {
     recclear(fol)
   }
   
-  def write(name: String, prop: String) {
-    val file = new File(s"$RESULTSFOLDER/$name")
+  def write(dir: String, filename:String, prop: String) {
+    val file = new File(s"$RESULTSFOLDER/$dir/$filename")
     if (file.exists()) {
       file.delete()
     }
@@ -62,34 +62,39 @@ object Utils extends LazyLogging {
     val writer = new PrintWriter(file)
     writer.print(prop)
     writer.close()
-    logger.info(s"Written $name")
+    logger.info(s"Written $file")
   }
   
   def check(name:String, desc:String, inv:Formula, spec:Spec, properties:InvProperties) = {
     val model = if (properties.stubborn) "stubborn" else "causal"
-		val filenames = s"${name}_$model${if (desc.isEmpty()) "" else s"_$desc"}"
-		
+
+    val basename = name.split("/").last
+		val filenames = s"${basename}_$model${if (desc.isEmpty()) "" else s"_$desc"}"
+
     // do not blow up the formula with auxilliary elimination
     val (res, graph, labelling, provens, dot, time) =
       InvariantChecker.checkInvariantFPLabelling(spec, inv, properties)
     for ((s, i) <- dot.zipWithIndex) {
-      Utils.write(s"${filenames}_$i.dot", s)
+      Utils.write(name,s"${filenames}_$i.dot", s)
     }
     val strengthenings = for (List(a, b) <- labelling.sliding(2) if (a != b)) yield {
       true
     }
-    
+
+    val elabdot = Encoding.toDot(graph, Some(properties, spec))(Map(), Set())
+    Utils.write(name, s"${filenames}_elaborated.dot", elabdot)
+
     val labels = (for ((node, inv) <- labelling.last) yield {
       s"Node ${node}:\n${inv.pretty()}\n"
     }).mkString("\n")
     
-    Utils.write(s"$filenames.invariants", labels)
+    Utils.write(name, s"$filenames.invariants", labels)
     
     val wfsize = graph.edges.size - 1
     val invsizes = labelling.last.map(_._2.opsize())
     val maxsize = invsizes.max
     val avgsize = invsizes.sum / invsizes.size
-    Utils.write(s"$filenames.metrics",
+    Utils.write(name, s"$filenames.metrics",
         s"""Name: $name
          Description: $desc
          Invariant: $inv

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

@@ -468,8 +468,10 @@ object FormulaFunctions extends LazyLogging {
       if (!changed) sub else toCNFSub(sub)
     }
 
+
     // FIXME: can we do it without prenex? may be expensive later on
-    val normalized = f.toNegNf.toPrenex.simplify()
+    val normalized = f.toNegNf.simplify().toPrenex.simplify()
+    logger.debug(s"Computing CNF of prenex formula of opsize ${normalized.opsize()}")
 
     // normalized is now Quantifiers, then only And/Or with Negation inside
     // no simplification here

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

@@ -122,7 +122,7 @@ object InvariantChecker extends LazyLogging {
           } else {
             logger.info("Relabelled initial node. Terminating.")
             // logger.info(s"Model: ${Z3.printModel(solver.getModel())}")
-            (false, newlabels, provenlist)
+            (false, labellist, provenlist)
           }
         }
       }
@@ -140,7 +140,8 @@ object InvariantChecker extends LazyLogging {
     
     val dot1 = labellings.zip(proven).reverse
     val dot2 = dot1.map(tup => Encoding.toDot(graph)(tup._1.map(t => (t._1, {
-      if (t._2.opsize() <= 5000) t._2.pretty() else "TOO BIG"
+      // if (t._2.opsize() <= 5000) t._2.pretty() else "TOO BIG"
+      t._2.pretty()
     })), tup._2))
 
     (result, graph, labellings.reverse, proven.reverse, dot2, time)

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

@@ -12,6 +12,7 @@ import de.tum.workflows.foltl.FOTransformers
 import de.tum.workflows.foltl.FormulaFunctions
 import it.unimi.dsi.fastutil.longs.Long2BooleanArrayMap
 
+
 object Z3QFree extends LazyLogging {
 
 

src/test/scala/de/tum/workflows/tests/papertests/DemoNoStrengtheningTests.scala

+package de.tum.workflows.tests.papertests
+
+import org.scalatest.FlatSpec
+import org.scalatest.Matchers._
+import org.scalatest.Inspectors._
+
+import de.tum.workflows.foltl.FOLTL._
+import de.tum.workflows.Implicits._
+import de.tum.workflows.blocks._
+import de.tum.workflows.Preconditions
+import de.tum.workflows.foltl.FormulaFunctions
+import de.tum.workflows.ExampleWorkflows
+import de.tum.workflows.toz3.InvariantChecker
+import de.tum.workflows.Encoding._
+import de.tum.workflows.Utils
+import de.tum.workflows.Encoding
+
+import de.tum.workflows.tests.TestUtils._
+import de.tum.workflows.toz3.InvariantGenerator
+
+class DemoNoStrengtheningTests extends FlatSpec {
+
+  // fixed arity, nonomitting - easy
+  it should "fail to prove nonomitting/fixedarity10 alleq" in {
+    val name = "nonomitting/fixedarity10"
+    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
+    assert(!checkSafeStubborn(name, "alleq", inv))
+  }
+  it should "prove nonomitting/fixedarity10_safe alleq" in {
+    val name = "nonomitting/fixedarity10safe"
+    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
+    assert(checkSafeStubborn(name, "alleq", inv))
+  }
+  it should "fail to prove nonomitting/fixedarity15 alleq" in {
+    val name = "nonomitting/fixedarity15"
+    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
+    assert(!checkSafeStubborn(name, "alleq", inv))
+  }
+  it should "prove nonomitting/fixedarity15_safe alleq" in {
+    val name = "nonomitting/fixedarity15safe"
+    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
+    assert(checkSafeStubborn(name, "alleq", inv))
+  }
+  it should "fail to prove nonomitting/fixedarity20 alleq" in {
+    val name = "nonomitting/fixedarity20"
+    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
+    assert(!checkSafeStubborn(name, "alleq", inv))
+  }
+  it should "prove nonomitting/fixedarity20_safe alleq" in {
+    val name = "nonomitting/fixedarity20safe"
+    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
+    assert(checkSafeStubborn(name, "alleq", inv))
+  }
+
+  // nonomitting, incarity
+  it should "prove nonomitting/incarity5 alleq" in {
+    val name = "nonomitting/incarity5"
+    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
+    assert(checkSafeStubborn(name, "alleq", inv))
+  }
+
+
+
+
+
+  // nonomitting, tests
+
+  it should "prove tests/simpleChoiceDeclassified alleq" in {
+    val name = "tests/simpleChoiceDeclassified"
+    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
+    assert(checkSafeStubborn(name, "alleq", inv))
+  }
+  it should "prove tests/simpleChoiceDeclassified causal alleq" in {
+    val name = "tests/simpleChoiceDeclassified"
+    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
+    assert(checkSafeCausal(name, "alleq", inv))
+  }
+  it should "prove tests/simpleChoiceCausal alleq" in {
+    val name = "tests/simpleChoiceCausal"
+    val inv = InvariantGenerator.invariantNoninterSingleBS(ExampleWorkflows.parseExample(name).get)
+    assert(checkSafeStubborn(name, "alleq", inv))
+  }
+  it should "prove tests/simpleChoiceCausal causal alleq" in {
+    val name = "tests/simpleChoiceCausal"
+    val inv = InvariantGenerator.invariantNoninterSingleBS(ExampleWorkflows.parseExample(name).get)
+    assert(!checkSafeCausal(name, "alleq", inv))
+  }
+}

src/test/scala/de/tum/workflows/tests/papertests/DemoNotebook.scala

+package de.tum.workflows.tests.papertests
+
+import org.scalatest.FlatSpec
+import org.scalatest.Matchers._
+import org.scalatest.Inspectors._
+
+import de.tum.workflows.foltl.FOLTL._
+import de.tum.workflows.Implicits._
+import de.tum.workflows.blocks._
+import de.tum.workflows.Preconditions
+import de.tum.workflows.foltl.FormulaFunctions
+import de.tum.workflows.ExampleWorkflows
+import de.tum.workflows.toz3.InvariantChecker
+import de.tum.workflows.Encoding._
+import de.tum.workflows.Utils
+import de.tum.workflows.Encoding
+
+import de.tum.workflows.tests.TestUtils._
+import de.tum.workflows.toz3.InvariantGenerator
+
+class DemoNotebookTest extends FlatSpec {
+
+  it should "prove nonomitting/notebook alleq" in {
+    val name = "nonomitting/notebook_stubborn"
+    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
+    assert(checkSafeStubbornNoElim(name, inv))
+  }
+
+  it should "prove nonomitting/notebook causal alleq" in {
+    val name = "nonomitting/notebook"
+    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
+    assert(checkSafeCausal(name, "alleq", inv))
+  }
+
+  it should "prove nonomitting/notebook causal elim alleq" in {
+    val name = "nonomitting/notebook"
+    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
+    assert(checkSafeCausalElim(name, "elim", inv))
+  }
+
+}