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

fix stuff, improve elimination

parent 0a3d0c62
......@@ -3,26 +3,31 @@ shopt -s nullglob
shopt -s globstar
TIMEOUT=1m
DIR=$1
if [ -z "$DIR" ]
then
DIR="*"
fi
echo "Gobbling up metrics"
rm -f results/allmetrics.metrics
touch results/allmetrics.metrics
for FILE in results/**/*.metrics
for FILE in results/$DIR/**/*.metrics
do
echo "${FILE}:" >> results/allmetrics.metrics
cat ${FILE} >> results/allmetrics.metrics
echo -e "\n\n" >> results/allmetrics.metrics
done
for FILE in results/**/*.png
for FILE in results/$DIR/**/*.png
do
echo "Deleting ${FILE}"
rm $FILE
done
for FILE in results/**/*.dot
for FILE in results/$DIR/**/*.dot
do
NAME=$(basename ${FILE} .dot)
DIR=$(dirname "${FILE}")
......
......@@ -259,11 +259,12 @@ object Encoding extends LazyLogging {
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
// 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))
// TODO: maybe introduce informedness as sig.pred?
map = map.updated(g.get(sourceid), sig.preds.map(_.name) ++ Some(Properties.INFNAME) )
for (elem <- nodes) {
// If all predecessors are known
......@@ -273,12 +274,6 @@ object Encoding extends LazyLogging {
map = map.updated(elem, union -- touched)
}
}
// For causal agents add informedness - only at the end to not propagate it (as its not mentioned in the graph)
if (!props.stubborn) {
map.updated(sourcenode, map(sourcenode) + Properties.INFNAME)
} else {
map
}
map
}
}
\ No newline at end of file
......@@ -147,28 +147,38 @@ object Preconditions extends LazyLogging {
val removed = FOTransformers.eliminateDoubleQuantifiers(replaced)
if (Utils.DEBUG_MODE) {
if (FormulaFunctions.collectQuantifiers(removed) != FormulaFunctions.collectQuantifiers(replaced)) {
logger.warn(s"Removed a quantifier:\nBefore: $replaced\nAfter:$removed")
logger.warn(s"Removed a quantifier:\nBefore: ${replaced}\nAfter:$removed")
}
}
removed
}
def abstractedPrecondition(f: Formula, b: SimpleBlock, s: Spec, properties: InvProperties, untouched: Set[String]) = {
val precond = weakestPrecondition(f, b, s, properties)
def abstractedPrecondition(f: Formula, b: SimpleBlock, spec: Spec, properties: InvProperties, untouched: Set[String]) = {
val precond = weakestPrecondition(f, b, spec, properties)
// Assume untoucheds empty
val untouchedprecond = precond.assumeEmpty(untouched.toList)
val z3simpednewinv = Z3BSFO.simplifyBS(untouchedprecond)
// if informedness untouched T1 and T2 are equal anyway, so remove annotations
// TODO: better recognition for necessarily equal
val removedannotations = if (untouched.contains(Properties.INFNAME)) {
val rels = spec.w.sig.preds.map(_.name)
rels.foldRight(z3simpednewinv)((r, f) => Z3BSFO.simplifyBS(FormulaFunctions.removeAnnotation(f, r)))
} else {
z3simpednewinv
}
// Abstract away inner existentials
val universalinv = if (z3simpednewinv.toNegNf.hasSubFormula {
val universalinv = if (removedannotations.toNegNf.hasSubFormula {
case e:Exists => true
}) {
FOTransformers.abstractExistentials(z3simpednewinv)
FOTransformers.abstractExistentials(removedannotations)
} else {
z3simpednewinv
removedannotations
}
// Eliminate Choices
......@@ -180,9 +190,7 @@ object Preconditions extends LazyLogging {
// Eliminate Oracles
val oless = if (properties.eliminateAux) {
val oracles = auxless.collect {
case f: Fun if f.isOracle() => List(f.name)
}.toSet
val oracles = spec.w.sig.oracles.map(_.name)
oracles.foldRight(auxless)((b, inv) => FOTransformers.eliminateAuxiliaryPredicate(inv, b))
} else {
auxless
......@@ -193,11 +201,21 @@ object Preconditions extends LazyLogging {
val bs = oless.collect {
case f:Fun if f.isB() => List(f.name)
}.toSet
if (bs.nonEmpty && !untouched.contains(Properties.INFNAME)) {
logger.error("Trying to compute strategies for B with B,B' not necessarily equal")
}
bs.foldRight(oless)((b, inv) => FOTransformers.eliminateBPredicate(inv, b)._1)
} else {
oless
}
if (Utils.DEBUG_MODE) {
val possibleAttack = Z3BSFO.debugmodelBS(Neg(bless))
logger.trace(s"Possible attack: $possibleAttack")
}
Z3BSFO.simplifyBS(bless.simplify)
}
}
\ No newline at end of file
......@@ -3,6 +3,7 @@ package de.tum.workflows.blocks
import de.tum.workflows.foltl.FOLTL._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils
import de.tum.workflows.foltl.Properties
case class Signature(oracles: Set[Fun], preds: Set[Fun])
object Signature {
......@@ -117,7 +118,13 @@ abstract sealed class SimpleBlock extends Block {
}
def updating:Set[String] = {
steps.map(_.fun).toSet
// This works because of the way the untouchedmap is computed.
// As soon as that changes, fix here.
if (isoracly) {
steps.map(_.fun).toSet + Properties.INFNAME
} else {
steps.map(_.fun).toSet
}
}
}
......
......@@ -378,33 +378,37 @@ object FormulaFunctions extends LazyLogging {
}
def collectQuantifiers(f: Formula): List[(Boolean, List[Var])] = {
f collect {
case Exists(xs, fsub) => (true, xs) :: collectQuantifiers(fsub)
case Forall(xs, fsub) => (false, xs) :: collectQuantifiers(fsub)
case BinOp(make, f1, f2) => {
val q1 = collectQuantifiers(f1)
val q2 = collectQuantifiers(f2)
// Merge while trying to stay in BS, if possible
// TODO: could be improved to minimize quantifier alternations)
// TODO: merge universals with same type by renaming
val ex1 = q1.takeWhile(_._1)
val rest1 = q1.drop(ex1.size)
// filter out same bound variables (TODO: could be improved if different names) (FIXME: Is this even correct?)
val existbound = ex1.flatMap(_._2)
val univbound = rest1.flatMap(_._2)
val exset = existbound.toSet
val univset = univbound.toSet
val ex2 = q2.takeWhile(_._1).map(q =>
(q._1, q._2.filterNot(exset.contains)))
val rest2 = q2.drop(ex2.size).map(q =>
(q._1, q._2.filterNot(univset.contains)))
ex1 ++ ex2 ++ rest1 ++ rest2
def collectQ(f2:Formula):List[(Boolean, List[Var])] = {
f2 collect {
case Exists(xs, fsub) => (true, xs) :: collectQ(fsub)
case Forall(xs, fsub) => (false, xs) :: collectQ(fsub)
case BinOp(make, f1, f2) => {
val q1 = collectQ(f1)
val q2 = collectQ(f2)
// Merge while trying to stay in BS, if possible
// TODO: could be improved to minimize quantifier alternations)
// TODO: merge universals with same type by renaming
val ex1 = q1.takeWhile(_._1)
val rest1 = q1.drop(ex1.size)
// filter out same bound variables on both sides
// FIXME: make sure that fixBindings is used where neccessary
val existbound = ex1.flatMap(_._2)
val univbound = rest1.flatMap(_._2)
val exset = existbound.toSet
val univset = univbound.toSet
val ex2 = q2.takeWhile(_._1).map(q =>
(q._1, q._2.filterNot(exset.contains)))
val rest2 = q2.drop(ex2.size).map(q =>
(q._1, q._2.filterNot(univset.contains)))
ex1 ++ ex2 ++ rest1 ++ rest2
}
}
}
collectQ(f.toNegNf)
}
def checkBindings(f: Formula) = {
......@@ -591,15 +595,11 @@ object FormulaFunctions extends LazyLogging {
val normalized = f.toPrenex.simplify
logger.debug(s"Computing CNF of prenex formula of opsize ${normalized.opsize}")
val quantifiers = FormulaFunctions.collectQuantifiers(normalized)
// normalized is now Quantifiers, then only And/Or with Negation inside
// no simplification here
val cnf1 = toCNFSub(normalized)
val cnf2 = everywhereBotUp({
case Or(And(f1, f2), f3) => And(Or(f1, f3), Or(f2, f3))
case Or(f1, And(f2, f3)) => And(Or(f1, f2), Or(f1, f3))
}, normalized)
val quantifiers = FormulaFunctions.collectQuantifiers(cnf1)
// Inspect clauses
val clauses = FOTransformers.collectClauses(cnf1)
......
......@@ -10,20 +10,26 @@ import de.tum.workflows.foltl.{FOTransformers, FormulaFunctions}
object Z3BSFO extends LazyLogging {
def createContext():(Context, Solver) = {
// Set up Z3
val cfg = new util.HashMap[String, String]()
cfg.put("timeout", Z3FOEncoding.TIMEOUT.toString())
val ctx = new Context(cfg)
val params = ctx.mkParams()
params.add("mbqi", true)
// params.add("mbqi.trace", true)
val s = ctx.mkSolver()
s.setParameters(params)
(ctx, s)
}
def checkAE(f: Formula) = {
val (time, res) = Utils.time {
// Set up Z3
val cfg = new util.HashMap[String, String]()
cfg.put("timeout", Z3FOEncoding.TIMEOUT.toString())
val ctx = new Context(cfg)
val params = ctx.mkParams()
params.add("mbqi", true)
// params.add("mbqi.trace", true)
val s = ctx.mkSolver()
s.setParameters(params)
val (ctx, s) = createContext()
val neg = Neg(f).simplify
......@@ -57,10 +63,9 @@ object Z3BSFO extends LazyLogging {
}
def simplifyBS(f: Formula) = {
val cfg = new util.HashMap[String, String]()
cfg.put("timeout", Z3FOEncoding.TIMEOUT.toString())
val ctx = new Context(cfg)
val (ctx, _) = createContext()
val simp = ctx.mkTactic("ctx-solver-simplify")
val simp2 = ctx.mkTactic("simplify")
......@@ -122,10 +127,9 @@ object Z3BSFO extends LazyLogging {
}
def toCNFQFreeClauses(f: Formula) = {
val cfg = new util.HashMap[String, String]()
cfg.put("timeout", Z3FOEncoding.TIMEOUT.toString())
val ctx = new Context(cfg)
val (ctx, _) = createContext()
val cnftactic = ctx.mkTactic("tseitin-cnf")
val simptactic = ctx.mkTactic("ctx-solver-simplify")
val bothtactics = ctx.andThen(cnftactic, simptactic)
......@@ -153,4 +157,25 @@ object Z3BSFO extends LazyLogging {
clauses
}
def debugmodelBS(f:Formula) = {
val (ctx, s) = createContext()
// Can only check universal things
if (!f.isBS) {
logger.error("Z3-BSFO: Trying to encode formula not in Bernays-Schönfinkel")
}
s.add(Z3FOEncoding.translate(f.simplify, ctx))
// Send to z3
val c = s.check()
if (c == Status.UNKNOWN) {
logger.warn(s"Z3-BSFO: Status unknown - ${s.getReasonUnknown()}")
} else if (c == Status.SATISFIABLE) {
s.getModel.toString
} else {
"No model found"
}
}
}
......@@ -113,6 +113,14 @@ class FOLTLTest extends FlatSpec {
)
)
}
it should "compute nested quantprefixes" in {
val x = Var("x", "S")
val f = Forall(x, Forall(x, Fun("f",x)))
FormulaFunctions.collectQuantifiers(f) should be {
List((false, List(x, x)))
}
}
it should "also compute CNF" in {
val f = Or.make(And("a", "b"), And("c","d"), And("e", "f"))
......
......@@ -30,4 +30,14 @@ class InferenceTests extends FlatSpec {
assert(checkSafeStubborn(name, inv))
}
it should "prove safe causal stuff safe" in {
val name = "tests/conference_linear_small_withB"
val xt = Var("xt","X")
val yt = Var("yt","X")
val pt = Var("pt","P")
// val rt = Var("rt","R")
val inv = Forall(List(xt, pt, yt), genEq("Comm", List(xt, yt, pt)))
assert(checkSafeCausalElim(name, "", inv))
}
}
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