InferenceTests.scala 2.47 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
fix  
Christian Müller committed
33
  "Invariant Inference" should "fail to prove unsafe stuff safe" in {
Christian Müller's avatar
Christian Müller committed
34 35 36 37 38 39
    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
  }

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

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


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

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

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