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

untouched map, paths

parent af9e6806
package de.tum.workflows
import scalax.collection.Graph // or scalax.collection.mutable.Graph
import scalax.collection.Graph
import scalax.collection.GraphPredef._
import scalax.collection.GraphEdge._
import scalax.collection.edge.LDiEdge // labeled directed edge
import scalax.collection.edge.Implicits._ // shortcuts
import scalax.collection.edge.LDiEdge
import scalax.collection.edge.Implicits._
import blocks._
import de.tum.workflows.foltl.FOLTL
import de.tum.workflows.foltl.FOLTL._
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._
import scalax.collection.GraphTraversal.{BreadthFirst, DepthFirst}
object Encoding extends LazyLogging {
......@@ -232,4 +230,34 @@ object Encoding extends LazyLogging {
g.toDot(root, edgeTransformer, None, Some(nodeTransformer))
}
/**
* Get an underapproximation of relation symbols that are sure to be untouched, i.e. empty
*
* @param w the graph
*/
def untouchedMap(g:WorkflowGraph, sig:Signature): Map[g.NodeT, Set[String]] = {
val sourceid = 0
val sourcenode = g.get(sourceid)
val nodes = sourcenode.withKind(BreadthFirst).filterNot(_ == sourcenode)
// FIXME: this could 1. be more functional, 2. not just give up for loops
var map:Map[g.NodeT, Set[String]] = Map().withDefault(_ => Set())
// initially all untouched
map = map.updated(g.get(sourceid), sig.preds.map(_.name))
for (elem <- nodes) {
// If all predecessors are known
if (elem.diPredecessors.forall(map.contains(_))) {
val union = elem.diPredecessors.flatMap(map(_))
val touched = elem.incoming.flatMap(_.updating)
map = map.updated(elem, union -- touched)
}
}
map
}
}
\ No newline at end of file
......@@ -14,7 +14,7 @@ import Implicits._
object MainInvariantsInference extends App with LazyLogging {
def generate(name: String, spec: Spec) {
def generate(name: String, spec: Spec, tar:Int) {
logger.info(s"Encoding Spec:\n$spec")
def invariant =
......@@ -27,13 +27,14 @@ object MainInvariantsInference extends App with LazyLogging {
val inv = invariant(spec)
val (res, graph, labels, t) = InvariantChecker.checkInvariantFPHeadLabel(spec, inv, props)
logger.info(s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n")
logger.info(s"Invariant was ${inv}")
logger.info(s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n")
logger.info(s"Graph: $graph")
val tar = 0
val headlabel = labels(graph.get(tar))
val src = 0
val headlabel = labels(graph.get(src))
// Invariant not valid
if (!res) {
......@@ -62,28 +63,67 @@ object MainInvariantsInference extends App with LazyLogging {
}
logger.info(s"Model Facts: ${facts}")
val vars = z3model.flatMap(_._1.freeVars()).distinct
val vars = z3model.flatMap { case (f:Fun,b:Formula) => f.freeVars() }.distinct
val groupedvars = vars.groupBy { _.typ }
// These should only contain Choice and Oracle predicates
val state = Model.emptystate(spec, groupedvars, props)
val model = Model(groupedvars, And.make(facts), state)
// get outgoing edge
// FIXME: Don't just take head
val edge = graph.get(tar).outgoing.head
val newmodel = Model.warp(And.make(facts), edge, spec, props, model)
logger.info(s"Initial Model: ${model.prettyprint()}")
// get path
val source = graph.get(0)
val target = graph.get(tar)
val path = source.shortestPathTo(target).get // Has to be connected
logger.info(s"Path from source to target: $path")
val newmodel = path.edges.foldLeft(model)((m, e) => m.warp(e, spec, props))
logger.info(s"Warped Model: ${newmodel.prettyprint}")
val inv = labels(edge.to)
val neginv = Neg(inv).toNegNf.simplify
val inv = labels(target)
val neginv = inv.toNegNf.simplify
logger.info(s"Invariant before: $neginv")
// Instantiate inv for given universe
val instInv = FOTransformers.instantiateExistentials(neginv, vars.toSet)
val instinv = FOTransformers.eliminateUniversals(neginv, vars)
logger.info(s"Invariant instantiated: $instinv")
val itp = Z3QFree.interpolate(model.stateFormula(), instInv)
// Put steering into instInv
val z3map = z3model.toMap
val steeredinv = instinv.everywhere {
case f:Fun if z3map.contains(f) => z3map(f)
}
// 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()
logger.info(s"inv: $easyinv")
val itp = Z3QFree.interpolate(newmodel.stateFormula(), easyinv)
logger.info(s"Interpolant is ${itp.get.toNegNf}")
// logger.info(s"Model for itp is ${Z3.printModel(Z3QFree.checkSatQFree(itp.get).get)}")
// val (s, satisfy) = Z3QFree.checkUniversal(Neg(easyinv))
// logger.info(s"Model: ${Z3.printModel(satisfy.getModel)}")
logger.info(s"Interpolant is $itp")
} else {
logger.error("Invariant not valid, but also not satisfiable.")
......@@ -94,7 +134,7 @@ object MainInvariantsInference extends App with LazyLogging {
}
def generateExample(name: String) {
def generateExample(name: String, target: Int) {
logger.info(s"Generating $name")
val spec = ExampleWorkflows.parseExample(name)
......@@ -102,20 +142,21 @@ object MainInvariantsInference extends App with LazyLogging {
logger.error(s"Not a valid spec: $name")
}
spec.foreach(generate(name, _))
spec.foreach(generate(name, _, target))
}
def generateAllExamples() {
clear()
// Fill results alphabetically
for (k <- ExampleWorkflows.examples.keys.toList.sorted) {
generateExample(k)
}
}
// 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/conference_linear_small", 1)
generateExample("nonomitting/conference_linear", 2)
// generateExample("tests/loopexampleNoOracle")
// generateAllExamples()
}
\ No newline at end of file
......@@ -106,6 +106,10 @@ abstract sealed class SimpleBlock extends Block {
before || after
}
def updating:Set[String] = {
steps.map(_.fun).toSet
}
}
abstract class Statement {
......
......@@ -254,7 +254,7 @@ object FormulaFunctions extends LazyLogging {
def assumeAllEmpty(f: Formula, names: List[String]) = {
// Assume all workflow relations empty
val assumers = names.map(p => (f: Formula) => assumeEmpty(f, p))
val allempty = assumers.reduce(_ andThen _)(f)
val allempty = assumers.foldLeft(f)((f, a) => a(f))
allempty.simplify()
}
......
......@@ -6,6 +6,7 @@ import de.tum.workflows.Preconditions
import de.tum.workflows.blocks.{SimpleBlock, Spec}
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.{FOTransformers, Properties}
import de.tum.workflows.synth.Model.logger
import de.tum.workflows.toz3.{InvProperties, InvariantChecker, Z3QFree}
case class Model(universe: Map[String, List[Var]], steering: Formula, state:Map[Fun, List[Formula]]) {
......@@ -28,6 +29,39 @@ case class Model(universe: Map[String, List[Var]], steering: Formula, state:Map[
}
And.make(formulas.toList)
}
def warp(b: SimpleBlock, spec: Spec, properties: InvProperties): Model = {
val facts = And.make(steering, stateFormula())
// logger.info(s"Current state: ${state.pretty()}")
val updated = for (rel <- state.keys) yield {
// logger.info(s"Computing new state of ${rel}")
val tups = FOTransformers.comb(rel.params.map(_.typ), universe)
val newstate = for (tup <- tups; trace <- List(Properties.T1, Properties.T2)) yield {
val post = Fun(rel.name, Some(trace), tup)
// logger.info(s"Checking tuple $post on trace $trace")
// Is now an E* formula
val pre = Preconditions.weakestPrecondition(post, b, spec, properties)
val inst = FOTransformers.instantiateExistentials(pre, universe.values.flatten.toSet)
val check = Implies(facts, inst)
// logger.info(s"Precondition is $check")
val (res, _) = Z3QFree.checkUniversal(check)
if (res == Status.SATISFIABLE) {
// Negation sat, so there are models where it's false
Neg(post)
} else {
post
}
}
rel -> newstate
}
Model(universe, steering, updated.toMap)
}
}
object Model extends LazyLogging {
......@@ -56,37 +90,6 @@ object Model extends LazyLogging {
emptystate toMap
}
def warp(modelfacts: Formula, b: SimpleBlock, spec: Spec, properties: InvProperties, model: Model): Model = {
logger.info(s"Initial Model: ${model}")
val state = And.make(model.steering, model.stateFormula())
logger.info(s"Current state: ${state.pretty()}")
// FIXME: This does not update the state of "informed"
val updated = for (rel <- spec.w.sig.preds) yield {
logger.info(s"Computing new state of ${rel}")
val tups = FOTransformers.comb(rel.params.map(_.typ), model.universe)
val newstate = for (tup <- tups; trace <- List(Properties.T1, Properties.T2)) yield {
val post = Fun(rel.name, Some(trace), tup)
logger.info(s"Checking tuple $post on trace $trace")
val pre = Preconditions.weakestPrecondition(post, b, spec, properties)
val check = Implies(state, pre)
logger.info(s"Precondition is $check")
val (res, _) = Z3QFree.checkUniversal(check)
if (res == Status.SATISFIABLE) {
// Negation sat, so there are models where it's false
Neg(post)
} else {
post
}
}
rel -> newstate
}
Model(model.universe, model.steering, updated.toMap)
}
}
\ No newline at end of file
......@@ -24,16 +24,18 @@ object InvProperties {
object InvariantChecker extends LazyLogging {
def checkBlockInvariant(spec:Spec, b: SimpleBlock, pre: Formula, post: Formula, isfirst: Boolean, properties:InvProperties) = {
def checkBlockInvariant(spec:Spec, b: SimpleBlock, pre: Formula, post: Formula, isfirst: Boolean, properties:InvProperties, untouched:Set[String]) = {
val precond = Preconditions.abstractedPrecondition(post, b, spec, properties)
// TODO: do we do this here?
val firstprecond = if (isfirst) {
precond.assumeEmpty(spec.w.sig.preds.map(_.name).toList)
} else { precond }
val noinfprecond = if (isfirst) {
firstprecond.assumeEmpty(List(Properties.INFNAME))
} else { firstprecond }
// Assume untoucheds empty
val untouchedprecond = precond.assumeEmpty(untouched.toList)
// val firstprecond = if (isfirst) {
// precond.assumeEmpty(spec.w.sig.preds.map(_.name).toList)
// } else { precond }
val noinfprecond = if (isfirst && !properties.stubborn) {
untouchedprecond.assumeEmpty(List(Properties.INFNAME))
} else { untouchedprecond }
val z3simpednewinv = Z3QFree.simplifyUniv(noinfprecond)
val gained = noinfprecond.toString().length() - z3simpednewinv.toString().length()
......@@ -54,6 +56,8 @@ object InvariantChecker extends LazyLogging {
type Node = graph.NodeT
type Edge = graph.EdgeT
val untouched = Encoding.untouchedMap(graph, spec.w.sig)
@tailrec
def checkInvariantRec(labellist: List[Map[Int, Formula]], provenlist: List[Set[Edge]]): (Boolean, List[Map[Int, Formula]], List[Set[Edge]]) = {
......@@ -71,19 +75,19 @@ object InvariantChecker extends LazyLogging {
// take the edge with a minimum of following unproven edges excluding selfloops
// val next = toProve.minBy(edge => ((edge.target.outgoing.filter(t => t.target != t.source) -- proven).size))
// take the edge with maximum source node first
val next = toProve.maxBy(edge => edge.source.value)
val nextEdge = toProve.maxBy(edge => edge.source.value)
// try to prove
val pre = labels(next._1)
val post = labels(next._2)
val isfirst = !next._1.hasPredecessors
val ((status, solver), strengthened) = checkBlockInvariant(spec, next, pre, post, isfirst, properties)
val pre = labels(nextEdge.from)
val post = labels(nextEdge.to)
val isfirst = !nextEdge.from.hasPredecessors
val ((status, solver), strengthened) = checkBlockInvariant(spec, nextEdge, pre, post, isfirst, properties, untouched(nextEdge.from))
if (status == Status.UNSATISFIABLE) {
// Negation of implication unsat
// --> safe, continue with larger proven set.
logger.info(s"Proven inductiveness for (${next._1} -> ${next._2}).")
checkInvariantRec(labels :: labellist, (proven + next) :: provenlist)
logger.info(s"Proven inductiveness for (${nextEdge._1} -> ${nextEdge.to}).")
checkInvariantRec(labels :: labellist, (proven + nextEdge) :: provenlist)
} else {
// Negation of implication sat
// --> unsafe, relabel incoming node, invalidate all proven guarantees for that node
......@@ -91,7 +95,7 @@ object InvariantChecker extends LazyLogging {
// never relabel initial node
logger.info(s"Invariant not inductive, strengthening.")
val newinv = And(labels(next._1), strengthened).simplify()
val newinv = And(labels(nextEdge._1), strengthened).simplify()
val nostrangebindings = FormulaFunctions.checkBindings(newinv)
if (!nostrangebindings) {
......@@ -99,20 +103,20 @@ object InvariantChecker extends LazyLogging {
logger.error(s"Invariant would be $newinv")
}
val newlabels = labels.updated(next._1, strengthened)
val newlabels = labels.updated(nextEdge._1, newinv)
if (!isfirst) {
val invalidated = proven.filter(_._2 == next._1)
val invalidated = proven.filter(_.from == nextEdge.to)
val newproven = (proven -- invalidated) + next
val newproven = (proven -- invalidated) + nextEdge
val (status2, solver2) = Z3QFree.checkUniversal(Implies(newinv, False))
if (status2 == Status.SATISFIABLE) {
// Negation of newinv still sat, newinv does not imply false)
logger.info(s"Relabeling ${next._1}. New size: ${newinv.opsize()}. Continuing.")
logger.info(s"Relabeling ${nextEdge._1}. New size: ${newinv.opsize()}. Continuing.")
checkInvariantRec(newlabels :: labellist, newproven :: provenlist)
} else {
logger.info(s"New invariant for ${next._1} not satisfiable. Terminating.")
logger.info(s"New invariant for ${nextEdge._1} not satisfiable. Terminating.")
(false, newlabels :: labellist, newproven :: provenlist)
}
} else {
......@@ -124,9 +128,15 @@ object InvariantChecker extends LazyLogging {
}
}
// create labelling - FIXME: maybe use inv only for last
// create labelling
val labels = (for (n <- graph.nodes) yield { n.value -> inv }).toMap
val (time, (result, labellings, proven)) = Utils.time { checkInvariantRec(labels, List(Set())) }
// update labels with untouched map
val untouchedlabels = for ((n, inv) <- labels) yield {
n -> inv.assumeEmpty(untouched(graph.get(n)).toList)
}
val (time, (result, labellings, proven)) = Utils.time { checkInvariantRec(untouchedlabels, List(Set())) }
val dot1 = labellings.zip(proven).reverse
val dot2 = dot1.map(tup => Encoding.toDot(graph)(tup._1.map(t => (t._1, {
......@@ -150,6 +160,7 @@ object InvariantChecker extends LazyLogging {
// Build graph
val graph = Encoding.toGraph(spec.w)
val untouched = Encoding.untouchedMap(graph, spec.w.sig)
val msg = new StringBuilder()
msg ++= s"Trying to prove safe with invariant:\n\n${inv.pretty()}\n\n"
......@@ -161,10 +172,9 @@ object InvariantChecker extends LazyLogging {
val b: SimpleBlock = e
// Special handling for first block
// TODO: Replace by iteration
val isfirst = !e.from.hasPredecessors
val ((res, solver), strengthened) = checkBlockInvariant(spec, b, inv, inv, isfirst, properties)
val ((res, solver), strengthened) = checkBlockInvariant(spec, b, inv, inv, isfirst, properties, untouched(e.from))
if (res != Status.UNSATISFIABLE) {
msg ++= s"Possibly unsafe: Block may not uphold invariant:\n\n${e.label}\n\n"
......
......@@ -46,7 +46,11 @@ object Z3QFree extends LazyLogging {
if (itp.status == Z3_lbool.Z3_L_FALSE) {
logger.debug("Unsat, interpolating")
Some(mapback(itp.interp.head))
} else None
} else {
logger.info("Sat instead")
logger.info(Z3.printModel(itp.model))
None
}
}
if (time > 1000) {
logger.debug(s"Z3 call took $time ms")
......@@ -55,6 +59,44 @@ object Z3QFree extends LazyLogging {
}
def checkSatQFree(f: Formula) = {
val (time, res) = Utils.time {
// Set up Z3
val cfg = new util.HashMap[String, String]()
cfg.put("timeout", TIMEOUT.toString())
val ctx = new Context(cfg)
val s = ctx.mkSolver()
// Can only check universal things
if (!f.isQFree) {
logger.error("Trying to encode formula with quantifiers")
}
val satform = FOTransformers.eliminatePredicates(f)
// Checking QFree
s.add(Z3QFree.translate(satform, 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 status satisfiable")
// logger.info(s"${s.getModel()}")
Some(s.getModel)
} else {
None
}
}
// Logging only calls that take longer than a second
if (time > 1000) {
logger.debug(s"Z3 call took $time ms")
}
res
}
def checkUniversal(f: Formula) = {
......
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