Commit aa3504e5 authored by Christian Müller's avatar Christian Müller

model extraction

parent 663f1e49
......@@ -11,7 +11,7 @@ libraryDependencies ++= Seq(
"ch.qos.logback" % "logback-classic" % "1.1.7",
"org.scalactic" %% "scalactic" % "3.0.4" % "test",
"org.scalatest" %% "scalatest" % "3.0.4" % "test",
"org.scala-graph" %% "graph-core" % "1.12.1",
"org.scala-graph" %% "graph-core" % "1.12.5",
"org.scala-graph" %% "graph-dot" % "1.12.1",
"org.scala-lang.modules" %% "scala-parser-combinators" % "1.0.5"
)
......
sbt.version=1.1.2
sbt.version=1.1.6
......@@ -27,10 +27,7 @@ object MainInvariants extends App with LazyLogging {
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
val (t, (res, dot)) = time {
// InvariantChecker.checkInvariantOnce(spec.w, inv(spec), true)
InvariantChecker.checkInvariantFP(spec, invariant(spec))
}
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)
......
package de.tum.workflows
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils._
import de.tum.workflows.blocks.Spec
import de.tum.workflows.toz3._
object MainInvariantsInference extends App with LazyLogging {
def generate(name: String, spec: Spec) {
logger.info(s"Encoding Spec:\n$spec")
def invariant =
InvariantGenerator.invariantNoninterStubbornSingleBS _
// InvariantGenerator.invariantNoninterStubbornBS _
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
val (res, label, t) = InvariantChecker.checkInvariantFPHeadLabel(spec, invariant(spec), InvProperties(stubborn = false, eliminateAux = false))
val msg = s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n"
// Invariant not valid
if (!res) {
// Try to break headlabel invariant
val (status, solver) = InvariantChecker.checkOnZ3(label)
if (status == Status.SATISFIABLE) {
// Broken, found model
// logger.info(s"Model:\n${Z3.printModel(solver.getModel())}")
logger.info(s"Initial State Invariant: ${label}")
val model = Z3QFree.modelFacts(solver.getModel())
model foreach { f => logger.info(f.toString()) }
// Not constant
val tar = 1
val g = Encoding.toGraph(spec.w)
} else {
logger.error("Invariant not valid, but also not satisfiable.")
}
}
}
def generateExample(name: String) {
logger.info(s"Generating $name")
val spec = ExampleWorkflows.parseExample(name)
if (spec.isEmpty) {
logger.error(s"Not a valid spec: $name")
}
spec.foreach(generate(name, _))
}
def generateAllExamples() {
clear()
// Fill results alphabetically
for (k <- ExampleWorkflows.examples.keys.toList.sorted) {
generateExample(k)
}
}
clear()
// generateExample("nonomitting/conference")
generateExample("tests/conference_linear_small")
// generateExample("tests/loopexampleNoOracle")
// generateAllExamples()
}
\ No newline at end of file
......@@ -70,7 +70,7 @@ object Utils extends LazyLogging {
val filenames = s"${name}_$model${if (desc.isEmpty()) "" else s"_$desc"}"
// do not blow up the formula with auxilliary elimination
val (res, graph, labelling, provens, dot, time) =
val (res, graph, labelling, provens, dot, time, headlabel) =
InvariantChecker.checkInvariantFPLabelling(spec, inv, properties)
for ((s, i) <- dot.zipWithIndex) {
Utils.write(s"${filenames}_$i.dot", s)
......
......@@ -22,7 +22,7 @@ import de.tum.workflows.foltl.Properties
case class InvProperties(stubborn:Boolean, eliminateAux:Boolean) { }
object InvProperties {
val DEFAULT = InvProperties(true, true)
val DEFAULT = InvProperties(stubborn = true, eliminateAux = true)
}
object InvariantChecker extends LazyLogging {
......@@ -47,10 +47,9 @@ object InvariantChecker extends LazyLogging {
// Can only check universal things
val neg = Neg(f).simplify()
// univfree is now in E*, so can be solved as SAT Problem
// neg is now in E*, so can be solved as SAT Problem
val stripped = FormulaFunctions.stripQuantifiers(neg)
// val prefix = FormulaFunctions.collectQuantifiersSub(univfree)
val satform = FOTransformers.eliminatePredicates(stripped)
// Checking QFree
......@@ -107,7 +106,7 @@ object InvariantChecker extends LazyLogging {
val labels = labellist.head
val proven = provenlist.head
// check if done, i.e. all edges proven
val toProve = (graph.edges -- proven)
val toProve = graph.edges -- proven
if (toProve.isEmpty) {
logger.info("Everything proven. Terminating.")
(true, labellist, provenlist)
......@@ -137,22 +136,22 @@ object InvariantChecker extends LazyLogging {
// check if relabelled invariant still satisfiable
// never relabel initial node
logger.info(s"Invariant not inductive, strengthening.")
if (!isfirst) {
// check if strengthened -> old_inv else use conjunction
// val strengthened = Preconditions.abstractPrecondition(post, next, spec, properties)
val newinv = And(labels(next._1), strengthened).simplify()
val nostrangebindings = FormulaFunctions.checkBindings(newinv)
if (!nostrangebindings) {
logger.error("New invariant binds variables more than once")
logger.error(s"Invariant would be $newinv")
}
val newlabels = labels.updated(next._1, strengthened)
val newinv = And(labels(next._1), strengthened).simplify()
val nostrangebindings = FormulaFunctions.checkBindings(newinv)
if (!nostrangebindings) {
logger.error("New invariant binds variables more than once")
logger.error(s"Invariant would be $newinv")
}
val newlabels = labels.updated(next._1, strengthened)
if (!isfirst) {
val invalidated = proven.filter(_._2 == next._1)
val newproven = (proven -- invalidated) + next
val (status2, solver2) = checkOnZ3(Implies(newinv, False))
if (status2 == Status.SATISFIABLE) {
// Negation of newinv still sat, newinv does not imply false)
......@@ -163,9 +162,9 @@ object InvariantChecker extends LazyLogging {
(false, newlabels :: labellist, newproven :: provenlist)
}
} else {
logger.info("Would have to relabel initial node. Terminating.")
logger.info(s"Model: ${Z3.printModel(solver.getModel())}")
(false, labellist, provenlist)
logger.info("Relabelled initial node. Terminating.")
// logger.info(s"Model: ${Z3.printModel(solver.getModel())}")
(false, newlabels, provenlist)
}
}
}
......@@ -176,16 +175,25 @@ object InvariantChecker extends LazyLogging {
val (time, (result, labellings, proven)) = Utils.time { checkInvariantRec(labels, List(Set())) }
val dot1 = labellings.zip(proven).reverse
val dot2 = dot1.map((tup) => Encoding.toDot(graph)(tup._1.map(t => (t._1, {
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"
})), tup._2))
// Find out label of initial node
val startnode = graph.find(0).get
val headlabel = labellings.last.get(startnode).get
(result, graph, labellings.reverse, proven.reverse, dot2, time)
(result, graph, labellings.reverse, proven.reverse, dot2, time, headlabel)
}
def checkInvariantFP(spec: Spec, inv: Formula, properties:InvProperties = InvProperties.DEFAULT) = {
val (result, graph, afterlabels, proven, dot, time) = checkInvariantFPLabelling(spec, inv, properties)
(result, dot)
def checkInvariantFPDot(spec: Spec, inv: Formula, properties:InvProperties = InvProperties.DEFAULT) = {
val (result, graph, afterlabels, proven, dot, time, _) = checkInvariantFPLabelling(spec, inv, properties)
(result, dot, time)
}
def checkInvariantFPHeadLabel(spec: Spec, inv: Formula, properties:InvProperties = InvProperties.DEFAULT) = {
val (result, graph, afterlabels, proven, dot, time, headlabel) = checkInvariantFPLabelling(spec, inv, properties)
(result, headlabel, time)
}
def checkInvariantOnce(spec: Spec, inv: Formula, properties: InvProperties) = {
......
......@@ -270,7 +270,7 @@ object Z3 extends LazyLogging {
// sb ++= s"Type $k: ${v.mkString(",")}\n"
// }
sb ++= "Evaluations:\n"
sb ++= "Relations:\n"
val sortedConsts = model.getConstDecls().sortBy(_.getName.toString())
val (l1, l2) = sortedConsts.partition(s => {
......@@ -279,7 +279,7 @@ object Z3 extends LazyLogging {
case _ => false
}
})
val funs = l1.map(s => {
val interp = model.getConstInterp(s)
(FunFromVar.unapply(s.getName.toString).get, interp.toString)
......@@ -299,6 +299,8 @@ object Z3 extends LazyLogging {
}
sb ++= "\n"
}
sb ++= "\nNon-Relations:\n"
// Rest of the consts
for (f <- l2) {
......
......@@ -146,6 +146,18 @@ object Z3QFree extends LazyLogging {
}
}
def modelFacts(model: Model): List[(Fun, Formula)] = {
val sortedConsts = model.getConstDecls().sortBy(_.getName.toString())
val funs = sortedConsts.map(s => {
val fun = FunFromVar.unapply(s.getName.toString).get
val interp = Z3QFree.mapback(model.getConstInterp(s))
(fun, interp)
}) toList
funs
}
def translate(f: Formula, ctx: Context) = {
// logger.info(s"Using formula:\n$f")
val expr = toZ3(ctx, f)
......
......@@ -42,7 +42,7 @@ class InvariantTest extends FlatSpec {
val inv = Forall(List("a", "b"), Eq(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
val (safe, msg) = InvariantChecker.checkInvariantFP(spec, inv)
val (safe, msg, time) = InvariantChecker.checkInvariantFPDot(spec, inv)
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