OmittingInvariantFilesTest.scala 1.46 KB
Newer Older
1
package de.tum.niwo.tests
Christian Müller's avatar
Christian Müller committed
2 3 4 5

import org.scalatest.FlatSpec
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
6 7 8 9
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.Implicits._
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FormulaFunctions
10
import de.tum.niwo.Examples
Christian Müller's avatar
Christian Müller committed
11
import de.tum.niwo.graphs.WFGraphEncoding._
12
import de.tum.niwo.Utils
Christian Müller's avatar
Christian Müller committed
13
import de.tum.niwo.graphs.WFGraphEncoding
14
import de.tum.niwo.invariants.{InvariantChecker, Preconditions}
15
import de.tum.niwo.tests.TestUtils._
16

Christian Müller's avatar
Christian Müller committed
17 18
class OmittingInvariantFilesTest extends FlatSpec {
  
19 20 21 22 23 24 25 26 27 28 29 30 31 32
//  "InvariantChecker" should "prove simple may things safe" in {
//    val name = "tests/simpleChoiceOmittingNoOracle"
//    val inv = 
//      And(Forall(List("xt"), genEq("S", List("xt"))), 
//        Forall(List("xt","st"), genEq("R",List("xt","st")))
//        )
//    assert(checkSafeStubborn(name, inv))
//  }
//    
//  it should "prove simple things safe" in {
//	  val name = "tests/simpleOmittingNoChoice"
//			  val inv = Forall(List("xt"), genEq("S",List("xt")))
//			  assert(checkSafeStubborn(name, inv))
//  }
Christian Müller's avatar
Christian Müller committed
33 34 35
  
  it should "fail on oracly things" in {
    val name = "tests/simpleChoiceOmitting"
Christian Müller's avatar
Christian Müller committed
36
    val inv = Forall(List("xt"), genEq("R", List("xt")))
Christian Müller's avatar
Christian Müller committed
37
    assert(!checkSafeStubborn(name, _ => inv))
Christian Müller's avatar
Christian Müller committed
38
  }
Christian Müller's avatar
Christian Müller committed
39
  
40 41 42 43 44
//  it should "work on declassified oracly things" in {
//    val name = "tests/simpleChoiceDeclassified"
//    val inv = Forall(List("xt"), genEq("R", List("xt")))
//    assert(checkSafeStubborn(name, inv))
//  }
Christian Müller's avatar
Christian Müller committed
45
}