Skip to content

GitLab

Commit 2e9e706a authored by Christian Müller's avatar Christian Müller
Browse files

inspector

parent 7df195e7
Pipeline #1204 failed with stages
in 23 seconds
Hide whitespace changes
Inline Side-by-side
Showing with 187 additions and 109 deletions
examples/omitting/conference.spec
View file @ 2e9e706a
......@@ -5,19 +5,19 @@ forallmay x:A,p:P
forallmay x:A,p:P
!Conf(x,p) → Assign += (x,p)
forall x:A,p:P,r:R
(Assign(x,p) ∧ O(x,p,r)) → Review += (x,p,r)
(Assign(x,p) ∧ Oracle(x,p,r)) → Review += (x,p,r)
loop {
forall x:A,y:A,p:P,r:R (Assign(x,p) ∧ Review(y,p,r)) → Read += (x,r)
forall xa:A,xb:A,p:P,r:R (Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,r)
forallmay x:A,p:P,r:R (Assign(x,p)) → Review += (x,p,r)
}
Declassify
O(x:A,p:P,r:R): ¬ Conf(xt:A,p:P)
Oracle(x:A,p:P,r:R): ¬ Conf(xat:A,p:P)
Target
Read(xt:A, rt:R)
Read(xat:A, rt:R)
Causality
......
src/main/scala/de/tum/workflows/InvariantInspector.scala
View file @ 2e9e706a
......@@ -16,6 +16,7 @@ import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.toz3.InvariantGenerator
import de.tum.workflows.toz3.InvProperties
import de.tum.workflows.toz3.Z3QFree
object InvariantInspector extends App with LazyLogging {
......@@ -37,10 +38,39 @@ object InvariantInspector extends App with LazyLogging {
val (t, (res, dot)) = time {
// InvariantChecker.checkInvariantOnce(spec.w, inv(spec), true)
val props = InvProperties(stubborn = false, eliminateAux = true)
val (result, graph, afterlabels, proven, dot, time) =
InvariantChecker.checkInvariantFPLabelling(spec, invariant(spec), InvProperties.DEFAULT)
println(graph)
println(afterlabels.last)
InvariantChecker.checkInvariantFPLabelling(spec, invariant(spec), props)
// non-omitting conference linear inspection
val lastlabels = afterlabels.last
val inv = lastlabels(2)
val emptyinv = inv.assumeEmpty(List("informed", "Read", "Comm")).simplify()
logger.info(s"empty: ${emptyinv.pretty()}")
// val auxes = List("O", "choice2")
// Different Os
val diffos = emptyinv everywhere {
case Fun("O", Some(t), vars) => Fun(s"O$t", vars)
}
val auxes = List("Ot1", "Ot2")
// val auxes = List()
val auxless = auxes.foldLeft(diffos)((inv, p) =>
FOTransformers.eliminateAuxiliaryPredicate(inv, p)
)
val simped = auxless.toCNF.simplify()
logger.info(s"auxless: ${simped.pretty()}")
logger.info("Computing with B now")
val withB = simped everywhere {
case Fun("Assign",t,vars) => And(Fun("Assign",t,vars), Neg(Fun("B",vars)))
// case Fun("Assign",t,vars) => Fun("B",vars)
}
logger.info(s"withB: ${withB.simplify().pretty()}")
logger.info(s"withB CNF: ${withB.toCNF.simplify().pretty()}")
logger.info(s"Graph: $graph")
logger.info(s"Final Invariants:\n${afterlabels.last}")
(result, dot)
}
val msg = s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n"
......@@ -51,7 +81,7 @@ object InvariantInspector extends App with LazyLogging {
}
}
// inspect("omitting/conference")
inspect("tests/loopexampleNoOracle")
inspect("nonomitting/conference_linear")
// inspect("tests/loopexampleNoOracle")
// generateAllExamples()
}
\ No newline at end of file
src/main/scala/de/tum/workflows/foltl/FOTransformers.scala
View file @ 2e9e706a
......@@ -52,17 +52,8 @@ object FOTransformers extends LazyLogging {
def eliminateAuxiliaryPredicate(f:Formula, AUX:String) = {
val (quantifiers, clauses) = FormulaFunctions.toCNFClauses(f)
// Inspect clauses
val simped =
for (c <- clauses;
removeclause = (for (c1 <- c if (c.contains(Neg(c1)))) yield true)
if (removeclause.isEmpty)
) yield {
c
}
// TODO: improve
val form = And.make(simped.map(Or.make))
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))
// TODO: add equalities?
......@@ -70,8 +61,8 @@ object FOTransformers extends LazyLogging {
case Neg(Fun(AUX, _, _)) => False
case Fun(AUX, _, _) => False
}
repld.simplify()
// TODO: improve runtime here
repld.toCNF.simplify()
}
/**
......
src/main/scala/de/tum/workflows/foltl/FormulaFunctions.scala
View file @ 2e9e706a
......@@ -7,7 +7,6 @@ import scala.annotation.tailrec
object FormulaFunctions extends LazyLogging {
def freeVars(t: Formula) = {
def free(t: Formula, bound: Set[Var]): Set[Var] = {
t match {
......@@ -31,67 +30,66 @@ object FormulaFunctions extends LazyLogging {
def simplify(t: Formula): Formula = {
val simp: PartialFunction[Formula, Formula] = {
// Push negation inward
case Neg(Or(t1, t2)) => And(Neg(t1), Neg(t2))
case Neg(And(t1, t2)) => Or(Neg(t1), Neg(t2))
case Neg(Globally(t)) => Finally(Neg(t))
case Neg(Finally(t)) => Globally(Neg(t))
case Neg(Next(t)) => Next(Neg(t))
case Neg(Forall(vars, t)) => Exists(vars, Neg(t))
case Neg(Exists(vars, t)) => Forall(vars, Neg(t))
case Neg(Implies(t1, t2)) => And(t1, Neg(t2))
case Neg(Or(t1, t2)) => And(Neg(t1), Neg(t2))
case Neg(And(t1, t2)) => Or(Neg(t1), Neg(t2))
case Neg(Globally(t)) => Finally(Neg(t))
case Neg(Finally(t)) => Globally(Neg(t))
case Neg(Next(t)) => Next(Neg(t))
case Neg(Forall(vars, t)) => Exists(vars, Neg(t))
case Neg(Exists(vars, t)) => Forall(vars, Neg(t))
case Neg(Implies(t1, t2)) => And(t1, Neg(t2))
// Simple laws
case Neg(True) => False
case Neg(False) => True
case Neg(Neg(t)) => t
case Or(True, t) => True
case Or(t, True) => True
case Or(False, t) => t
case Or(t, False) => t
case And(False, t) => False
case And(t, False) => False
case And(True, t) => t
case And(t, True) => t
case Implies(False, t) => True
case Implies(True, t) => t
case Or(Neg(t1), t2) if t1 == t2 => True
case And(Neg(t1), t2) if t1 == t2 => False
case Or(t1, Neg(t2)) if t1 == t2 => True
case And(t1, Neg(t2)) if t1 == t2 => False
case Neg(True) => False
case Neg(False) => True
case Neg(Neg(t)) => t
case Or(True, t) => True
case Or(t, True) => True
case Or(False, t) => t
case Or(t, False) => t
case And(False, t) => False
case And(t, False) => False
case And(True, t) => t
case And(t, True) => t
case Implies(False, t) => True
case Implies(True, t) => t
case Or(Neg(t1), t2) if t1 == t2 => True
case And(Neg(t1), t2) if t1 == t2 => False
case Or(t1, Neg(t2)) if t1 == t2 => True
case And(t1, Neg(t2)) if t1 == t2 => False
// left-trees
case And(And(t1, t2), t3) => And(t1, And(t2, t3))
case Or(Or(t1, t2), t3) => Or(t1, Or(t2, t3))
case And(And(t1, t2), t3) => And(t1, And(t2, t3))
case Or(Or(t1, t2), t3) => Or(t1, Or(t2, t3))
// equal things in tree
case And(t1, t2) if t1 == t2 => t1
case Or(t1, t2) if t1 == t2 => t1
case And(t1, t2) if t1 == t2 => t1
case Or(t1, t2) if t1 == t2 => t1
case And(t1, And(t2, t3)) if (t1 == t2) => And(t1, t3)
case And(t1, And(t2, t3)) if (t1 == t3) => And(t1, t2)
case Or(t1, Or(t2, t3)) if (t1 == t2) => Or(t1, t3)
case Or(t1, Or(t2, t3)) if (t1 == t3) => Or(t1, t2)
case Or(t1, Or(t2, t3)) if (t1 == t2) => Or(t1, t3)
case Or(t1, Or(t2, t3)) if (t1 == t3) => Or(t1, t2)
// And Or
case And(t1, Or(t2, t3)) if (t1 == t3) => t1
case And(t1, Or(t2, t3)) if (t1 == t2) => t1
case And(Or(t2, t3), t1) if (t1 == t3) => t1
case And(Or(t2, t3), t1) if (t1 == t2) => t1
case And(t1, Or(t2, t3)) if (t1 == t3) => t1
case And(t1, Or(t2, t3)) if (t1 == t2) => t1
case And(Or(t2, t3), t1) if (t1 == t3) => t1
case And(Or(t2, t3), t1) if (t1 == t2) => t1
// case Or(t1, Neg(t2)) if t1 == t2 => True
// Equivalence
case Eq(t1, t2) if t1 == t2 => True
case Eq(t1, t2) if t1 == t2 => True
// Double Temporals
case Finally(Finally(t)) => Finally(t)
case Globally(Globally(t)) => Globally(t)
case Finally(Finally(t)) => Finally(t)
case Globally(Globally(t)) => Globally(t)
// Remove quantifiers if empty
case Quantifier(_, xs, t) if xs.isEmpty => t
case Quantifier(_, _, True) => True
case Quantifier(_, _, False) => False
case Quantifier(_, _, True) => True
case Quantifier(_, _, False) => False
// Quantifiers binding same things
case And(Forall(vars1, t1), Forall(vars2, t2)) if (vars1 == vars2) => Forall(vars1, And(t1, t2))
case Or(Forall(vars1, t1), Forall(vars2, t2)) if (vars1 == vars2) => Forall(vars1, Or(t1, t2))
......@@ -99,8 +97,8 @@ object FormulaFunctions extends LazyLogging {
case Or(Exists(vars1, t1), Exists(vars2, t2)) if (vars1 == vars2) => Exists(vars1, Or(t1, t2))
// Gobble up equal quantifiers
case Forall(vars1, Forall(vars2, f)) => Forall(vars1 ++ vars2, f)
case Exists(vars1, Exists(vars2, f)) => Exists(vars1 ++ vars2, f)
case Forall(vars1, Forall(vars2, f)) => Forall(vars1 ++ vars2, f)
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 =>
......@@ -111,13 +109,43 @@ object FormulaFunctions extends LazyLogging {
// make(t1, qmake(xs, t2))
// case Quantifier(qmake, xs, BinOp(make, t1, t2)) if (t2.freeVars().intersect(xs.toSet)).isEmpty =>
// make(qmake(xs, t1), t2)
// Declass seen often enough
case And(Or(f1, f2), Or(f3, f4)) if (f2 == f4 && f1 == Neg(f3).simplify()) => f2
}
// val (changed, t1) = everywhereFP(simp, t)
// if (!changed) t1 else simplify(t1)
// val (changed, t1) = everywhereFP(simp, t)
// if (!changed) t1 else simplify(t1)
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 eliminateImplication(f: Formula): Formula = {
f everywhere {
case Implies(f1, f2) => Or(Neg(eliminateImplication(f1)), eliminateImplication(f2))
......@@ -133,7 +161,7 @@ object FormulaFunctions extends LazyLogging {
}
}
}
def everywhereFP(trans: PartialFunction[Formula, Formula], t: Formula): (Boolean, Formula) = {
if (trans.isDefinedAt(t))
(true, trans(t))
......@@ -144,16 +172,16 @@ object FormulaFunctions extends LazyLogging {
val sub = everywhereFP(trans, t1)
(sub._1, make(ps, sub._2))
}
case UnOp(make, t1) => {
case UnOp(make, t1) => {
val sub = everywhereFP(trans, t1)
(sub._1, make(sub._2))
}
case BinOp(make, t1, t2) => {
case BinOp(make, t1, t2) => {
val (c1, sub1) = everywhereFP(trans, t1)
val (c2, sub2) = everywhereFP(trans, t2)
(c1 || c2, make(sub1, sub2))
}
case x => (false, x)
case x => (false, x)
}
}
......@@ -169,7 +197,7 @@ object FormulaFunctions extends LazyLogging {
case x => x
}
}
def everywhereBotUp(trans: PartialFunction[Formula, Formula], t: Formula): Formula = {
// First apply trans to push negation inward etc
if (trans.isDefinedAt(t))
......@@ -226,7 +254,7 @@ object FormulaFunctions extends LazyLogging {
}
}
def hasSubFormula(coll: PartialFunction[Formula, Boolean], t: Formula):Boolean = {
def hasSubFormula(coll: PartialFunction[Formula, Boolean], t: Formula): Boolean = {
def or(bs: Boolean*) = { bs.exists(identity) }
collect(or)(coll, t)
}
......@@ -347,33 +375,31 @@ object FormulaFunctions extends LazyLogging {
// TODO: merge universals with same type by renaming
val ex1 = q1.takeWhile(_._1)
val rest1 = q1.drop(ex1.size)
// filter out same bound variables (TODO: could be improved if different names)
val existbound = ex1.flatMap(_._2)
val univbound = rest1.flatMap(_._2)
val exset = existbound.toSet
val univset = univbound.toSet
val ex2 = q2.takeWhile(_._1).map(q =>
(q._1, q._2.filterNot(exset.contains))
)
(q._1, q._2.filterNot(exset.contains)))
val rest2 = q2.drop(ex2.size).map(q =>
(q._1, q._2.filterNot(univset.contains))
)
(q._1, q._2.filterNot(univset.contains)))
ex1 ++ ex2 ++ rest1 ++ rest2
}
}
}
def checkBindings(f:Formula) = {
def checkBindingsSub(f: Formula, bound:Set[Var]):List[Var] = {
f collect {
case Quantifier(make, xs, inner) => {
val conflicts = xs.filter(bound.contains)
conflicts ++ checkBindingsSub(inner, bound ++ xs)
}
def checkBindings(f: Formula) = {
def checkBindingsSub(f: Formula, bound: Set[Var]): List[Var] = {
f collect {
case Quantifier(make, xs, inner) => {
val conflicts = xs.filter(bound.contains)
conflicts ++ checkBindingsSub(inner, bound ++ xs)
}
}
}
checkBindingsSub(f, Set()).isEmpty
}
......@@ -389,16 +415,15 @@ object FormulaFunctions extends LazyLogging {
def isQFree(formula: Formula): Boolean = {
!formula.hasSubFormula {
case q:Quantifier => true
case q: Quantifier => true
}
}
def toNegNf(f: Formula) = {
// val bound = if (hasDuplicateBindings(f)) {
// // logger.info(s"Formula binds variables more than once - renaming bindings: ${f.pretty}")
// FormulaFunctions.fixBinding(f, Set())._1
// } else f
// val bound = if (hasDuplicateBindings(f)) {
// // logger.info(s"Formula binds variables more than once - renaming bindings: ${f.pretty}")
// FormulaFunctions.fixBinding(f, Set())._1
// } else f
val noeq = eliminateEq(f)
eliminateImplication(noeq).simplify()
}
......@@ -445,9 +470,9 @@ object FormulaFunctions extends LazyLogging {
}
// TODO: make sure no quantifiers in scope of others with same name
def toPrenex(f: Formula):Formula = {
def toPrenex(f: Formula): Formula = {
val negnf = f.toNegNf
// val (simp, boundVars) = fixBinding(negnf, Set())
// val (simp, boundVars) = fixBinding(negnf, Set())
// Simplify first to push negation inward
val quants = collectQuantifiers(negnf)
......@@ -478,25 +503,37 @@ object FormulaFunctions extends LazyLogging {
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)
// 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())
logger.debug(s"Computing CNF of a formula with ${sorted.size} clauses")
// Remove trivial clauses
val notrivials = sorted.filterNot(c => {
c.exists(f => c.contains(Neg(f)))
})
// TODO improve runtime
val simpedset = clauses.toSet
val simped = simpedset.filterNot(c => simpedset.exists(c2 => {
val simped = notrivials.filterNot(c => notrivials.exists(c2 => {
// check if c is superset of c2
c != c2 && c.startsWith(c2)
// c != c2 && c.startsWith(c2)
c != c2 && c.forall(f => c2.contains(f))
}))
(quantifiers, clauses)
logger.debug(s"After simplification ${simped.size} unsubsumed clauses remaining.")
(quantifiers, simped)
}
def toCNF(f:Formula) = {
val (quantifiers, clauses) = toCNFClauses(f)
def toCNF(f: Formula) = {
val (quantifiers, clauses) = toCNFClauses(f)
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))
val newform = quantifiers.foldRight(form)((q, inner) => if (q._1) Exists(q._2, inner) else Forall(q._2, inner))
newform
}
......
src/main/scala/de/tum/workflows/toz3/InvariantGenerator.scala
View file @ 2e9e706a
......@@ -42,6 +42,8 @@ object InvariantGenerator {
val conclusion = genEq(spec.target, spec.target.params)
Forall(spec.target.params, conclusion).simplify()
// Constants
// conclusion
}
// def invariantNoninterStubbornBS(spec: Spec) = {
......
src/test/scala/de/tum/workflows/tests/FOLTLTest.scala
View file @ 2e9e706a
......@@ -6,6 +6,7 @@ import org.scalatest.Inspectors._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.Implicits._
import de.tum.workflows.foltl.FOLTL
import de.tum.workflows.foltl.FormulaFunctions
class FOLTLTest extends FlatSpec {
"Formulas" should "be constructed correctly" in {
......@@ -150,4 +151,20 @@ class FOLTLTest extends FlatSpec {
))
)
}
it should "not fail at doing so" in {
val f = Forall(List("xt","pt","yt","p"), And.make(
Neg(Fun("B", List("xt","pt"))),
Neg(Fun("B", List("yt","p"))),
Neg(Fun("B", List("yt","pt"))),
Neg(Fun("Conf",Some("t1"),List("xt","p")))
))
f.toCNF should be (f)
}
"quantifier pushing" should "work" in {
val f = Forall("x", And(Fun("f","x"), Fun("f","c")))
FormulaFunctions.pushQuantifiers(f) should be (And(Forall("x", Fun("f","x")),Fun("f","c")))
}
}
\ No newline at end of file
src/test/scala/de/tum/workflows/tests/FOTransformTest.scala
View file @ 2e9e706a
......@@ -151,4 +151,5 @@ class FOTransformSpec extends FlatSpec {
)
}
}
\ No newline at end of file
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