ParserTest.scala 6.18 KB
Newer Older
1
package de.tum.niwo.tests
2 3 4 5

import org.scalatest._
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
6 7 8 9
import de.tum.niwo.blocks._
import de.tum.niwo.blocks
import de.tum.niwo.Implicits._
import de.tum.niwo.foltl.FOLTL._
10
import com.typesafe.scalalogging.LazyLogging
11
import de.tum.niwo.parser.WorkflowParser
12

13
class ParserTest extends FlatSpec {
Christian Müller's avatar
Christian Müller committed
14

15
  val oxrxssig = Signature(Set(Fun("O", List("x","s"))), Set(), Set(), Set(Fun("R", List("x", "s"))), Set())
16 17 18 19 20 21 22 23 24

  def testResult(s: String, sig: Signature) {
    testResult(s, Workflow(sig, List()))
  }

  def testResult(s: String, wf: Workflow) {
    val parsed = WorkflowParser.parseWorkflow(s)

    if (!parsed.successful) {
25
      info(s"Parsing unsuccessful: $parsed")
26 27 28 29 30 31
    }

    parsed.successful should be(true)
    val pwf = parsed.get

    pwf.sig should be(wf.sig)
Christian Müller's avatar
Christian Müller committed
32
    if (wf.steps.nonEmpty) {
33 34
      pwf.steps should be(wf.steps)
    }
35
  }
36

Christian Müller's avatar
Christian Müller committed
37
  def testSpecResult(s: String, spec: blocks.NISpec) {
38 39 40
    val parsed = WorkflowParser.parseSpec(s)

    if (!parsed.successful) {
41
      info(s"Parsing unsuccessful: $parsed")
42 43 44
    }

    parsed.successful should be(true)
Christian Müller's avatar
Christian Müller committed
45
    val pwf = parsed.get.w
46

Christian Müller's avatar
Christian Müller committed
47
    pwf.sig should be(spec.w.sig)
Christian Müller's avatar
Christian Müller committed
48
    if (spec.w.steps.nonEmpty) {
Christian Müller's avatar
Christian Müller committed
49
      pwf.steps should be(spec.w.steps)
50 51
    }

Christian Müller's avatar
Christian Müller committed
52 53
    parsed.get.declass should be(spec.declass)
    parsed.get.target should be(spec.target)
54 55 56
  }

  "Workflow Parser" should "parse a single may block" in {
Christian Müller's avatar
Christian Müller committed
57
    val s = "forallmay x,s O(x,s) → R += (x,s)"
Christian Müller's avatar
Christian Müller committed
58

59
    testResult(s, Workflow(oxrxssig, List(ForallMayWFBlock(List("x", "s"), "choice0", List(Add(Fun("O", List("x","s")), "R", List("x", "s")))))))
60 61
  }

62
  it should "parse a block with 2 stmts" in {
63 64
    val s = """
      forallmay x,s 
Christian Müller's avatar
Christian Müller committed
65 66
        O(x,s) → R += (x,s)
        (True ∧ O(x,s)) → R -= (s,x)
67
    """
Christian Müller's avatar
Christian Müller committed
68
    testResult(s, oxrxssig)
69 70
  }

Christian Müller's avatar
Christian Müller committed
71 72 73 74 75 76 77 78 79 80 81 82
//  it should "parse a loop block with 2 stmts" in {
//    val s = """
//      loop {
//        forallmay x,s 
//          O(x,s) → R += (x,s)
//          (True ∧ O(x,s)) → R -= (s,x)
//        forall x
//          O(x,s) → R += (x,x)
//      }
//    """
//    testResult(s, oxrxssig)
//  }
83

84
  it should "parse prevexample" in {
85 86 87 88 89 90 91 92 93
    val s = """
        forallmay x,s O(s) -> Q += (x,s)
        loop {
	        forall x,y,s R(y,s) -> S += (x,y,s)
	        forall x,s Q(x,s) -> R += (x,s)
        }
      """
    val w = Workflow(
      Signature(
Christian Müller's avatar
Christian Müller committed
94
        Set(Fun("O", List("s"))),
Christian Müller's avatar
ineq  
Christian Müller committed
95
        Set(),
Christian Müller's avatar
Christian Müller committed
96
        Set(),
Christian Müller's avatar
Christian Müller committed
97
        Set(
98 99
          Fun("S", List("x", "y", "s")),
          Fun("R", List("y", "s")),
100 101
          Fun("Q", List("x", "s"))),
        Set()),
102
      List(
103
        ForallMayWFBlock(List("x", "s"), "choice0",
104
          Add(Fun("O", "s"), "Q", List("x", "s"))),
105 106
        WFLoop(List(
          ForallWFBlock(List("x", "y", "s"),
107
            Add(Fun("R", List("y", "s")), "S", List("x", "y", "s"))),
108
          ForallWFBlock(List("x", "s"),
109
            Add(Fun("Q", List("x", "s")), "R", List("x", "s")))))))
110 111

    testResult(s, w)
112
  }
113 114

