InvariantEasychairTest.scala 7.87 KB
Newer Older
1
package de.tum.niwo.tests.papertests
Christian Müller's avatar
Christian Müller committed
2

Christian Müller's avatar
Christian Müller committed
3
import org.scalatest.{FlatSpec, Ignore}
Christian Müller's avatar
Christian Müller committed
4 5
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
6 7 8 9
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.Implicits._
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FormulaFunctions
10
import de.tum.niwo.Examples
Christian Müller's avatar
Christian Müller committed
11
import de.tum.niwo.graphs.WFGraphEncoding._
12
import de.tum.niwo.Utils
13
import de.tum.niwo.Examples
Christian Müller's avatar
Christian Müller committed
14
import de.tum.niwo.graphs.WFGraphEncoding
Christian Müller's avatar
Christian Müller committed
15 16
import de.tum.niwo.invariants.{InvProperties, InvariantGenerator}
import de.tum.niwo.invariants.InvariantGenerator._
17
import de.tum.niwo.tests.TestUtils._
Christian Müller's avatar
Christian Müller committed
18 19 20

class InvariantEasychairTest extends FlatSpec {

Christian Müller's avatar
Christian Müller committed
21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
  "InvariantChecker" should "prove trivial nonomitting/conference safe" in {
    val name = "nonomitting/conference"
    val x = Var("xt", "A")
    val p = Var("pt","P")
    val inv = Forall(List(x, p), genEq("Conf", List(x, p)))
    assert(checkSafeStubborn(name, "onlyconf", _ => inv))
  }

  it should "prove stubborn conference" in {
    val name = "nonomitting/conference_stubborn"
    val inv = InvariantGenerator.invariantNoninterSingleBS _
    assert(checkSafe(name, "", inv, InvProperties(
      stubborn = true,
      approxElim = false
    )))
  }

  // TODO: seems brittle to approxelim
  it should "prove stubborn conference accept" in {
    val name = "nonomitting/conference-acceptance"
    val inv = InvariantGenerator.invariantNoninterSingleBS _
    assert(checkSafe(name, "", inv, InvProperties(
      stubborn = true,
      approxElim = false
    )))
  }

  it should "prove stubborn conference accept even with approxElim" in {
    val name = "nonomitting/conference-acceptance"
    val inv = InvariantGenerator.invariantNoninterSingleBS _
    assert(checkSafe(name, "", inv, InvProperties(
      stubborn = true,
      approxElim = true
    )))
  }

57 58
  // heap space
  it should "fail to prove causal conference accept without approxElim" ignore {
Christian Müller's avatar
Christian Müller committed
59 60
    val name = "nonomitting/conference-acceptance"
    val inv = InvariantGenerator.invariantNoninterSingleBS _
61
    assert(!checkSafe(name, "", inv, InvProperties(
Christian Müller's avatar
Christian Müller committed
62 63 64 65 66
      stubborn = false,
      approxElim = false
    )))
  }

67
  it should "fail to prove causal conference accept with approxElim" in {
Christian Müller's avatar
Christian Müller committed
68 69
    val name = "nonomitting/conference-acceptance"
    val inv = InvariantGenerator.invariantNoninterSingleBS _
70
    assert(!checkSafe(name, "", inv, InvProperties(
Christian Müller's avatar
Christian Müller committed
71 72 73 74
      stubborn = true,
      approxElim = true
    )))
  }
Christian Müller's avatar
Christian Müller committed
75 76 77 78 79 80 81 82 83 84
  //
  //  it should "prove nonomitting/conference_linear with declass safe" ignore {
  //    val name = "nonomitting/conference_linear"
  //    val x = Var("xt", "X")
  //    val y = Var("yt","X")
  //    val p = Var("pt","P")
  //    val inv = Forall(List(x, p), genEq("Comm", List(x, y, p)))
  //    assert(checkSafeStubborn(name, inv))
  //  }
  //
85 86 87 88 89
//    it should "prove stubborn conference_linear alleq" in {
//      val name = "omitting/conference_linear_fixed_stubborn"
//      val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
//      assert(checkSafeStubbornNoElim(name, inv))
//    }
Christian Müller's avatar
Christian Müller committed
90

91 92 93 94 95
//  it should "prove stubborn conference_linear alleq" in {
//    val name = "omitting/conference_linear_fixed_stubborn"
//    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
//    assert(checkSafeStubborn(name, "with_elim", inv))
//  }
Christian Müller's avatar
Christian Müller committed
96

97 98 99 100 101 102 103 104 105
  it should "prove omitting/conference_fixed without eliminating Aux" in {
    val name = "omitting/conference_fixed_stubborn"
    val inv = InvariantGenerator.invariantNoninterSingleBS _
    assert(checkSafe(name, "", inv, InvProperties(
      stubborn = true,
      eliminateA = false,
      approxElim = false
    )))
  }
Christian Müller's avatar
Christian Müller committed
106

107 108 109 110 111 112 113 114 115 116 117
  // HEAP SPACE
  it should "prove omitting/conference_fixed" ignore {
    val name = "omitting/conference_fixed_stubborn"
    val inv = InvariantGenerator.invariantNoninterSingleBS _
    assert(checkSafe(name, "", inv, InvProperties(
      stubborn = true,
      approxElim = false
    )))
  }

