Commit 0485d936 authored by Christian Müller's avatar Christian Müller

add check for first, fix empty implications etc

parent 1606f086
......@@ -11,6 +11,7 @@ object FOLTL {
def freeVars() = FormulaFunctions.freeVars(this)
def everywhere(trans: PartialFunction[Formula, Formula]) = FormulaFunctions.everywhere(trans, this)
def assumeEmpty(name: String) = FormulaFunctions.assumeEmpty(this, name)
def assumeEmpty(names: List[String]) = FormulaFunctions.assumeAllEmpty(this, names)
def in(name: String) = FormulaFunctions.annotate(this, name)
def in(name: String, ignore: Set[String]) = FormulaFunctions.annotate(this, name, ignore)
def collect[T](coll: PartialFunction[Formula, List[T]]) = FormulaFunctions.collect(coll, this)
......
......@@ -2,6 +2,7 @@ package de.tum.workflows.foltl
import FOLTL._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.blocks.Workflow
object FormulaFunctions extends LazyLogging {
......@@ -139,6 +140,13 @@ object FormulaFunctions extends LazyLogging {
case Fun(f, _, _) if f == name => False
})
}
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)
allempty.simplify()
}
def annotate(t: Formula, name: String) = {
t.everywhere({
......@@ -238,13 +246,13 @@ object FormulaFunctions extends LazyLogging {
def isBS(f:Formula) = {
val quantprefix = collectQuantifiersSub(f.toNegNf())
// has forall exists in quantifier prefix
quantprefix.sliding(2).exists(list => !list(0)._1 && list(1)._1)
// has no forall exists in quantifier prefix
!quantprefix.sliding(2).exists(list => !list(0)._1 && list(1)._1)
}
def toNegNf(f:Formula) = {
val bound = if (hasDuplicateBindings(f)) {
logger.info(s"Formula $f binds variables more than once - renaming bindings")
// logger.info(s"Formula binds variables more than once - renaming bindings: ${f.pretty}")
FormulaFunctions.fixBinding(f, Set())._1
} else f
eliminateImplication(bound).simplify()
......
......@@ -42,11 +42,54 @@ object InvariantChecker extends LazyLogging {
logger.info(s"Z3 status unknown: ${s.getReasonUnknown()}")
}
if (c == Status.SATISFIABLE) {
logger.info(s"Z3 model:\n${s.getModel()}")
logger.info(s"Z3 status satisfiable")
// logger.info(s"${s.getModel()}")
}
(c, s)
}
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
val stubprecond = if (stubborn) {
precond.everywhere {
case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
}
} else precond
// TODO: do not do this here
val firstprecond = if (isfirst) {
stubprecond.assumeEmpty(sig.preds.map(_.name).toList)
} else { stubprecond }
// val test1 = inv.toPrenex()
// val test2 = stubprecond.toPrenex()
val f = Implies(pre, firstprecond)
logger.info(s"Checking invariant implication for $b")
val tocheck = Neg(f).simplify()
// val test3 = tocheck.toPrenex()
// Transform to existential
if (!tocheck.isBS()) {
logger.error(s"Not in BS: Invariant implication ${tocheck.pretty}")
}
val negnf = tocheck.toNegNf()
val (agents, inner) = LTL.eliminateExistentials(negnf)
val existbound = Exists(agents, inner)
val univfree = LTL.eliminateUniversals(existbound, agents)
// val test3 = univfree.pretty()
// println(test3)
checkOnZ3(univfree.simplify())
}
def checkInvariant(w: Workflow, inv: Formula, stubborn: Boolean) = {
// Build graph
......@@ -60,41 +103,13 @@ object InvariantChecker extends LazyLogging {
// 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 = if (stubborn) {
precond.everywhere {
case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
}
} else precond
// val test1 = inv.toPrenex()
// val test2 = stubprecond.toPrenex()
val f = Implies(inv, stubprecond)
logger.info(s"Checking invariant implication for ${e.label}")
val tocheck = Neg(f).simplify()
// val test3 = tocheck.toPrenex()
// Transform to existential
if (!tocheck.isBS()) {
logger.error(s"Invariant implication $tocheck is not in BS fragment!")
}
val negnf = tocheck.toNegNf()
val (agents, inner) = LTL.eliminateExistentials(negnf)
val existbound = Exists(agents, inner)
val univfree = LTL.eliminateUniversals(existbound, agents)
// Special handling for first block
// TODO: Replace by iteration
val isfirst = !e.from.hasPredecessors
// val test3 = univfree.pretty()
// println(test3)
val (res, solver) = checkBlockInvariant(w.sig, b, inv, inv, stubborn, isfirst)
val (res, solver) = checkOnZ3(univfree)
if (res != Status.UNSATISFIABLE) {
msg ++= s"Possibly unsafe: Block may not uphold invariant:\n\n${e.label}\n\n"
if (res == Status.SATISFIABLE) {
......
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