Commit 6fec927c authored by Christian Müller's avatar Christian Müller

add invariant checker

parent 1268024b
......@@ -14,7 +14,7 @@ import de.tum.workflows.foltl.FormulaFunctions._
import com.typesafe.scalalogging._
import scalax.collection.edge.LBase.LEdgeImplicits
object BlockImplicit extends LEdgeImplicits[SimpleBlock]; import BlockImplicit._
import Implicits._
object Encoding extends LazyLogging {
......
package de.tum.workflows
import de.tum.workflows.foltl.FOLTL._
import scalax.collection.edge.LBase.LEdgeImplicits
import de.tum.workflows.blocks.SimpleBlock
object Implicits {
object Implicits extends LEdgeImplicits[SimpleBlock] {
implicit def toList[A](v: A): List[A] = List(v)
// Logic
......
......@@ -44,7 +44,7 @@ case class Spec(w: Workflow, declass: List[(Fun, Formula)], target: Fun, causals
s match {
case b:SimpleBlock => {
// all predicates should only appear at most once
val pred = w.sig.preds.find(p => b.steps.count(s => s.fun == p.name) <= 1)
val pred = w.sig.preds.find(p => b.steps.count(s => s.fun == p.name) > 1)
pred.map(p =>
logger.error(s"Predicate $p updated more than once in $b")
)
......
......@@ -15,7 +15,8 @@ object FormulaFunctions extends LazyLogging {
// And, Or, Eq, Implies
case BinOp(_, t1, t2) => free(t1, bound) ++ free(t2, bound)
case Fun(_, Some(ind), ps) => (ps.toSet -- bound) + Var(ind)
// TODO: path is not a free variable anymore
// case Fun(_, Some(ind), ps) => (ps.toSet -- bound) + Var(ind)
case Fun(_, _, ps) => (ps.toSet -- bound)
case v: Var if !bound(v) => Set(v)
case x => Set()
......
package de.tum.workflows.toz3
import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.ltl.LTL
import de.tum.workflows.Implicits._
import de.tum.workflows.WorkflowParser
import de.tum.workflows.Encoding
import de.tum.workflows.Preconditions
import scalax.collection.edge.LDiEdge // labeled directed edge
import com.microsoft.z3.Context
import java.util.HashMap
import org.omg.CORBA.TIMEOUT
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
object InvariantChecker extends LazyLogging {
val TIMEOUT = 60000 // in milliseconds
def checkOnZ3(f:Formula) = {
// Set up Z3
val cfg = new HashMap[String, String]()
cfg.put("timeout", TIMEOUT.toString())
val ctx = new Context(cfg)
// val t = ctx.andThen(ctx.mkTactic("qe"), ctx.mkTactic("smt"))
val s = ctx.mkSolver()
s.add(toZ3.translate(f, ctx))
// Send to z3
val c = s.check()
if (c == Status.UNKNOWN) {
logger.info(s"Z3 status unknown: ${s.getReasonUnknown()}")
}
if (c == Status.SATISFIABLE) {
logger.info(s"Z3 model:\n${s.getModel()}")
}
c
}
def checkStubborn(w:Workflow, inv:Formula) = {
// Build graph
val graph = Encoding.toGraph(w)
// Check all edges
val list = for (e <- graph.edges) yield {
// Check I -> WP[w](inv)
val b:SimpleBlock = e
val precond = Preconditions.weakestPrecondition(inv, b)
// Stubborn agents -> remove trace variable from choice predicate
val stubprecond = precond.everywhere {
case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
}
val f = Implies(inv, stubprecond)
logger.info(s"Checking invariant implication for ${e.label}")
val tocheck = Neg(f).simplify()
val res = checkOnZ3(tocheck)
if (res != Status.UNSATISFIABLE) {
logger.info(s"Could not prove invariant $inv")
logger.info(s"Z3 status $res")
logger.info(s"Block ${e.label} may not uphold it")
}
res == Status.UNSATISFIABLE
}
val safe = list.reduceLeft(_ && _)
if (safe) {
logger.info(s"Workflow $w proven safe for invariant $inv")
}
safe
}
}
\ No newline at end of file
......@@ -225,6 +225,11 @@ object toZ3 extends LazyLogging {
def translate(f: Formula, ctx: Context) = {
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")
......@@ -233,6 +238,11 @@ object toZ3 extends LazyLogging {
def translate(f: Formula, ctx: Context, varctx: VarCtx) = {
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")
......
......@@ -20,7 +20,7 @@ import de.tum.workflows.blocks._
class EncodingTest extends FlatSpec {
val w = ExampleWorkflows.parseExample("test/simpleChoice").get.w
val w = ExampleWorkflows.parseExample("tests/simpleChoice").get.w
// shorthands
val n0 = Fun("n0", List())
......
package de.tum.workflows.ltl.tests
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
class InvariantTest extends FlatSpec {
"InvariantChecker" should "prove simple things safe" in {
val wf = ExampleWorkflows.parseExample("tests/simpleChoiceNoOracle").get.w
val inv = Forall(List("a","b"), Eq(Fun("R", Some("t1"), List("a","b")), Fun("R", Some("t2"), List("a","b"))))
val safe = InvariantChecker.checkStubborn(wf, inv)
safe should be (true)
}
it should "prove fail to prove unsafe workflows safe" in {
val wf = ExampleWorkflows.parseExample("tests/simpleChoice").get.w
val inv = Forall(List("a","b"), Eq(Fun("R", Some("t1"), List("a","b")), Fun("R", Some("t2"), List("a","b"))))
val safe = InvariantChecker.checkStubborn(wf, inv)
safe should be (false)
}
}
\ No newline at end of file
......@@ -25,7 +25,7 @@ class Z3Test extends FlatSpec with LazyLogging with BeforeAndAfterEach {
var ctx: Context = null
var s: Solver = null
val TIMEOUT = 60000 // in milliseconds
val TIMEOUT = 30000 // in milliseconds
override def beforeEach() = {
val cfg = new HashMap[String, String]()
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment