Commit 57f880ed authored by Christian Müller's avatar Christian Müller

leaders

parent 565ddafd
Workflow
forallmay a,b
Inext(a,b) -> msg += (a,b)
loop {
forall a
msg(a,a) -> leader += (a)
forallmay a,b,c
(Inext(b, c) ∧ msg(a, b) ∧ Ile(b, a)) -> msg += (a,c)
}
Target
msg(a1, a2)
Causality
Workflow
forallmay a,b
B(a,b) -> msg += (a,b)
loop {
forall a
msg(a,a) -> leader += (a)
forallmay a,b,c
(Inext(b, c) ∧ msg(a, b) ∧ Ile(b, a)) -> msg += (a,c)
}
Target
msg(a1, a2)
Causality
......@@ -166,7 +166,8 @@ object Preconditions extends LazyLogging {
}
}
replaced
// replaced
removed
}
def abstractedPrecondition(f: Formula, b: SimpleBlock, spec: NISpec, properties: InvProperties, untouched: Set[String]): Formula = {
......
......@@ -26,6 +26,7 @@ object FOTransformers extends LazyLogging {
def collectClauses(f:Formula):List[List[Formula]] = {
def collectClause(f:Formula):List[Formula] = f collect {
case t:Equal => List(t)
case t:Var => List(t)
case t:Neg => List(t)
case t:Fun => List(t)
......@@ -151,7 +152,8 @@ object FOTransformers extends LazyLogging {
val simpfFGineq = Z3BSFO.simplifyBS(fFGineq) // FIXME: is this correct? there are no quantifiers binding stuff
val GHineq = for ((hl, hargs) <- hls.zip(HPositiveargs); (gk, gargs) <- gks.zip(Gargs); harg <- hargs; garg <- gargs) yield {
Or.make(hl, gk, ineq(harg, garg))
// Or.make(hl, gk, ineq(harg, garg))
Or.make(hl, gk).parallelRename(harg, garg)
}
val fGHineq = And.make(FGineq)
val simpfGHineq = Z3BSFO.simplifyBS(fGHineq)
......@@ -164,8 +166,10 @@ object FOTransformers extends LazyLogging {
val freeparams = b.params.map(p => FormulaFunctions.generateName(p, bounds.toSet))
val gkineq = for ((gk, gargs) <- gks.zip(Gargs); garg <- gargs) yield {
Or.make(gk, ineq(garg, freeparams))
// Or.make(gk, ineq(garg, freeparams))
gk.parallelRename(garg, freeparams)
}
val fsol:Formula = And.make(gkineq)
val fsolq = FormulaFunctions.rewrapQuantifiers(quantifiers, fsol)
......
......@@ -37,7 +37,7 @@ class LeaderElectionTest extends FlatSpec {
val next_axioms = List(
// "∀a (¬Inext(a,a))",
"∀a,b. (¬Inext(a,b) ∨ ∀x. (x = a ∨ x = b ∨ Ibtw(a,b,x)))",
"∀a,b. (Inext(a,b) ∨ ∃x. (x ≠ a ∧ x ≠ b ∧ ¬Ibtw(a,x,b)))"
// "∀a,b. (Inext(a,b) ∨ ∃x. (x ≠ a ∧ x ≠ b ∧ ¬Ibtw(a,x,b)))"
).map(WorkflowParser.parseTerm).map(_.get)
val inductive_inv = List(
......@@ -65,8 +65,69 @@ class LeaderElectionTest extends FlatSpec {
assert(check(name, inv, knowledge, properties))
}
it should "be proven safe with As" in {
val name = "tests/leaderelection_withA"
val knowledge = And.make(
And.make(le_total_order_axioms),
And.make(ringtop_axioms),
And.make(next_axioms)
)
val inv = And.make(inductive_inv)
assert(check(name, inv, knowledge, properties))
}
it should "be proven safe with Bs" in {
val name = "tests/leaderelection_withB"
val knowledge = And.make(
And.make(le_total_order_axioms),
And.make(ringtop_axioms),
And.make(next_axioms)
)
val inv = And.make(inductive_inv)
assert(check(name, inv, knowledge, properties))
}
"Deterministic Leader election" should "be inferred safe" in {
val name = "tests/leaderelection"
println(le_total_order_axioms)
println(ringtop_axioms)
println(next_axioms)
val knowledge = And.make(
And.make(le_total_order_axioms),
And.make(ringtop_axioms),
And.make(next_axioms)
)
println(inductive_inv)
val inv = inductive_inv.head
assert(check(name, inv, knowledge, properties))
}
it should "be inferred safe with Bs" in {
val name = "tests/leaderelection_withB"
val knowledge = And.make(
And.make(le_total_order_axioms),
And.make(ringtop_axioms),
And.make(next_axioms)
)
val inv = inductive_inv.head
assert(check(name, inv, knowledge, properties))
}
"Unsafe Deterministic Leader election" should "be proven unsafe" in {
val name = "tests/leaderelection_nonext_unsafe"
val name = "tests/leaderelection_unsafe"
val total_order = And.make(le_total_order_axioms)
val ringtop = And.make(ringtop_axioms)
......@@ -74,14 +135,13 @@ class LeaderElectionTest extends FlatSpec {
val knowledge = And.make(
total_order,
ringtop
// ,
// next
ringtop,
next
)
// val knowledge = True
// val inv = And.make(inductive_inv)
val inv = inductive_inv.head
val inv = And.make(inductive_inv)
// val inv = inductive_inv.head
val exists = WorkflowParser.parseTerm("∃a,b. (a ≠ b)").get
val forall = WorkflowParser.parseTerm("∃a,b,c. (a ≠ b ∧ b ≠ c ∧ Ibtw(a,b,c))").get
......
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