Skip to content

N
NIWO
Commit 19b3239c authored by Christian Müller's avatar Christian Müller
Browse files
Options

src

parent b410e6bf
Hide whitespace changes
Inline Side-by-side
Showing with 569 additions and 274 deletions
src/main/scala/de/tum/workflows/MainInvariantsInference.scala
View file @ 19b3239c
package de.tum.workflows
import com.typesafe.scalalogging.LazyLogging
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils._
......@@ -24,116 +25,18 @@ object MainInvariantsInference extends App with LazyLogging {
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
val props = InvProperties(stubborn = false, eliminateAux = false)
val props = InvProperties(
stubborn = true,
eliminateAux = true,
eliminateB = true
)
val inv = invariant(spec)
val (res, graph, labels, t) = InvariantChecker.checkInvariantFPHeadLabel(spec, inv, props)
logger.info(s"Invariant was ${inv}")
logger.info(s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n")
logger.info(s"Graph: $graph")
val src = 0
val headlabel = labels(graph.get(src))
// Invariant not valid
if (!res) {
// Try to break headlabel invariant
val (status, solver) = Z3QFree.checkUniversal(headlabel)
if (status == Status.SATISFIABLE) {
// Broken, found model
// logger.info(s"Model:\n${Z3.printModel(solver.getModel())}")
logger.info(s"State Invariant: ${headlabel}")
val z3model = Z3QFree.modelFacts(solver.getModel())
// make facts
// filter only workflow rels
// val relfacts = model
logger.info(s"Z3model: $z3model")
val facts = for ((f, b) <- z3model) yield {
if (b == True) {
f
} else {
Neg(f)
}
}
logger.info(s"Model Facts: ${facts}")
val vars = z3model.flatMap { case (f:Fun,b:Formula) => f.freeVars }.distinct
val groupedvars = vars.groupBy { _.typ }
// These should only contain Choice and Oracle predicates
val state = Model.emptystate(spec, groupedvars, props)
val model = Model(groupedvars, And.make(facts), state)
logger.info(s"Initial Model: ${model.prettyprint()}")
// get path
val source = graph.get(0)
val target = graph.get(tar)
val path = source.shortestPathTo(target).get // Has to be connected
logger.info(s"Path from source to target: $path")
val newmodel = path.edges.foldLeft(model)((m, e) => m.warp(e, spec, props))
logger.info(s"Warped Model: ${newmodel.prettyprint}")
val inv = labels(target)
val neginv = inv.toNegNf.simplify
logger.info(s"Invariant before: $neginv")
// Instantiate inv for given universe
val instinv = FOTransformers.eliminateUniversals(neginv, vars)
logger.info(s"Invariant instantiated: $instinv")
// Put steering into instInv
val z3map = z3model.toMap
val steeredinv = instinv.everywhere {
case f:Fun if z3map.contains(f) => z3map(f)
}
val steeredInfinv = steeredinv.assumeEmpty(Properties.INFNAME)
// just for testing
val tocheck = List("Assign")
val modelmap = for ((f, vs) <- newmodel.state; v <- vs if !tocheck.contains(f.name)) yield {
v match {
case Neg(f) => (f, False)
case f:Fun => (f, True)
}
}
val modelinv = steeredInfinv.everywhere {
case f:Fun if modelmap.contains(f) => modelmap(f)
}
// val easyinv = modelinv.simplify()
val easyinv = steeredInfinv.simplify()
logger.info(s"inv: $easyinv")
val itp = Z3QFree.interpolate(newmodel.stateFormula(), easyinv)
logger.info(s"Interpolant is ${itp.get.toNegNf}")
// logger.info(s"Model for itp is ${Z3.printModel(Z3QFree.checkSatQFree(itp.get).get)}")
// val (s, satisfy) = Z3QFree.checkUniversal(Neg(easyinv))
// logger.info(s"Model: ${Z3.printModel(satisfy.getModel)}")
} else {
logger.error("Invariant not valid, but also not satisfiable.")
}
}
}
......@@ -148,18 +51,18 @@ object MainInvariantsInference extends App with LazyLogging {
spec.foreach(generate(name, _, target))
}
// def generateAllExamples() {
// clear()
// // Fill results alphabetically
// for (k <- ExampleWorkflows.examples.keys.toList.sorted) {
// generateExample(k)
// }
// }
// def generateAllExamples() {
// clear()
// // Fill results alphabetically
// for (k <- ExampleWorkflows.examples.keys.toList.sorted) {
// generateExample(k)
// }
// }
// clear()
// clear()
// generateExample("nonomitting/conference")
// generateExample("tests/conference_linear_small", 1)
generateExample("nonomitting/conference_linear", 2)
// generateExample("tests/loopexampleNoOracle")
generateExample("tests/conference_linear_small", 1)
// generateExample("nonomitting/conference_linear", 2)
// generateExample("tests/loopexampleNoOracle")
// generateAllExamples()
}
\ No newline at end of file
}
src/main/scala/de/tum/workflows/MainInvariantsInterpolation.scala 0 → 100644
View file @ 19b3239c
package de.tum.workflows
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils._
import de.tum.workflows.blocks.{SimpleBlock, Spec}
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.FOTransformers
import de.tum.workflows.synth.Model
import de.tum.workflows.toz3._
import de.tum.workflows.foltl.Properties
// Labelled Edge to Block
import Implicits._
object MainInvariantsInterpolation extends App with LazyLogging {
def generate(name: String, spec: Spec, tar:Int) {
logger.info(s"Encoding Spec:\n$spec")
def invariant =
InvariantGenerator.invariantNoninterSingleBS _
// InvariantGenerator.invariantNoninterStubbornBS _
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
val props = InvProperties(stubborn = false, eliminateAux = true)
val inv = invariant(spec)
val (res, graph, labels, t) = InvariantChecker.checkInvariantFPHeadLabel(spec, inv, props)
logger.info(s"Invariant was ${inv}")
logger.info(s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n")
logger.info(s"Graph: $graph")
val src = 0
val headlabel = labels(graph.get(src))
// Invariant not valid
if (!res) {
// Try to break headlabel invariant
val (status, solver) = Z3QFree.checkUniversal(headlabel)
if (status == Status.SATISFIABLE) {
// Broken, found model
// logger.info(s"Model:\n${Z3.printModel(solver.getModel())}")
logger.info(s"State Invariant: ${headlabel}")
val z3model = Z3QFree.modelFacts(solver.getModel())
// make facts
// filter only workflow rels
// val relfacts = model
logger.info(s"Z3model: $z3model")
val facts = for ((f, b) <- z3model) yield {
if (b == True) {
f
} else {
Neg(f)
}
}
logger.info(s"Model Facts: ${facts}")
val vars = z3model.flatMap { case (f:Fun,b:Formula) => f.freeVars }.distinct
val groupedvars = vars.groupBy { _.typ }
// These should only contain Choice and Oracle predicates
val state = Model.emptystate(spec, groupedvars, props)
val model = Model(groupedvars, And.make(facts), state)
logger.info(s"Initial Model: ${model.prettyprint()}")
// get path
val source = graph.get(0)
val target = graph.get(tar)
val path = source.shortestPathTo(target).get // Has to be connected
logger.info(s"Path from source to target: $path")
val newmodel = path.edges.foldLeft(model)((m, e) => m.warp(e, spec, props))
logger.info(s"Warped Model: ${newmodel.prettyprint}")
val inv = labels(target)
val neginv = inv.toNegNf.simplify
logger.info(s"Invariant before: $neginv")
// Instantiate inv for given universe
val instinv = FOTransformers.eliminateUniversals(neginv, vars)
logger.info(s"Invariant instantiated: $instinv")
// Put steering into instInv
val z3map = z3model.toMap
val steeredinv = instinv.everywhere {
case f:Fun if z3map.contains(f) => z3map(f)
}
val steeredInfinv = steeredinv.assumeEmpty(Properties.INFNAME)
// just for testing
val tocheck = List("Assign")
val modelmap = for ((f, vs) <- newmodel.state; v <- vs if !tocheck.contains(f.name)) yield {
v match {
case Neg(f) => (f, False)
case f:Fun => (f, True)
}
}
val modelinv = steeredInfinv.everywhere {
case f:Fun if modelmap.contains(f) => modelmap(f)
}
// val easyinv = modelinv.simplify()
val easyinv = steeredInfinv.simplify()
logger.info(s"inv: $easyinv")
val itp = Z3QFree.interpolate(newmodel.stateFormula(), easyinv)
logger.info(s"Interpolant is ${itp.get.toNegNf}")
// logger.info(s"Model for itp is ${Z3.printModel(Z3QFree.checkSatQFree(itp.get).get)}")
// val (s, satisfy) = Z3QFree.checkUniversal(Neg(easyinv))
// logger.info(s"Model: ${Z3.printModel(satisfy.getModel)}")
} else {
logger.error("Invariant not valid, but also not satisfiable.")
}
}
}
def generateExample(name: String, target: Int) {
logger.info(s"Generating $name")
val spec = ExampleWorkflows.parseExample(name)
if (spec.isEmpty) {
logger.error(s"Not a valid spec: $name")
}
spec.foreach(generate(name, _, target))
}
// def generateAllExamples() {
// clear()
// // Fill results alphabetically
// for (k <- ExampleWorkflows.examples.keys.toList.sorted) {
// generateExample(k)
// }
// }
// clear()
// generateExample("nonomitting/conference")
generateExample("tests/conference_linear_small", 1)
// generateExample("nonomitting/conference_linear", 2)
// generateExample("tests/loopexampleNoOracle")
// generateAllExamples()
}
\ No newline at end of file
src/main/scala/de/tum/workflows/Preconditions.scala
View file @ 19b3239c
......@@ -178,6 +178,19 @@ object Preconditions extends LazyLogging {
} else {
universalinv
}
// Win game
val bless = if (properties.eliminateB) {
val bs = (auxless.collect {
// FIXME: better recognition of Bs
case Fun(name, _, _) if name.startsWith("B") => List(name)
}).toSet
val eliminv = bs.foldRight(universalinv)((b, inv) => FOTransformers.eliminateBPredicate(inv, b)._1)
eliminv
} else {
universalinv
}
auxless.simplify()
}
}
\ No newline at end of file
src/main/scala/de/tum/workflows/Utils.scala
View file @ 19b3239c
......@@ -11,6 +11,7 @@ import com.typesafe.scalalogging.LazyLogging
object Utils extends LazyLogging {
val RESULTSFOLDER = "results"
val DEBUG_MODE = true
def mkString[T](string: Iterable[T], start: String, mid: String, end: String) = {
if (string.isEmpty) "" else string.mkString(start, mid, end)
......
src/main/scala/de/tum/workflows/foltl/FOLTL.scala
View file @ 19b3239c
package de.tum.workflows.foltl
import de.tum.workflows.Utils
import de.tum.workflows.foltl.FOLTL.FunFromVar
import de.tum.workflows.foltl.FOLTL.FunFromVar.getVars
import scala.annotation.tailrec
//import de.tum.workflows.foltl.TermFunctions._
......@@ -25,6 +28,7 @@ object FOLTL {
def toCNF: Formula = FormulaFunctions.toCNF(this)
lazy val isBS: Boolean = FormulaFunctions.isBS(this)
lazy val isUniversal: Boolean = FormulaFunctions.isU(this)
lazy val isQFree: Boolean = FormulaFunctions.isQFree(this)
def removeOTQuantifiers(): Formula = FormulaFunctions.removeOTQuantifiers(this)
......@@ -41,7 +45,7 @@ object FOLTL {
def land(f2: Formula) = And(this, f2)
def /\(f2: Formula) = And(this, f2)
def ∧(f2: Formula) = And(this, f2)
def lor(f2: Formula) = And(this, f2)
def lor(f2: Formula) = Or(this, f2)
def ∨(f2: Formula) = Or(this, f2)
def \/(f2: Formula) = Or(this, f2)
......@@ -82,6 +86,17 @@ object FOLTL {
object Fun {
def apply(name: String, params: List[Var]): Fun = Fun(name, None, params)
}
object FunNameFromVar {
val PredicateNoParam = "([a-zA-Z0-9]+)(#([a-zA-Z0-9]+))?".r
def unapply(s: String): Option[(String, Option[String])] = {
s match {
case PredicateNoParam(name, null, _*) => Some((name, None))
case PredicateNoParam(name, _, ind, _*) => Some((name, Some(ind)))
case _ => None
}
}
}
object FunFromVar {
val Predicate = "([a-zA-Z0-9]+)(#([a-zA-Z0-9]+))?((_[a-zA-Z0-9]+#[a-zA-Z0-9]+)*)".r
......@@ -118,6 +133,10 @@ object FOLTL {
val tup = params.map(p => p.name + "#" + p.typ)
Var(name + pi + Utils.mkString(tup, "_", "_", ""))
}
def encodeName() = {
val pi = if (ind.isDefined) "#" + ind.get else ""
name + pi
}
}
trait Quantifier extends Formula {
......
src/main/scala/de/tum/workflows/foltl/FOTransformers.scala
View file @ 19b3239c
package de.tum.workflows.foltl
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.toz3.Z3BSFO
object FOTransformers extends LazyLogging {
......@@ -50,19 +52,73 @@ object FOTransformers extends LazyLogging {
}
def eliminateAuxiliaryPredicate(f:Formula, AUX:String) = {
val (quantifiers, clauses) = FormulaFunctions.toCNFClauses(f)
// TODO: improve
val form = And.make(clauses.map(Or.make))
val newform = quantifiers.foldRight(form)((q, inner) => if(q._1) Exists(q._2, inner) else Forall(q._2, inner))
logger.info(s"Eliminating universal second order predicate $AUX")
val cnf = f.toCNF
// TODO: add equalities?
val repld = newform everywhere {
val repld = cnf everywhere {
case Neg(Fun(AUX, _, _)) => False
case Fun(AUX, _, _) => False
}
// TODO: improve runtime here
repld.toCNF.simplify()
repld.simplify()
}
def eliminateBPredicate(f:Formula, B:String) = {
// SOQE: \exists B. f <-> f'
logger.info(s"Eliminating existential second order predicate $B")
if (!f.isUniversal) {
logger.error("Trying to use SOQE on a non-universal formula")
}
val (quantifiers, clauses) = FormulaFunctions.toCNFClauses(f)
// Group clauses by positive/negative occurences
def ispositive(clause: List[Formula]) =
clause.exists {
case Fun(B, _, _) => true
case _ => false
}
def isnegative(clause: List[Formula]) =
clause.exists {
case Neg(Fun(B, _, _)) => true
case _ => false
}
def pruneBs(clause: List[Formula]) = {
clause.filterNot {
case Neg(Fun(B, _, _)) => true
case Fun(B, _, _) => true
case _ => false
}
}
val E = clauses.filter(c => !ispositive(c) && !isnegative(c))
val F = clauses.filter(c => ispositive(c) && !isnegative(c))
val G = clauses.filter(c => isnegative(c) && !ispositive(c))
val H = clauses.filter(c => ispositive(c) && isnegative(c))
if (H.nonEmpty) {
logger.warn("BSFO SOQE: H is not empty, Ackermann not applicable")
}
val fE = And.make(E.map(c => Or.make(pruneBs(c))))
val fF = And.make(F.map(c => Or.make(pruneBs(c))))
val fG = And.make(G.map(c => Or.make(pruneBs(c))))
val felim:Formula = fE /\ (fF \/ fG)
val fsol:Formula = fG
// wrap quantifiers around
// FIXME: add equalities
val felimq = quantifiers.foldRight(felim)((q, inner) => if (q._1) Exists(q._2, inner) else Forall(q._2, inner))
val fsolq = quantifiers.foldRight(fsol)((q, inner) => if (q._1) Exists(q._2, inner) else Forall(q._2, inner))
val z3fsolq = Z3BSFO.simplifyBS(fsolq)
if (Utils.DEBUG_MODE) {
logger.info(s"BSFO SOQE: strategy for $B: $z3fsolq")
}
(Z3BSFO.simplifyBS(felimq), z3fsolq)
}
/**
......
src/main/scala/de/tum/workflows/foltl/FormulaFunctions.scala
View file @ 19b3239c
......@@ -3,6 +3,8 @@ package de.tum.workflows.foltl
import FOLTL._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.blocks.Workflow
import de.tum.workflows.toz3.Z3BSFO
import scala.annotation.tailrec
object FormulaFunctions extends LazyLogging {
......@@ -101,8 +103,8 @@ object FormulaFunctions extends LazyLogging {
case Exists(vars1, Exists(vars2, f)) => Exists(vars1 ++ vars2, f)
// Remove variables from quantifiers if not used in the body: Caution - expensive
// case Quantifier(qmake, xs, t) if !(xs.toSet -- t.freeVars()).isEmpty =>
// qmake((xs.toSet.intersect(t.freeVars())).toList, t)
case Quantifier(qmake, xs, t) if (xs.toSet -- t.freeVars).nonEmpty =>
qmake(xs.toSet.intersect(t.freeVars).toList, t)
//
// // Split off binops from quantifiers
// case Quantifier(qmake, xs, BinOp(make, t1, t2)) if (t1.freeVars().intersect(xs.toSet)).isEmpty =>
......@@ -119,31 +121,37 @@ object FormulaFunctions extends LazyLogging {
everywhereBotUp(simp, t)
}
def pushQuantifiers(f: Formula): Formula = {
f everywhere {
case Forall(vars, BinOp(make, f1, f2)) if {
val leftvars = f1.freeVars
val rightvars = f2.freeVars
val varset = vars.toSet
val onlyleft = leftvars.intersect(varset) -- rightvars
val onlyright = rightvars.intersect(varset) -- leftvars
!onlyleft.isEmpty || !onlyright.isEmpty
} => {
val leftvars = f1.freeVars
val rightvars = f2.freeVars
val varset = vars.toSet
val bothvars = leftvars.intersect(rightvars).intersect(varset)
val onlyleft = leftvars.intersect(varset) -- rightvars
val onlyright = rightvars.intersect(varset) -- leftvars
Forall.make(
bothvars.toList,
make(
pushQuantifiers(Forall.make(onlyleft.toList, f1)),
pushQuantifiers(Forall.make(onlyright.toList, f2))))
def pushUniversalQuantifiers(f: Formula): Formula = {
def push(f:Formula):Formula = {
f everywhere {
case Forall(vars, BinOp(make, f1, f2)) if {
val leftvars = f1.freeVars
val rightvars = f2.freeVars
val varset = vars.toSet
val onlyleft = leftvars.intersect(varset) -- rightvars
val onlyright = rightvars.intersect(varset) -- leftvars
!onlyleft.isEmpty || !onlyright.isEmpty
} => {
val leftvars = f1.freeVars
val rightvars = f2.freeVars
val varset = vars.toSet
val bothvars = leftvars.intersect(rightvars).intersect(varset)
val onlyleft = leftvars.intersect(varset) -- rightvars
val onlyright = rightvars.intersect(varset) -- leftvars
Forall.make(
bothvars.toList,
make(
push(Forall.make(onlyleft.toList, f1)),
push(Forall.make(onlyright.toList, f2))))
}
}
}
if (!f.isUniversal) {
logger.error("Trying to push universal quantifiers inside non-universal formula")
}
push(f).simplify()
}
def eliminateImplication(f: Formula): Formula = {
......@@ -376,7 +384,7 @@ object FormulaFunctions extends LazyLogging {
val ex1 = q1.takeWhile(_._1)
val rest1 = q1.drop(ex1.size)
// filter out same bound variables (TODO: could be improved if different names)
// filter out same bound variables (TODO: could be improved if different names) (FIXME: Is this even correct?)
val existbound = ex1.flatMap(_._2)
val univbound = rest1.flatMap(_._2)
......@@ -413,6 +421,12 @@ object FormulaFunctions extends LazyLogging {
}
}
def isU(formula:Formula): Boolean = {
!formula.toNegNf.hasSubFormula {
case e:Exists => true
}
}
def isQFree(formula: Formula): Boolean = {
!formula.hasSubFormula {
case q: Quantifier => true
......@@ -472,15 +486,29 @@ object FormulaFunctions extends LazyLogging {
// TODO: make sure no quantifiers in scope of others with same name
def toPrenex(f: Formula): Formula = {
val negnf = f.toNegNf
// val (simp, boundVars) = fixBinding(negnf, Set())
// TODO: test fix bindings
val (simp, boundVars) = fixBinding(negnf, Set())
// val simp = negnef
// Simplify first to push negation inward
val quants = collectQuantifiers(negnf)
val stripped = stripQuantifiers(negnf)
val quants = collectQuantifiers(simp)
val stripped = stripQuantifiers(simp)
quants.foldRight(stripped)((quant, inner) => {
rewrapQuantifiers(quants, stripped)
}
def rewrapQuantifiers(quantifiers: List[(Boolean, List[Var])], f:Formula) = {
val wrapped = quantifiers.foldRight(f)((quant, inner) => {
if (quant._1) Exists(quant._2, inner) else Forall(quant._2, inner)
}).simplify()
// if all universal, push them inward
if (quantifiers.forall(!_._1)) {
FormulaFunctions.pushUniversalQuantifiers(wrapped)
} else {
wrapped
}
}
def toCNFClauses(f: Formula) = {
......@@ -493,55 +521,61 @@ object FormulaFunctions extends LazyLogging {
if (!changed) sub else toCNFSub(sub)
}
if (f.isUniversal) {
Z3BSFO.toCNFClausesUniversal(f)
} else {
logger.warn("Using internal CNF conversion - may blow up")
// FIXME: can we do it without prenex? may be expensive later on
val normalized = f.toNegNf.simplify().toPrenex.simplify()
logger.debug(s"Computing CNF of prenex formula of opsize ${normalized.opsize}")
// FIXME: can we do it without prenex? may be expensive later on
val normalized = f.toPrenex.simplify()
logger.debug(s"Computing CNF of prenex formula of opsize ${normalized.opsize}")
// normalized is now Quantifiers, then only And/Or with Negation inside
// no simplification here
val cnf1 = toCNFSub(normalized)
val cnf2 = everywhereBotUp({
case Or(And(f1, f2), f3) => And(Or(f1, f3), Or(f2, f3))
case Or(f1, And(f2, f3)) => And(Or(f1, f2), Or(f1, f3))
}, normalized)
// normalized is now Quantifiers, then only And/Or with Negation inside
// no simplification here
val cnf1 = toCNFSub(normalized)
val cnf2 = everywhereBotUp({
case Or(And(f1, f2), f3) => And(Or(f1, f3), Or(f2, f3))
case Or(f1, And(f2, f3)) => And(Or(f1, f2), Or(f1, f3))
}, normalized)
val quantifiers = FormulaFunctions.collectQuantifiers(cnf1)
val quantifiers = FormulaFunctions.collectQuantifiers(cnf1)
// Inspect clauses
val clauses = FOTransformers.collectClauses(cnf1)
// Inspect clauses
val clauses = FOTransformers.collectClauses(cnf1)
// TODO: improve, don't sort by tostring
val sorted = clauses.map(c => c.sortBy(_.toString())).sortBy(f => f.toString())
// Simplify clauses
// TODO: improve, don't sort by tostring
val sorted = clauses.map(c => c.sortBy(_.toString())).sortBy(f => f.toString())
logger.debug(s"Computing CNF of a formula with ${sorted.size} clauses")
logger.debug(s"Computing CNF of a formula with ${sorted.size} clauses")
// Remove trivial clauses