EncodingTest.scala 3.39 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
package de.tum.workflows.tests
2 3 4 5 6 7

import org.scalatest._
import org.scalatest.Matchers._
import org.scalatest.Inspectors._

import de.tum.workflows.Implicits._
Christian Müller's avatar
Christian Müller committed
8
import de.tum.workflows.blocks.Workflow._
9 10 11 12
import de.tum.workflows.Encoding
import de.tum.workflows.foltl.Noninterference
import de.tum.workflows.foltl.Stubborn
import de.tum.workflows.foltl.FOLTL._
Christian Müller's avatar
Christian Müller committed
13
import de.tum.workflows.Utils._
14
import de.tum.workflows.foltl.Properties
Christian Müller's avatar
Christian Müller committed
15
import Properties._
Christian Müller's avatar
Christian Müller committed
16
import de.tum.workflows.foltl.FOTransformers
17
import de.tum.workflows.ExampleWorkflows
Christian Müller's avatar
Christian Müller committed
18 19
import de.tum.workflows.blocks._

20 21
class EncodingTest extends FlatSpec {

Christian Müller's avatar
Christian Müller committed
22
  val w = ExampleWorkflows.parseExample("tests/simpleChoice").get.w
23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39

  // shorthands
  val n0 = Fun("n0", List())
  val n1 = Fun("n1", List())
  val aux0xs = Fun("choice0", List("x", "s"))
  val Os = Fun("O", List("s"))
  val Rxs = Fun("R", List("x", "s"))

  "Workflow encoding" should "work" in {
    val g = Encoding.toGraph(w)
    val cfg = Encoding.encodeGraph(g)
    val sanity = Encoding.encodeSanity(g)
    val sem = Encoding.encodeSem(w.sig, g)
    val init = Encoding.encodeInitial(w.sig, g)

    cfg should be(
      Globally(
Christian Müller's avatar
Christian Müller committed
40
        And(Implies(n0, Next(n1)), Implies(n1, Next(n1)))))
41 42

    sanity should be(
43
      And.make(n0, Neg(n1), Globally(Neg(And(n0, n1)))))
44

Christian Müller's avatar
Christian Müller committed
45 46
    val rstays = Forall(List("x", "s"), Equiv(Next(Rxs), Rxs))
    val ostays = Forall(List("s"), Equiv(Next(Os), Os))
47

48 49 50 51 52 53 54 55 56
    //    if O stays
    //    sem should be(
    //      Globally(
    //        And(
    //          Implies(And(n0, Next(n1)), And(
    //            Forall(List("x", "s"), Eq(Next(Rxs), Or(Rxs, And(Os, aux0xs)))),
    //            ostays)),
    //          Implies(And(n1, Next(n1)), And(ostays, rstays)))))

57 58 59
    sem should be(
      Globally(
        And(
60
          Implies(And(n0, Next(n1)),
Christian Müller's avatar
Christian Müller committed
61
            Forall(List("x", "s"), Equiv(Next(Rxs), Or(Rxs, And(Os, aux0xs))))),
62
          Implies(And(n1, Next(n1)), rstays))))
63 64

    init should be(
65
      Forall(List("x", "s"), Neg(Rxs)))
66
  }
Christian Müller's avatar
Christian Müller committed
67

68
  "Stubbornness encoding" should "work" in {
69
    val choices = Set(Fun("choice0", List("x", "y")))
Christian Müller's avatar
Christian Müller committed
70

Christian Müller's avatar
Christian Müller committed
71
    val stubness = Stubborn("a1", choices)
72
    val auxa1 = Fun("choice0", List("a1", "y"))
Christian Müller's avatar
Christian Müller committed
73

74
    stubness should be (
Christian Müller's avatar
Christian Müller committed
75
      Globally(
Christian Müller's avatar
Christian Müller committed
76
        Forall(List("y"), Equiv(auxa1.in(T1), auxa1.in(T2)))))
77
  }
Christian Müller's avatar
Christian Müller committed
78

79
  "Noninterference encoding" should "work" in {
Christian Müller's avatar
Christian Müller committed
80
    
81
    val choices = Set(Fun("choice0", List("x", "y")))
Christian Müller's avatar
Christian Müller committed
82
    val Rab = Fun("R", List("a", "b"))
Christian Müller's avatar
Christian Müller committed
83
    
Christian Müller's avatar
Christian Müller committed
84
    val s = Spec(Workflow.EMPTY, Map(), Rab, List())
Christian Müller's avatar
Christian Müller committed
85

Christian Müller's avatar
Christian Müller committed
86
    val nonint = Noninterference(choices, s)
Christian Müller's avatar
Christian Müller committed
87

88
    val aux0ay = Fun("choice0", List("a", "y"))
Christian Müller's avatar
Christian Müller committed
89 90

    nonint should be(
91
      Exists(List("a"), And(
Christian Müller's avatar
Christian Müller committed
92 93
        Globally(Forall("y", Equiv(aux0ay.in("t1"), aux0ay.in("t2")))),
        Finally(Exists("b", Neg(Equiv(Rab.in("t1"), Rab.in("t2"))))))))
94
  }
95

Christian Müller's avatar
Christian Müller committed
96 97
  "Property encoding" should "work" in {
    val choices = allchoices(w)
98

99
    choices should be (Set(Fun("choice0", List("x", "s"))))
100
    val ce = Fun("R", List("ax", "as"))
Christian Müller's avatar
Christian Müller committed
101
    
Christian Müller's avatar
Christian Müller committed
102
    val s = Spec(Workflow.EMPTY, Map(), ce, List())
103

Christian Müller's avatar
Christian Müller committed
104
    val noninter = Noninterference(choices, s)
105 106
    noninter should be (
      Exists("ax", And(
Christian Müller's avatar
Christian Müller committed
107
        Stubborn("ax", choices),
Christian Müller's avatar
Christian Müller committed
108
        Finally(Exists("as", Neg(Equiv(ce.in(T1), ce.in(T2))))))))
109

Christian Müller's avatar
Christian Müller committed
110
    val s2 = Spec(w, Map(), Fun("R", List("ax", "as")), List())
Christian Müller's avatar
Christian Müller committed
111
    val prop = Properties.noninterStubborn(s2)
112

Christian Müller's avatar
Christian Müller committed
113
    val (agents, res) = FOTransformers.eliminateExistentials(prop)
Christian Müller's avatar
Christian Müller committed
114
    
115
    agents should be (List(Var("ax"), Var("as")))
Christian Müller's avatar
Christian Müller committed
116
  }
117
}