Commit 81b7e2b3 authored by Christian Müller's avatar Christian Müller
Browse files

add error messages

parent 4351dd62
...@@ -131,6 +131,6 @@ object Main extends App with LazyLogging { ...@@ -131,6 +131,6 @@ object Main extends App with LazyLogging {
// clear() // clear()
// generateExample("omitting/conference") // generateExample("omitting/conference")
generateExample("tests/declasstest") // generateExample("tests/declasstest")
// generateAllExamples() generateAllExamples()
} }
\ No newline at end of file
...@@ -23,6 +23,10 @@ object FOLTL { ...@@ -23,6 +23,10 @@ object FOLTL {
case _: BinOp => "(" + this + ")" case _: BinOp => "(" + this + ")"
case _ => this.toString() case _ => this.toString()
} }
def (f2:Formula) = Implies(this, f2)
def (f2:Formula) = And(this, f2)
def (f2:Formula) = Or(this, f2)
def pretty(): String = { def pretty(): String = {
val s = this.toString val s = this.toString
......
...@@ -27,7 +27,6 @@ object InvariantChecker extends LazyLogging { ...@@ -27,7 +27,6 @@ object InvariantChecker extends LazyLogging {
val cfg = new HashMap[String, String]() val cfg = new HashMap[String, String]()
cfg.put("timeout", TIMEOUT.toString()) cfg.put("timeout", TIMEOUT.toString())
val ctx = new Context(cfg) val ctx = new Context(cfg)
// val t = ctx.andThen(ctx.mkTactic("qe"), ctx.mkTactic("smt"))
val s = ctx.mkSolver() val s = ctx.mkSolver()
s.add(toZ3.translate(f, ctx)) s.add(toZ3.translate(f, ctx))
...@@ -76,8 +75,8 @@ object InvariantChecker extends LazyLogging { ...@@ -76,8 +75,8 @@ object InvariantChecker extends LazyLogging {
if (res == Status.SATISFIABLE) { if (res == Status.SATISFIABLE) {
msg ++= "Satisfying model:\n" msg ++= "Satisfying model:\n"
msg ++= toZ3.printModel(solver.getModel()) msg ++= toZ3.printModel(solver.getModel())
} else { } else if (res == Status.UNKNOWN) {
msg ++= s"Z3 result: $res\n" msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
} }
msg ++= "\n" msg ++= "\n"
logger.info(s"Could not prove invariant $inv") logger.info(s"Could not prove invariant $inv")
...@@ -113,7 +112,7 @@ object InvariantChecker extends LazyLogging { ...@@ -113,7 +112,7 @@ object InvariantChecker extends LazyLogging {
Forall(quant, genEq(r, agent :: quant)) Forall(quant, genEq(r, agent :: quant))
}) })
Forall(agent, Implies(premise, conclusion)).simplify() Forall(agent, premise conclusion).simplify()
} }
} }
\ No newline at end of file
...@@ -8,6 +8,11 @@ import de.tum.workflows.foltl.FOLTL._ ...@@ -8,6 +8,11 @@ import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.Implicits._ import de.tum.workflows.Implicits._
class FOLTLTest extends FlatSpec { class FOLTLTest extends FlatSpec {
"Formulas" should "be constructed correctly" in {
True Var("x") should be (Implies(True, Var("x")))
}
"Formula functions" should "generate inequalities" in { "Formula functions" should "generate inequalities" 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