Commit e59e0ae8 authored by Eugen Zalinescu's avatar Eugen Zalinescu

Term -> Formula; plus advances towards translation to Z3

parent 94384fd3
package de.tum.workflows.ltl.tests;
import org.scalatest._
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
class Z3Test extends FlatSpec {
val p = Fun("p", List())
"Z3" should "work" in {
val easyForm = Globally(And(p, Globally(p)))
val cfg = new HashMap[String, String]();
cfg.put("model", "true");
val ctx = new Context(cfg);
val bexpr = toZ3.toZ3(ctx, easyForm, ctx.mkInt(0), 0)
println(bexpr)
val s = ctx.mkSolver()
s.add(bexpr)
val c = s.check()
c should be(Status.SATISFIABLE)
println(s.getModel())
}
}
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