  // Brittle against approx elim
Christian Müller's avatar
Christian Müller committed
118
  it should "prove omitting/conference_fixed with auxelim approximation" in {
119 120 121 122 123 124 125
    val name = "omitting/conference_fixed_stubborn"
    val inv = InvariantGenerator.invariantNoninterSingleBS _
    assert(checkSafe(name, "", inv, InvProperties(
      stubborn = true,
      approxElim = true
    )))
  }
Christian Müller's avatar
Christian Müller committed
126

127 128 129 130 131
//  it should "prove omitting/conference_fixed alleq" in {
//    val name = "omitting/conference_fixed_stubborn"
//    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
//    assert(checkSafeStubborn(name, "alleq", inv))
//  }
Christian Müller's avatar
Christian Müller committed
132

133 134 135 136 137 138 139 140 141 142 143 144 145 146
//  it should "prove stubborn conference" in {
//    val name = "omitting/conference_stubborn"
//    val x = Var("xt", "A")
//    val r = Var("rt", "R")
//    val inv = Forall(List(x, r), genEq("Read", List(x, r)))
//    assert(checkSafeStubbornNoElim(name, inv))
//  }
//
//  it should "prove stubborn conference alleq" in {
//    val name = "omitting/conference_stubborn"
//    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
//    assert(checkSafeStubborn(name, "alleq", inv))
//  }
//
147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175

  it should "prove stubborn conference_linear_fixed" in {
    val name = "omitting/conference_linear_fixed_stubborn"
    val inv = InvariantGenerator.invariantNoninterSingleBS _
    assert(checkSafe(name, "", inv, InvProperties(
      stubborn = true,
      approxElim = false
    )))
  }

  // Brittle vs approxElim
  it should "prove causal conference_linear_fixed with elim approx" in {
    val name = "omitting/conference_linear_fixed_stubborn"
    val inv = InvariantGenerator.invariantNoninterSingleBS _
    assert(checkSafe(name, "", inv, InvProperties(
      stubborn = false,
      approxElim = true
    )))
  }

  // CNF has 14k clauses
  it should "prove causal conference_linear_fixed" in {
    val name = "omitting/conference_linear_fixed_stubborn"
    val inv = InvariantGenerator.invariantNoninterSingleBS _
    assert(checkSafe(name, "", inv, InvProperties(
      stubborn = false,
      approxElim = false
    )))
  }
Christian Müller's avatar
Christian Müller committed
176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213

  //  it should "prove stubborn conference_linear_fixed alleq" ignore {
  //    val name = "omitting/conference_linear_fixed"
  //    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
  //    assert(checkSafeStubborn(name, "alleq", inv))
  //  }
  //
  //  it should "prove tests/conferenceNoOracle safe" ignore {
  //    val name = "tests/conferenceNoOracle"
  //    val xa = Var("xat","A")
  //    val xb = Var("xbt","A")
  //    val p = Var("pt","P")
  //    val inv = Forall(List(xa, xb, p), genEq("Read", List(xa, xb, p)))
  //    assert(checkSafeStubborn(name, inv))
  //  }
  //
  //  it should "prove tests/omittingConferenceNoOracle safe" in {
  //    val name = "tests/omittingConferenceNoOracle"
  //    val xa = Var("xat","A")
  //    val xb = Var("xbt","A")
  //    val inv = Forall(List(xa, xb), genEq("Read", List(xa, xb)))
  //    assert(checkSafeStubborn(name, inv))
  //  }
  //
  //  it should "fail on oracly nonomitting/conference without declass" ignore {
  //    val name = "nonomitting/conferenceNoDeclass"
  //    val xa = Var("xat","A")
  //    val xb = Var("xbt","A")
  //    val p = Var("pt", "P")
  //    val r = Var("rt", "R")
  //    val inv = Forall(List(xa, xb, p, r), genEq("Read", List(xa, xb, p, r)))
  //    assert(!checkSafeStubborn(name, inv))
  //  }
  //
  //  it should "fail on oracly nonomitting/conference without declass alleq" in {
  //    val name = "nonomitting/conferenceNoDeclass"
  //    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
  //    assert(!checkSafeStubborn(name, "alleq", inv))
Christian Müller's avatar
Christian Müller committed
214 215 216 217 218 219 220 221 222 223 224
//    }

//    it should "prove oracly nonomitting/conference with declass" ignore {
//      val name = "nonomitting/conference"
//      val xa = Var("xat","A")
//      val xb = Var("xbt","A")
//      val p = Var("pt", "P")
//      val r = Var("rt", "R")
//      val inv = Forall(List(xa, xb, p, r), genEq("Read", List(xa, xb, p, r)))
//      assert(checkSafeStubborn(name, inv))
//    }
Christian Müller's avatar
Christian Müller committed
225
  //
Christian Müller's avatar
Christian Müller committed
226

Christian Müller's avatar
Christian Müller committed
227
}