InferenceTests.scala 2.02 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
package de.tum.workflows.tests

import org.scalatest.FlatSpec
import org.scalatest.FlatSpec
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.Implicits._
import de.tum.workflows.blocks._
import de.tum.workflows.Preconditions
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.ExampleWorkflows
import de.tum.workflows.toz3.{InvariantChecker, InvariantGenerator}
import de.tum.workflows.Encoding._
import de.tum.workflows.Utils
import de.tum.workflows.Encoding
import de.tum.workflows.tests.TestUtils._
import de.tum.workflows.foltl.Properties


class InferenceTests  extends FlatSpec {

  "Invariant Inference" should "prove safe stuff safe" in {
    val name = "tests/conference_linear_small_withB"
    val xt = Var("xt","X")
    val yt = Var("yt","X")
    val pt = Var("pt","P")
//    val rt = Var("rt","R")
Christian Müller's avatar
Christian Müller committed
29
    val inv = Forall(List(xt, pt, yt), genEq("Comm", List(xt, yt, pt)))
30 31 32
    assert(checkSafeStubborn(name, inv))
  }

33 34 35 36 37 38 39 40 41 42
  it should "prove safe causal stuff safe" in {
    val name = "tests/conference_linear_small_withB"
    val xt = Var("xt","X")
    val yt = Var("yt","X")
    val pt = Var("pt","P")
    //    val rt = Var("rt","R")
    val inv = Forall(List(xt, pt, yt), genEq("Comm", List(xt, yt, pt)))
    assert(checkSafeCausalElim(name, "", inv))
  }

Christian Müller's avatar
Christian Müller committed
43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
  it should "prove safe loopy stubborn stuff safe" in {
    val name = "tests/conference_stubborn_withB"
    val xat = Var("xat","A")
    val xbt = Var("xbt","A")
    val pt = Var("pt","P")
    //    val rt = Var("rt","R")
    val inv = Forall(List(xat, xbt, pt), genEq("Read", List(xat, xbt, pt)))
    assert(checkSafeStubborn(name, "", inv))
  }

  ignore should "prove safe loopy causal stuff safe" in {
    val name = "tests/conference_stubborn_withB"
    val xat = Var("xat","A")
    val xbt = Var("xbt","A")
    val pt = Var("pt","P")
    //    val rt = Var("rt","R")
    val inv = Forall(List(xat, xbt, pt), genEq("Read", List(xat, xbt, pt)))
    assert(checkSafeCausalElim(name, "", inv))
  }
62
}