Z3Test.scala 7.19 KB
Newer Older
1
2
3
package de.tum.workflows.ltl.tests;

import org.scalatest._
Eugen Zalinescu's avatar
Eugen Zalinescu committed
4
5
import com.typesafe.scalalogging.LazyLogging

6
7
8
9
10
11
12
13
14
15
import org.scalatest.Matchers._
import org.scalatest.Inspectors._

import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.ltl.LTL
import de.tum.workflows.Implicits._
import de.tum.workflows.toz3._
import com.microsoft.z3.Context
import java.util.HashMap
import com.microsoft.z3.Status
Eugen Zalinescu's avatar
Eugen Zalinescu committed
16
import de.tum.workflows.ExampleWorkflows
17

Christian Müller's avatar
Christian Müller committed
18
import de.tum.workflows.blocks
Eugen Zalinescu's avatar
Eugen Zalinescu committed
19
20
import de.tum.workflows.foltl.Stubborn
import de.tum.workflows.foltl.Properties
Christian Müller's avatar
Christian Müller committed
21
import com.microsoft.z3.Solver
Eugen Zalinescu's avatar
Eugen Zalinescu committed
22

Christian Müller's avatar
Christian Müller committed
23
24
25
26
27
class Z3Test extends FlatSpec with LazyLogging with BeforeAndAfterEach {

  var ctx: Context = null
  var s: Solver = null

Christian Müller's avatar
Christian Müller committed
28
  val TIMEOUT = 60000 // in milliseconds
Christian Müller's avatar
Christian Müller committed
29
30
31
32

  override def beforeEach() = {
    val cfg = new HashMap[String, String]()
    cfg.put("timeout", TIMEOUT.toString())
Christian Müller's avatar
Christian Müller committed
33

Christian Müller's avatar
Christian Müller committed
34
    val ctx = new Context(cfg)
Christian Müller's avatar
Christian Müller committed
35

Christian Müller's avatar
Christian Müller committed
36
37
38
    val qe = ctx.mkTactic("qe")
    val default = ctx.mkTactic("smt")
    val t = ctx.andThen(qe, default)
Christian Müller's avatar
Christian Müller committed
39

Christian Müller's avatar
Christian Müller committed
40
    val s = ctx.mkSolver(t)
Christian Müller's avatar
Christian Müller committed
41

Christian Müller's avatar
Christian Müller committed
42
43
44
    this.ctx = ctx
    this.s = s
  }
Christian Müller's avatar
Christian Müller committed
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76

  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
Christian Müller's avatar
Christian Müller committed
77
78
79
80
81
82
83
84
  }

  override def afterEach() = {
    ctx.close()
  }

  def check(s: Solver, res: Status) = {
    val c = s.check()
Christian Müller's avatar
Christian Müller committed
85
86
87
    if (c == Status.UNKNOWN) {
      println(s"Z3 status unknown: ${s.getReasonUnknown()}")
    }
Christian Müller's avatar
Christian Müller committed
88
    c should be(res)
Christian Müller's avatar
Christian Müller committed
89
    if (res == Status.SATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
90
      println(s"Z3 model:\n${s.getModel()}")
Christian Müller's avatar
Christian Müller committed
91
92
    }
  }
Eugen Zalinescu's avatar
Eugen Zalinescu committed
93

Christian Müller's avatar
Christian Müller committed
94
95
  "Z3" should "check Globally" in {
    val easyForm = Globally(And(Fun("p", List()), Globally(Fun("p", List()))))
Christian Müller's avatar
Christian Müller committed
96

Christian Müller's avatar
Christian Müller committed
97
98
99
    s.add(toZ3.translate(easyForm, ctx))
    check(s, Status.SATISFIABLE)
  }
Christian Müller's avatar
Christian Müller committed
100

Christian Müller's avatar
Christian Müller committed
101
102
  it should "check small things" in {
    val easyForm = Forall(List("x", "s"), Neg(Fun("R", List("x", "s"))))
Eugen Zalinescu's avatar
Eugen Zalinescu committed
103

Christian Müller's avatar
Christian Müller committed
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
    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)
  }
Christian Müller's avatar
Christian Müller committed
125

Christian Müller's avatar
Christian Müller committed
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
  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
  }
Eugen Zalinescu's avatar
Eugen Zalinescu committed
144

Eugen Zalinescu's avatar
Eugen Zalinescu committed
145
  // NOTE: next 3 formulas are from "On finite domains in FOLTL" ATVA2016
146

Christian Müller's avatar
Christian Müller committed
147
  it should "check infinite models 1" in {
148

Christian Müller's avatar
Christian Müller committed
149
150
151
152
    val f = Globally(Exists("x", And(
      Fun("p", "x"),
      Next(Globally(Neg(Fun("p", "x")))))))
    println(f)
Eugen Zalinescu's avatar
Eugen Zalinescu committed
153

Christian Müller's avatar
Christian Müller committed
154
155
156
157
    s.add(toZ3.translate(f, ctx))
    // check(s,c,Status.SATISFIABLE) // only on infinite domains
    check(s, Status.UNSATISFIABLE) // only on finite domains
  }
Eugen Zalinescu's avatar
Eugen Zalinescu committed
158

Christian Müller's avatar
Christian Müller committed
159
  it should "check infinite models 2" in {
160

Christian Müller's avatar
Christian Müller committed
161
162
163
164
165
166
167
168
    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)
Christian Müller's avatar
Christian Müller committed
169

Christian Müller's avatar
Christian Müller committed
170
171
172
173
    s.add(toZ3.translate(f, ctx))
    // check(s,c,Status.SATISFIABLE) // only on infinite domains
    check(s, Status.UNSATISFIABLE) // only on finite domains
  }
Christian Müller's avatar
Christian Müller committed
174

Christian Müller's avatar
Christian Müller committed
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
  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)
  }
Christian Müller's avatar
Christian Müller committed
194
195

  it should "check tests/simpleChoiceTyped (nonomitting, stubborn) as LTL prop" in {
Christian Müller's avatar
Christian Müller committed
196
197
198
    val s = checkNonOmittingWF(ExampleWorkflows.parseExample("tests/simpleChoiceTyped").get)
    check(s, Status.SATISFIABLE)
  }
Christian Müller's avatar
Christian Müller committed
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220

  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 {
Christian Müller's avatar
Christian Müller committed
221
    val s = checkNonOmittingWF(ExampleWorkflows.parseExample("tests/simpleChoiceNoOracle").get)
Christian Müller's avatar
Christian Müller committed
222
    check(s, Status.UNSATISFIABLE) // takes > 60s
Christian Müller's avatar
Christian Müller committed
223
  }
Christian Müller's avatar
Christian Müller committed
224
225

  it should "check tests/loopexample (nonomitting, stubborn) as LTL prop" ignore {
Christian Müller's avatar
Christian Müller committed
226
    val s = checkNonOmittingWF(ExampleWorkflows.parseExample("tests/loopexample").get)
Christian Müller's avatar
Christian Müller committed
227
    check(s, Status.SATISFIABLE) // takes > 60s
Christian Müller's avatar
Christian Müller committed
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
  }

  //  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())
  //  }
247
}
Eugen Zalinescu's avatar
Eugen Zalinescu committed
248
249

// TODO: set domain size from the test?