  it should "parse simplechoice" in {
115 116
    val s = """
      forallmay x,s
Christian Müller's avatar
Christian Müller committed
117
	      O(x,s) -> R += (x,s)
118 119
      """
    val w = Workflow(
Christian Müller's avatar
Christian Müller committed
120
      oxrxssig,
121
      List(
122
        ForallMayWFBlock(List("x", "s"), "choice0",
Christian Müller's avatar
Christian Müller committed
123
          Add(Fun("O", List("x","s")), "R", List("x", "s")))))
124

125 126
    testResult(s, w)
  }
127 128

  it should "parse simpleNochoice" in {
129 130
    val s = """
      forallmay x,s
Christian Müller's avatar
Christian Müller committed
131
	      O(x,s) -> R += (x,s)
132 133
      """
    val w = Workflow(
Christian Müller's avatar
Christian Müller committed
134
      oxrxssig,
135
      List(
136
        ForallMayWFBlock(List("x", "s"), "choice0",
Christian Müller's avatar
Christian Müller committed
137
          Add(Fun("O", List("x","s")), "R", List("x", "s")))))
138

139 140
    testResult(s, w)
  }
Christian Müller's avatar
Christian Müller committed
141

142 143 144 145 146 147 148
  it should "fail on conflicting arities" in {
    val s = """
      forallmay x,s
        O(x) -> R += (x,s)
      forall x,y,s
        O(s) -> R += (x,y,s)  
    """
Christian Müller's avatar
Christian Müller committed
149
    WorkflowParser.parseWorkflow(s).successful should be(false)
150
  }
Christian Müller's avatar
Christian Müller committed
151

152 153 154 155 156
  it should "parse typed variables" in {
    val st = """
      forallmay x:Agent,s:Paper
	      O(x) -> R += (x,s)
    """
Christian Müller's avatar
Christian Müller committed
157 158 159
    val x = Var("x", "Agent")
    val s = Var("s", "Paper")

160
    val typedsig = Signature(Set(Fun("O", List(x))), Set(), Set(), Set(Fun("R", List(x, s))), Set())
Christian Müller's avatar
Christian Müller committed
161

162 163 164
    val w = Workflow(
      typedsig,
      List(
165
        ForallMayWFBlock(List(x, s), "choice0",
Christian Müller's avatar
Christian Müller committed
166 167
          Add(Fun("O", x), "R", List(x, s)))))

168 169
    testResult(st, w)
  }
170

171 172 173 174 175 176 177 178 179
  "Spec Parser" should "parse simpleNochoice" in {
    val s = """
      Workflow
      
      forallmay x,s
	      O(s) -> R += (x,s)
	      
	    Target
	    
Christian Müller's avatar
Christian Müller committed
180
	    R(x,s)
181 182 183
      """
    val w = Workflow(
      Signature(
Christian Müller's avatar
Christian Müller committed
184
        Set(Fun("O", List("s"))),
Christian Müller's avatar
ineq  
Christian Müller committed
185
        Set(),
Christian Müller's avatar
Christian Müller committed
186
        Set(),
187 188
        Set(Fun("R", List("x", "s"))),
        Set()),
189
      List(
190
        ForallMayWFBlock(List("x", "s"), "choice0",
191 192
          Add(Fun("O", "s"), "R", List("x", "s")))))

Christian Müller's avatar
Christian Müller committed
193 194
    val t = Fun("R", List("x", "s"))

Christian Müller's avatar
Christian Müller committed
195
    testSpecResult(s, NISpec(w, Map(), True, t, List()))
Christian Müller's avatar
Christian Müller committed
196
  }
Christian Müller's avatar
Christian Müller committed
197

Christian Müller's avatar
Christian Müller committed
198 199 200 201
  it should "parse simpleNochoice with declassification" in {
    val s = """
      Workflow
      
Christian Müller's avatar
Christian Müller committed
202 203
      forall x,s
	      O(x,s) -> R += (x,s)
Christian Müller's avatar
Christian Müller committed
204 205 206
	      
	    Declassify
	    
Christian Müller's avatar
Christian Müller committed
207
	    O(x,s): True
Christian Müller's avatar
Christian Müller committed
208 209 210 211 212 213 214 215
	      
	    Target
	    
	    R(x,s)
      """
    val w = Workflow(
      oxrxssig,
      List(
216
        ForallWFBlock(List("x", "s"),
Christian Müller's avatar
Christian Müller committed
217
          Add(Fun("O", List("x","s")), "R", List("x", "s")))))
Christian Müller's avatar
Christian Müller committed
218 219

    val t = Fun("R", List("x", "s"))
220

Christian Müller's avatar
Christian Müller committed
221 222 223 224
    val xt = Var("x","T")
    val st = Var("s","T")
    
    val map = Map("O" -> (List(xt,st), True))
Christian Müller's avatar
Christian Müller committed
225

Christian Müller's avatar
Christian Müller committed
226
    testSpecResult(s, NISpec(w, map, True, t, List()))
227
  }
Christian Müller's avatar
Christian Müller committed
228 229

