DemoNoStrengtheningTests.scala 3.46 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
package de.tum.workflows.tests.papertests

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.tests.TestUtils._
import de.tum.workflows.toz3.InvariantGenerator

class DemoNoStrengtheningTests extends FlatSpec {

  // fixed arity, nonomitting - easy
  it should "fail to prove nonomitting/fixedarity10 alleq" in {
    val name = "nonomitting/fixedarity10"
    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
    assert(!checkSafeStubborn(name, "alleq", inv))
  }
  it should "prove nonomitting/fixedarity10_safe alleq" in {
    val name = "nonomitting/fixedarity10safe"
    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
    assert(checkSafeStubborn(name, "alleq", inv))
  }
  it should "fail to prove nonomitting/fixedarity15 alleq" in {
    val name = "nonomitting/fixedarity15"
    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
    assert(!checkSafeStubborn(name, "alleq", inv))
  }
  it should "prove nonomitting/fixedarity15_safe alleq" in {
    val name = "nonomitting/fixedarity15safe"
    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
    assert(checkSafeStubborn(name, "alleq", inv))
  }
  it should "fail to prove nonomitting/fixedarity20 alleq" in {
    val name = "nonomitting/fixedarity20"
    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
    assert(!checkSafeStubborn(name, "alleq", inv))
  }
  it should "prove nonomitting/fixedarity20_safe alleq" in {
    val name = "nonomitting/fixedarity20safe"
    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
    assert(checkSafeStubborn(name, "alleq", inv))
  }

  // nonomitting, incarity
  it should "prove nonomitting/incarity5 alleq" in {
    val name = "nonomitting/incarity5"
    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
    assert(checkSafeStubborn(name, "alleq", inv))
  }





  // nonomitting, tests

  it should "prove tests/simpleChoiceDeclassified alleq" in {
    val name = "tests/simpleChoiceDeclassified"
    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
    assert(checkSafeStubborn(name, "alleq", inv))
  }
  it should "prove tests/simpleChoiceDeclassified causal alleq" in {
    val name = "tests/simpleChoiceDeclassified"
    val inv = InvariantGenerator.invariantAllEqual(ExampleWorkflows.parseExample(name).get)
    assert(checkSafeCausal(name, "alleq", inv))
  }
  it should "prove tests/simpleChoiceCausal alleq" in {
    val name = "tests/simpleChoiceCausal"
    val inv = InvariantGenerator.invariantNoninterSingleBS(ExampleWorkflows.parseExample(name).get)
    assert(checkSafeStubborn(name, "alleq", inv))
  }
  it should "prove tests/simpleChoiceCausal causal alleq" in {
    val name = "tests/simpleChoiceCausal"
    val inv = InvariantGenerator.invariantNoninterSingleBS(ExampleWorkflows.parseExample(name).get)
    assert(!checkSafeCausal(name, "alleq", inv))
  }
}