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

Christian Müller's avatar
Christian Müller committed
3
import org.scalatest.{FlatSpec, Ignore}
4 5
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
6 7 8 9 10
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.Implicits._
import de.tum.niwo.blocks._
import de.tum.niwo.Preconditions
import de.tum.niwo.foltl.FormulaFunctions
11
import de.tum.niwo.Examples
12 13 14 15 16 17
import de.tum.niwo.toz3.InvariantChecker
import de.tum.niwo.Encoding._
import de.tum.niwo.Utils
import de.tum.niwo.Encoding
import de.tum.niwo.tests.TestUtils._
import de.tum.niwo.toz3.InvariantGenerator
18

Christian Müller's avatar
Christian Müller committed
19
@Ignore
20 21 22 23 24
class DemoNoStrengtheningTests extends FlatSpec {

  // fixed arity, nonomitting - easy
  it should "fail to prove nonomitting/fixedarity10 alleq" in {
    val name = "nonomitting/fixedarity10"
25
    val inv = InvariantGenerator.invariantAllEqual(Examples.parseExampleWF(name).get)
26 27 28 29
    assert(!checkSafeStubborn(name, "alleq", inv))
  }
  it should "prove nonomitting/fixedarity10_safe alleq" in {
    val name = "nonomitting/fixedarity10safe"
30
    val inv = InvariantGenerator.invariantAllEqual(Examples.parseExampleWF(name).get)
31 32 33 34
    assert(checkSafeStubborn(name, "alleq", inv))
  }
  it should "fail to prove nonomitting/fixedarity15 alleq" in {
    val name = "nonomitting/fixedarity15"
35
    val inv = InvariantGenerator.invariantAllEqual(Examples.parseExampleWF(name).get)
36 37 38 39
    assert(!checkSafeStubborn(name, "alleq", inv))
  }
  it should "prove nonomitting/fixedarity15_safe alleq" in {
    val name = "nonomitting/fixedarity15safe"
40
    val inv = InvariantGenerator.invariantAllEqual(Examples.parseExampleWF(name).get)
41 42 43 44
    assert(checkSafeStubborn(name, "alleq", inv))
  }
  it should "fail to prove nonomitting/fixedarity20 alleq" in {
    val name = "nonomitting/fixedarity20"
45
    val inv = InvariantGenerator.invariantAllEqual(Examples.parseExampleWF(name).get)
46 47 48 49
    assert(!checkSafeStubborn(name, "alleq", inv))
  }
  it should "prove nonomitting/fixedarity20_safe alleq" in {
    val name = "nonomitting/fixedarity20safe"
50
    val inv = InvariantGenerator.invariantAllEqual(Examples.parseExampleWF(name).get)
51 52 53 54 55 56
    assert(checkSafeStubborn(name, "alleq", inv))
  }

  // nonomitting, incarity
  it should "prove nonomitting/incarity5 alleq" in {
    val name = "nonomitting/incarity5"
57
    val inv = InvariantGenerator.invariantAllEqual(Examples.parseExampleWF(name).get)
58 59 60 61 62 63 64 65 66 67 68
    assert(checkSafeStubborn(name, "alleq", inv))
  }





  // nonomitting, tests

  it should "prove tests/simpleChoiceDeclassified alleq" in {
    val name = "tests/simpleChoiceDeclassified"
69
    val inv = InvariantGenerator.invariantAllEqual(Examples.parseExampleWF(name).get)
70 71 72 73
    assert(checkSafeStubborn(name, "alleq", inv))
  }
  it should "prove tests/simpleChoiceDeclassified causal alleq" in {
    val name = "tests/simpleChoiceDeclassified"
74
    val inv = InvariantGenerator.invariantAllEqual(Examples.parseExampleWF(name).get)
75
    assert(checkSafeCausalNoElim(name, "alleq", inv))
76 77 78
  }
  it should "prove tests/simpleChoiceCausal alleq" in {
    val name = "tests/simpleChoiceCausal"
79
    val inv = InvariantGenerator.invariantNoninterSingleBS(Examples.parseExampleWF(name).get)
80 81 82 83
    assert(checkSafeStubborn(name, "alleq", inv))
  }
  it should "prove tests/simpleChoiceCausal causal alleq" in {
    val name = "tests/simpleChoiceCausal"
84
    val inv = InvariantGenerator.invariantNoninterSingleBS(Examples.parseExampleWF(name).get)
85
    assert(!checkSafeCausalNoElim(name, "alleq", inv))
86 87
  }
}