Skip to content

N
NIWO
Commit 0826f803 authored by Eugen Zalinescu's avatar Eugen Zalinescu
Browse files
Options

after a workflow test

parent 9bdd62d2
Hide whitespace changes
Inline Side-by-side
Showing with 138 additions and 95 deletions
src/main/scala/de/tum/workflows/foltl/FOLTLTermFunctions.scala
View file @ 0826f803
......@@ -154,7 +154,7 @@ object FormulaFunctions extends LazyLogging {
frees.isEmpty
}
def removeOTQuantifiers(f: Formula) = {
def removeOTQuantifiers(f: Formula):Formula = {
f.everywhere({
case ForallOtherThan(vars, otherthan, fp) => {
val eqs = for (x <- vars; y <- otherthan) yield {
......
src/main/scala/de/tum/workflows/toz3/toz3.scala
View file @ 0826f803
......@@ -25,15 +25,16 @@ object toZ3 extends LazyLogging {
}
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 {
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")) {
ctx.getBoolSort()
} else {
ctx.mkFiniteDomainSort(v.typ, 10) // TODO: sort size?
ctx.mkFiniteDomainSort(v.typ, 1) // TODO: sort size?
}
v -> (i, ctx.mkBound(i, sort), sort)
}) toMap
......@@ -185,6 +186,12 @@ 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)
ctx.mkEq(e1, e2)
}
case Or(f1, f2) => {
val e1 = toZ3(ctx, f1, texpr, tvar, var_ctx)
......
src/test/scala/de/tum/workflows/ltl/tests/Z3Test.scala
View file @ 0826f803
package de.tum.workflows.ltl.tests;
import org.scalatest._
import com.typesafe.scalalogging.LazyLogging
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
......@@ -11,107 +13,141 @@ import de.tum.workflows.toz3._
import com.microsoft.z3.Context
import java.util.HashMap
import com.microsoft.z3.Status
import de.tum.workflows.ExampleWorkflows
class Z3Test extends FlatSpec {
import de.tum.workflows.foltl.Stubborn
import de.tum.workflows.foltl.Properties
// "Z3" should "check Globally" in {
// val easyForm = Globally(And(p, Globally(p)))
//
// val s = toZ3.checkZ3(easyForm)
// val c = s.check()
//
// c should be(Status.SATISFIABLE)
// println(s.getModel())
// }
//
// "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()
//
// 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())
// }
class Z3Test extends FlatSpec with LazyLogging {
// "Z3" should "check Globally" in {
// val easyForm = Globally(And(p, Globally(p)))
//
// 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()
//
// c should be(Status.SATISFIABLE)
// println(s.getModel())
// }
//
// "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()
//
// 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())
// }
// 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)
// "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()
//
// // c should be(Status.SATISFIABLE) // only on infinite domains
// c should be(Status.UNSATISFIABLE) // only on finite domains
// // println(s.getModel())
// }
val s = toZ3.checkZ3(f)
val c = s.check()
// "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()
//
// // c should be(Status.SATISFIABLE) // only on infinite domains
// c should be(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()
//
// // c should be(Status.SATISFIABLE) // only on infinite domains
// c should be(Status.UNSATISFIABLE) // only on finite domains
// // println(s.getModel())
// }
"Z3" should "check workflows" in {
val spec = ExampleWorkflows.parseExample("tests/simpleChoice").get
logger.info(s"Encoding Spec:\n$spec")
val t1 = "pi1"
val t2 = "pi2"
// c should be(Status.SATISFIABLE) // only on infinite domains
c should be(Status.UNSATISFIABLE) // only on infinite domains
// println(s.getModel())
logger.info(s"Computing noninterference for target ${spec.target} using only stubborn agents")
val prop = Properties.noninterStubborn(spec)
val sprop = prop.simplify()
println(sprop)
val s = toZ3.checkZ3(sprop)
val c = s.check()
c should be(Status.SATISFIABLE)
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