  it should "parse encoded vars back to strings" in {
Christian Müller's avatar
Christian Müller committed
230
    val s = "R1#t1_a#T_b#T"
Christian Müller's avatar
Christian Müller committed
231 232 233 234

    val f = FunFromVar.unapply(s)
    f should be(Some(Fun("R1", Some("t1"), List("a", "b"))))

Christian Müller's avatar
Christian Müller committed
235
    val s2 = "R1_a#T_b#T"
Christian Müller's avatar
Christian Müller committed
236 237 238 239

    val f2 = FunFromVar.unapply(s2)
    f2 should be(Some(Fun("R1", None, List("a", "b"))))
  }
Christian Müller's avatar
Christian Müller committed
240 241 242 243 244 245

  it should "parse quantified stuff" in {

    val f1 = "∀x. ∃y. fun(x, y)"
    val r1 = Forall("x", Exists("y", Fun("fun",List("x","y"))))

246
    WorkflowParser.parseFormula(f1).get should be (r1)
Christian Müller's avatar
Christian Müller committed
247 248 249

    val f2 = "∀x ∃y (fun(x, y) ∨ ¬fun(y,x))"
    val r2 = Forall("x", Exists("y", Fun("fun",List("x","y")) \/ Neg(Fun("fun", List("y","x")))))
250
    val parsed = WorkflowParser.parseFormula(f2)
Christian Müller's avatar
Christian Müller committed
251 252 253 254 255

    parsed.get should be (r2)

    val f3 = "∃y. (fun(y) ⟹ fun(y))"
    val r3 = Exists("y", Fun("fun", "y") --> Fun("fun", "y"))
256
    WorkflowParser.parseFormula(f3).get should be (r3)
Christian Müller's avatar
Christian Müller committed
257
  }
258
}