LeaderElectionTest.scala 4.36 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
package de.tum.workflows.tests.papertests

import de.tum.workflows.{ExampleWorkflows, Utils, WorkflowParser}
import de.tum.workflows.Utils.check
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.tests.TestUtils.{checkSafeStubborn, genEq}
import de.tum.workflows.toz3.{InvProperties, Z3BSFO}
import org.scalatest.FlatSpec

class LeaderElectionTest extends FlatSpec {

  def check(name:String, inv:Formula, knowledge:Formula, properties:InvProperties):Boolean = {
    val spec = ExampleWorkflows.parseExample(name).get

    val spec2 = spec.addKnowledge(knowledge)
    Utils.check(name, "", inv, spec2, properties)
  }

  val properties = InvProperties(stubborn = true, eliminateA = true, eliminateB = true)


  val le_total_order_axioms = List(
    "∀x. Ile(x,x)",
    "∀x,y,z. (¬Ile(x,y) ∨ ¬Ile(y,z) ∨ Ile(x,z))",
    "∀x,y. (¬Ile(x,y) ∨ ¬Ile(y,x) ∨ x = y)",
    "∀x,y. (Ile(x,y) ∨ Ile(y,x))"

  ).map(WorkflowParser.parseTerm).map(_.get)

  val ringtop_axioms = List(
    "∀x,y,z. (¬Ibtw(x,y,z) ∨ Ibtw(y,z,x))",
    "∀w,x,y,z. (¬Ibtw(w,x,y) ∨ ¬Ibtw(w,y,z) ∨ Ibtw(w,x,z))",
    "∀w,x,y. (¬Ibtw(w,x,y) ∨ ¬Ibtw(w,y,x))",
    "∀w,x,y. (w = x ∨ w = y ∨ x = y ∨ Ibtw(w, x, y) ∨ Ibtw(w, y, x))"
  ).map(WorkflowParser.parseTerm).map(_.get)

  val next_axioms = List(
//    "∀a (¬Inext(a,a))",
    "∀a,b. (¬Inext(a,b) ∨ ∀x. (x = a ∨ x = b ∨ Ibtw(a,b,x)))",
Christian Müller's avatar
Christian Müller committed
40
//    "∀a,b. (Inext(a,b) ∨ ∃x. (x ≠ a ∧ x ≠ b ∧ ¬Ibtw(a,x,b)))"
Christian Müller's avatar
Christian Müller committed
41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67
  ).map(WorkflowParser.parseTerm).map(_.get)

  val inductive_inv = List(
    "∀n1,n2. (¬leader(n1) ∨ ¬leader(n2) ∨ n1 = n2)",
    "∀n1,n2. (n1 = n2 ∨ ¬leader(n1) ∨ ¬Ile(n1, n2))",
    "∀n1,n2. (n1 = n2 ∨ ¬msg(n1, n1) ∨ ¬Ile(n1, n2))",
    "∀n1,n2,n3. (¬Ibtw(n1,n2,n3) ∨ ¬msg(n2,n1) ∨ ¬Ile(n2,n3))"
  ).map(WorkflowParser.parseTerm).map(_.get)

  "Deterministic Leader election" should "be proven 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 = And.make(inductive_inv)

    assert(check(name, inv, knowledge, properties))
  }

Christian Müller's avatar
Christian Müller committed
68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
  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))
  }

Christian Müller's avatar
Christian Müller committed
129
  "Unsafe Deterministic Leader election" should "be proven unsafe" in {
Christian Müller's avatar
Christian Müller committed
130
    val name = "tests/leaderelection_unsafe"
Christian Müller's avatar
Christian Müller committed
131 132 133 134 135 136 137

    val total_order = And.make(le_total_order_axioms)
    val ringtop = And.make(ringtop_axioms)
    val next = And.make(next_axioms)

    val knowledge = And.make(
      total_order,
Christian Müller's avatar
Christian Müller committed
138 139
      ringtop,
      next
Christian Müller's avatar
Christian Müller committed
140 141 142
    )
//    val knowledge = True

Christian Müller's avatar
Christian Müller committed
143 144
    val inv = And.make(inductive_inv)
//    val inv = inductive_inv.head
Christian Müller's avatar
Christian Müller committed
145 146 147 148 149 150 151 152 153 154 155

    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

//    println(Z3BSFO.debugmodelBS(And.make(ringtop, next, forall)))

    assert(!check(name, inv, knowledge, properties))
  }


}