ParserTest.scala 5.32 KB
Newer Older
1
2
3
4
5
6
7
8
package de.tum.workflows.ltl.tests

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

import de.tum.workflows.WorkflowParser
import de.tum.workflows.blocks._
Christian Müller's avatar
Christian Müller committed
9
import de.tum.workflows.blocks
10
11
12
13
import de.tum.workflows.Implicits._
import de.tum.workflows.foltl.FOLTL._
import com.typesafe.scalalogging.LazyLogging

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

Christian Müller's avatar
Christian Müller committed
16
  val oxrxssig = Signature(Set(Fun("O", List("x"))), Set(Fun("R", List("x", "s"))))
Christian Müller's avatar
Christian Müller committed
17
18
19
20
21
22
23
24
25

  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) {
26
      info(s"Parsing unsuccessful: $parsed")
Christian Müller's avatar
Christian Müller committed
27
28
29
30
31
32
33
34
35
    }

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

    pwf.sig should be(wf.sig)
    if (!wf.steps.isEmpty) {
      pwf.steps should be(wf.steps)
    }
36
  }
Christian Müller's avatar
Christian Müller committed
37

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

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

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

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

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

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

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

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

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

Christian Müller's avatar
Christian Müller committed
85
  it should "parse prevexample" in {
86
87
88
89
90
91
92
93
94
    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
95
96
        Set(Fun("O", List("s"))),
        Set(
97
98
99
100
101
102
103
104
105
106
107
          Fun("S", List("x", "y", "s")),
          Fun("R", List("y", "s")),
          Fun("Q", List("x", "s")))),
      List(
        ForallMayBlock(List("x", "s"), "choice0",
          Add(Fun("O", "s"), "Q", List("x", "s"))),
        Loop(List(
          ForallBlock(List("x", "y", "s"),
            Add(Fun("R", List("y", "s")), "S", List("x", "y", "s"))),
          ForallBlock(List("x", "s"),
            Add(Fun("Q", List("x", "s")), "R", List("x", "s")))))))
Christian Müller's avatar
Christian Müller committed
108
109

    testResult(s, w)
110
  }
Christian Müller's avatar
Christian Müller committed
111
112

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

123
124
    testResult(s, w)
  }
Christian Müller's avatar
Christian Müller committed
125
126

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

137
138
    testResult(s, w)
  }
Christian Müller's avatar
Christian Müller committed
139

140
141
142
143
144
145
146
  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
147
    WorkflowParser.parseWorkflow(s).successful should be(false)
148
  }
Christian Müller's avatar
Christian Müller committed
149

150
151
152
153
154
  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
155
156
157
    val x = Var("x", "Agent")
    val s = Var("s", "Paper")

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

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

166
167
    testResult(st, w)
  }
168

Christian Müller's avatar
Christian Müller committed
169
170
171
172
173
174
175
176
177
  "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
178
	    R(x,s)
Christian Müller's avatar
Christian Müller committed
179
180
181
      """
    val w = Workflow(
      Signature(
Christian Müller's avatar
Christian Müller committed
182
183
        Set(Fun("O", List("s"))),
        Set(Fun("R", List("x", "s")))),
Christian Müller's avatar
Christian Müller committed
184
185
186
187
      List(
        ForallMayBlock(List("x", "s"), "choice0",
          Add(Fun("O", "s"), "R", List("x", "s")))))

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

Christian Müller's avatar
Christian Müller committed
190
    testSpecResult(s, Spec(w, List(), t, List()))
Christian Müller's avatar
Christian Müller committed
191
  }
Christian Müller's avatar
Christian Müller committed
192

Christian Müller's avatar
Christian Müller committed
193
194
195
196
197
198
199
200
201
  it should "parse simpleNochoice with declassification" in {
    val s = """
      Workflow
      
      forallmay x,s
	      O(x) -> R += (x,s)
	      
	    Declassify
	    
Christian Müller's avatar
Christian Müller committed
202
	    O(x): True
Christian Müller's avatar
Christian Müller committed
203
204
205
206
207
208
209
210
211
212
213
214
	      
	    Target
	    
	    R(x,s)
      """
    val w = Workflow(
      oxrxssig,
      List(
        ForallMayBlock(List("x", "s"), "choice0",
          Add(Fun("O", "x"), "R", List("x", "s")))))

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

Christian Müller's avatar
Christian Müller committed
216
    testSpecResult(s, Spec(w, List((Fun("O", List("x")), True)), t, List()))
Christian Müller's avatar
Christian Müller committed
217
  }
Christian Müller's avatar
Christian Müller committed
218
219
220
221
222
223
224
225
226
227
228
229

  it should "parse encoded vars back to strings" in {
    val s = "R1#t1_a_b"

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

    val s2 = "R1_a_b"

    val f2 = FunFromVar.unapply(s2)
    f2 should be(Some(Fun("R1", None, List("a", "b"))))
  }
230
}