InvariantFilesTest.scala 1.88 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
example  
Christian Müller committed
17
18
19
20

class InvariantFilesTest extends FlatSpec {

  "InvariantChecker" should "prove simple things safe" in {
Christian Müller's avatar
Christian Müller committed
21
22
23
24
    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
25

Christian Müller's avatar
Christian Müller committed
26
27
28
29
30
31
32
33
34
35
36
  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
37

Christian Müller's avatar
Christian Müller committed
38
39
40
41
  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
42
43
  }
  
Christian Müller's avatar
Christian Müller committed
44
45
46
47
48
49
50
51
52
53
54
55
  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
56

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

Christian Müller's avatar
example  
Christian Müller committed
63
}