InvariantCausalFilesTest.scala 3.49 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
package de.tum.workflows.ltl.tests

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
import de.tum.workflows.Encoding._
import de.tum.workflows.Utils
import de.tum.workflows.Encoding

import de.tum.workflows.tests.TestUtils._
Christian Müller's avatar
Christian Müller committed
19
import de.tum.workflows.foltl.Properties
Christian Müller's avatar
Christian Müller committed
20 21 22 23 24 25 26 27 28 29 30 31 32 33 34

class InvariantCausalFilesTest extends FlatSpec {
  
  "InvariantChecker" should "prove simple causal may things safe" in {
    val name = "tests/simpleChoiceOmittingNoOracle"
    val inv = Forall(List("xt"), genEq("R", List("xt", "st")))
    assert(checkSafeCausal(name, inv))
  }
  
  it should "fail to prove simple causal may things" in {
    val name = "tests/simpleChoiceCausal"
    val inv = Forall(List("xt"), genEq("S", List("xt")))
    assert(!checkSafeCausal(name, inv))
  }
  
Christian Müller's avatar
Christian Müller committed
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
  it should "fail to prove conference_linear_small" in {
    val name = "tests/conference_linear_small"
    val xt = Var("xt","X")
    val yt = Var("yt","X")
    val pt = Var("pt","P")
    val inv = Forall(List(xt, pt, yt), genEq("Comm", List(xt, yt, pt)))
    assert(!checkSafeCausal(name, inv))
  }
  
//  it should "fail to prove conference_linear_small with informedness inv" in {
//    val name = "tests/conference_linear_small"
//    val xt = Var("xt","X")
//    val inv = Forall(List(xt), Neg(Fun(Properties.INFNAME, Some("t1"), List(xt))))
//    assert(!checkSafeCausal(name, inv))
//  }
  
  it should "prove conference_linear_small with trivial inv 1" in {
    val name = "tests/conference_linear_small"
    val xt = Var("xt","X")
    val pt = Var("pt","P")
    val rt = Var("rt", "R")
    val inv = Forall(List(xt, pt), genEq("Conf", List(xt,pt)))
    assert(checkSafeCausal(name, inv))
  }
  
  it should "prove conference_linear_small with trivial inv 2" in {
    val name = "tests/conference_linear_small"
    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, yt, pt, rt), genEq("Read", List(yt,pt,rt)))
    assert(!checkSafeCausal(name, inv))
  }
    
  it should "fail to prove conference_linear" in {
Christian Müller's avatar
Christian Müller committed
71 72 73 74 75 76 77
    val name = "nonomitting/conference_linear"
    val xt = Var("xt","X")
    val yt = Var("yt","X")
    val pt = Var("pt","P")
    val inv = Forall(List(xt, pt, yt), genEq("Comm", List(xt, yt, pt)))
    assert(!checkSafeCausal(name, inv))
  }
Christian Müller's avatar
Christian Müller committed
78
  
Christian Müller's avatar
Christian Müller committed
79 80 81 82 83 84 85 86 87
  it should "fail to prove conference_linear with elim" in {
    val name = "nonomitting/conference_linear"
    val xt = Var("xt","X")
    val yt = Var("yt","X")
    val pt = Var("pt","P")
    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
88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105
  it should "fail to prove nonomitting/conference" in {
    val name = "nonomitting/conference"
    val xt = Var("xat","X")
    val yt = Var("xbt","X")
    val pt = Var("pt","P")
    val rt = Var("rt","R")
    val inv = Forall(List(xt, pt, yt, rt), genEq("Read", List(xt, yt, pt, rt)))
    assert(!checkSafeCausal(name, inv))
  }
  
  it should "fail to prove omitting/conference" in {
    val name = "omitting/conference"
    val xt = Var("xat","X")
    val pt = Var("pt","P")
    val rt = Var("rt","R")
    val inv = Forall(List(xt, pt), genEq("Read", List(xt, pt, rt)))
    assert(!checkSafeCausal(name, inv))
  }
Christian Müller's avatar
Christian Müller committed
106 107
    
}