Commit 02fbf6ec authored by Christian Müller's avatar Christian Müller

indentation, alleqal inv

parent 9efcecbe
...@@ -117,11 +117,16 @@ object Main extends App with LazyLogging { ...@@ -117,11 +117,16 @@ object Main extends App with LazyLogging {
if (checkinvariants) { if (checkinvariants) {
def invariants = List( def invariants = List(
timeNoninter _, InvariantChecker.invariantNoninterStubborn _,
timeAllEqual _ InvariantChecker.invariantAllEqual _
) )
def msgs = invariants.map(_(spec)) def msgs = for (inv <- invariants) yield {
val (t, (safe, msg)) = time {
InvariantChecker.checkInvariant(spec.w, inv(spec), true)
}
s"Proving Invariant (took $t ms):\n$msg\n"
}
write(s"$FOLDER/${name}.inv", msgs.mkString("\n")) write(s"$FOLDER/${name}.inv", msgs.mkString("\n"))
} }
......
...@@ -74,7 +74,7 @@ object InvariantChecker extends LazyLogging { ...@@ -74,7 +74,7 @@ object InvariantChecker extends LazyLogging {
msg ++= s"Possibly unsafe: Block may not uphold invariant:\n\n${e.label}\n\n" msg ++= s"Possibly unsafe: Block may not uphold invariant:\n\n${e.label}\n\n"
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()).lines.map(" " + _).mkString("\n")
} else if (res == Status.UNKNOWN) { } else if (res == Status.UNKNOWN) {
msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n" msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
} }
......
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