DemoNotebookTest.scala 1.87 KB
Newer Older
1
package de.tum.niwo.tests.papertests
2

Christian Müller's avatar
Christian Müller committed
3
import de.tum.niwo.invariants.{InvProperties, InvariantGenerator}
4
import de.tum.niwo.tests.TestUtils._
Christian Müller's avatar
Christian Müller committed
5 6
import org.scalatest.FlatSpec
import org.scalatest.Matchers._
7 8 9

class DemoNotebookTest extends FlatSpec {

Christian Müller's avatar
Christian Müller committed
10
  "Inference" should "prove nonomitting/notebook alleq" in {
11
    val name = "nonomitting/notebook_stubborn"
Christian Müller's avatar
Christian Müller committed
12
    val inv = InvariantGenerator.invariantNoninterSingleBS _
Christian Müller's avatar
pics  
Christian Müller committed
13
    assert(checkSafeStubborn(name, inv))
14 15
  }

Christian Müller's avatar
pics  
Christian Müller committed
16 17 18 19 20 21
//  should this happen?
//  it should "fail to prove nonomitting/notebook causal" in {
//    val name = "nonomitting/notebook"
//    val inv = InvariantGenerator.invariantNoninterSingleBS(ExampleWorkflows.parseExample(name).get)
//    assert(checkSafeCausal(name, "", inv))
//  }
22

23
  it should "prove nonomitting/notebook causal elim with cnf building" in {
24
    val name = "nonomitting/notebook"
Christian Müller's avatar
Christian Müller committed
25
    val inv = InvariantGenerator.invariantNoninterSingleBS _
Christian Müller's avatar
Christian Müller committed
26 27
    assert(checkSafe(name, "elim", inv,
      InvProperties(stubborn = false, approxElim = false)))
28
  }
Christian Müller's avatar
Christian Müller committed
29 30 31 32 33 34 35 36 37

  // FIXME: this seems brittle, depending on CNF or DNF of theta
  it should "prove nonomitting/notebook causal elim" in {
    val name = "nonomitting/notebook"
    val inv = InvariantGenerator.invariantNoninterSingleBS _
    assert(checkSafe(name, "elim", inv,
      InvProperties(stubborn = false, approxElim = true)))
  }

Christian Müller's avatar
pics  
Christian Müller committed
38
  it should "prove omitting/notebook_unsafe stubborn elim alleq" in {
Christian Müller's avatar
Christian Müller committed
39
    val name = "omitting/notebook_unsafe"
Christian Müller's avatar
Christian Müller committed
40
    val inv = InvariantGenerator.invariantAllEqual _
41 42 43 44
    assert(!checkSafe(name, "", inv, InvProperties(
      stubborn = true,
      approxElim = true
    )))
Christian Müller's avatar
Christian Müller committed
45
  }
46
  it should "fail to prove omitting/notebook_unsafe causal elim alleq" in {
Christian Müller's avatar
pics  
Christian Müller committed
47
    val name = "omitting/notebook_unsafe"
Christian Müller's avatar
Christian Müller committed
48
    val inv = InvariantGenerator.invariantNoninterSingleBS _
49 50 51 52
    assert(checkSafe(name, "", inv, InvProperties(
      stubborn = false,
      approxElim = true
    )))
Christian Müller's avatar
pics  
Christian Müller committed
53
  }
54
}