Commit 655c4be6 authored by Eugen Zalinescu's avatar Eugen Zalinescu

new invariant

parent e3cd409a
......@@ -237,7 +237,7 @@ object toZ3 extends LazyLogging {
}
def translate(f: Formula, ctx: Context, varctx: VarCtx) = {
logger.info(s"Using formula:\n${f.pretty()}")
// logger.info(s"Using formula:\n${f.pretty()}")
if (!f.freeVars().isEmpty) {
logger.error(s"Cannot check - formula contains free variables ${f.freeVars()}")
......@@ -245,7 +245,7 @@ object toZ3 extends LazyLogging {
fun_ctx.clear()
val expr = toZ3(ctx, f, ctx.mkInt(0), None, varctx)
logger.info(s"Built Z3 expression:\n$expr")
// logger.info(s"Built Z3 expression:\n$expr")
expr
}
}
......@@ -25,7 +25,7 @@ class InvariantTest extends FlatSpec {
safe should be (true)
}
it should "prove fail to prove unsafe workflows safe" in {
it should "fail to prove unsafe workflows safe" in {
val wf = ExampleWorkflows.parseExample("tests/simpleChoice").get.w
......@@ -40,14 +40,35 @@ class InvariantTest extends FlatSpec {
val wf = ExampleWorkflows.parseExample("omitting/conference").get.w
val x = Var("x", "A")
val y = Var("y", "A")
val p = Var("p","P")
val r = Var("r","R")
val c = Fun("Conf", Some("t1"), List(x,p))
//
val ceq = genEq("Conf", List(x,p))
val oeq = genEq("O", List(x,p,r))
val readeq = genEq("Read", List(x,p,r))
val assigneq = genEq("Assign", List(x,p))
val revieweq = genEq("Review", List(x,p,r))
// val premise = And(Neg(c), oeq)
// val conclusion = And.make(ceq, readeq, assigneq, Forall(y, revieweq))
val inv = Forall(List(x,p,r), Implies(Fun("Conf", List(x,p)), Neg(Fun("Read", List(x,p,r)))))
val premise = Forall(List(p,r), And(Neg(c), oeq))
val conclusion = Forall(List(p,r), And.make(ceq, readeq, assigneq, revieweq))
val inv = Forall(List(x),
Implies(premise, conclusion)
)
val safe = InvariantChecker.checkStubborn(wf, inv)
safe should be (true)
}
def genEq(name:String, params: List[Var]) = {
val o1 = Fun(name, Some("t1"), params)
val o2 = Fun(name, Some("t2"), params)
Eq(o1, o2)
}
}
\ 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