Skip to content

GitLab

Commit d5e78c71 authored by Christian Müller's avatar Christian Müller
Browse files

better tests

parent 8542dd8d
Hide whitespace changes
Inline Side-by-side
Showing with 213 additions and 176 deletions
src/main/scala/de/tum/workflows/toz3/toz3.scala
View file @ d5e78c71
......@@ -10,6 +10,9 @@ import java.util.HashMap
import com.typesafe.scalalogging.LazyLogging
object toZ3 extends LazyLogging {
type VarCtx = Map[Var, (Option[Int], Expr, Sort)]
def succ(ctx: Context, e: ArithExpr) = {
val One = ctx.mkInt(1)
ctx.mkAdd(e, One)
......@@ -17,6 +20,7 @@ object toZ3 extends LazyLogging {
var counter = 0
// TODO: how to not make this static?
val fun_ctx = new HashMap[String, FuncDecl]()
def new_tname() = {
......@@ -24,7 +28,7 @@ object toZ3 extends LazyLogging {
"t" + counter
}
def buildVarCtx(ctx: Context, var_ctx: Map[Var, (Int, Expr, Sort)], vars: List[Var]) = {
def buildVarCtx(ctx: Context, var_ctx: VarCtx, vars: List[Var]): VarCtx = {
val indices = (vars.size - 1) to 0 by -1
val newexprs = (for ((v, i) <- vars.zip(indices)) yield {
// count = count - 1;
......@@ -35,26 +39,31 @@ object toZ3 extends LazyLogging {
} else {
ctx.mkFiniteDomainSort(v.typ, 1) // TODO: sort size?
}
v -> (i, ctx.mkBound(i, sort), sort)
v -> (Some(i), ctx.mkBound(i, sort), sort)
}) toMap
// if the index is defined, increment, otherwise use the expr (which is a constant f.e.)
val oldvars = (for ((v, (i, e, s)) <- var_ctx) yield {
val newi = i + vars.size
val newbound = ctx.mkBound(newi, s)
v -> (newi, newbound, s)
if (i.isDefined) {
val newi = i.get + vars.size
val newbound = ctx.mkBound(newi, s)
v -> (Some(newi), newbound, s)
} else {
v -> (i, e, s)
}
})
newexprs ++ oldvars
}
def updateTime(texpr: ArithExpr, tvar: Option[Var], oldctx: Map[Var, (Int, Expr, Sort)], newctx: Map[Var, (Int, Expr, Sort)]) = {
def updateTime(texpr: ArithExpr, tvar: Option[Var], oldctx: VarCtx, newctx: VarCtx) = {
if (tvar.isEmpty) { texpr } else {
texpr.substitute(oldctx(tvar.get)._2, newctx(tvar.get)._2).asInstanceOf[ArithExpr]
}
}
def unaryTemporalOperator(ctx: Context, f: Formula, texpr: ArithExpr, tvar: Option[Var],
var_ctx: Map[Var, (Int, Expr, Sort)]) = {
var_ctx: VarCtx) = {
val new_tvar_name = new_tname()
val new_tsymbol = ctx.mkSymbol(new_tvar_name)
val new_tvar = Var(new_tvar_name, "Int")
......@@ -71,7 +80,7 @@ object toZ3 extends LazyLogging {
}
def toZ3(ctx: Context, f: Formula, texpr: ArithExpr, tvar: Option[Var],
var_ctx: Map[Var, (Int, Expr, Sort)]): BoolExpr = {
var_ctx: VarCtx): BoolExpr = {
// texpr is an expression e with the form given by the following grammar:
// e ::= 0 | t | succ(e)
// tvar is Some(t) if e contains t or None otherwise
......@@ -214,24 +223,19 @@ object toZ3 extends LazyLogging {
}
}
def checkZ3(f: Formula) = {
val cfg = new HashMap[String, String]();
cfg.put("model", "true");
val ctx = new Context(cfg);
def translate(f: Formula, ctx: Context) = {
logger.info(s"Using formula:\n$f")
fun_ctx.clear()
val expr = toZ3(ctx, f, ctx.mkInt(0), None, Map())
logger.info(s"Checking Z3 expression:\n$expr")
val s = ctx.mkSolver()
s.add(expr)
s
logger.info(s"Built Z3 expression:\n$expr")
expr
}
def checkZ3(f: Formula, ctx: Context, varctx: Map[Var, (Int, Expr, Sort)]) = {
def translate(f: Formula, ctx: Context, varctx: VarCtx) = {
logger.info(s"Using formula:\n${f.pretty()}")
fun_ctx.clear()
val expr = toZ3(ctx, f, ctx.mkInt(0), None, varctx)
logger.info(s"Checking Z3 expression:\n$expr")
val s = ctx.mkSolver()
s.add(expr)
s
logger.info(s"Built Z3 expression:\n$expr")
expr
}
}
src/test/scala/de/tum/workflows/ltl/tests/Z3Test.scala
View file @ d5e78c71
......@@ -15,183 +15,216 @@ import java.util.HashMap
import com.microsoft.z3.Status
import de.tum.workflows.ExampleWorkflows
import de.tum.workflows.blocks
import de.tum.workflows.foltl.Stubborn
import de.tum.workflows.foltl.Properties
import com.microsoft.z3.Solver
class Z3Test extends FlatSpec with LazyLogging {
class Z3Test extends FlatSpec with LazyLogging with BeforeAndAfterEach {
var ctx: Context = null
var s: Solver = null
val TIMEOUT = 5000 // in milliseconds
override def beforeEach() = {
val cfg = new HashMap[String, String]()
cfg.put("timeout", TIMEOUT.toString())
val ctx = new Context(cfg)
val qe = ctx.mkTactic("qe")
val default = ctx.mkTactic("smt")
val t = ctx.andThen(qe, default)
val s = ctx.mkSolver(t)
this.ctx = ctx
this.s = s
}
def checkNonOmittingWF(spec:blocks.Spec) = {
logger.info(s"Encoding Spec:\n$spec")
val t1 = "pi1"
val t2 = "pi2"
logger.info(s"Computing noninterference for target ${spec.target} using only stubborn agents")
val prop = Properties.noninterStubborn(spec)
val sprop = prop.simplify()
println(sprop.pretty())
val (agents, res) = LTL.eliminateExistentials(sprop)
val universe = agents.map(_.withType()).mkString(", ")
logger.info(s"Using universe $universe")
val quantfree = LTL.eliminateUniversals(res, agents)
val ltlprop = LTL.eliminatePredicates(quantfree)
val mapped = agents.groupBy(v => v.typ)
// maybe go to LTL and make all variables bool?
val sortedagents = for ((s, list) <- mapped) yield {
val sort = ctx.mkFiniteDomainSort(s, mapped(s).size)
sort -> list
}
val varctx = for ((s, l) <- sortedagents; a <- l) yield {
a -> (None, ctx.mkConst(a.name, s), s)
}
def check(s:Solver, c:Status, res: Status) = {
s.add(toZ3.translate(quantfree, ctx, varctx))
s
}
override def afterEach() = {
ctx.close()
}
def check(s: Solver, res: Status) = {
val c = s.check()
if (c == Status.UNKNOWN) {
println(s"Z3 status unknown: ${s.getReasonUnknown()}")
}
c should be (res)
c should be(res)
if (res == Status.SATISFIABLE) {
println(s"Z3 model: ${s.getModel()}")
println(s"Z3 model:\n${s.getModel()}")
}
}
// "Z3" should "check Globally" in {
// val easyForm = Globally(And(p, Globally(p)))
//
// val s = toZ3.checkZ3(easyForm)
// val c = s.check()
//
// check(s,c,Status.SATISFIABLE)
// }
"Z3" should "check Globally" in {
val easyForm = Globally(And(Fun("p", List()), Globally(Fun("p", List()))))
// "Z3" should "check small things" in {
// val easyForm = Forall(List("x","s"), Neg(Fun("R",List("x","s"))))
//
// val s = toZ3.checkZ3(easyForm)
// val c = s.check()
//
// check(s,c,Status.SATISFIABLE)
// }
s.add(toZ3.translate(easyForm, ctx))
check(s, Status.SATISFIABLE)
}
//
// "Z3" should "check quantifiers 1" in {
//
// val f = Globally(Forall(List("x"), Fun("p", "x")))
// println(f)
//
// val s = toZ3.checkZ3(f)
// val c = s.check()
//
// check(s,c,Status.SATISFIABLE)
// }
//
// "Z3" should "check quantifiers 2" in {
//
// val f = Globally(Forall(List("x"), And(Fun("p", "x"), Next(Neg(Forall("y", Globally(Next(Fun("p", "y")))))))))
// println(f)
//
// val s = toZ3.checkZ3(f)
// val c = s.check()
//
// check(s,c,Status.UNSATISFIABLE)
// }
it should "check small things" in {
val easyForm = Forall(List("x", "s"), Neg(Fun("R", List("x", "s"))))
// "Z3" should "check Until" in {
//
// val f = Globally(Forall(List("x"), Next(
// Until(Fun("p", "x"), Next(Forall("y", Finally(Next(Fun("q", "y")))))))))
// println(f)
//
// val s = toZ3.checkZ3(f)
// val c = s.check()
//
// check(s,c,Status.SATISFIABLE) // Z3 does not finish
// }
s.add(toZ3.translate(easyForm, ctx))
check(s, Status.SATISFIABLE)
}
it should "check quantifiers 1" in {
val f = Globally(Forall(List("x"), Fun("p", "x")))
println(f)
s.add(toZ3.translate(f, ctx))
check(s, Status.SATISFIABLE)
}
it should "check quantifiers 2" in {
val f = Globally(Forall(List("x"), And(Fun("p", "x"), Next(Neg(Forall("y", Globally(Next(Fun("p", "y")))))))))
println(f)
s.add(toZ3.translate(f, ctx))
check(s, Status.UNSATISFIABLE)
}
it should "check Until" in {
val f = Until(Fun("p", List()), Forall("y", Fun("q", "y")))
println(f)
s.add(toZ3.translate(f, ctx))
check(s, Status.SATISFIABLE)
}
it should "check more complex Until" ignore {
val f = Globally(Forall(List("x"), Next(
Until(Fun("p", "x"), Next(Forall("y", Finally(Next(Fun("q", "y")))))))))
println(f)
s.add(toZ3.translate(f, ctx))
check(s, Status.SATISFIABLE) // Z3 does not finish
}
// NOTE: next 3 formulas are from "On finite domains in FOLTL" ATVA2016
// "Z3" should "check infinite models 1" in {
//
// val f = Globally(Exists("x", And (
// Fun("p", "x"),
// Next(Globally(Neg(Fun("p", "x")))))))
// println(f)
//
// val s = toZ3.checkZ3(f)
// val c = s.check()
//
// // check(s,c,Status.SATISFIABLE) // only on infinite domains
// check(s,c,Status.UNSATISFIABLE) // only on finite domains
// // println(s.getModel())
// }
it should "check infinite models 1" in {
// "Z3" should "check infinite models 2" in {
//
// val f = Exists("c", Forall("x", Exists("y", And(
// Fun("p", "c"),
// Globally(Implies(
// Fun("p", "x"),
// Next(And(
// Fun("p", "y"),
// Globally(Neg(Fun("p", "x")))))))))))
// println(f)
//
// val s = toZ3.checkZ3(f)
// val c = s.check()
//
// // check(s,c,Status.SATISFIABLE) // only on infinite domains
// check(s,c,Status.UNSATISFIABLE) // only on finite domains
// // println(s.getModel())
// }
//
// "Z3" should "check infinite models 3" in {
//
// val f = Exists("c", Forall("x", Exists("y", And(
// Fun("p", "c"),
// Until(
// And(Fun("p", "x"), Fun("p", "y")),
// And(Neg(Fun("p", "x")), Fun("p", "y")))))))
// println(f)
//
// val s = toZ3.checkZ3(f)
// val c = s.check()
//
// // check(s,c,Status.SATISFIABLE) // only on infinite domains
// check(s,c,Status.UNSATISFIABLE) // only on finite domains
// // println(s.getModel())
// }
val f = Globally(Exists("x", And(
Fun("p", "x"),
Next(Globally(Neg(Fun("p", "x")))))))
println(f)
"Z3" should "check LTL prop workflows" in {
val spec = ExampleWorkflows.parseExample("tests/simpleChoice").get
s.add(toZ3.translate(f, ctx))
// check(s,c,Status.SATISFIABLE) // only on infinite domains
check(s, Status.UNSATISFIABLE) // only on finite domains
}
logger.info(s"Encoding Spec:\n$spec")
val t1 = "pi1"
val t2 = "pi2"
it should "check infinite models 2" in {
logger.info(s"Computing noninterference for target ${spec.target} using only stubborn agents")
val prop = Properties.noninterStubborn(spec)
val sprop = prop.simplify()
println(sprop.pretty())
val (agents, res) = LTL.eliminateExistentials(sprop)
val universe = agents.map(_.withType()).mkString(", ")
logger.info(s"Using universe $universe")
val f = Exists("c", Forall("x", Exists("y", And(
Fun("p", "c"),
Globally(Implies(
Fun("p", "x"),
Next(And(
Fun("p", "y"),
Globally(Neg(Fun("p", "x")))))))))))
println(f)
val quantfree = LTL.eliminateUniversals(res, agents)
val ltlprop = LTL.eliminatePredicates(quantfree)
val mapped = agents.groupBy(v => v.typ)
val ctx = new Context()
// TODO: does not work yet - maybe use enum sorts?
// also maybe go to LTL and make all variables bool?
val sortedagents = for ((s, list) <- mapped) yield {
val sort = ctx.mkFiniteDomainSort(s, mapped(s).size)
sort -> list
}
val varctx = for ((s, l) <- sortedagents; a <- l) yield {
a -> (0, ctx.mkConst(a.name, s), s)
}
s.add(toZ3.translate(f, ctx))
// check(s,c,Status.SATISFIABLE) // only on infinite domains
check(s, Status.UNSATISFIABLE) // only on finite domains
}
val s = toZ3.checkZ3(quantfree, ctx, varctx)
val c = s.check()
check(s, c, Status.SATISFIABLE)
}
// "Z3" should "check FO workflows" in {
// val spec = ExampleWorkflows.parseExample("tests/simpleChoice").get
//
// logger.info(s"Encoding Spec:\n$spec")
// val t1 = "pi1"
// val t2 = "pi2"
//
// logger.info(s"Computing noninterference for target ${spec.target} using only stubborn agents")
// val prop = Properties.noninterStubborn(spec)
// val sprop = prop.simplify()
// println(sprop.pretty())
//
// val s = toZ3.checkZ3(sprop)
// val c = s.check()
// c should be(Status.SATISFIABLE)
// println(s.getModel())
// }
it should "check infinite models 3" in {
val f = Exists("c", Forall("x", Exists("y", And(
Fun("p", "c"),
Until(
And(Fun("p", "x"), Fun("p", "y")),
And(Neg(Fun("p", "x")), Fun("p", "y")))))))
println(f)
s.add(toZ3.translate(f, ctx))
// check(s,c,Status.SATISFIABLE) // only on infinite domains
check(s, Status.UNSATISFIABLE) // only on finite domains
// println(s.getModel())
}
it should "check tests/simpleChoice (nonomitting) as LTL prop" in {
val s = checkNonOmittingWF(ExampleWorkflows.parseExample("tests/simpleChoice").get)
check(s, Status.SATISFIABLE)
}
it should "check tests/simpleChoiceTyped (nonomitting, stubborn) as LTL prop" in {
val s = checkNonOmittingWF(ExampleWorkflows.parseExample("tests/simpleChoiceTyped").get)
check(s, Status.SATISFIABLE)
}
it should "check tests/simpleChoiceNoOracle (nonomitting, stubborn) as LTL prop" in {
val s = checkNonOmittingWF(ExampleWorkflows.parseExample("tests/simpleChoiceNoOracle").get)
check(s, Status.UNSATISFIABLE) // takes long
}
it should "check tests/loopexample (nonomitting, stubborn) as LTL prop" in {
val s = checkNonOmittingWF(ExampleWorkflows.parseExample("tests/loopexample").get)
check(s, Status.SATISFIABLE) // takes long
}
// it should "check FO workflows" in {
// val spec = ExampleWorkflows.parseExample("tests/simpleChoice").get
//
// logger.info(s"Encoding Spec:\n$spec")
// val t1 = "pi1"
// val t2 = "pi2"
//
// logger.info(s"Computing noninterference for target ${spec.target} using only stubborn agents")
// val prop = Properties.noninterStubborn(spec)
// val sprop = prop.simplify()
// println(sprop.pretty())
//
// val s = toZ3.checkZ3(sprop)
// val c = s.check()
// c should be(Status.SATISFIABLE)
// println(s.getModel())
// }
}
// TODO: set domain size from the test?
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