NonOmittingInvariantFilesTest.scala 1.91 KB
Newer Older
Christian Müller's avatar
example    
Christian Müller committed
1
2
3
4
5
6
7
8
9
10
11
12
13
package de.tum.workflows.ltl.tests

import org.scalatest.FlatSpec
import org.scalatest.Matchers._
import org.scalatest.Inspectors._

import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.Implicits._
import de.tum.workflows.blocks._
import de.tum.workflows.Preconditions
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.ExampleWorkflows
import de.tum.workflows.toz3.InvariantChecker
Christian Müller's avatar
Christian Müller committed
14
15
16
import de.tum.workflows.Encoding._
import de.tum.workflows.Utils
import de.tum.workflows.Encoding
Christian Müller's avatar
Christian Müller committed
17
18
import de.tum.workflows.ExampleWorkflows
import de.tum.workflows.toz3.InvariantChecker
Christian Müller's avatar
example    
Christian Müller committed
19

20
21
import de.tum.workflows.tests.TestUtils._

Christian Müller's avatar
Christian Müller committed
22
class NonOmittingInvariantFilesTest extends FlatSpec {
Christian Müller's avatar
example    
Christian Müller committed
23
24

  "InvariantChecker" should "prove simple things safe" in {
Christian Müller's avatar
Christian Müller committed
25
    val name = "tests/simpleNoChoice2"
26
    val inv = Forall(List("xt", "st"), genEq("R", List("xt", "st")))
Christian Müller's avatar
Christian Müller committed
27
    assert(checkSafeStubborn(name, inv))
Christian Müller's avatar
Christian Müller committed
28
  }
Christian Müller's avatar
Christian Müller committed
29
30
31
  
  it should "prove simple may blocks safe" in {
    val name = "tests/simpleChoiceNoOracle"
32
    val inv = Forall(List("xt", "st"), genEq("R", List("xt", "st")))
Christian Müller's avatar
Christian Müller committed
33
    assert(checkSafeStubborn(name, inv))
Christian Müller's avatar
Christian Müller committed
34
  }
Christian Müller's avatar
example    
Christian Müller committed
35

Christian Müller's avatar
Christian Müller committed
36
37
  it should "prove simple loops safe" in {
    val name = "tests/loopexampleNoOracle"
38
    val inv = Forall(List("xt", "st"), genEq("R", List("xt", "st")))
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
42
43
  }
  
  it should "prove simple loops safe and iterate" in {
    val name = "tests/loopexampleNoOracle"
44
    val inv = Forall(List("xt", "yt", "st"), genEq("S", List("xt", "yt", "st")))
Christian Müller's avatar
Christian Müller committed
45
    assert(checkSafeStubborn(name, inv))
Christian Müller's avatar
Christian Müller committed
46
  }
Christian Müller's avatar
example    
Christian Müller committed
47

Christian Müller's avatar
Christian Müller committed
48
  it should "fail on oracly things" in {
Christian Müller's avatar
Christian Müller committed
49
    val name = "tests/simpleOracle"
50
    val inv = Forall(List("xt", "st"), genEq("R", List("xt", "st")))
Christian Müller's avatar
Christian Müller committed
51
    assert(!checkSafeStubborn(name, inv))
Christian Müller's avatar
example    
Christian Müller committed
52
53
  }
  
Christian Müller's avatar
Christian Müller committed
54
55
  it should "fail on loopy oracly things" in {
    val name = "tests/loopexample"
56
    val inv = Forall(List("xt", "yt", "st"), genEq("S", List("xt", "yt", "st")))
Christian Müller's avatar
Christian Müller committed
57
    assert(!checkSafeStubborn(name, inv))
Christian Müller's avatar
Christian Müller committed
58
  }
Christian Müller's avatar
example    
Christian Müller committed
59
}