InvariantTest.scala 3.71 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
package de.tum.workflows.tests
Christian Müller's avatar
Christian Müller committed
2 3 4 5 6 7 8 9 10 11 12 13

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
Christian Müller's avatar
Christian Müller committed
14
import de.tum.workflows.toz3.InvariantGenerator
Christian Müller's avatar
Christian Müller committed
15 16 17

class InvariantTest extends FlatSpec {

Christian Müller's avatar
Christian Müller committed
18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37
//  "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
38
  
39 40 41 42
  "InvariantChecker" should "prove simple things safe" in {

    val spec = ExampleWorkflows.parseExample("tests/simpleChoiceNoOracle").get

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

Christian Müller's avatar
Christian Müller committed
45
    val (safe, msg, time) = InvariantChecker.checkInvariantFPDot(spec, inv)
46 47 48

    safe should be(true)
  }
Eugen Zalinescu's avatar
Eugen Zalinescu committed
49 50 51 52 53 54 55
//
//  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"))))
//
56
//    val (safe, msg) = InvariantChecker.checkInvariantFP(wf, inv, true)
Eugen Zalinescu's avatar
Eugen Zalinescu committed
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 89 90
//
//    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)
//  }
//  
//
Eugen Zalinescu's avatar
Eugen Zalinescu committed
91 92 93
  def genEq(name:String, params: List[Var]) = {
    val o1 = Fun(name, Some("t1"), params)
    val o2 = Fun(name, Some("t2"), params)
Christian Müller's avatar
Christian Müller committed
94
    Equiv(o1, o2)
Eugen Zalinescu's avatar
Eugen Zalinescu committed
95
  }
Eugen Zalinescu's avatar
Eugen Zalinescu committed
96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113
//  
//  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
114

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