DemoUniversityTest.scala 1.05 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
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.Implicits._
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FormulaFunctions
10
import de.tum.niwo.Examples
Christian Müller's avatar
Christian Müller committed
11
import de.tum.niwo.graphs.WFGraphEncoding._
12
import de.tum.niwo.Utils
Christian Müller's avatar
Christian Müller committed
13
import de.tum.niwo.graphs.WFGraphEncoding
14
import de.tum.niwo.invariants.{InvProperties, InvariantChecker, InvariantGenerator, Preconditions}
15
import de.tum.niwo.tests.TestUtils._
16 17 18

class DemoUniversityTest extends FlatSpec {

19
  "Inference" should "prove nonomitting/university alleq" in {
20
    val name = "nonomitting/university"
Christian Müller's avatar
Christian Müller committed
21
    val inv = InvariantGenerator.invariantAllEqual _
22
    assert(checkSafeStubborn(name, inv))
23 24
  }

25
  it should "prove nonomitting/university causal" in {
26
    val name = "nonomitting/university"
Christian Müller's avatar
Christian Müller committed
27
    val inv = InvariantGenerator.invariantNoninterSingleBS _
28 29 30 31
    assert(!checkSafe(name, "", inv, InvProperties(
      stubborn = false,
      approxElim = true
    )))
32 33 34
  }

}