InferenceTests.scala 2.29 KB
Newer Older
1
package de.tum.niwo.tests
2 3 4 5 6

import org.scalatest.FlatSpec
import org.scalatest.FlatSpec
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
7 8 9 10 11
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.Implicits._
import de.tum.niwo.blocks._
import de.tum.niwo.Preconditions
import de.tum.niwo.foltl.FormulaFunctions
12
import de.tum.niwo.Examples
13 14 15 16 17 18
import de.tum.niwo.toz3.{InvariantChecker, InvariantGenerator}
import de.tum.niwo.Encoding._
import de.tum.niwo.Utils
import de.tum.niwo.Encoding
import de.tum.niwo.tests.TestUtils._
import de.tum.niwo.foltl.Properties
19 20 21 22 23 24 25 26 27 28


class InferenceTests  extends FlatSpec {

  "Invariant Inference" should "prove safe stuff safe" in {
    val name = "tests/conference_linear_small_withB"
    val xt = Var("xt","X")
    val yt = Var("yt","X")
    val pt = Var("pt","P")
//    val rt = Var("rt","R")
Christian Müller's avatar
Christian Müller committed
29
    val inv = Forall(List(xt, pt, yt), genEq("Comm", List(xt, yt, pt)))
30 31 32
    assert(checkSafeStubborn(name, inv))
  }

Christian Müller's avatar
Christian Müller committed
33 34 35 36 37 38 39 40 41 42
  "Invariant Inference" should "fail prove unsafe stuff safe" in {
    val name = "tests/conference_linear_small_unsafe"
    val xt = Var("xt","X")
    val yt = Var("yt","X")
    val pt = Var("pt","P")
    //    val rt = Var("rt","R")
    val inv = Forall(List(xt, pt, yt), genEq("Comm", List(xt, yt, pt)))
    assert(!checkSafeStubborn(name, inv))
  }

43 44 45 46 47 48 49 50 51 52
  it should "prove safe causal stuff safe" in {
    val name = "tests/conference_linear_small_withB"
    val xt = Var("xt","X")
    val yt = Var("yt","X")
    val pt = Var("pt","P")
    //    val rt = Var("rt","R")
    val inv = Forall(List(xt, pt, yt), genEq("Comm", List(xt, yt, pt)))
    assert(checkSafeCausalElim(name, "", inv))
  }

Christian Müller's avatar
Christian Müller committed
53 54 55 56 57 58 59 60 61 62
  it should "prove safe loopy stubborn stuff safe" in {
    val name = "tests/conference_stubborn_withB"
    val xat = Var("xat","A")
    val xbt = Var("xbt","A")
    val pt = Var("pt","P")
    //    val rt = Var("rt","R")
    val inv = Forall(List(xat, xbt, pt), genEq("Read", List(xat, xbt, pt)))
    assert(checkSafeStubborn(name, "", inv))
  }

Christian Müller's avatar
stuff  
Christian Müller committed
63
  it should "prove safe loopy causal stuff safe" ignore {
Christian Müller's avatar
Christian Müller committed
64 65 66 67 68 69 70 71
    val name = "tests/conference_stubborn_withB"
    val xat = Var("xat","A")
    val xbt = Var("xbt","A")
    val pt = Var("pt","P")
    //    val rt = Var("rt","R")
    val inv = Forall(List(xat, xbt, pt), genEq("Read", List(xat, xbt, pt)))
    assert(checkSafeCausalElim(name, "", inv))
  }
72
}