InferenceTests.scala 2.46 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
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.Implicits._
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FormulaFunctions
11
import de.tum.niwo.Examples
Christian Müller's avatar
Christian Müller committed
12
import de.tum.niwo.graphs.WFGraphEncoding._
13 14 15
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
16
import de.tum.niwo.graphs.WFGraphEncoding
17
import de.tum.niwo.invariants.{InvariantGenerator, Preconditions}
18 19 20 21 22 23 24 25 26 27


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
28
    val inv = Forall(List(xt, pt, yt), genEq("Comm", List(xt, yt, pt)))
Christian Müller's avatar
Christian Müller committed
29
    assert(checkSafeStubborn(name, _ => inv))
30 31
  }

Christian Müller's avatar
fix  
Christian Müller committed
32
  "Invariant Inference" should "fail to prove unsafe stuff safe" in {
Christian Müller's avatar
Christian Müller committed
33 34 35 36 37 38
    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
39
    assert(!checkSafeStubborn(name, _ => inv))
Christian Müller's avatar
Christian Müller committed
40 41
  }

Christian Müller's avatar
fix  
Christian Müller committed
42 43 44 45 46 47
//  type TSGraph = Graph[Int, LDiEdge]

//  def toBlock(e:TSGraph#EdgeT):SimpleTSBlock = e
//  def toNumber(n:TSGraph#NodeT):Int = n.toOuter


48 49 50 51 52 53 54
  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
55
    assert(checkSafeCausalElim(name, "", _ => inv))
56 57
  }

Christian Müller's avatar
Christian Müller committed
58 59 60 61 62 63 64
  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
65
    assert(checkSafeStubborn(name, "", _ => inv))
Christian Müller's avatar
Christian Müller committed
66 67
  }

Christian Müller's avatar
stuff  
Christian Müller committed
68
  it should "prove safe loopy causal stuff safe" ignore {
Christian Müller's avatar
Christian Müller committed
69 70 71 72 73 74
    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
75
    assert(checkSafeCausalElim(name, "", _ => inv))
Christian Müller's avatar
Christian Müller committed
76
  }
77
}