NonOmittingInvariantFilesTest.scala 1.97 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

Christian Müller's avatar
Christian Müller committed
20
class NonOmittingInvariantFilesTest extends FlatSpec {
Christian Müller's avatar
example  
Christian Müller committed
21
22

  "InvariantChecker" should "prove simple things safe" in {
Christian Müller's avatar
Christian Müller committed
23
24
25
26
    val name = "tests/simpleNoChoice2"
    val inv = Forall(List("x", "s"), genEq("R", List("x", "s")))
    assert(checkSafe(name, inv))
  }
Christian Müller's avatar
example  
Christian Müller committed
27

Christian Müller's avatar
Christian Müller committed
28
29
30
31
32
33
34
35
36
37
38
  it should "prove simple loops safe" in {
    val name = "tests/loopexampleNoOracle"
    val inv = Forall(List("x", "s"), genEq("R", List("x", "s")))
    assert(checkSafe(name, inv))
  }
  
  it should "prove simple loops safe and iterate" in {
    val name = "tests/loopexampleNoOracle"
    val inv = Forall(List("x", "y", "s"), genEq("S", List("x", "y", "s")))
    assert(checkSafe(name, inv))
  }
Christian Müller's avatar
example  
Christian Müller committed
39

Christian Müller's avatar
Christian Müller committed
40
41
42
43
  it should "fail on oracly things" in {
    val name = "tests/simpleChoice"
    val inv = Forall(List("x", "s"), genEq("R", List("x", "s")))
    assert(!checkSafe(name, inv))
Christian Müller's avatar
example  
Christian Müller committed
44
45
  }
  
Christian Müller's avatar
Christian Müller committed
46
47
48
49
50
51
52
53
54
55
56
57
  it should "fail on loopy oracly things" in {
    val name = "tests/loopexample"
    val inv = Forall(List("x", "y", "s"), genEq("S", List("x", "y", "s")))
    assert(!checkSafe(name, inv))
  }

  def checkSafe(name: String, inv: Formula) = {
    val spec = ExampleWorkflows.parseExample(name).get
    val (res, dot) = InvariantChecker.checkInvariantFP(spec.w, inv, true)
    Utils.write(s"${name}.dot", dot)
    res
  }
Christian Müller's avatar
example  
Christian Müller committed
58

Christian Müller's avatar
Christian Müller committed
59
  def genEq(name: String, params: List[Var]) = {
Christian Müller's avatar
example  
Christian Müller committed
60
61
62
63
64
    val o1 = Fun(name, Some("t1"), params)
    val o2 = Fun(name, Some("t2"), params)
    Eq(o1, o2)
  }
}