Commit 2928551f authored by Christian Müller's avatar Christian Müller

tactics etc

parent d5e78c71
Workflow
forallmay i,j O(i,j) -> A += (i,j)
forall i,j A(i,j) -> B += (i,j)
forall i,j B(i,j) -> C += (i,j)
Target
C(x,y)
Workflow
forallmay i,j O(i,j) -> A += (i,j)
forall i,j A(i,j) -> B += (i,j)
forall i,j B(i,j) -> C += (i,j)
forall i,j C(i,j) -> D += (i,j)
forall i,j D(i,j) -> E += (i,j)
Target
E(x,y)
Workflow
forallmay i,j O(i,j) -> A += (i,j)
forall i,j A(i,j) -> B += (i,j)
forall i,j B(i,j) -> C += (i,j)
forall i,j C(i,j) -> D += (i,j)
forall i,j D(i,j) -> E += (i,j)
forall i,j E(i,j) -> F += (i,j)
forall i,j F(i,j) -> G += (i,j)
forall i,j G(i,j) -> H += (i,j)
Target
H(x,y)
Workflow
forallmay x,s
O(s) -> R += (x)
Target
R(x)
......@@ -25,56 +25,55 @@ class Z3Test extends FlatSpec with LazyLogging with BeforeAndAfterEach {
var ctx: Context = null
var s: Solver = null
val TIMEOUT = 5000 // in milliseconds
val TIMEOUT = 60000 // 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)
}
s.add(toZ3.translate(quantfree, ctx, varctx))
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)
}
s.add(toZ3.translate(quantfree, ctx, varctx))
s
}
override def afterEach() = {
......@@ -123,7 +122,7 @@ class Z3Test extends FlatSpec with LazyLogging with BeforeAndAfterEach {
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")))
......@@ -192,20 +191,40 @@ class Z3Test extends FlatSpec with LazyLogging with BeforeAndAfterEach {
val s = checkNonOmittingWF(ExampleWorkflows.parseExample("tests/simpleChoice").get)
check(s, Status.SATISFIABLE)
}
it should "check tests/simpleChoiceTyped (nonomitting, stubborn) as LTL prop" in {
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 {
it should "check tests/fixedarity3 (nonomitting, stubborn) as LTL prop" in {
val s = checkNonOmittingWF(ExampleWorkflows.parseExample("tests/fixedarity3").get)
check(s, Status.SATISFIABLE)
}
it should "check tests/fixedarity5 (nonomitting, stubborn) as LTL prop" in {
val s = checkNonOmittingWF(ExampleWorkflows.parseExample("tests/fixedarity5").get)
check(s, Status.SATISFIABLE)
}
it should "check tests/fixedarity8 (nonomitting, stubborn) as LTL prop" ignore {
val s = checkNonOmittingWF(ExampleWorkflows.parseExample("tests/fixedarity8").get)
check(s, Status.SATISFIABLE) // takes > 60s
}
it should "check nonomitting/fixedarity10 (nonomitting, stubborn) as LTL prop" ignore {
val s = checkNonOmittingWF(ExampleWorkflows.parseExample("nonomitting/fixedarity10").get)
check(s, Status.SATISFIABLE) // takes > 60s
}
it should "check tests/simpleChoiceNoOracle (nonomitting, stubborn) as LTL prop" ignore {
val s = checkNonOmittingWF(ExampleWorkflows.parseExample("tests/simpleChoiceNoOracle").get)
check(s, Status.UNSATISFIABLE) // takes long
check(s, Status.UNSATISFIABLE) // takes > 60s
}
it should "check tests/loopexample (nonomitting, stubborn) as LTL prop" in {
it should "check tests/loopexample (nonomitting, stubborn) as LTL prop" ignore {
val s = checkNonOmittingWF(ExampleWorkflows.parseExample("tests/loopexample").get)
check(s, Status.SATISFIABLE) // takes long
check(s, Status.SATISFIABLE) // takes > 60s
}
// it should "check FO workflows" in {
......
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