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

example

parent ade38ae1
Workflow
forall a,b,i
(Inext(a,b) ∧ B(i,a,b)) -> msg += (i,b)
(Inext(a,b) ∧ B(a,b,i)) -> msg += (i,b)
loop {
forall a
msg(a,a) -> leader += (a)
......
......@@ -100,7 +100,7 @@ object Preconditions extends LazyLogging {
val (repname, (vars, form)) = update
val fixupdate = FormulaFunctions.fixBinding(form, boundvars -- vars)
f everywhere {
val res = f everywhere {
case Fun(name, ind, params) if name == repname => {
val renamed = fixupdate.parallelRename(vars, params)
......@@ -112,6 +112,7 @@ object Preconditions extends LazyLogging {
}
}
}
res
})
}
......
......@@ -90,6 +90,13 @@ class LeaderElectionTest extends FlatSpec {
val inv = And.make(inductive_inv)
val emptyinv = inv.assumeEmpty(List("msg", "leader"))
val impl = Z3BSFO.debugmodelBS(knowledge land emptyinv)
// println(impl)
// knowledge /\ !emptyinv is unsat
// knowledge /\ emptyinv is sat
// !emptyinv is unsat
assert(check(name, inv, knowledge, properties))
}
......
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