NonOmittingInvariantFilesTest.scala 1.86 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
28
    assert(checkSafe(name, inv))
  }
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
34
    assert(checkSafe(name, inv))
  }
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
40
41
42
43
    assert(checkSafe(name, inv))
  }
  
  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
46
    assert(checkSafe(name, inv))
  }
Christian Müller's avatar
example    
Christian Müller committed
47

Christian Müller's avatar
Christian Müller committed
48
49
  it should "fail on oracly things" in {
    val name = "tests/simpleChoice"
50
    val inv = Forall(List("xt", "st"), genEq("R", List("xt", "st")))
Christian Müller's avatar
Christian Müller committed
51
    assert(!checkSafe(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
58
    assert(!checkSafe(name, inv))
  }
Christian Müller's avatar
example    
Christian Müller committed
59
}