Commit 9d5cd1c4 authored by Christian Müller's avatar Christian Müller

inv

parent 5b9d9ef0
......@@ -95,6 +95,17 @@ class InvariantCausalFilesTest extends FlatSpec {
assert(!checkSafeCausal(name, inv))
}
// HEAP SPACE
it should "fail to prove nonomitting/conference with elim" ignore {
val name = "nonomitting/conference"
val xt = Var("xat","X")
val yt = Var("xbt","X")
val pt = Var("pt","P")
val rt = Var("rt","R")
val inv = Forall(List(xt, pt, yt, rt), genEq("Read", List(xt, yt, pt, rt)))
assert(!checkSafeCausalElim(name, inv))
}
it should "fail to prove omitting/conference" in {
val name = "omitting/conference"
val xt = Var("xat","X")
......@@ -103,5 +114,14 @@ class InvariantCausalFilesTest extends FlatSpec {
val inv = Forall(List(xt, pt), genEq("Read", List(xt, pt, rt)))
assert(!checkSafeCausal(name, inv))
}
it should "fail to prove omitting/conference with elim" in {
val name = "omitting/conference"
val xt = Var("xat","X")
val pt = Var("pt","P")
val rt = Var("rt","R")
val inv = Forall(List(xt, pt), genEq("Read", List(xt, pt, rt)))
assert(!checkSafeCausalElim(name, inv))
}
}
\ No newline at end of file
......@@ -11,7 +11,7 @@ object TestUtils {
val spec = ExampleWorkflows.parseExample(name).get
// do not blow up the formula with auxilliary elimination
val (time, (res, dot)) = Utils.time {
InvariantChecker.checkInvariantFP(spec, inv, InvProperties(false, false))
InvariantChecker.checkInvariantFP(spec, inv, properties)
}
for ((s, i) <- dot.zipWithIndex) {
Utils.write(s"${name}_${desc}_${i}.dot", s)
......
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