add counterexample

build.sbt

@@ -2,7 +2,7 @@ name := "LoopingWorkflows"
 
 version := "0.1"
 
-scalaVersion := "2.12.1"
+scalaVersion := "2.12.2"
 
 EclipseKeys.withBundledScalaContainers := false
 

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

@@ -40,7 +40,7 @@ object InvariantChecker extends LazyLogging {
       if (c == Status.SATISFIABLE) {
         logger.info(s"Z3 model:\n${s.getModel()}")
       }
-      c
+      (c, s)
   }
   
   def checkStubborn(w:Workflow, inv:Formula) = {
@@ -68,9 +68,16 @@ object InvariantChecker extends LazyLogging {
       logger.info(s"Checking invariant implication for ${e.label}")
       val tocheck = Neg(f).simplify()
       
-      val res = checkOnZ3(tocheck)
+      val (res, solver) = checkOnZ3(tocheck)
       if (res != Status.UNSATISFIABLE) {
-        msg ++= s"Possibly unsafe: Block\n\n${e.label}\n\nmay not uphold invariant.\n"
+        msg ++= s"Possibly unsafe: Block may not uphold invariant:\n\n${e.label}\n\n"
+        if (res == Status.SATISFIABLE) {
+          msg ++= "Satisfying model:\n"
+          msg ++= toZ3.printModel(solver.getModel())
+        } else {
+          msg ++= s"Z3 result: $res\n"
+        }
+        msg ++= "\n"
         logger.info(s"Could not prove invariant $inv")
         logger.info(s"Z3 status $res")
         logger.info(s"Block ${e.label} may not uphold it")

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

@@ -190,8 +190,6 @@ object toZ3 extends LazyLogging {
         ctx.mkForall(sorts, names, e1, 0, null, null, null, null)
       }
 
-      // TODO: forallotherthan
-
       case And(f1, f2) => {
         val e1 = toZ3(ctx, f1, texpr, tvar, var_ctx)
         val e2 = toZ3(ctx, f2, texpr, tvar, var_ctx)
@@ -220,7 +218,7 @@ object toZ3 extends LazyLogging {
         val e = toZ3(ctx, f1, texpr, tvar, var_ctx)
         ctx.mkNot(e)
       }
-      
+
       case True => {
         ctx.mkTrue()
       }
@@ -231,28 +229,60 @@ object toZ3 extends LazyLogging {
   }
 
   def translate(f: Formula, ctx: Context) = {
-//    logger.info(s"Using formula:\n$f")
-    
+    //    logger.info(s"Using formula:\n$f")
+
     if (!f.freeVars().isEmpty) {
       logger.error(s"Cannot check - formula contains free variables ${f.freeVars()}")
     }
-    
+
     fun_ctx.clear()
     val expr = toZ3(ctx, f, ctx.mkInt(0), None, Map())
-//    logger.info(s"Built Z3 expression:\n$expr")
+    //    logger.info(s"Built Z3 expression:\n$expr")
     expr
   }
 
   def translate(f: Formula, ctx: Context, varctx: VarCtx) = {
-//    logger.info(s"Using formula:\n${f.pretty()}")
-    
+    //    logger.info(s"Using formula:\n${f.pretty()}")
+
     if (!f.freeVars().isEmpty) {
       logger.error(s"Cannot check - formula contains free variables ${f.freeVars()}")
     }
-    
+
     fun_ctx.clear()
     val expr = toZ3(ctx, f, ctx.mkInt(0), None, varctx)
-//    logger.info(s"Built Z3 expression:\n$expr")
+    //    logger.info(s"Built Z3 expression:\n$expr")
     expr
   }
+
+  def printModel(model: Model) = {
+
+    val sb = new StringBuilder()
+
+    val consts = model.getConstDecls()
+
+    val vals = consts.map(_.apply())
+    val typedvals = vals.groupBy(_.getSort)
+
+    sb ++= "Universe:\n"
+    for ((k, v) <- typedvals) {
+      sb ++= s"Type $k: ${v.mkString(",")}\n"
+    }
+
+    sb ++= "Evaluations:\n"
+    val sorted = model.getFuncDecls().sortBy(_.getName.toString())
+    for (f <- sorted) {
+      val interp = model.getFuncInterp(f)
+      val entries = interp.getEntries
+      for (e <- entries) {
+        val args = for (arg <- e.getArgs.toList) yield {
+          arg.getSort + " " + arg
+        }
+        sb ++= f.getName + args.mkString("(", ", ", ")") + " = " + e.getValue() + "\n"
+      }
+
+      val emptyargs = List.fill(f.getArity)("_")
+      sb ++= f.getName + emptyargs.mkString("(", ", ", ")") + " = " + interp.getElse() + "\n\n"
+    }
+    sb.toString()
+  }
 }

src/test/scala/Test.scala

 import de.tum.workflows.foltl.FOLTL._
 import de.tum.workflows.foltl.FOLTL
+import com.microsoft.z3.Context
+import java.util.HashMap
+import com.microsoft.z3.Status
+import de.tum.workflows.toz3.toZ3
+import org.omg.CORBA.TIMEOUT
 
+import de.tum.workflows.Implicits._
+import com.microsoft.z3.Model
 
 object Test extends App {
   
-  val a = Var("a", "A")
-  val a2 = Var("a", "A")
+  val TIMEOUT = 30000 // in milliseconds
+
+  val easyForm = Exists(List("x"), And(Fun("p", List("x")), Next(Neg(Fun("p", List("x"))))))
+
+  val cfg = new HashMap[String, String]()
+  cfg.put("timeout", TIMEOUT.toString())
+
+  val ctx = new Context(cfg)
+
+  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(easyForm, ctx))
+  val c = s.check()
+  val model = s.getModel()
+  
+  println(s"Z3 model:\n${model}")
+  
+  val consts = model.getConstDecls()
+  println(consts(0).getName)
   
-  val test = List(a)
+  println("MODEL:")
+  toZ3.printModel(model)
   
-  println(test.contains(a2))
 }
\ No newline at end of file