Commit e58d987c authored by Christian Müller's avatar Christian Müller

invariant found

parent 791bb3d5
...@@ -17,7 +17,7 @@ Oracle(x:A,p:P,r:R): ¬ Conf(xat:A,p:P) ...@@ -17,7 +17,7 @@ Oracle(x:A,p:P,r:R): ¬ Conf(xat:A,p:P)
Target Target
Read(xat:A, p:P, rt:R) Read(xat:A, pt:P, rt:R)
Causality Causality
......
...@@ -11,7 +11,7 @@ import de.tum.niwo.foltl.Properties ...@@ -11,7 +11,7 @@ import de.tum.niwo.foltl.Properties
import java.io.PrintWriter import java.io.PrintWriter
import java.io.File import java.io.File
import de.tum.niwo.blocks.{NISpec, TSConverter, Workflow} import de.tum.niwo.blocks.{InvSpecInstantiator, NISpec, TSConverter, Workflow}
import de.tum.niwo.foltl.FormulaFunctions import de.tum.niwo.foltl.FormulaFunctions
import de.tum.niwo.invariants.{InvProperties, InvariantChecker, InvariantGenerator} import de.tum.niwo.invariants.{InvProperties, InvariantChecker, InvariantGenerator}
import de.tum.niwo.toz3.Z3QFree import de.tum.niwo.toz3.Z3QFree
......
...@@ -8,7 +8,7 @@ import de.tum.niwo.Utils._ ...@@ -8,7 +8,7 @@ import de.tum.niwo.Utils._
import java.io.PrintWriter import java.io.PrintWriter
import java.io.File import java.io.File
import de.tum.niwo.blocks.{InvariantSpec, NISpec, TSConverter, Workflow} import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FormulaFunctions import de.tum.niwo.foltl.FormulaFunctions
import de.tum.niwo.invariants.{InvProperties, InvariantChecker, InvariantGenerator} import de.tum.niwo.invariants.{InvProperties, InvariantChecker, InvariantGenerator}
......
...@@ -3,7 +3,7 @@ package de.tum.niwo ...@@ -3,7 +3,7 @@ package de.tum.niwo
import com.microsoft.z3.Status import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.Utils._ import de.tum.niwo.Utils._
import de.tum.niwo.blocks.{NISpec, SimpleWFBlock, TSConverter} import de.tum.niwo.blocks.{InvSpecInstantiator, NISpec, SimpleWFBlock, TSConverter}
import de.tum.niwo.foltl.FOLTL._ import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.FOTransformers import de.tum.niwo.foltl.FOTransformers
import de.tum.niwo.synth.Model import de.tum.niwo.synth.Model
......
...@@ -78,7 +78,7 @@ object Utils extends LazyLogging { ...@@ -78,7 +78,7 @@ object Utils extends LazyLogging {
def check(name:String, desc:String, spec:InvariantSpec, properties:InvProperties):Boolean = { def check(name:String, desc:String, spec:InvariantSpec, properties:InvProperties):Boolean = {
clear(name) clear(name)
infer(name:String, desc:String, spec:InvariantSpec, properties:InvProperties) infer(name, desc, spec, properties)
} }
def check(name:String, desc:String, inv:NISpec => Formula, properties:InvProperties):Boolean = { def check(name:String, desc:String, inv:NISpec => Formula, properties:InvProperties):Boolean = {
...@@ -112,8 +112,12 @@ object Utils extends LazyLogging { ...@@ -112,8 +112,12 @@ object Utils extends LazyLogging {
val basename = name.split("/").last val basename = name.split("/").last
val filenames = s"${basename}_$model${if (desc.isEmpty) "" else s"_$desc"}" val filenames = s"${basename}_$model${if (desc.isEmpty) "" else s"_$desc"}"
val fixspec = properties.universe.map(u =>
InvSpecInstantiator.instantiate(spec, u)
).getOrElse(spec)
val (res, graph, labelling, provens, dot, time) = val (res, graph, labelling, provens, dot, time) =
InvariantChecker.checkInvariantFPLabelling(spec, properties) InvariantChecker.checkInvariantFPLabelling(fixspec, properties)
logger.info(s"Invariant was ${spec.inv}") logger.info(s"Invariant was ${spec.inv}")
logger.info(s"Invariant was ${if (res) "" else "not "}proven (took $time ms)\n") logger.info(s"Invariant was ${if (res) "" else "not "}proven (took $time ms)\n")
...@@ -154,7 +158,9 @@ object Utils extends LazyLogging { ...@@ -154,7 +158,9 @@ object Utils extends LazyLogging {
| Proof steps: ${dot.size} | Proof steps: ${dot.size}
| Strengthenings: ${strengthenings.size} | Strengthenings: ${strengthenings.size}
| Largest Inv: $maxsize | Largest Inv: $maxsize
| Average Inv: $avgsize""".stripMargin | Average Inv: $avgsize
| Properties: $properties
| """.stripMargin
) )
res res
} }
......
...@@ -43,7 +43,7 @@ object TSConverter extends LazyLogging { ...@@ -43,7 +43,7 @@ object TSConverter extends LazyLogging {
InvariantSpec(ts, spec.axioms, invgen(spec)) InvariantSpec(ts, spec.axioms, invgen(spec))
} }
private def everywhere(list: List[WFBlock], def everywhere(list: List[WFBlock],
update: SimpleWFBlock[_] => List[SimpleWFBlock[_]]):List[WFBlock] = { update: SimpleWFBlock[_] => List[SimpleWFBlock[_]]):List[WFBlock] = {
list match { list match {
case (l:WFLoop) :: xs => l.update(everywhere(l.steps, update)) :: everywhere(xs, update) case (l:WFLoop) :: xs => l.update(everywhere(l.steps, update)) :: everywhere(xs, update)
......
package de.tum.niwo.blocks
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.foltl.FOLTL.Var
import de.tum.niwo.foltl.FOTransformers
object InvSpecInstantiator extends LazyLogging {
def instantiate(spec:InvariantSpec, universe:Map[String, List[Var]]) = {
val newaxioms = FOTransformers.eliminateQuantifiers(spec.axioms, universe)
val newinv = FOTransformers.eliminateQuantifiers(spec.inv, universe)
val tsblocks = spec.ts.steps.map(_.mapStatements(
stmt => stmt.update(guard = FOTransformers.eliminateQuantifiers(stmt.guard, universe))
))
val newsig = spec.ts.sig.copy(constants = spec.ts.sig.constants ++ universe.values.flatten)
val newts = spec.ts.copy(steps = tsblocks, sig = newsig)
spec.copy(ts = newts, axioms = newaxioms, inv = newinv)
}
}
\ No newline at end of file
...@@ -186,10 +186,18 @@ object FOLTL { ...@@ -186,10 +186,18 @@ object FOLTL {
val qname = "∃" val qname = "∃"
val make: (List[Var], Formula) => Formula = Quantifier.make(Exists.apply, _, _) val make: (List[Var], Formula) => Formula = Quantifier.make(Exists.apply, _, _)
} }
// object Exists {
// def apply(v:Var, t:Formula) = Exists(List(v), t)
// def apply(tup:(Var, Var), t:Formula) = Exists(List(tup._1, tup._2), t)
// }
case class Forall(vars: List[Var], t: Formula) extends Quantifier { case class Forall(vars: List[Var], t: Formula) extends Quantifier {
val qname = "∀" val qname = "∀"
val make: (List[Var], Formula) => Formula = Quantifier.make(Forall.apply, _, _) val make: (List[Var], Formula) => Formula = Quantifier.make(Forall.apply, _, _)
} }
// object Forall {
// def apply(v:Var, t:Formula) = Forall(List(v), t)
// def apply(tup:(Var, Var), t:Formula) = Forall(List(tup._1, tup._2), t)
// }
case class ForallOtherThan(vars: List[Var], otherthan: List[Var], t: Formula) extends Quantifier { case class ForallOtherThan(vars: List[Var], otherthan: List[Var], t: Formula) extends Quantifier {
val qname = "∀" val qname = "∀"
val make = ForallOtherThan.apply(_: List[Var], otherthan, _: Formula) val make = ForallOtherThan.apply(_: List[Var], otherthan, _: Formula)
......
...@@ -264,6 +264,53 @@ object FOTransformers extends LazyLogging { ...@@ -264,6 +264,53 @@ object FOTransformers extends LazyLogging {
} }
}) })
} }
def eliminateQuantifiers(t:Formula, universe:Map[String,List[FOLTL.Var]]):Formula = {
def instantiateE(tup:List[Var],t:Formula) = {
if (!tup.forall(v => universe.contains(v.typ))) {
False
} else {
val replacements = comb(tup.map(_.typ), universe)
val terms = for (repl <- replacements) yield {
val mapping = tup.zip(repl) toMap
t.everywhere({
// do replacement
case Fun(f, id, vars) => Fun(f, id, vars.map(a => mapping.getOrElse(a, a)))
case v: Var => mapping.getOrElse(v, v)
})
}
eliminateQuantifiers(Or.make(terms), universe)
}
}
def instantiateA(tup:List[Var],t:Formula) = {
if (!tup.forall(v => universe.contains(v.typ))) {
True
} else {
val replacements = comb(tup.map(_.typ), universe)
val terms = for (repl <- replacements) yield {
val mapping = tup.zip(repl) toMap
t.everywhere({
// do replacement
case Fun(f, id, vars) => Fun(f, id, vars.map(a => mapping.getOrElse(a, a)))
case v: Var => mapping.getOrElse(v, v)
})
}
eliminateQuantifiers(And.make(terms), universe)
}
}
t everywhere {
case Exists(tup, term) =>
instantiateE(tup, term)
case Forall(tup, term) =>
instantiateA(tup, term)
}
}
/** /**
* Replace function calls Fun("f", Some("t1"), List("x")) by Var("f#t1_x") * Replace function calls Fun("f", Some("t1"), List("x")) by Var("f#t1_x")
......
...@@ -12,7 +12,16 @@ import de.tum.niwo.Utils ...@@ -12,7 +12,16 @@ import de.tum.niwo.Utils
import scala.annotation.tailrec import scala.annotation.tailrec
case class InvProperties(stubborn:Boolean, eliminateA:Boolean = true, eliminateB:Boolean = true, approxElim:Boolean = true) { } case class InvProperties(stubborn:Boolean,
eliminateA:Boolean = true,
eliminateB:Boolean = true,
approxElim:Boolean = true,
universe:Option[Map[String, List[Var]]] = None) {
override def toString: String = {
s"InvProperties(stubborn=$stubborn, eliminateA=$eliminateA, eliminateB=$eliminateB," +
s"approxElim=$approxElim,universe:$universe)"
}
}
object InvProperties { object InvProperties {
val DEFAULT = InvProperties( val DEFAULT = InvProperties(
stubborn = true, stubborn = true,
...@@ -73,8 +82,14 @@ object InvariantChecker extends LazyLogging { ...@@ -73,8 +82,14 @@ object InvariantChecker extends LazyLogging {
// take the edge with a minimum of following unproven edges excluding selfloops // take the edge with a minimum of following unproven edges excluding selfloops
// val next = toProve.minBy(edge => ((edge.target.outgoing.filter(t => t.target != t.source) -- proven).size)) // val next = toProve.minBy(edge => ((edge.target.outgoing.filter(t => t.target != t.source) -- proven).size))
// take the edge with maximum source node first // take the edge with maximum source node first
val nextEdge = toProve.maxBy(edge => edge.source.value) val nextEdge = if (properties.universe.isDefined) {
// counterexample mode: try to go to source
toProve.minBy(edge => edge.source.value)
} else {
// proving mode: try to iterate loops
toProve.maxBy(edge => edge.source.value)
}
// try to prove // try to prove
val pre = labels(nextEdge.from) val pre = labels(nextEdge.from)
val post = labels(nextEdge.to) val post = labels(nextEdge.to)
...@@ -102,7 +117,11 @@ object InvariantChecker extends LazyLogging { ...@@ -102,7 +117,11 @@ object InvariantChecker extends LazyLogging {
// --> unsafe, relabel incoming node, invalidate all proven guarantees for that node // --> unsafe, relabel incoming node, invalidate all proven guarantees for that node
// check if relabelled invariant still satisfiable // check if relabelled invariant still satisfiable
// never relabel initial node // never relabel initial node
logger.info(s"Invariant not inductive, strengthening.") logger.info(s"Invariant not inductive for ($from -> $to), strengthening.")
if (Utils.DEBUG_MODE) {
val model = solver.getModel
logger.debug(model.toString)
}
val newinv = And(labels(from), strengthened).simplify val newinv = And(labels(from), strengthened).simplify
...@@ -145,6 +164,8 @@ object InvariantChecker extends LazyLogging { ...@@ -145,6 +164,8 @@ object InvariantChecker extends LazyLogging {
n -> inv.assumeEmpty(untouched(graph.get(n)).toList) n -> inv.assumeEmpty(untouched(graph.get(n)).toList)
} }
logger.info(s"Beginning inference for invariant $spec.inv")
val (time, (result, labellings, proven)) = Utils.time { checkInvariantRec(List(untouchedlabels), List(Set())) } val (time, (result, labellings, proven)) = Utils.time { checkInvariantRec(List(untouchedlabels), List(Set())) }
val dot1 = labellings.zip(proven).reverse val dot1 = labellings.zip(proven).reverse
......
...@@ -40,7 +40,8 @@ object InvariantGenerator { ...@@ -40,7 +40,8 @@ object InvariantGenerator {
// val quants = premise.flatMap(_._1).toSet.toList // eliminate doubles // val quants = premise.flatMap(_._1).toSet.toList // eliminate doubles
val conclusion = genEq(spec.target) val conclusion = genEq(spec.target)
Forall(spec.target.params, conclusion).simplify // TODO: tail here?
Forall(spec.target.params.tail, conclusion).simplify
// Constants // Constants
// conclusion // conclusion
} }
......
...@@ -5,8 +5,7 @@ import org.scalatest.Matchers._ ...@@ -5,8 +5,7 @@ import org.scalatest.Matchers._
import org.scalatest.Inspectors._ import org.scalatest.Inspectors._
import de.tum.niwo.foltl.FOLTL._ import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.Implicits._ import de.tum.niwo.Implicits._
import de.tum.niwo.foltl.FOLTL import de.tum.niwo.foltl.{FOLTL, FOTransformers, FormulaFunctions}
import de.tum.niwo.foltl.FormulaFunctions
class FOLTLTest extends FlatSpec { class FOLTLTest extends FlatSpec {
"Formulas" should "be constructed correctly" in { "Formulas" should "be constructed correctly" in {
...@@ -220,5 +219,36 @@ class FOLTLTest extends FlatSpec { ...@@ -220,5 +219,36 @@ class FOLTLTest extends FlatSpec {
} }
"Universe instantiation" should "work" in {
val universe = Map(
"A" -> List(Var("x","A"), Var("y","A")),
"B" -> List(Var("b","B")),
"C" -> List()
)
val a = Var("a", "A")
val b = Var("b", "A")
val xa = Var("x", "A")
val ya = Var("y", "A")
val za = Var("z","A")
val tests = Map(
True -> True,
False -> False,
Forall(Var("z","A"), Fun("f", List(Var("z", "A")))) ->
And.make(Fun("f", List(Var("x", "A"))), Fun("f", List(Var("y", "A")))),
Exists(Var("z","B"), Fun("f", List(Var("z", "B")))) ->
Fun("f", List(Var("b", "B"))),
Forall(Var("c","C"), Fun("f", List(Var("c", "C")))) ->
True,
Forall(a, Exists(b, Fun("f", List(a, b)))) ->
And.make(Or.make(Fun("f", List(xa, xa)), Fun("f", List(xa, ya))),
Or.make(Fun("f", List(ya, xa)), Fun("f", List(ya, ya))))
)
for ((from, to) <- tests) {
FOTransformers.eliminateQuantifiers(from, universe) should be (to)
}
}
} }
\ No newline at end of file
package de.tum.niwo.tests.papertests package de.tum.niwo.tests.papertests
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.blocks.NISpec import de.tum.niwo.blocks.NISpec
import de.tum.niwo.foltl.FOLTL import de.tum.niwo.foltl.{FOLTL, FOTransformers, FormulaFunctions}
import de.tum.niwo.foltl.FOLTL.{And, Forall, Fun, Neg, Var} import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.invariants.InvariantGenerator.genEq import de.tum.niwo.invariants.InvariantGenerator.genEq
import de.tum.niwo.{Examples, Utils} import de.tum.niwo.{Examples, Utils}
import de.tum.niwo.invariants.{InvProperties, InvariantGenerator} import de.tum.niwo.invariants.{InvProperties, InvariantGenerator}
import de.tum.niwo.parser.{TransitionSystemParser, WorkflowParser}
import de.tum.niwo.tests.TestUtils.{checkSafe, checkSafeCausalElim} import de.tum.niwo.tests.TestUtils.{checkSafe, checkSafeCausalElim}
import org.scalatest.FlatSpec import org.scalatest.FlatSpec
class CCSSubmissionTest extends FlatSpec { class CCSSubmissionTest extends FlatSpec with LazyLogging {
def checkTS(name:String, properties:InvProperties):Boolean = { def checkTS(name:String, properties:InvProperties):Boolean = {
val spec = Examples.parseExampleTS(name).get val spec = Examples.parseExampleTS(name).get
...@@ -130,16 +132,77 @@ class CCSSubmissionTest extends FlatSpec { ...@@ -130,16 +132,77 @@ class CCSSubmissionTest extends FlatSpec {
))) )))
} }
it should "prove counterexample for conference" in {
val name = "omitting/conference"
val inv = (spec:NISpec) => {
val i = InvariantGenerator.invariantNoninterSingleBS(spec)
val reninv = i.parallelRename(List(Var("xat","A")), List(Var("a1", "A")))
FormulaFunctions.eliminateEq(reninv)
}
assert(!checkSafe(name, "", inv, InvProperties(
stubborn = false,
approxElim = false,
eliminateA = true,
universe = Some(
Map(
"A" -> List(Var("a1", "A"), Var("a2", "A")),
"P" -> List(Var("p1", "P"), Var("p2", "P")),
"R" -> List(Var("r1", "R"))
)
)
)))
}
it should "prove causal omitting/conference_fixed for a given invariant" in { it should "prove causal omitting/conference_fixed for a given invariant" in {
val name = "omitting/conference_withB" val name = "omitting/conference_withB"
// val inv = InvariantGenerator.invariantNoninterSingleBS _ // val inv = InvariantGenerator.invariantNoninterSingleBS _
import InvariantGenerator.genEq
val x = Var("ix","A")
val xt = Var("xt","A")
val y = Var("iy", "A")
val z = Var("iz","A")
val p = Var("ip","P")
val q = Var("iq","P")
val r = Var("ir","R")
val ceq = Forall(List(x, p), genEq("Conf", List(x,p)))
val asseq = Forall(List(x, p), genEq("Assign", List(x,p)))
val xyass = Forall(List(y,p), (Fun("Assign", List(xt,p)) land Fun("Assign", List(y, p))) -->
(
Forall(List(q,r), genEq("Review", List(y,q,r))) land
Neg(Fun("informed", List(y))) land
Forall(List(q,r), genEq("Read", List(y,q,r))) land
Forall(List(q), Fun("Conf", List(xt, p)) --> Fun("Conf", List(y, q))) land
Forall(List(z,q), (Fun ("Assign", List(y, q)) land Fun("Assign", List(z,q))) -->
Fun("Assign", List(z,p))
)
)
)
// val readimplass = Forall(List(y, q, r), Fun("Read", List(y,p,r)) --> Fun("Assign", List(y,p)))
val revimplass = Forall(List(y, p, r), Fun("Review", List(y,p,r)) --> Fun("Assign", List(y,p)))
// val rt = Var("rt","R")
// val i0 = "∀x:A,p:P,r:R (Read(x,p,r) ⟹ Assign(x,p))"
// val i1 = "∀x:A,p:P,r:R (Review(x,p,r) ⟹ Assign(x,p))"
// val i2 = "∀x:A,y:A,p:P,q:P ¬(Conf(x,p) ∧ Assign(x,q) ∧ Assign(y,p) ∧ Assign(y,q))"
// val i3 = "∀x:A,p:P,y:A,q:P ¬(Assign(x,p) ∧ Review(y,p,r) ∧ Conf(x,q) ∧ Assign(y,q))"
// val i3 = "∀x:A,y:A,p:P ¬(informed(y) ∧ Assign(x,p) ∧ Assign(y,p))"
// val i4 = "∀x:A,p:P,r:R ¬(Read(x,p,r) ∧ ¬Assign(x,p))"
// val invs = List(
//
// )
// val parsed = invs.map(TransitionSystemParser.parseFormula(_))
// logger.info(parsed.mkString)
// val ip = And.make(parsed.map(_.get))
val invs = List(asseq, ceq, xyass.in("t1"), revimplass.in("t1"), revimplass.in("t2"))
val xat = Var("xat","A")
val pt = Var("pt","P")
val rt = Var("rt","R")
// val rt = Var("rt","R") // val rt = Var("rt","R")
val inv = (spec:NISpec) => And.make(InvariantGenerator.invariantAllEqual(spec), Forall(List(xat), Neg(Fun("informed", Some("t1"), List(xat))))) val inv = (spec:NISpec) => And.make(InvariantGenerator.invariantNoninterSingleBS(spec), And.make(invs))
// val inv = InvariantGenerator.invariantNoninterSingleBS _ // val inv = InvariantGenerator.invariantNoninterSingleBS _
assert(checkSafe(name, "", inv, InvProperties( assert(checkSafe(name, "", inv, InvProperties(
......
package de.tum.niwo.tests.papertests package de.tum.niwo.tests.papertests
import de.tum.niwo.{Examples, Utils} import de.tum.niwo.{Examples, Utils}
import de.tum.niwo.blocks.TSConverter import de.tum.niwo.blocks.{InvSpecInstantiator, TSConverter}
import de.tum.niwo.foltl.FOLTL._ import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.invariants.InvProperties import de.tum.niwo.invariants.InvProperties
import de.tum.niwo.parser.WorkflowParser import de.tum.niwo.parser.WorkflowParser
......
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