Commit 305343f5 authored by Christian Müller's avatar Christian Müller

fix iteration, add test

parent 5acbb2b7
...@@ -103,6 +103,7 @@ object InvariantChecker extends LazyLogging { ...@@ -103,6 +103,7 @@ object InvariantChecker extends LazyLogging {
// check if done, i.e. all edges proven // check if done, i.e. all edges proven
val toProve = (graph.edges -- proven) val toProve = (graph.edges -- proven)
if (toProve.isEmpty) { if (toProve.isEmpty) {
logger.info("Everything proven. Terminating.")
Some(labels) Some(labels)
} else { } else {
...@@ -116,7 +117,8 @@ object InvariantChecker extends LazyLogging { ...@@ -116,7 +117,8 @@ object InvariantChecker extends LazyLogging {
if (status == Status.UNSATISFIABLE) { if (status == Status.UNSATISFIABLE) {
// Negation of implication unsat // Negation of implication unsat
// --> safe, continue with larger proven set // --> safe, continue with larger proven set.
logger.info(s"Proven inductiveness for (${next._1} -> ${next._2}).")
checkInvariantRec(labels, proven + next) checkInvariantRec(labels, proven + next)
} else { } else {
// Negation of implication sat // Negation of implication sat
...@@ -132,6 +134,7 @@ object InvariantChecker extends LazyLogging { ...@@ -132,6 +134,7 @@ object InvariantChecker extends LazyLogging {
// Negation of newinv still unsat, newinv still sat // Negation of newinv still unsat, newinv still sat
checkInvariantRec(newlabels, newproven) checkInvariantRec(newlabels, newproven)
} else { } else {
logger.info("New invariant not satisfiable. Terminating.")
None None
} }
} }
......
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