ElimTests.scala 833 Bytes
Newer Older
1 2 3 4 5 6 7 8 9
package de.tum.niwo.tests.papertests

import org.scalatest.{FlatSpec, Ignore}
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
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.{InvariantChecker, InvariantGenerator, Preconditions}
15 16 17 18 19 20 21 22
import de.tum.niwo.tests.TestUtils._

@Ignore
class ElimTests extends FlatSpec {

  // HEAP SPACE
  it should "prove nonomitting/conference_linear_fixed elim" in {
    val name = "omitting/conference_linear_fixed"
Christian Müller's avatar
Christian Müller committed
23
    val inv = InvariantGenerator.invariantNoninterSingleBS _
24 25 26
    assert(checkSafeCausalElim(name, "elim", inv))
  }
}