DemoNoStrengtheningTests.scala 3.42 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 11 12 13 14 15 16 17
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
import de.tum.niwo.ExampleWorkflows
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 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
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)
75
    assert(checkSafeCausalNoElim(name, "alleq", inv))
76 77 78 79 80 81 82 83 84
  }
  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)
85
    assert(!checkSafeCausalNoElim(name, "alleq", inv))
86 87
  }
}