Commit ca549501 authored by Christian Müller's avatar Christian Müller

fix tests

parent 68ca8742
...@@ -157,7 +157,7 @@ class ParserTest extends FlatSpec { ...@@ -157,7 +157,7 @@ class ParserTest extends FlatSpec {
val x = Var("x", "Agent") val x = Var("x", "Agent")
val s = Var("s", "Paper") 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( val w = Workflow(
typedsig, typedsig,
...@@ -181,7 +181,7 @@ class ParserTest extends FlatSpec { ...@@ -181,7 +181,7 @@ class ParserTest extends FlatSpec {
""" """
val w = Workflow( val w = Workflow(
Signature( Signature(
Set(Fun("O", List("s"))), Set(Fun("O", List("s")), Fun("choice0", List("x", "s"))),
Set(), Set(),
Set(), Set(),
Set(Fun("R", List("x", "s"))), Set(Fun("R", List("x", "s"))),
...@@ -199,7 +199,7 @@ class ParserTest extends FlatSpec { ...@@ -199,7 +199,7 @@ class ParserTest extends FlatSpec {
val s = """ val s = """
Workflow Workflow
forall x,s forallmay x,s
O(x,s) -> R += (x,s) O(x,s) -> R += (x,s)
Declassify Declassify
...@@ -213,7 +213,7 @@ class ParserTest extends FlatSpec { ...@@ -213,7 +213,7 @@ class ParserTest extends FlatSpec {
val w = Workflow( val w = Workflow(
oxrxssig, oxrxssig,
List( List(
ForallWFBlock(List("x", "s"), ForallMayWFBlock(List("x", "s"), "choice0",
Add(Fun("O", List("x","s")), "R", List("x", "s"))))) Add(Fun("O", List("x","s")), "R", List("x", "s")))))
val t = Fun("R", List("x", "s")) val t = Fun("R", List("x", "s"))
......
...@@ -14,7 +14,7 @@ import de.tum.niwo.foltl.FOLTL._ ...@@ -14,7 +14,7 @@ import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.toz3.{Z3FOEncoding, Z3QFree} import de.tum.niwo.toz3.{Z3FOEncoding, Z3QFree}
import com.microsoft.z3.Status 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 ctx: Context = null
var s: Solver = null var s: Solver = null
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment