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

import org.scalatest._
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
Christian Müller's avatar
Christian Müller committed
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
Christian Müller's avatar
Christian Müller committed
11
import de.tum.niwo.parser.WorkflowParser
12

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

Christian Müller's avatar
Christian Müller committed
15
  val oxrxssig = Signature(Set(Fun("O", List("x","s")), Fun("choice0", List("x","s"))), Set(), Set(), Set(Fun("R", List("x", "s"))), Set())
Christian Müller's avatar
Christian Müller committed
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")
Christian Müller's avatar
Christian Müller committed
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) {
Christian Müller's avatar
Christian Müller committed
33
34
      pwf.steps should be(wf.steps)
    }
35
  }
Christian Müller's avatar
Christian Müller committed
36

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

    if (!parsed.successful) {
41
      info(s"Parsing unsuccessful: $parsed")
Christian Müller's avatar
Christian Müller committed
42
43
44
    }

    parsed.successful should be(true)
Christian Müller's avatar
Christian Müller committed
45
    val pwf = parsed.get.w
Christian Müller's avatar
Christian Müller committed
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)
Christian Müller's avatar
Christian Müller committed
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

Christian Müller's avatar
Christian Müller committed
59
    testResult(s, Workflow(oxrxssig, List(ForallMayWFBlock(List("x", "s"), "choice0", List(Add(Fun("O", List("x","s")), "R", List("x", "s")))))))
60
61
  }

Christian Müller's avatar
Christian Müller committed
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

Christian Müller's avatar
Christian Müller committed
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")), Fun("choice0", List("x","s"))),
Christian Müller's avatar
ineq    
Christian Müller committed
95
        Set(),
Christian Müller's avatar
leaders    
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")),
Christian Müller's avatar
Christian Müller committed
100
101
          Fun("Q", List("x", "s"))),
        Set()),
102
      List(
Christian Müller's avatar
Christian Müller committed
103
        ForallMayWFBlock(List("x", "s"), "choice0",
104
          Add(Fun("O", "s"), "Q", List("x", "s"))),
Christian Müller's avatar
Christian Müller committed
105
106
        WFLoop(List(
          ForallWFBlock(List("x", "y", "s"),
107
            Add(Fun("R", List("y", "s")), "S", List("x", "y", "s"))),
Christian Müller's avatar
Christian Müller committed
108
          ForallWFBlock(List("x", "s"),
109
            Add(Fun("Q", List("x", "s")), "R", List("x", "s")))))))
Christian Müller's avatar
Christian Müller committed
110
111

    testResult(s, w)
112
  }
Christian Müller's avatar
Christian Müller committed
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,
Christian Müller's avatar
Christian Müller committed
121
      List(
Christian Müller's avatar
Christian Müller committed
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")))))
Christian Müller's avatar
Christian Müller committed
124

125
126
    testResult(s, w)
  }
Christian Müller's avatar
Christian Müller committed
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,
Christian Müller's avatar
Christian Müller committed
135
      List(
Christian Müller's avatar
Christian Müller committed
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")))))
Christian Müller's avatar
Christian Müller committed
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")

Christian Müller's avatar
Christian Müller committed
160
    val typedsig = Signature(Set(Fun("O", List(x)), Fun("choice0", 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(
Christian Müller's avatar
Christian Müller committed
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

Christian Müller's avatar
Christian Müller committed
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)
Christian Müller's avatar
Christian Müller committed
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
leaders    
Christian Müller committed
186
        Set(),
Christian Müller's avatar
Christian Müller committed
187
188
        Set(Fun("R", List("x", "s"))),
        Set()),
Christian Müller's avatar
Christian Müller committed
189
      List(
Christian Müller's avatar
Christian Müller committed
190
        ForallMayWFBlock(List("x", "s"), "choice0",
Christian Müller's avatar
Christian Müller committed
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
leaders    
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(
Christian Müller's avatar
Christian Müller committed
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"))
Christian Müller's avatar
Christian Müller committed
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
leaders    
Christian Müller committed
226
    testSpecResult(s, NISpec(w, map, True, t, List()))
Christian Müller's avatar
Christian Müller committed
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"))))

Christian Müller's avatar
Christian Müller committed
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")))))
Christian Müller's avatar
Christian Müller committed
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"))
Christian Müller's avatar
Christian Müller committed
256
    WorkflowParser.parseFormula(f3).get should be (r3)
Christian Müller's avatar
Christian Müller committed
257
  }
258
}