From ca5495011a748920e83e5057c1cfd594cb8f7a9e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Christian=20M=C3=BCller?= <christian.mueller@in.tum.de>
Date: Tue, 26 Mar 2019 19:04:43 +0100
Subject: [PATCH] fix tests

---
 src/test/scala/de/tum/niwo/tests/ParserTest.scala         | 8 ++++----
 .../tests/{Z3LTLQFreeTest.scala => Z3QFreeTest.scala}     | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)
 rename src/test/scala/de/tum/niwo/tests/{Z3LTLQFreeTest.scala => Z3QFreeTest.scala} (96%)

diff --git a/src/test/scala/de/tum/niwo/tests/ParserTest.scala b/src/test/scala/de/tum/niwo/tests/ParserTest.scala
index c0ad207..f7ccbd6 100644
--- a/src/test/scala/de/tum/niwo/tests/ParserTest.scala
+++ b/src/test/scala/de/tum/niwo/tests/ParserTest.scala
@@ -157,7 +157,7 @@ class ParserTest extends FlatSpec {
     val x = Var("x", "Agent")
     val s = Var("s", "Paper")
 
-    val typedsig = Signature(Set(Fun("O", List(x)), Fun("choice0", List(x))), Set(), Set(), Set(Fun("R", List(x, s))), Set())
+    val typedsig = Signature(Set(Fun("O", List(x)), Fun("choice0", List(x,s))), Set(), Set(), Set(Fun("R", List(x, s))), Set())
 
     val w = Workflow(
       typedsig,
@@ -181,7 +181,7 @@ class ParserTest extends FlatSpec {
       """
     val w = Workflow(
       Signature(
-        Set(Fun("O", List("s"))),
+        Set(Fun("O", List("s")), Fun("choice0", List("x", "s"))),
         Set(),
         Set(),
         Set(Fun("R", List("x", "s"))),
@@ -199,7 +199,7 @@ class ParserTest extends FlatSpec {
     val s = """
       Workflow
       
-      forall x,s
+      forallmay x,s
 	      O(x,s) -> R += (x,s)
 	      
 	    Declassify
@@ -213,7 +213,7 @@ class ParserTest extends FlatSpec {
     val w = Workflow(
       oxrxssig,
       List(
-        ForallWFBlock(List("x", "s"),
+        ForallMayWFBlock(List("x", "s"), "choice0",
           Add(Fun("O", List("x","s")), "R", List("x", "s")))))
 
     val t = Fun("R", List("x", "s"))
diff --git a/src/test/scala/de/tum/niwo/tests/Z3LTLQFreeTest.scala b/src/test/scala/de/tum/niwo/tests/Z3QFreeTest.scala
similarity index 96%
rename from src/test/scala/de/tum/niwo/tests/Z3LTLQFreeTest.scala
rename to src/test/scala/de/tum/niwo/tests/Z3QFreeTest.scala
index e712399..93a5198 100644
--- a/src/test/scala/de/tum/niwo/tests/Z3LTLQFreeTest.scala
+++ b/src/test/scala/de/tum/niwo/tests/Z3QFreeTest.scala
@@ -14,7 +14,7 @@ import de.tum.niwo.foltl.FOLTL._
 import de.tum.niwo.toz3.{Z3FOEncoding, Z3QFree}
 import com.microsoft.z3.Status
 
-  class Z3QFreeTest extends FlatSpec with LazyLogging with BeforeAndAfterEach {
+class Z3QFreeTest extends FlatSpec with LazyLogging with BeforeAndAfterEach {
 
   var ctx: Context = null
   var s: Solver = null
-- 
2.24.1