DemoNoStrengtheningTests.scala 3.05 KB
Newer Older
1
package de.tum.niwo.tests.papertests
2

3
import de.tum.niwo.Examples
Christian Müller's avatar
Christian Müller committed
4
import de.tum.niwo.invariants.InvariantGenerator
5
import de.tum.niwo.tests.TestUtils._
Christian Müller's avatar
Christian Müller committed
6
import org.scalatest.{FlatSpec, Ignore}
7 8 9 10 11 12

class DemoNoStrengtheningTests extends FlatSpec {

  // fixed arity, nonomitting - easy
  it should "fail to prove nonomitting/fixedarity10 alleq" in {
    val name = "nonomitting/fixedarity10"
13
    val inv = InvariantGenerator.invariantAllEqual(Examples.parseExampleWF(name).get)
Christian Müller's avatar
Christian Müller committed
14
    assert(!checkSafeStubborn(name, "alleq", _ => inv))
15 16 17
  }
  it should "prove nonomitting/fixedarity10_safe alleq" in {
    val name = "nonomitting/fixedarity10safe"
18
    val inv = InvariantGenerator.invariantAllEqual(Examples.parseExampleWF(name).get)
Christian Müller's avatar
Christian Müller committed
19
    assert(checkSafeStubborn(name, "alleq", _ => inv))
20 21 22
  }
  it should "fail to prove nonomitting/fixedarity15 alleq" in {
    val name = "nonomitting/fixedarity15"
23
    val inv = InvariantGenerator.invariantAllEqual(Examples.parseExampleWF(name).get)
Christian Müller's avatar
Christian Müller committed
24
    assert(!checkSafeStubborn(name, "alleq", _ => inv))
25 26 27
  }
  it should "prove nonomitting/fixedarity15_safe alleq" in {
    val name = "nonomitting/fixedarity15safe"
28
    val inv = InvariantGenerator.invariantAllEqual(Examples.parseExampleWF(name).get)
Christian Müller's avatar
Christian Müller committed
29
    assert(checkSafeStubborn(name, "alleq", _ => inv))
30 31 32
  }
  it should "fail to prove nonomitting/fixedarity20 alleq" in {
    val name = "nonomitting/fixedarity20"
33
    val inv = InvariantGenerator.invariantAllEqual(Examples.parseExampleWF(name).get)
Christian Müller's avatar
Christian Müller committed
34
    assert(!checkSafeStubborn(name, "alleq", _ => inv))
35 36 37
  }
  it should "prove nonomitting/fixedarity20_safe alleq" in {
    val name = "nonomitting/fixedarity20safe"
38
    val inv = InvariantGenerator.invariantAllEqual(Examples.parseExampleWF(name).get)
Christian Müller's avatar
Christian Müller committed
39
    assert(checkSafeStubborn(name, "alleq", _ => inv))
40 41 42 43 44
  }

  // nonomitting, incarity
  it should "prove nonomitting/incarity5 alleq" in {
    val name = "nonomitting/incarity5"
45
    val inv = InvariantGenerator.invariantAllEqual(Examples.parseExampleWF(name).get)
Christian Müller's avatar
Christian Müller committed
46
    assert(checkSafeStubborn(name, "alleq", _ => inv))
47 48 49 50 51 52
  }

  // nonomitting, tests

  it should "prove tests/simpleChoiceDeclassified alleq" in {
    val name = "tests/simpleChoiceDeclassified"
53
    val inv = InvariantGenerator.invariantAllEqual(Examples.parseExampleWF(name).get)
Christian Müller's avatar
Christian Müller committed
54
    assert(checkSafeStubborn(name, "alleq", _ => inv))
55 56 57
  }
  it should "prove tests/simpleChoiceDeclassified causal alleq" in {
    val name = "tests/simpleChoiceDeclassified"
58
    val inv = InvariantGenerator.invariantAllEqual(Examples.parseExampleWF(name).get)
Christian Müller's avatar
Christian Müller committed
59
    assert(checkSafeCausalNoElim(name, "alleq", _ => inv))
60 61 62
  }
  it should "prove tests/simpleChoiceCausal alleq" in {
    val name = "tests/simpleChoiceCausal"
63
    val inv = InvariantGenerator.invariantNoninterSingleBS(Examples.parseExampleWF(name).get)
Christian Müller's avatar
Christian Müller committed
64
    assert(checkSafeStubborn(name, "alleq", _ => inv))
65 66 67
  }
  it should "prove tests/simpleChoiceCausal causal alleq" in {
    val name = "tests/simpleChoiceCausal"
68
    val inv = InvariantGenerator.invariantNoninterSingleBS(Examples.parseExampleWF(name).get)
Christian Müller's avatar
Christian Müller committed
69
    assert(!checkSafeCausalNoElim(name, "alleq", _ => inv))
70 71
  }
}