Commit 5acbb2b7 authored by Christian Müller's avatar Christian Müller

fix iteration, add dot support

parent 25b85f4d
......@@ -2,7 +2,7 @@ name := "LoopingWorkflows"
version := "0.1"
scalaVersion := "2.12.2"
scalaVersion := "2.12.3"
EclipseKeys.withBundledScalaContainers := false
......@@ -11,7 +11,8 @@ libraryDependencies ++= Seq(
"ch.qos.logback" % "logback-classic" % "1.1.7",
"org.scalactic" %% "scalactic" % "3.0.1",
"org.scalatest" %% "scalatest" % "3.0.1" % "test",
"org.scala-graph" %% "graph-core" % "1.11.4",
"org.scala-graph" %% "graph-core" % "1.12.1",
"org.scala-graph" %% "graph-dot" % "1.12.1",
"org.scala-lang.modules" %% "scala-parser-combinators" % "1.0.5"
)
......@@ -14,6 +14,8 @@ import de.tum.workflows.foltl.FormulaFunctions._
import com.typesafe.scalalogging._
import scalax.collection.edge.LBase.LEdgeImplicits
import scalax.collection.io.dot._
import implicits._
import Implicits._
object Encoding extends LazyLogging {
......@@ -180,7 +182,7 @@ object Encoding extends LazyLogging {
// def toFOLTL(w: Workflow) = {
// val g = toGraph(w)
// logger.info("Graph of w:\n" + g)
//
//
// val cfg = encodeGraph(g)
// logger.info(s"cfg(w): $cfg")
// val sanity = encodeSanity(g)
......@@ -189,7 +191,30 @@ object Encoding extends LazyLogging {
// logger.info(s"sem(w): $sem")
// val init = encodeInitial(w.sig, g)
// logger.info(s"init(w): $init")
//
//
// And.make(List(cfg, sanity, sem, init))
// }
def toDot(g: WorkflowGraph, labels:Map[WorkflowGraph#NodeT, String]) = {
val root = DotRootGraph(
directed = true,
id = Some("Invariant Labelling"))
def edgeTransformer(innerEdge: WorkflowGraph#EdgeT): Option[(DotGraph, DotEdgeStmt)] = innerEdge.edge match {
case LDiEdge(source, target, label) => label match {
case label: SimpleBlock =>
Some((
root,
DotEdgeStmt(
source.toString,
target.toString,
if (label.nonEmpty) List(DotAttr("label", label.toString))
else Nil)))
}
}
def nodeTransformer(innerNode: WorkflowGraph#NodeT): Option[(DotGraph, DotNodeStmt)] =
Some(root, DotNodeStmt(innerNode.toString, List(DotAttr("label", labels(innerNode)))))
g.toDot(root, edgeTransformer, None, Some(nodeTransformer))
}
}
\ No newline at end of file
......@@ -15,27 +15,27 @@ import de.tum.workflows.blocks.Spec
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.toz3.InvariantChecker
object Main extends App with LazyLogging {
object MainInvariants extends App with LazyLogging {
def generate(name: String, spec: Spec) {
logger.info(s"Encoding Spec:\n$spec")
val t1 = "pi1"
val t2 = "pi2"
def invariants = List(
InvariantChecker.invariantNoninterStubbornBS _
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
)
def invariant =
InvariantChecker.invariantNoninterStubbornBS _
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
def msgs = for (inv <- invariants) yield {
val (t, (safe, msg)) = time {
InvariantChecker.checkInvariant(spec.w, inv(spec), true)
}
s"Proving Invariant (took $t ms):\n$msg\n"
val (t, (res, dot)) = time {
// InvariantChecker.checkInvariantOnce(spec.w, inv(spec), true)
InvariantChecker.checkInvariantFP(spec.w, invariant(spec), true)
}
val worked = res.isDefined
val msg = s"Invariant was ${if (worked) "" else "not "}proven (took $t ms)\n"
write(s"${name}.inv", msgs.mkString("\n"))
write(s"${name}.inv", msg)
write(s"${name}.dot", dot)
}
def generateExample(name: String) {
......
......@@ -18,6 +18,9 @@ import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.foltl.Properties
import de.tum.workflows.foltl.FormulaFunctions
import scalax.collection.Graph
import de.tum.workflows.Encoding.WorkflowGraph
import scala.annotation.tailrec
object InvariantChecker extends LazyLogging {
......@@ -29,15 +32,28 @@ object InvariantChecker extends LazyLogging {
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)
// val qe = ctx.mkTactic("qe")
// val default = ctx.mkTactic("smt")
// val t = ctx.andThen(qe, default)
// val s = ctx.mkSolver(t)
val s = ctx.mkSolver()
// Make QFree - will work for any A* or A*E* formula
val tocheck = Neg(f).simplify()
if (!tocheck.isBS()) {
logger.error(s"Not in BS: ${tocheck.pretty}")
}
val univfree = LTL.instantiateUniversals(tocheck)
// univfree is now in E*, so can be solved as SAT Problem
val stripped = FormulaFunctions.stripQuantifiers(univfree)
// val prefix = FormulaFunctions.collectQuantifiersSub(univfree)
val satform = LTL.eliminatePredicates(stripped)
// Checking QFree
s.add(Z3QFree.translate(f, ctx))
s.add(Z3QFree.translate(satform, ctx))
// Send to z3
val c = s.check()
......@@ -46,12 +62,12 @@ object InvariantChecker extends LazyLogging {
}
if (c == Status.SATISFIABLE) {
logger.info(s"Z3 status satisfiable")
// logger.info(s"${s.getModel()}")
// logger.info(s"${s.getModel()}")
}
(c, s)
}
def checkBlockInvariant(sig:Signature, b: SimpleBlock, pre: Formula, post: Formula, stubborn: Boolean, isfirst: Boolean) = {
def checkBlockInvariant(sig: Signature, b: SimpleBlock, pre: Formula, post: Formula, stubborn: Boolean, isfirst: Boolean) = {
val precond = Preconditions.weakestPrecondition(post, b)
// Stubborn agents -> remove trace variable from choice predicate
......@@ -60,7 +76,7 @@ object InvariantChecker extends LazyLogging {
case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
}
} else precond
// TODO: do we do this here?
val firstprecond = if (isfirst) {
stubprecond.assumeEmpty(sig.preds.map(_.name).toList)
......@@ -72,31 +88,66 @@ object InvariantChecker extends LazyLogging {
val f = Implies(pre, firstprecond)
logger.info(s"Checking invariant implication for $b")
val tocheck = Neg(f).simplify()
// val test3 = tocheck.toPrenex()
checkOnZ3(f.simplify())
}
// Transform to existential
if (!tocheck.isBS()) {
logger.error(s"Not in BS: Invariant implication ${tocheck.pretty}")
def checkInvariantFP(w: Workflow, inv: Formula, stubborn: Boolean) = {
val graph = Encoding.toGraph(w)
type Node = graph.NodeT
type Edge = graph.EdgeT
@tailrec
def checkInvariantRec(labels: Map[Node, Formula], proven: Set[Edge]): Option[Map[Node, Formula]] = {
// check if done, i.e. all edges proven
val toProve = (graph.edges -- proven)
if (toProve.isEmpty) {
Some(labels)
} else {
// take one edge to prove
val next = toProve.head
// try to prove
val pre = labels(next._1)
val post = labels(next._2)
val (status, solver) = checkBlockInvariant(w.sig, next, pre, post, stubborn, next._1.hasPredecessors)
if (status == Status.UNSATISFIABLE) {
// Negation of implication unsat
// --> safe, continue with larger proven set
checkInvariantRec(labels, proven + next)
} else {
// Negation of implication sat
// --> unsafe, relabel incoming node, invalidate all proven guarantees for that node
// check if relabelled invariant still satisfiable
val newinv = And(labels(next._1), Preconditions.weakestPrecondition(post, next))
val (status2, solver2) = checkOnZ3(newinv)
val newlabels = labels.updated(next._1, newinv)
val newproven = proven.filterNot(_._1 == next._1)
if (status2 == Status.UNSATISFIABLE) {
// Negation of newinv still unsat, newinv still sat
checkInvariantRec(newlabels, newproven)
} else {
None
}
}
}
}
val univfree = LTL.instantiateUniversals(tocheck)
// univfree is now in E*, so can be solved as SAT Problem
val stripped = FormulaFunctions.stripQuantifiers(univfree)
// val prefix = FormulaFunctions.collectQuantifiersSub(univfree)
val satform = LTL.eliminatePredicates(stripped)
// create labelling
val labels = (for (n <- graph.nodes) yield { n -> inv }) toMap
val result = checkInvariantRec(labels, Set())
// val test3 = stripped.pretty()
// println(test3)
val dot = Encoding.toDot(graph, labels.map(t => (t._1, t._2.pretty())))
checkOnZ3(satform.simplify())
(result, dot)
}
def checkInvariant(w: Workflow, inv: Formula, stubborn: Boolean) = {
def checkInvariantOnce(w: Workflow, inv: Formula, stubborn: Boolean) = {
// Build graph
val graph = Encoding.toGraph(w)
......@@ -104,16 +155,16 @@ object InvariantChecker extends LazyLogging {
val msg = new StringBuilder()
msg ++= s"Trying to prove safe with invariant:\n\n${inv.pretty()}\n\n"
// Check all edges
// Check all edges
val list = for (e <- graph.edges) yield {
// Check I -> WP[w](inv)
val b: SimpleBlock = e
// Special handling for first block
// TODO: Replace by iteration
val isfirst = !e.from.hasPredecessors
val (res, solver) = checkBlockInvariant(w.sig, b, inv, inv, stubborn, isfirst)
if (res != Status.UNSATISFIABLE) {
......@@ -149,7 +200,7 @@ object InvariantChecker extends LazyLogging {
val agent = spec.target.params(0)
val premise = And.make(for ((o, t) <- spec.declass) yield {
// Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
// Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
Forall(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
})
......@@ -165,7 +216,7 @@ object InvariantChecker extends LazyLogging {
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)
// 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
......
......@@ -29,7 +29,7 @@ class InvariantTest extends FlatSpec {
val newinv = And(inv, both)
val (safe, msg) = InvariantChecker.checkInvariant(spec.w, newinv, true)
val (safe, msg) = InvariantChecker.checkInvariantOnce(spec.w, newinv, true)
println(msg.toString())
safe should be(true)
......
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