InvariantEasychairTest.scala 2.54 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
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
import de.tum.workflows.Encoding._
import de.tum.workflows.Utils
import de.tum.workflows.Encoding
import de.tum.workflows.ExampleWorkflows
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.toz3.InvariantGenerator

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

Christian Müller's avatar
Christian Müller committed
23
24
25
26
class InvariantEasychairTest extends FlatSpec {

  "InvariantChecker" should "prove nonomitting/conference safe" in {
    val name = "nonomitting/conference"
Christian Müller's avatar
Christian Müller committed
27
28
    val x = Var("xt", "A")
    val p = Var("pt","P")
Christian Müller's avatar
Christian Müller committed
29
    val inv = Forall(List(x, p), genEq("Conf", List(x, p)))
Christian Müller's avatar
Christian Müller committed
30
    assert(checkSafeStubborn(name, inv))
Christian Müller's avatar
Christian Müller committed
31
32
  }
  
Christian Müller's avatar
Christian Müller committed
33
34
35
36
37
38
  it should "prove nonomitting/conference_linear with declass safe" in {
    val name = "nonomitting/conference_linear"
    val x = Var("xt", "X")
    val y = Var("yt","X")
    val p = Var("pt","P")
    val inv = Forall(List(x, p), genEq("Comm", List(x, y, p)))
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
  }
  
  
Christian Müller's avatar
Christian Müller committed
43
44
  it should "prove tests/conferenceNoOracle safe" in {
    val name = "tests/conferenceNoOracle"
Christian Müller's avatar
Christian Müller committed
45
46
47
    val xa = Var("xat","A")
    val xb = Var("xbt","A")
    val p = Var("pt","P")
Christian Müller's avatar
Christian Müller committed
48
    val inv = Forall(List(xa, xb, p), genEq("Read", List(xa, xb, p)))
Christian Müller's avatar
Christian Müller committed
49
    assert(checkSafeStubborn(name, inv))
Christian Müller's avatar
Christian Müller committed
50
51
52
53
  }
  
  it should "prove tests/omittingConferenceNoOracle safe" in {
    val name = "tests/omittingConferenceNoOracle"
Christian Müller's avatar
Christian Müller committed
54
55
    val xa = Var("xat","A")
    val xb = Var("xbt","A")
Christian Müller's avatar
Christian Müller committed
56
    val inv = Forall(List(xa, xb), genEq("Read", List(xa, xb)))
Christian Müller's avatar
Christian Müller committed
57
    assert(checkSafeStubborn(name, inv))
Christian Müller's avatar
Christian Müller committed
58
59
60
  }
  
  it should "fail on oracly nonomitting/conference without declass" in {
Christian Müller's avatar
Christian Müller committed
61
62
63
64
65
    val name = "nonomitting/conferenceNoDeclass"
    val xa = Var("xat","A")
    val xb = Var("xbt","A")
    val p = Var("pt", "P")
    val r = Var("rt", "R")
Christian Müller's avatar
Christian Müller committed
66
    val inv = Forall(List(xa, xb, p, r), genEq("Read", List(xa, xb, p, r)))
Christian Müller's avatar
Christian Müller committed
67
    assert(!checkSafeStubborn(name, inv))
Christian Müller's avatar
Christian Müller committed
68
69
  }
  
Christian Müller's avatar
Christian Müller committed
70
  it should "prove oracly nonomitting/conference with declass" in {
Christian Müller's avatar
Christian Müller committed
71
    val name = "nonomitting/conference"
Christian Müller's avatar
Christian Müller committed
72
73
74
75
76
    val xa = Var("xat","A")
    val xb = Var("xbt","A")
    val p = Var("pt", "P")
    val r = Var("rt", "R")
    val inv = Forall(List(xa, xb, p, r), genEq("Read", List(xa, xb, p, r)))
Christian Müller's avatar
Christian Müller committed
77
    assert(checkSafeStubborn(name, inv))
Christian Müller's avatar
Christian Müller committed
78
79
  }
}