Commit 06c44ac5 authored by Christian Müller's avatar Christian Müller

make iteration return all intermediate proven labellings

parent 27f1422f
......@@ -203,7 +203,7 @@ object Encoding extends LazyLogging {
def edgeTransformer(innerEdge: WorkflowGraph#EdgeT): Option[(DotGraph, DotEdgeStmt)] = innerEdge.edge match {
case LDiEdge(source, target, label) => label match {
case label: SimpleBlock => {
val green = edges.exists(_.label == label)
val green = edges.exists(_ == innerEdge)
val color = List(DotAttr("color", if (green) "green" else "red"))
val labelled = if (label.nonEmpty) {
......
......@@ -29,12 +29,14 @@ object MainInvariants extends App with LazyLogging {
val (t, (res, dot)) = time {
// InvariantChecker.checkInvariantOnce(spec.w, inv(spec), true)
InvariantChecker.checkInvariantFP(spec.w, invariant(spec), true)
InvariantChecker.checkInvariantFP(spec, invariant(spec), true)
}
val msg = s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n"
write(s"${name}.inv", msg)
write(s"${name}.dot", dot)
for ((s, i) <- dot.zipWithIndex) {
write(s"${name}_${i}.dot", s)
}
}
def generateExample(name: String) {
......
......@@ -11,19 +11,82 @@ import de.tum.workflows.ltl.FOTransformers
object Preconditions extends LazyLogging {
def weakestPrecondition(f: Formula, b: SimpleBlock) = {
val INFNAME = "informed"
val T1 = "t1"
val T2 = "t2"
def elaborateSteps(b:SimpleBlock, s:Spec) = {
val newsteps = (for (stmt <- b.steps) yield {
val first = stmt.tuple.head
if (first.typ == s.target.params.head.typ) {
val fun = Fun(stmt.fun, stmt.tuple)
// TODO
val guard = Neg(Eq(fun.in(T1), fun.in(T2)))
List(stmt, Add(guard, INFNAME, List(first)))
} else List(stmt)
})
newsteps.flatten
}
def subst(f:Formula, updates: List[(String, (List[FOLTL.Var], FOLTL.Formula))], b:SimpleBlock) = {
updates.foldRight(f)((update, f) => {
val (repname, (vars, form)) = update
f everywhere {
case Fun(name, ind, params) if name == repname => {
val renamed = form.parallelRename(vars, params)
// Annotate the precondition with the index
if (ind.isDefined) {
FormulaFunctions.annotate(renamed, ind.get)
} else {
renamed
}
}
}
})
}
def weakestPrecondition(f: Formula, b: SimpleBlock, spec:Spec, stubborn:Boolean) = {
// elaborate only if non-stubborn
val steps = if (stubborn) elaborateSteps(b, spec) else b.steps
val choice = b.pred.map(n => Fun(n, b.agents))
// TODO: Only introduce quantifiers if not already in scope
val updates = b.steps.map(s => {
val updates = steps.map(s => {
s.fun -> (s.tuple, {
val frees = s.guard.freeVars() -- s.tuple.toSet
val list = List(s.guard) ++ choice.toList
val guard = And.make(list)
// val list = List(s.guard) ++ choice.toList
// val guard = And.make(list)
val first = s.tuple.head
// Trace related substitution for informedness
// TODO: make switch on/off etc
val con = if (choice.isDefined) {
val inner = if (first.typ == spec.target.params.head.typ) {
val inf = Fun(INFNAME, List(s.tuple.head))
if (stubborn) {
choice.get.in(T1)
} else {
Or(And(Neg(inf.in(T1)), choice.get.in(T1)), And(inf.in(T1), choice.get))
}
} else {
choice.get
}
inner
} else {
True
}
val guard = And(s.guard, con).simplify()
// val guard = True
s match {
val form = s match {
case Add(_, _, _) => {
Or(Fun(s.fun, s.tuple), Exists(frees.toList, guard)).simplify()
}
......@@ -31,47 +94,38 @@ object Preconditions extends LazyLogging {
And(Fun(s.fun, s.tuple), Forall(frees.toList, Neg(guard))).simplify()
}
}
form
})
}) toMap
})
// Replace literals with their precondition
val replaced = f everywhere {
case Fun(name, ind, params) if b.steps.exists(s => s.fun == name) => {
val up = updates(name)
val renamed = up._2.parallelRename(up._1, params)
// Annotate the precondition with the index
if (ind.isDefined) {
FormulaFunctions.annotate(renamed, ind.get)
} else {
renamed
}
}
}
val replaced = subst(f, updates, b)
// TODO: have we proven this correct?
val removed = FOTransformers.eliminateDoubleQuantifiers(replaced)
removed
}
def abstractPrecondition(f:Formula, b:SimpleBlock, stubborn:Boolean) = {
val precond = weakestPrecondition(f, b)
def abstractPrecondition(f:Formula, b:SimpleBlock, stubborn:Boolean, s:Spec) = {
val precond = weakestPrecondition(f, b, s, stubborn)
// Stubborn agents -> remove trace variable from choice predicate
val stubprecond = if (stubborn) {
precond.everywhere {
case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
}
} else precond
// Not neccessary anymore
// val stubprecond = if (stubborn) {
// precond.everywhere {
// case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
// }
// } else precond
// Abstract away inner existentials
val universalinv = if (b.isomitting) {
FOTransformers.abstractExistentials(stubprecond).simplify()
FOTransformers.abstractExistentials(precond).simplify()
} else {
stubprecond
precond
}
val cnf = universalinv.toCNF().simplify()
// val cnf = universalinv.toCNF().simplify()
// Abstract away auxilliaries
val auxless = if (b.pred.isDefined) {
......@@ -81,6 +135,4 @@ object Preconditions extends LazyLogging {
}
auxless
}
// TODO: Replace oracles and choices by fresh predicates?
}
\ No newline at end of file
......@@ -67,7 +67,14 @@ object FOTransformers extends LazyLogging {
c
}
val form = And.make(simped.map(Or.make _))
// TODO improve runtime
val simp2 = simped.filterNot(c => simped.exists(c2 => {
// check if c is superset of c2
c != c2 && c2.forall(x => c.contains(x))
}))
val form = And.make(simp2.map(Or.make _))
// TODO: improve
val newform = quantifiers.foldRight(form)((q, inner) => if(q._1) Exists(q._2, inner) else Forall(q._2, inner))
......
......@@ -58,12 +58,12 @@ object InvariantChecker extends LazyLogging {
(c, s)
}
def checkBlockInvariant(sig: Signature, b: SimpleBlock, pre: Formula, post: Formula, stubborn: Boolean, isfirst: Boolean) = {
val precond = Preconditions.abstractPrecondition(post, b, stubborn)
def checkBlockInvariant(spec:Spec, b: SimpleBlock, pre: Formula, post: Formula, stubborn: Boolean, isfirst: Boolean) = {
val precond = Preconditions.abstractPrecondition(post, b, stubborn, spec)
// TODO: do we do this here?
val firstprecond = if (isfirst) {
precond.assumeEmpty(sig.preds.map(_.name).toList)
precond.assumeEmpty(spec.w.sig.preds.map(_.name).toList)
} else { precond }
// val test1 = inv.toPrenex()
......@@ -76,42 +76,48 @@ object InvariantChecker extends LazyLogging {
checkOnZ3(f.simplify())
}
def checkInvariantFP(w: Workflow, inv: Formula, stubborn: Boolean) = {
val graph = Encoding.toGraph(w)
def checkInvariantFP(spec: Spec, inv: Formula, stubborn: Boolean) = {
val graph = Encoding.toGraph(spec.w)
type Node = graph.NodeT
type Edge = graph.EdgeT
@tailrec
def checkInvariantRec(labels: Map[Node, Formula], proven: Set[Edge]): (Boolean, Map[Node, Formula], Set[Edge]) = {
def checkInvariantRec(labellist: List[Map[Node, Formula]], provenlist: List[Set[Edge]]): (Boolean, List[Map[Node, Formula]], List[Set[Edge]]) = {
val labels = labellist.head
val proven = provenlist.head
// check if done, i.e. all edges proven
val toProve = (graph.edges -- proven)
if (toProve.isEmpty) {
logger.info("Everything proven. Terminating.")
(true, labels, proven)
(true, labellist, provenlist)
} else {
// take one edge to prove
val next = toProve.head
// val next = toProve.head
// 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)
// try to prove
val pre = labels(next._1)
val post = labels(next._2)
val isfirst = !next._1.hasPredecessors
val (status, solver) = checkBlockInvariant(w.sig, next, pre, post, stubborn, isfirst)
val (status, solver) = checkBlockInvariant(spec, next, pre, post, stubborn, isfirst)
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, proven + next)
checkInvariantRec(labels :: labellist, (proven + next) :: provenlist)
} else {
// Negation of implication sat
// --> unsafe, relabel incoming node, invalidate all proven guarantees for that node
// check if relabelled invariant still satisfiable
// never relabel initial node
if (!isfirst) {
val newinv = And(labels(next._1), Preconditions.abstractPrecondition(post, next, stubborn)).simplify()
val newinv = And(labels(next._1), Preconditions.abstractPrecondition(post, next, stubborn, spec)).simplify()
val (status2, solver2) = checkOnZ3(Implies(newinv, False))
......@@ -129,14 +135,14 @@ object InvariantChecker extends LazyLogging {
if (status2 == Status.SATISFIABLE) {
// Negation of newinv still sat, newinv does not imply false)
logger.info(s"Relabeling ${next._1}. Continuing.")
checkInvariantRec(newlabels, newproven)
checkInvariantRec(newlabels :: labellist, newproven :: provenlist)
} else {
logger.info(s"New invariant for ${next._1} not satisfiable. Terminating.")
(false, newlabels, newproven)
(false, newlabels :: labellist, newproven :: provenlist)
}
} else {
logger.info("Would have to relabel initial node. Terminating.")
(false, labels, proven)
(false, labellist, provenlist)
}
}
}
......@@ -144,16 +150,19 @@ object InvariantChecker extends LazyLogging {
// create labelling - FIXME: maybe use inv only for last
val labels = (for (n <- graph.nodes) yield { n -> inv }).toMap
val (result, afterlabels, proven) = checkInvariantRec(labels, Set())
val (result, afterlabels, proven) = checkInvariantRec(labels, List(Set()))
val dot1 = afterlabels.zip(proven).reverse
val dot = Encoding.toDot(graph)(afterlabels.map(t => (t._1, t._2.pretty())), proven)
(result, dot)
val dot2 = dot1.map((tup) => Encoding.toDot(graph)(tup._1.map(t => (t._1, t._2.pretty())), tup._2))
(result, dot2)
}
def checkInvariantOnce(w: Workflow, inv: Formula, stubborn: Boolean) = {
def checkInvariantOnce(spec: Spec, inv: Formula, stubborn: Boolean) = {
// Build graph
val graph = Encoding.toGraph(w)
val graph = Encoding.toGraph(spec.w)
val msg = new StringBuilder()
msg ++= s"Trying to prove safe with invariant:\n\n${inv.pretty()}\n\n"
......@@ -168,7 +177,7 @@ object InvariantChecker extends LazyLogging {
// TODO: Replace by iteration
val isfirst = !e.from.hasPredecessors
val (res, solver) = checkBlockInvariant(w.sig, b, inv, inv, stubborn, isfirst)
val (res, solver) = checkBlockInvariant(spec, b, inv, inv, stubborn, isfirst)
if (res != Status.UNSATISFIABLE) {
msg ++= s"Possibly unsafe: Block may not uphold invariant:\n\n${e.label}\n\n"
......@@ -189,7 +198,7 @@ object InvariantChecker extends LazyLogging {
val safe = list.reduceLeft(_ && _)
if (safe) {
msg ++= s"Proven safe.\n"
logger.info(s"Workflow $w\n proven safe for invariant:\n${inv.pretty()}")
logger.info(s"Workflow ${spec.w}\n proven safe for invariant:\n${inv.pretty()}")
}
(safe, msg)
}
......
......@@ -11,21 +11,16 @@ import com.microsoft.z3.Model
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.ExampleWorkflows
import de.tum.workflows.Utils
import de.tum.workflows.tests.TestUtils._
object Test extends App {
val name = "tests/loopexample"
val inv = Forall(List("x", "y", "s"), genEq("S", List("x", "y", "s")))
val spec = ExampleWorkflows.parseExample(name).get
val (safe, dot) = InvariantChecker.checkInvariantFP(spec.w, inv, true)
assert(safe) // should be safe
Utils.write(s"${name}.dot", dot)
def genEq(name: String, params: List[Var]) = {
val o1 = Fun(name, Some("t1"), params)
val o2 = Fun(name, Some("t2"), params)
Eq(o1, o2)
}
object Test extends App {
// val name = "tests/loopexample"
// val inv = Forall(List("x", "y", "s"), genEq("S", List("x", "y", "s")))
//
// val spec = ExampleWorkflows.parseExample(name).get
// val (safe, dot) = InvariantChecker.checkInvariantFP(spec, inv, true)
// assert(safe) // should be safe
// val TIMEOUT = 30000 // in milliseconds
//
......
......@@ -18,6 +18,8 @@ import de.tum.workflows.ExampleWorkflows
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.toz3.InvariantGenerator
import de.tum.workflows.tests.TestUtils._
class InvariantEasychairTest extends FlatSpec {
"InvariantChecker" should "prove nonomitting/conference safe" in {
......@@ -66,17 +68,5 @@ class InvariantEasychairTest extends FlatSpec {
val inv = InvariantGenerator.invariantNoninterStubbornSingleBS(spec)
assert(checkSafe(name, inv))
}
def checkSafe(name: String, inv: Formula) = {
val spec = ExampleWorkflows.parseExample(name).get
val (res, dot) = InvariantChecker.checkInvariantFP(spec.w, inv, true)
Utils.write(s"${name}.dot", dot)
res
}
def genEq(name: String, params: List[Var]) = {
val o1 = Fun(name, Some("t1"), params)
val o2 = Fun(name, Some("t2"), params)
Eq(o1, o2)
}
}
\ No newline at end of file
......@@ -17,54 +17,43 @@ import de.tum.workflows.Encoding
import de.tum.workflows.ExampleWorkflows
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.tests.TestUtils._
class NonOmittingInvariantFilesTest extends FlatSpec {
"InvariantChecker" should "prove simple things safe" in {
val name = "tests/simpleNoChoice2"
val inv = Forall(List("x", "s"), genEq("R", List("x", "s")))
val inv = Forall(List("xt", "st"), genEq("R", List("xt", "st")))
assert(checkSafe(name, inv))
}
it should "prove simple may blocks safe" in {
val name = "tests/simpleChoiceNoOracle"
val inv = Forall(List("x", "s"), genEq("R", List("x", "s")))
val inv = Forall(List("xt", "st"), genEq("R", List("xt", "st")))
assert(checkSafe(name, inv))
}
it should "prove simple loops safe" in {
val name = "tests/loopexampleNoOracle"
val inv = Forall(List("x", "s"), genEq("R", List("x", "s")))
val inv = Forall(List("xt", "st"), genEq("R", List("xt", "st")))
assert(checkSafe(name, inv))
}
it should "prove simple loops safe and iterate" in {
val name = "tests/loopexampleNoOracle"
val inv = Forall(List("x", "y", "s"), genEq("S", List("x", "y", "s")))
val inv = Forall(List("xt", "yt", "st"), genEq("S", List("xt", "yt", "st")))
assert(checkSafe(name, inv))
}
it should "fail on oracly things" in {
val name = "tests/simpleChoice"
val inv = Forall(List("x", "s"), genEq("R", List("x", "s")))
val inv = Forall(List("xt", "st"), genEq("R", List("xt", "st")))
assert(!checkSafe(name, inv))
}
it should "fail on loopy oracly things" in {
val name = "tests/loopexample"
val inv = Forall(List("x", "y", "s"), genEq("S", List("x", "y", "s")))
val inv = Forall(List("xt", "yt", "st"), genEq("S", List("xt", "yt", "st")))
assert(!checkSafe(name, inv))
}
def checkSafe(name: String, inv: Formula) = {
val spec = ExampleWorkflows.parseExample(name).get
val (res, dot) = InvariantChecker.checkInvariantFP(spec.w, inv, true)
Utils.write(s"${name}.dot", dot)
res
}
def genEq(name: String, params: List[Var]) = {
val o1 = Fun(name, Some("t1"), params)
val o2 = Fun(name, Some("t2"), params)
Eq(o1, o2)
}
}
\ No newline at end of file
......@@ -15,6 +15,8 @@ import de.tum.workflows.Encoding._
import de.tum.workflows.Utils
import de.tum.workflows.Encoding
import de.tum.workflows.tests.TestUtils._
class OmittingInvariantFilesTest extends FlatSpec {
......@@ -38,17 +40,4 @@ class OmittingInvariantFilesTest extends FlatSpec {
val inv = Forall(List("x"), genEq("R", List("x")))
assert(!checkSafe(name, inv))
}
def checkSafe(name: String, inv: Formula) = {
val spec = ExampleWorkflows.parseExample(name).get
val (res, dot) = InvariantChecker.checkInvariantFP(spec.w, inv, true)
Utils.write(s"${name}.dot", dot)
res
}
def genEq(name: String, params: List[Var]) = {
val o1 = Fun(name, Some("t1"), params)
val o2 = Fun(name, Some("t2"), params)
Eq(o1, o2)
}
}
\ No newline at end of file
......@@ -12,70 +12,72 @@ import de.tum.workflows.foltl.FormulaFunctions
class PreconditionTest extends FlatSpec {
"Preconditions" should "work on simple blocks" in {
// forall a,b S(a) -> R += (a,b)
val s = Add(Fun("S", List("a")), "R", List("a", "b"))
val b = ForallMayBlock(List("a","b"), "choice1", List(s))
val f = Fun("R", Some("t1"), List("x", "y"))
val pre = Preconditions.weakestPrecondition(f, b)
pre should be (
FormulaFunctions.annotate(
Or(Fun("R", List("x","y")), And(Fun("S", List("x")), Fun("choice1", List("x","y")))),
"t1"
)
)
val f2 = Fun("R", Some("t1"), List("a", "b"))
val pre2 = Preconditions.weakestPrecondition(f2, b)
pre2 should be (
FormulaFunctions.annotate(
Or(Fun("R", List("a","b")), And(Fun("S", List("a")), Fun("choice1", List("a","b")))),
"t1"
)
)
}
// TODO: These tests don't work as we now depend on the spec
// "Preconditions" should "work on simple blocks" in {
//
// // forall a,b S(a) -> R += (a,b)
// val s = Add(Fun("S", List("a")), "R", List("a", "b"))
// val b = ForallMayBlock(List("a","b"), "choice1", List(s))
// val f = Fun("R", Some("t1"), List("x", "y"))
//
// val pre = Preconditions.weakestPrecondition(f, b)
//
// pre should be (
// FormulaFunctions.annotate(
// Or(Fun("R", List("x","y")), And(Fun("S", List("x")), Fun("choice1", List("x","y")))),
// "t1"
// )
// )
//
// val f2 = Fun("R", Some("t1"), List("a", "b"))
// val pre2 = Preconditions.weakestPrecondition(f2, b)
//
// pre2 should be (
// FormulaFunctions.annotate(
// Or(Fun("R", List("a","b")), And(Fun("S", List("a")), Fun("choice1", List("a","b")))),
// "t1"
// )
// )
// }
//
// it should "work on omitting workflows" in {
// // forall a,b S(a,b) -> R += (a)
// val s = Add(Fun("S", List("a","b")), "R", List("b"))
// val b = ForallMayBlock(List("a","b"), "choice1", List(s))
//
// val f = Fun("R", Some("t1"), List("x"))
// val pre = Preconditions.weakestPrecondition(f, b)
//
// pre should be (
// FormulaFunctions.annotate(
// Or(Fun("R", List("x")), Exists("a", And(Fun("S", List("a", "x")), Fun("choice1", List("a","x"))))),
// "t1"
// )
// )
// }
it should "work on omitting workflows" in {
// forall a,b S(a,b) -> R += (a)
val s = Add(Fun("S", List("a","b")), "R", List("b"))
val b = ForallMayBlock(List("a","b"), "choice1", List(s))
val f = Fun("R", Some("t1"), List("x"))
val pre = Preconditions.weakestPrecondition(f, b)
pre should be (
FormulaFunctions.annotate(
Or(Fun("R", List("x")), Exists("a", And(Fun("S", List("a", "x")), Fun("choice1", List("a","x"))))),
"t1"
)
)
}
it should "work on blocks with several statements" in {
// forall a,b
// R(a,b) -> S += b
// S(a) -> T -= (a,b)
val s1 = Add(Fun("R", List("a","b")), "S", List("b"))
val s2 = Remove(Fun("S", List("b")), "T", List("a"))
val b = ForallMayBlock(List("a","b"), "choice1", List(s1, s2))
val f = Exists("x", And(Fun("S", Some("t1"), List("x")), Fun("T", Some("t2"), List("y"))))
val pre = Preconditions.weakestPrecondition(f, b)
val res1 = FormulaFunctions.annotate(
Or(Fun("S", List("x")), Exists("a", And(Fun("R", List("a", "x")), Fun("choice1", List("a","x"))))),
"t1").simplify()
val res2 = FormulaFunctions.annotate(
And(Fun("T",List("y")), Forall("b", Neg(And(Fun("S", List("b")), Fun("choice1", List("y","b")))))),
"t2").simplify()
pre should be (
Exists("x", And(res1, res2))
)
}
// it should "work on blocks with several statements" in {
// // forall a,b
// // R(a,b) -> S += b
// // S(a) -> T -= (a,b)
// val s1 = Add(Fun("R", List("a","b")), "S", List("b"))
// val s2 = Remove(Fun("S", List("b")), "T", List("a"))
// val b = ForallMayBlock(List("a","b"), "choice1", List(s1, s2))
//
// val f = Exists("x", And(Fun("S", Some("t1"), List("x")), Fun("T", Some("t2"), List("y"))))
//
// val pre = Preconditions.weakestPrecondition(f, b, spec, false)
//
// val res1 = FormulaFunctions.annotate(
// Or(Fun("S", List("x")), Exists("a", And(Fun("R", List("a", "x")), Fun("choice1", List("a","x"))))),
// "t1").simplify()
// val res2 = FormulaFunctions.annotate(
// And(Fun("T",List("y")), Forall("b", Neg(And(Fun("S", List("b")), Fun("choice1", List("y","b")))))),
// "t2").simplify()
//
// pre should be (
// Exists("x", And(res1, res2))
// )
// }
}
\ No newline at end of file
package de.tum.workflows.tests
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows._
object TestUtils {
def checkSafe(name: String, inv: Formula) = {
val spec = ExampleWorkflows.parseExample(name).get
val (res, dot) = InvariantChecker.checkInvariantFP(spec, inv, true)
for ((s, i) <- dot.zipWithIndex) {
Utils.write(s"${name}_${i}.dot", s)
}
res
}
def genEq(name: String, params: List[Var]) = {
val o1 = Fun(name, Some("t1"), params)
val o2 = Fun(name, Some("t2"), params)
Eq(o1, o2)
}
}
\ No newline at end of file
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