InvariantTest.scala 3.56 KB
Newer Older
1
package de.tum.niwo.tests
Christian Müller's avatar
Christian Müller committed
2 3 4 5

import org.scalatest.FlatSpec
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
11
import de.tum.niwo.invariants.{InvProperties, InvariantChecker, InvariantGenerator, Preconditions}
Christian Müller's avatar
Christian Müller committed
12 13 14

class InvariantTest extends FlatSpec {

Christian Müller's avatar
Christian Müller committed
15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
//  "InvariantChecker" should "prove simple things safe" in {
//
//    val spec = ExampleWorkflows.parseExample("nonomitting/conference").get
//
////    val inv = Forall(List("a", "b"), Eq(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
//
//    val inv = InvariantGenerator.invariantNoninterStubbornBS(spec)
//    
//    val added = Or(Neg(Fun("Assign", List(Var("x","A"), Var("p","P")))),
//          Neg(Fun("Conf", List(Var("x","A"), Var("p","P")))))
//    
//    val both = Forall(List(Var("x","A"), Var("p","P")), And(added.in("t1"), added.in("t2")))
//    
//    val newinv = And(inv, both)
//    
//    val (safe, msg) = InvariantChecker.checkInvariantOnce(spec.w, newinv, true)
//
//    println(msg.toString())
//    safe should be(true)
//  }
Eugen Zalinescu's avatar
Eugen Zalinescu committed
35
  
36 37
  "InvariantChecker" should "prove simple things safe" in {

38
    val spec = Examples.parseExampleWF("tests/simpleChoiceNoOracle").get
39

Christian Müller's avatar
Christian Müller committed
40
    val inv = Forall(List("a", "b"), Equiv(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
41

Christian Müller's avatar
Christian Müller committed
42 43
    val invspec = TSConverter.toInvariantSpec(spec, InvProperties.DEFAULT, _ => inv)
    val (safe, msg, time) = InvariantChecker.checkInvariantFPDot(invspec)
44 45 46

    safe should be(true)
  }
Eugen Zalinescu's avatar
Eugen Zalinescu committed
47 48 49 50 51 52 53
//
//  it should "fail to prove unsafe workflows safe" in {
//    
//    val wf = ExampleWorkflows.parseExample("tests/simpleChoice").get.w
//
//    val inv = Forall(List("a", "b"), Eq(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
//
54
//    val (safe, msg) = InvariantChecker.checkInvariantFP(wf, inv, true)
Eugen Zalinescu's avatar
Eugen Zalinescu committed
55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
//
//    safe should be(false)
//  }
//
//  it should "prove the paper example" in {
//    val wf = ExampleWorkflows.parseExample("omitting/conference").get.w
//
//    val x = Var("x", "A")
//    val y = Var("y", "A")
//    val p = Var("p","P")
//    val r = Var("r","R")
//    val c = Fun("Conf", Some("t1"), List(x,p))
//
////    
//    val ceq = genEq("Conf", List(x,p))
//    val oeq = genEq("O", List(x,p,r))
//    val readeq = genEq("Read", List(x,p,r)) 
//    val assigneq = genEq("Assign", List(x,p))
//    val revieweq = genEq("Review", List(x,p,r))
////    val premise = And(Neg(c), oeq)
////    val conclusion = And.make(ceq, readeq, assigneq, Forall(y, revieweq))
//    
//    val premise = Forall(List(p,r), And(Neg(c), oeq))
//    val conclusion = Forall(List(p,r), And.make(ceq, readeq, assigneq, revieweq))
//    
//    val inv = Forall(List(x), 
//        Implies(premise, conclusion)
//    )
//    val (safe, msg) = InvariantChecker.checkInvariant(wf, inv, true)
//    
//    safe should be (true)
//  }
//  
//
Christian Müller's avatar
Christian Müller committed
89
//
Eugen Zalinescu's avatar
Eugen Zalinescu committed
90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106
//  it should "prove noninter invariants" in {
//    val spec = ExampleWorkflows.parseExample("tests/simpleChoice").get
//
//    val inv = InvariantChecker.invariantNoninterStubborn(spec)
//    val (safe, msg) = InvariantChecker.checkInvariant(spec.w, inv, true)
//
//    safe should be(false)
//  }
//
//  it should "prove the paper example as noninter invariant" in {
//    val spec = ExampleWorkflows.parseExample("omitting/conference").get
//
//    val inv = InvariantChecker.invariantNoninterStubborn(spec)
//    val (safe, msg) = InvariantChecker.checkInvariant(spec.w, inv,true)
//
//    safe should be(true)
//  }
Christian Müller's avatar
Christian Müller committed
107

Christian Müller's avatar
Christian Müller committed
108
}