Commit 0965fd1e authored by Christian Müller's avatar Christian Müller

inference

parent e7a605d5
......@@ -20,10 +20,13 @@ object MainInvariantsInference extends App with LazyLogging {
logger.info(s"Encoding Spec:\n$spec")
def invariant =
InvariantGenerator.invariantNoninterSingleBS _
// InvariantGenerator.invariantNoninterSingleBS _
// InvariantGenerator.invariantNoninterStubbornBS _
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
(_:Spec) => Forall(List("x","p"), Fun("Assign", List("x", "p")) --> Neg(Fun("Conf", List("x", "p")))).in(Properties.T1)
// TODO: Add single trace properties
val props = InvProperties(
stubborn = true,
......
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