Commit a43fd80b authored by Christian Müller's avatar Christian Müller

Merge branch 'master' of versioncontrolseidl.in.tum.de:mueller/loopingworkflows

parents 53138bc3 1c832a5d
......@@ -59,7 +59,7 @@ object LTL extends LazyLogging {
def eliminateUniversals(t: Formula, agents: List[Var]):Formula = {
if (agents.isEmpty) {
logger.error("Agent list should never be empty")
logger.warn("Agent list empty")
}
val universe = agents.groupBy(_.typ)
......
......@@ -16,78 +16,99 @@ class InvariantTest extends FlatSpec {
"InvariantChecker" should "prove simple things safe" in {
val wf = ExampleWorkflows.parseExample("tests/simpleChoiceNoOracle").get.w
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 = Forall(List("a", "b"), Eq(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
val (safe, msg) = InvariantChecker.checkInvariant(wf, inv, true)
safe should be(true)
}
it should "fail to prove unsafe workflows safe" in {
val inv = InvariantChecker.invariantNoninterStubbornBS(spec)
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"))))
val (safe, msg) = InvariantChecker.checkInvariant(wf, inv, true)
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 added = Or(Neg(Fun("Assign", List(Var("x","A"), Var("p","P")))),
Neg(Fun("Conf", List(Var("x","A"), Var("p","P")))))
val premise = Forall(List(p,r), And(Neg(c), oeq))
val conclusion = Forall(List(p,r), And.make(ceq, readeq, assigneq, revieweq))
val both = Forall(List(Var("x","A"), Var("p","P")), And(added.in("t1"), added.in("t2")))
val inv = Forall(List(x),
Implies(premise, conclusion)
)
val (safe, msg) = InvariantChecker.checkInvariant(wf, inv, true)
val newinv = And(inv, both)
safe should be (true)
val (safe, msg) = InvariantChecker.checkInvariant(spec.w, newinv, true)
println(msg.toString())
safe should be(true)
}
// "InvariantChecker" should "prove simple things safe" in {
//
// val wf = ExampleWorkflows.parseExample("tests/simpleChoiceNoOracle").get.w
//
// val inv = Forall(List("a", "b"), Eq(Fun("R", Some("t1"), List("a", "b")), Fun("R", Some("t2"), List("a", "b"))))
//
// val (safe, msg) = InvariantChecker.checkInvariant(wf, inv, true)
//
// safe should be(true)
// }
//
// 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"))))
//
// val (safe, msg) = InvariantChecker.checkInvariant(wf, inv, true)
//
// 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)
// }
//
//
def genEq(name:String, params: List[Var]) = {
val o1 = Fun(name, Some("t1"), params)
val o2 = Fun(name, Some("t2"), params)
Eq(o1, o2)
}
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)
}
//
// 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)
// }
}
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment