Skip to content

N
NIWO
Commit 3f59003d authored by Eugen Zalinescu's avatar Eugen Zalinescu
Browse files
Options

added Finally and Until

parent 4466e442
Hide whitespace changes
Inline Side-by-side
Showing with 147 additions and 51 deletions
src/main/scala/de/tum/workflows/toz3/toz3.scala
View file @ 3f59003d
......@@ -19,29 +19,19 @@ object toZ3 extends LazyLogging {
val fun_ctx = new HashMap[String, FuncDecl]()
def new_tvar(ctx: Context) = {
def new_tname() = {
counter = counter + 1
"t" + counter
}
// def getSort(ctx: Context, typ: String) = {
// if (!sort_ctx.isDefinedAt(typ)) {
// // TODO: size of the finite domain?!
// val s = ctx.mkFiniteDomainSort(typ, 2)
// sort_ctx += (typ -> s)
// }
// sort_ctx(typ)
// }
def buildVarCtx(ctx: Context, var_ctx: Map[Var, (Int, Expr, Sort)], vars: List[Var]) = {
val newexprs = (for ((v, i) <- vars.zip(vars.size - 1 to 0)) yield {
// TODO: size?
val sort = if (v.typ.equals("Int")) {
ctx.getIntSort()
} else if (v.typ.equals("Bool")) {
ctx.getBoolSort()
} else {
ctx.mkFiniteDomainSort(v.typ, 2)
ctx.mkFiniteDomainSort(v.typ, 10) // TODO: sort size?
}
v -> (i, ctx.mkBound(i, sort), sort)
......@@ -56,20 +46,36 @@ object toZ3 extends LazyLogging {
newexprs ++ oldvars
}
def updateTime(tvar: Option[Var], texpr:ArithExpr, oldctx:Map[Var, (Int, Expr, Sort)], newctx:Map[Var, (Int, Expr, Sort)]) = {
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)]) = {
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 = {
// tvar can be an expression e with the form
// given by the following grammar:
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 v: Var => // TODO
case Fun(name, ind, params) => {
var fdecl = fun_ctx.get(name)
......@@ -83,6 +89,7 @@ object toZ3 extends LazyLogging {
}
// all variables should be quantified, so they should be part of var_ctx
// TODO: support constants/free variables
val all_args = texpr :: params.map(x => var_ctx(x)._2)
fdecl.apply(all_args: _*).asInstanceOf[BoolExpr]
}
......@@ -92,41 +99,67 @@ object toZ3 extends LazyLogging {
}
case Globally(f1) => {
val newt = new_tvar(ctx)
val quantifiername = "G" + counter
val sortInt = ctx.getIntSort()
val (new_tsymbol, e_guard, e_formula) =
unaryTemporalOperator(ctx, f1, texpr, tvar, var_ctx)
val body = ctx.mkImplies(e_guard, e_formula)
val variable = Var(newt, "Int")
ctx.mkForall(Array(ctx.getIntSort()), Array(new_tsymbol), body,
0, null, null, null, null)
}
val newctx = buildVarCtx(ctx, var_ctx, List(variable))
case Finally(f1) => {
val (new_tsymbol, e_guard, e_formula) =
unaryTemporalOperator(ctx, f1, texpr, tvar, var_ctx)
val body = ctx.mkAnd(e_guard, e_formula)
val new_texpr = newctx(variable)._2.asInstanceOf[ArithExpr]
val e1 = toZ3(ctx, f1, new_texpr, Some(variable), newctx)
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)
// replace old timevar in old ctx by new timevar
val old_texpr = updateTime(tvar, texpr, var_ctx, newctx)
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 e0 = ctx.mkLe(old_texpr, new_texpr.asInstanceOf[ArithExpr])
val body = ctx.mkImplies(e0, e1)
val fa_upd_texpr = updateTime(ex_upd_texpr, tvar, ex_var_ctx, fa_var_ctx)
val fa_g1 = ctx.mkLe(fa_upd_texpr, fa_texpr)
val upd_ex_texpr = updateTime(ex_texpr, Some(ex_tvar), ex_var_ctx, fa_var_ctx)
val fa_g2 = ctx.mkLt(fa_texpr, upd_ex_texpr)
val fa_guard = ctx.mkAnd(fa_g1, fa_g2)
ctx.mkForall(Array(sortInt), Array(ctx.mkSymbol(newt)), body, 0, null, null,
ctx.mkSymbol(quantifiername), null)
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 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)
}
// case Finally(f1) => {
//
// }
//
// case Until(f1, f2) => {
//
// }
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(tvar, texpr, var_ctx, newctx)
val upd_texpr = updateTime(texpr, tvar, var_ctx, newctx)
val e1 = toZ3(ctx, f1, upd_texpr, tvar, newctx)
......@@ -138,7 +171,7 @@ object toZ3 extends LazyLogging {
val newctx = buildVarCtx(ctx, var_ctx, vars)
val sorts = vars.map(newctx(_)._3) toArray
val upd_texpr = updateTime(tvar, texpr, var_ctx, newctx)
val upd_texpr = updateTime(texpr, tvar, var_ctx, newctx)
val e1 = toZ3(ctx, f1, upd_texpr, tvar, newctx)
......
src/test/scala/de/tum/workflows/ltl/tests/Z3Test.scala
View file @ 3f59003d
......@@ -14,9 +14,7 @@ import com.microsoft.z3.Status
class Z3Test extends FlatSpec {
val p = Fun("p", List())
// "Z3" should "work" in {
// "Z3" should "check Globally" in {
// val easyForm = Globally(And(p, Globally(p)))
//
// val s = toZ3.checkZ3(easyForm)
......@@ -25,8 +23,8 @@ class Z3Test extends FlatSpec {
// c should be(Status.SATISFIABLE)
// println(s.getModel())
// }
// it should "check quantifiers" in {
//
// "Z3" should "check quantifiers 1" in {
//
// val f = Globally(Forall(List("x"), Fun("p", "x")))
// println(f)
......@@ -36,19 +34,84 @@ class Z3Test extends FlatSpec {
//
// c should be(Status.SATISFIABLE)
// println(s.getModel())
// }
//
// "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()
//
// c should be(Status.UNSATISFIABLE)
// }
// "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()
//
// c should be(Status.SATISFIABLE) // Z3 does not finish
// println(s.getModel())
// }
"Z3" should "check quantifiers" in {
// NOTE: next 3 formulas are from "On finite domains in FOLTL" ATVA2016
"Z3" should "check infinite models 1" in {
val f = Globally(Forall(List("x"), And(Fun("p", "x"), Next(Neg(Forall("y", Globally(Next(Fun("p", "y")))))))))
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()
c should be(Status.UNSATISFIABLE)
// c should be(Status.SATISFIABLE) // only on infinite domains
c should be(Status.UNSATISFIABLE) // only on infinite domains
// println(s.getModel())
}
// "Z3" should "check infinite models 2" in {
//
// val f = 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()
//
// // c should be(Status.SATISFIABLE) // only on infinite domains
// c should be(Status.UNSATISFIABLE) // only on infinite domains
// // println(s.getModel())
// }
//
// "Z3" should "check infinite models 3" in {
//
// val f = 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()
//
// // c should be(Status.SATISFIABLE) // only on infinite domains
// c should be(Status.UNSATISFIABLE) // only on infinite domains
// // 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