Commit e3cd409a authored by Christian Müller's avatar Christian Müller
Browse files

add paper example, not passing

parent 6fec927c
......@@ -35,5 +35,19 @@ class InvariantTest extends FlatSpec {
safe should be (false)
it should "prove the paper example" in {
val wf = ExampleWorkflows.parseExample("omitting/conference").get.w
val x = Var("x", "A")
val p = Var("p","P")
val r = Var("r","R")
val inv = Forall(List(x,p,r), Implies(Fun("Conf", List(x,p)), Neg(Fun("Read", List(x,p,r)))))
val safe = InvariantChecker.checkStubborn(wf, inv)
safe should be (true)
\ 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