Commit 7c277482 authored by Christian Müller's avatar Christian Müller

improve cnf generation, add mroe tests

parent 11419365
......@@ -67,8 +67,6 @@ object Preconditions extends LazyLogging {
}
def getUpdate(s:Statement, b:SimpleBlock, choice:Option[Fun], isOracly:Boolean, spec:Spec, properties:InvProperties) = {
val frees = s.guard.freeVars() -- s.tuple.toSet
// val list = List(s.guard) ++ choice.toList
// val guard = And.make(list)
......@@ -99,6 +97,7 @@ object Preconditions extends LazyLogging {
val guard = And(s.guard, con).simplify()
// val guard = True
val frees = guard.freeVars() -- s.tuple.toSet
val form = s match {
case Add(_, _, _) => {
......
......@@ -6,8 +6,9 @@ import java.io.File
import java.io.PrintWriter
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.toz3.InvProperties
import com.typesafe.scalalogging.LazyLogging
object Utils {
object Utils extends LazyLogging {
val RESULTSFOLDER = "results"
......@@ -61,11 +62,13 @@ object Utils {
val writer = new PrintWriter(file)
writer.print(prop)
writer.close()
logger.info(s"Written $name")
}
def check(name:String, desc:String, inv:Formula, spec:Spec, properties:InvProperties) = {
val model = if (properties.stubborn) "stubborn" else "causal"
val filenames = s"${name}_${model}_${desc}"
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) =
InvariantChecker.checkInvariantFPLabelling(spec, inv, properties)
......@@ -75,6 +78,13 @@ object Utils {
val strengthenings = for (List(a, b) <- labelling.sliding(2) if (a != b)) yield {
true
}
val labels = (for ((node, inv) <- labelling.last) yield {
s"Node ${node.value}:\n${inv.pretty()}\n"
}).mkString("\n")
Utils.write(s"$filenames.invariants", labels)
val wfsize = graph.edges.size - 1
val invsizes = labelling.last.map(_._2.opsize())
val maxsize = invsizes.max
......
......@@ -162,6 +162,21 @@ object FormulaFunctions extends LazyLogging {
case x => x
}
}
def everywhereBotUp(trans: PartialFunction[Formula, Formula], t: Formula): Formula = {
if (trans.isDefinedAt(t))
everywhereBotUp(trans, trans(t))
else {
val sub = t match {
// Extractors
case Quantifier(make, ps, t) => make(ps, everywhereBotUp(trans, t))
case UnOp(make, t1) => make(everywhereBotUp(trans, t1))
case BinOp(make, t1, t2) => make(everywhereBotUp(trans, t1), everywhereBotUp(trans, t2))
case x => x
}
sub
}
}
def opsize(t: Formula): Int = {
t match {
......@@ -436,12 +451,16 @@ object FormulaFunctions extends LazyLogging {
// normalized is now Quantifiers, then only And/Or with Negation inside
// no simplification here
val cnf = toCNFSub(normalized)
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(cnf)
val quantifiers = FormulaFunctions.collectQuantifiers(cnf1)
// Inspect clauses
val clauses = FOTransformers.collectClauses(cnf)
val clauses = FOTransformers.collectClauses(cnf1)
// TODO improve runtime
val simpedset = clauses.toSet
......
......@@ -135,7 +135,7 @@ object InvariantChecker extends LazyLogging {
// --> unsafe, relabel incoming node, invalidate all proven guarantees for that node
// check if relabelled invariant still satisfiable
// never relabel initial node
logger.info(s"Invariant not inductive, strengthening")
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)
......@@ -155,7 +155,7 @@ object InvariantChecker extends LazyLogging {
val (status2, solver2) = checkOnZ3(Implies(newinv, False))
if (status2 == Status.SATISFIABLE) {
// Negation of newinv still sat, newinv does not imply false)
logger.info(s"Relabeling ${next._1}. Continuing.")
logger.info(s"Relabeling ${next._1}. New size: ${newinv.opsize()}. Continuing.")
checkInvariantRec(newlabels :: labellist, newproven :: provenlist)
} else {
logger.info(s"New invariant for ${next._1} not satisfiable. Terminating.")
......@@ -163,6 +163,7 @@ object InvariantChecker extends LazyLogging {
}
} else {
logger.info("Would have to relabel initial node. Terminating.")
logger.info(s"Model: ${Z3.printModel(solver.getModel())}")
(false, labellist, provenlist)
}
}
......
......@@ -92,6 +92,36 @@ class FOLTLTest extends FlatSpec {
)
}
it should "also compute CNF" in {
val f = Or.make(And("a", "b"), And("c","d"), And("e", "f"))
f.toCNF().simplify() should be (
And.make(
Or.make("a", "c", "e"),
Or.make("a", "c", "f"),
Or.make("a","d", "e"),
Or.make("a","d","f"),
Or.make("b","c","e"),
Or.make("b","c","f"),
Or.make("b","d","e"),
Or.make("b","d","f")
)
)
}
it should "also compute CNF for weird structural things" in {
val f = Or.make(And("a", "b"), And("c","d"), Or("e", "f"))
f.toCNF().simplify() should be (
And.make(
Or.make("a", "c", "e", "f"),
Or.make("a","d", "e", "f"),
Or.make("b","c","e", "f"),
Or.make("b","d","e", "f")
)
)
}
it should "compute CNF for formulas with quantifiers" in {
val f = Or(And(Exists("c", "c"), "b"), And(Exists("c", "c"),"d"))
f.toCNF().simplify() should be (
......
......@@ -82,10 +82,10 @@ class FOTransformSpec extends FlatSpec {
}
it should "work with constants" in {
val f = Forall(List("x"), Or(Var("c"), Exists("z", Fun("f", List("x","z")))))
val f = Forall(List("x"), Or(Fun("f", "c"), Exists("z", Fun("g", List("x","z")))))
FOTransformers.abstractExistentials(f) should be (
Forall(List("x"), Or(Var("c"), Or(Fun("f", List("x","c")), Fun("f", List("x","x")))))
Forall(List("x"), Or(Fun("f", "c"), Or(Fun("g", List("x","c")), Fun("g", List("x","x")))))
)
}
......
......@@ -53,7 +53,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.checkInvariant(wf, inv, true)
// val (safe, msg) = InvariantChecker.checkInvariantFP(wf, inv, true)
//
// safe should be(false)
// }
......
......@@ -19,20 +19,20 @@ import de.tum.workflows.tests.TestUtils._
class OmittingInvariantFilesTest extends FlatSpec {
"InvariantChecker" should "prove simple may things safe" in {
val name = "tests/simpleChoiceOmittingNoOracle"
val inv =
And(Forall(List("xt"), genEq("S", List("xt"))),
Forall(List("xt","st"), genEq("R",List("xt","st")))
)
assert(checkSafeStubborn(name, inv))
}
it should "prove simple things safe" in {
val name = "tests/simpleOmittingNoChoice"
val inv = Forall(List("xt"), genEq("S",List("xt")))
assert(checkSafeStubborn(name, inv))
}
// "InvariantChecker" should "prove simple may things safe" in {
// val name = "tests/simpleChoiceOmittingNoOracle"
// val inv =
// And(Forall(List("xt"), genEq("S", List("xt"))),
// Forall(List("xt","st"), genEq("R",List("xt","st")))
// )
// assert(checkSafeStubborn(name, inv))
// }
//
// it should "prove simple things safe" in {
// val name = "tests/simpleOmittingNoChoice"
// val inv = Forall(List("xt"), genEq("S",List("xt")))
// assert(checkSafeStubborn(name, inv))
// }
it should "fail on oracly things" in {
val name = "tests/simpleChoiceOmitting"
......@@ -40,9 +40,9 @@ class OmittingInvariantFilesTest extends FlatSpec {
assert(!checkSafeStubborn(name, inv))
}
it should "work on declassified oracly things" in {
val name = "tests/simpleChoiceDeclassified"
val inv = Forall(List("xt"), genEq("R", List("xt")))
assert(checkSafeStubborn(name, inv))
}
// it should "work on declassified oracly things" in {
// val name = "tests/simpleChoiceDeclassified"
// val inv = Forall(List("xt"), genEq("R", List("xt")))
// assert(checkSafeStubborn(name, inv))
// }
}
\ No newline at end of file
......@@ -28,8 +28,8 @@ object TestUtils {
check(name, desc, inv, InvProperties(false, false))
}
def checkSafeCausalElim(name: String, inv: Formula) = {
check(name, "w/ elim", inv, InvProperties(false, true))
def checkSafeCausalElim(name: String, desc:String, inv: Formula) = {
check(name, s"${desc}_elim", inv, InvProperties(false, true))
}
def genEq(name: String, params: List[Var]) = {
......
......@@ -21,7 +21,7 @@ import de.tum.workflows.toz3.InvariantGenerator
class InvariantCausalFilesTest extends FlatSpec {
// it should "fail to prove conference_linear" ignore {
// it should "fail to prove conference_linear" in {
// val name = "nonomitting/conference_linear"
// val xt = Var("xt","X")
// val yt = Var("yt","X")
......@@ -33,7 +33,7 @@ class InvariantCausalFilesTest extends FlatSpec {
it should "fail to prove conference_linear alleq" in {
val name = "nonomitting/conference_linear"
val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
assert(!checkSafeCausal(name, "alleq", inv))
assert(!checkSafeCausalElim(name, "alleq", inv))
}
//
// // HEAP SPACE
......
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