Skip to content

N
NIWO
Commit 37bd0626 authored by Christian Müller's avatar Christian Müller
Browse files
Options

add nonquant workflow test

parent 0826f803
Hide whitespace changes
Inline Side-by-side
Showing with 126 additions and 72 deletions
src/main/scala/de/tum/workflows/toz3/toz3.scala
View file @ 37bd0626
......@@ -25,9 +25,9 @@ object toZ3 extends LazyLogging {
}
def buildVarCtx(ctx: Context, var_ctx: Map[Var, (Int, Expr, Sort)], vars: List[Var]) = {
val indices = (vars.size - 1) to 0 by - 1
val newexprs = (for ((v,i) <- vars.zip(indices)) yield {
// count = count - 1;
val indices = (vars.size - 1) to 0 by -1
val newexprs = (for ((v, i) <- vars.zip(indices)) yield {
// count = count - 1;
val sort = if (v.typ.equals("Int")) {
ctx.getIntSort()
} else if (v.typ.equals("Bool")) {
......@@ -46,47 +46,50 @@ object toZ3 extends LazyLogging {
newexprs ++ oldvars
}
def updateTime(texpr:ArithExpr, tvar: Option[Var], oldctx:Map[Var, (Int, Expr, Sort)], newctx:Map[Var, (Int, Expr, Sort)]) = {
if (tvar.isEmpty) { texpr } else {
texpr.substitute(oldctx(tvar.get)._2, newctx(tvar.get)._2).asInstanceOf[ArithExpr]
}
def updateTime(texpr: ArithExpr, tvar: Option[Var], oldctx: Map[Var, (Int, Expr, Sort)], newctx: Map[Var, (Int, Expr, Sort)]) = {
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)]) = {
def unaryTemporalOperator(ctx: Context, f: Formula, texpr: ArithExpr, tvar: Option[Var],
var_ctx: Map[Var, (Int, Expr, Sort)]) = {
val new_tvar_name = new_tname()
val new_tsymbol = ctx.mkSymbol(new_tvar_name)
val new_tvar = Var(new_tvar_name, "Int")
val new_var_ctx = buildVarCtx(ctx, var_ctx, List(new_tvar))
val new_texpr = new_var_ctx(new_tvar)._2.asInstanceOf[ArithExpr]
val e_formula = toZ3(ctx, f, new_texpr, Some(new_tvar), new_var_ctx)
// replace old tvar in old texpr using old ctx by new timevar
val upd_texpr = updateTime(texpr, tvar, var_ctx, new_var_ctx)
val e_guard = ctx.mkLe(upd_texpr, new_texpr)
(new_tsymbol, e_guard, e_formula)
}
def toZ3(ctx: Context, f: Formula, texpr: ArithExpr, tvar: Option[Var],
var_ctx: Map[Var, (Int, Expr, Sort)]): BoolExpr = {
def toZ3(ctx: Context, f: Formula, texpr: ArithExpr, tvar: Option[Var],
var_ctx: Map[Var, (Int, Expr, Sort)]): 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
f match {
case Fun(name, ind, params) => {
var fdecl = fun_ctx.get(name)
val pi = if (ind.isDefined) "_" + ind.get else ""
val indexedname = name + pi
var fdecl = fun_ctx.get(indexedname)
if (fdecl == null) {
val pi = if (ind.isDefined) "_" + ind.get else ""
val sorts = params.map(x => var_ctx(x)._3)
// first sort is Int, as it stores time values
val new_sorts = (ctx.getIntSort() :: sorts).toArray[Sort]
fdecl = ctx.mkFuncDecl(name + pi, new_sorts, ctx.getBoolSort())
fun_ctx.put(name, fdecl)
fdecl = ctx.mkFuncDecl(indexedname, new_sorts, ctx.getBoolSort())
fun_ctx.put(indexedname, fdecl)
}
// all variables should be quantified, so they should be part of var_ctx
......@@ -100,41 +103,41 @@ object toZ3 extends LazyLogging {
}
case Globally(f1) => {
val (new_tsymbol, e_guard, e_formula) =
val (new_tsymbol, e_guard, e_formula) =
unaryTemporalOperator(ctx, f1, texpr, tvar, var_ctx)
val body = ctx.mkImplies(e_guard, e_formula)
ctx.mkForall(Array(ctx.getIntSort()), Array(new_tsymbol), body,
0, null, null, null, null)
ctx.mkForall(Array(ctx.getIntSort()), Array(new_tsymbol), body,
0, null, null, null, null)
}
case Finally(f1) => {
val (new_tsymbol, e_guard, e_formula) =
val (new_tsymbol, e_guard, e_formula) =
unaryTemporalOperator(ctx, f1, texpr, tvar, var_ctx)
val body = ctx.mkAnd(e_guard, e_formula)
ctx.mkExists(Array(ctx.getIntSort()), Array(new_tsymbol), body,
0, null, null, null, null)
ctx.mkExists(Array(ctx.getIntSort()), Array(new_tsymbol), body,
0, null, null, null, null)
}
case Until(f1, f2) => {
val ex_tvar_name = new_tname()
val ex_tsymbol = ctx.mkSymbol(ex_tvar_name)
val ex_tvar = Var(ex_tvar_name, "Int")
val ex_var_ctx = buildVarCtx(ctx, var_ctx, List(ex_tvar))
val ex_texpr = ex_var_ctx(ex_tvar)._2.asInstanceOf[ArithExpr]
val ex_expr = toZ3(ctx, f2, ex_texpr, Some(ex_tvar), ex_var_ctx)
val ex_upd_texpr = updateTime(texpr, tvar, var_ctx, ex_var_ctx)
val ex_guard = ctx.mkLe(ex_upd_texpr, ex_texpr)
val fa_tvar_name = new_tname()
val fa_tsymbol = ctx.mkSymbol(fa_tvar_name)
val fa_tvar = Var(fa_tvar_name, "Int")
val fa_var_ctx = buildVarCtx(ctx, ex_var_ctx, List(fa_tvar))
val fa_texpr = fa_var_ctx(fa_tvar)._2.asInstanceOf[ArithExpr]
val fa_expr = toZ3(ctx, f1, fa_texpr, Some(fa_tvar), fa_var_ctx)
val fa_upd_texpr = updateTime(ex_upd_texpr, tvar, ex_var_ctx, fa_var_ctx)
......@@ -143,25 +146,24 @@ object toZ3 extends LazyLogging {
val fa_g2 = ctx.mkLt(fa_texpr, upd_ex_texpr)
val fa_guard = ctx.mkAnd(fa_g1, fa_g2)
val fa_body = ctx.mkImplies(fa_guard, fa_expr)
val fa_fa_expr = ctx.mkForall(Array(ctx.getIntSort()), Array(fa_tsymbol), fa_body,
0, null, null, null, null)
val fa_fa_expr = ctx.mkForall(Array(ctx.getIntSort()), Array(fa_tsymbol), fa_body,
0, null, null, null, null)
val ex_body1 = ctx.mkAnd(ex_expr, fa_fa_expr)
val ex_body = ctx.mkAnd(ex_guard, ex_body1)
ctx.mkExists(Array(ctx.getIntSort()), Array(ex_tsymbol), ex_body,
0, null, null, null, null)
ctx.mkExists(Array(ctx.getIntSort()), Array(ex_tsymbol), ex_body,
0, null, null, null, null)
}
case FOLTL.Exists(vars, f1) => {
val names: Array[Symbol] = vars.map(v => ctx.mkSymbol(v.name)) toArray
val newctx = buildVarCtx(ctx, var_ctx, vars)
val sorts = vars.map(newctx(_)._3) toArray
val upd_texpr = updateTime(texpr, tvar, var_ctx, newctx)
val e1 = toZ3(ctx, f1, upd_texpr, tvar, newctx)
ctx.mkExists(sorts, names, e1, 0, null, null, null, null)
......@@ -171,9 +173,9 @@ object toZ3 extends LazyLogging {
val names: Array[Symbol] = vars.map(v => ctx.mkSymbol(v.name)) toArray
val newctx = buildVarCtx(ctx, var_ctx, vars)
val sorts = vars.map(newctx(_)._3) toArray
val upd_texpr = updateTime(texpr, tvar, var_ctx, newctx)
val e1 = toZ3(ctx, f1, upd_texpr, tvar, newctx)
ctx.mkForall(sorts, names, e1, 0, null, null, null, null)
......@@ -186,7 +188,7 @@ object toZ3 extends LazyLogging {
val e2 = toZ3(ctx, f2, texpr, tvar, var_ctx)
ctx.mkAnd(e1, e2)
}
case Eq(f1, f2) => {
val e1 = toZ3(ctx, f1, texpr, tvar, var_ctx)
val e2 = toZ3(ctx, f2, texpr, tvar, var_ctx)
......@@ -219,7 +221,15 @@ object toZ3 extends LazyLogging {
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
}
def checkZ3(f: Formula, ctx: Context, varctx: Map[Var, (Int, Expr, Sort)]) = {
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
......
src/test/scala/de/tum/workflows/ltl/tests/Z3Test.scala
View file @ 37bd0626
......@@ -17,9 +17,19 @@ import de.tum.workflows.ExampleWorkflows
import de.tum.workflows.foltl.Stubborn
import de.tum.workflows.foltl.Properties
import com.microsoft.z3.Solver
class Z3Test extends FlatSpec with LazyLogging {
def check(s:Solver, c:Status, res: Status) = {
if (c == Status.UNKNOWN) {
println(s"Z3 status unknown: ${s.getReasonUnknown()}")
}
c should be (res)
if (res == Status.SATISFIABLE) {
println(s"Z3 model: ${s.getModel()}")
}
}
// "Z3" should "check Globally" in {
// val easyForm = Globally(And(p, Globally(p)))
......@@ -27,20 +37,18 @@ class Z3Test extends FlatSpec with LazyLogging {
// val s = toZ3.checkZ3(easyForm)
// val c = s.check()
//
// c should be(Status.SATISFIABLE)
// println(s.getModel())
// check(s,c,Status.SATISFIABLE)
// }
// "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()
//
// c should be(Status.SATISFIABLE)
// println(s.getModel())
// }
// "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)
// }
//
// "Z3" should "check quantifiers 1" in {
//
......@@ -50,8 +58,7 @@ class Z3Test extends FlatSpec with LazyLogging {
// val s = toZ3.checkZ3(f)
// val c = s.check()
//
// c should be(Status.SATISFIABLE)
// println(s.getModel())
// check(s,c,Status.SATISFIABLE)
// }
//
// "Z3" should "check quantifiers 2" in {
......@@ -62,7 +69,7 @@ class Z3Test extends FlatSpec with LazyLogging {
// val s = toZ3.checkZ3(f)
// val c = s.check()
//
// c should be(Status.UNSATISFIABLE)
// check(s,c,Status.UNSATISFIABLE)
// }
// "Z3" should "check Until" in {
......@@ -74,8 +81,7 @@ class Z3Test extends FlatSpec with LazyLogging {
// val s = toZ3.checkZ3(f)
// val c = s.check()
//
// c should be(Status.SATISFIABLE) // Z3 does not finish
// println(s.getModel())
// check(s,c,Status.SATISFIABLE) // Z3 does not finish
// }
// NOTE: next 3 formulas are from "On finite domains in FOLTL" ATVA2016
......@@ -90,8 +96,8 @@ class Z3Test extends FlatSpec with LazyLogging {
// val s = toZ3.checkZ3(f)
// val c = s.check()
//
// // c should be(Status.SATISFIABLE) // only on infinite domains
// c should be(Status.UNSATISFIABLE) // only on finite domains
// // check(s,c,Status.SATISFIABLE) // only on infinite domains
// check(s,c,Status.UNSATISFIABLE) // only on finite domains
// // println(s.getModel())
// }
......@@ -109,8 +115,8 @@ class Z3Test extends FlatSpec with LazyLogging {
// val s = toZ3.checkZ3(f)
// val c = s.check()
//
// // c should be(Status.SATISFIABLE) // only on infinite domains
// c should be(Status.UNSATISFIABLE) // only on finite domains
// // check(s,c,Status.SATISFIABLE) // only on infinite domains
// check(s,c,Status.UNSATISFIABLE) // only on finite domains
// // println(s.getModel())
// }
//
......@@ -126,12 +132,12 @@ class Z3Test extends FlatSpec with LazyLogging {
// val s = toZ3.checkZ3(f)
// val c = s.check()
//
// // c should be(Status.SATISFIABLE) // only on infinite domains
// c should be(Status.UNSATISFIABLE) // only on finite domains
// // check(s,c,Status.SATISFIABLE) // only on infinite domains
// check(s,c,Status.UNSATISFIABLE) // only on finite domains
// // println(s.getModel())
// }
"Z3" should "check workflows" in {
"Z3" should "check LTL prop workflows" in {
val spec = ExampleWorkflows.parseExample("tests/simpleChoice").get
logger.info(s"Encoding Spec:\n$spec")
......@@ -141,13 +147,51 @@ class Z3Test extends FlatSpec with LazyLogging {
logger.info(s"Computing noninterference for target ${spec.target} using only stubborn agents")
val prop = Properties.noninterStubborn(spec)
val sprop = prop.simplify()
println(sprop)
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)
val ctx = new Context()
val s = toZ3.checkZ3(sprop)
// 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)
}
val s = toZ3.checkZ3(quantfree, ctx, varctx)
val c = s.check()
c should be(Status.SATISFIABLE)
println(s.getModel())
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())
// }
}
// 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