InferenceTests.scala 2.33 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
Christian Müller's avatar
Christian Müller committed
13
import de.tum.niwo.graphs.WFGraphEncoding._
14 15 16
import de.tum.niwo.Utils
import de.tum.niwo.tests.TestUtils._
import de.tum.niwo.foltl.Properties
Christian Müller's avatar
Christian Müller committed
17
import de.tum.niwo.graphs.WFGraphEncoding
Christian Müller's avatar
Christian Müller committed
18
import de.tum.niwo.invariants.InvariantGenerator
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)))
Christian Müller's avatar
Christian Müller committed
30
    assert(checkSafeStubborn(name, _ => inv))
31 32
  }

Christian Müller's avatar
Christian Müller committed
33 34 35 36 37 38 39
  "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)))
Christian Müller's avatar
Christian Müller committed
40
    assert(!checkSafeStubborn(name, _ => inv))
Christian Müller's avatar
Christian Müller committed
41 42
  }

43 44 45 46 47 48 49
  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)))
Christian Müller's avatar
Christian Müller committed
50
    assert(checkSafeCausalElim(name, "", _ => inv))
51 52
  }

Christian Müller's avatar
Christian Müller committed
53 54 55 56 57 58 59
  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)))
Christian Müller's avatar
Christian Müller committed
60
    assert(checkSafeStubborn(name, "", _ => inv))
Christian Müller's avatar
Christian Müller committed
61 62
  }

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
    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)))
Christian Müller's avatar
Christian Müller committed
70
    assert(checkSafeCausalElim(name, "", _ => inv))
Christian Müller's avatar
Christian Müller committed
71
  }
72
}