diff --git a/src/test/scala/de/tum/niwo/tests/ParserTest.scala b/src/test/scala/de/tum/niwo/tests/ParserTest.scala index c0ad20712de40d9df03f87ba3239aaba0a19b591..f7ccbd66a5788dd615a088136ea076283de097a0 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 e712399245dd714638045d9c8003d08897c04545..93a519855dff84be42428ce459550ad17ee5e9b0 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