Commit 1268024b authored by Christian Müller's avatar Christian Müller

add preconditions

parent 2928551f
package de.tum.workflows
import com.typesafe.scalalogging._
import blocks._
import de.tum.workflows.foltl.FOLTL
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.FormulaFunctions._
import de.tum.workflows.foltl.FormulaFunctions
object Preconditions extends LazyLogging {
def weakestPrecondition(f: Formula, b: SimpleBlock) = {
// TODO: f can't be temporal yet
val choice = b.pred.map(n => Fun(n, b.agents))
val updates = b.steps.map(s => {
s.fun -> (s.tuple, {
val frees = s.guard.freeVars() -- s.tuple.toSet
val list = List(s.guard) ++ choice.toList
val guard = And.make(list)
s match {
case Add(_, _, _) => {
Or(Fun(s.fun, s.tuple), Exists(frees.toList, guard)).simplify()
}
case Remove(_, _, _) => {
And(Fun(s.fun, s.tuple), Forall(frees.toList, Neg(guard))).simplify()
}
}
})
}) toMap
// Replace literals with their precondition
f everywhere {
case Fun(name, ind, params) if b.steps.exists(s => s.fun == name) => {
val up = updates(name)
val renamed = up._2.parallelRename(up._1, params)
// Annotate the precondition with the index
if (ind.isDefined) {
FormulaFunctions.annotate(renamed, ind.get)
} else {
renamed
}
}
}
}
}
\ No newline at end of file
......@@ -38,6 +38,26 @@ case class Spec(w: Workflow, declass: List[(Fun, Formula)], target: Fun, causals
sane = false
}
// check same relation only updated once per block
def isSane(steps:List[Block]):Boolean = {
val sanes = steps map {s =>
s match {
case b:SimpleBlock => {
// all predicates should only appear at most once
val pred = w.sig.preds.find(p => b.steps.count(s => s.fun == p.name) <= 1)
pred.map(p =>
logger.error(s"Predicate $p updated more than once in $b")
)
pred.isEmpty
}
case Loop(steps) => isSane(steps)
case NondetChoice(left, right) => isSane(left) && isSane(right)
}
}
sanes reduce (_ && _)
}
sane &&= isSane(w.steps)
sane
}
}
......
......@@ -17,6 +17,7 @@ object FOLTL {
def opsize() = FormulaFunctions.opsize(this)
def removeOTQuantifiers() = FormulaFunctions.removeOTQuantifiers(this)
def parallelRename(vars:List[Var], newvars:List[Var]) = FormulaFunctions.parallelRename(this, vars, newvars)
def bracketed(): String = this match {
case _: BinOp => "(" + this + ")"
......
......@@ -27,39 +27,39 @@ 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 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
// 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
// Remove variables from quantifiers if not used in the body
// case Quantifier(qmake, xs, t) if !(xs.toSet -- t.freeVars()).isEmpty =>
......@@ -98,7 +98,7 @@ object FormulaFunctions extends LazyLogging {
case x => 1
}
}
def collect[T](combine: (T*) => T, empty: T)(coll: PartialFunction[Formula, T], t: Formula): T = {
if (coll.isDefinedAt(t))
coll(t)
......@@ -153,15 +153,33 @@ object FormulaFunctions extends LazyLogging {
frees.isEmpty
}
def removeOTQuantifiers(f: Formula):Formula = {
def removeOTQuantifiers(f: Formula): Formula = {
f.everywhere({
case ForallOtherThan(vars, otherthan, fp) => {
val eqs = for (x <- vars; y <- otherthan) yield {
Neg(Eq(x,y))
Neg(Eq(x, y))
}
Forall(vars, Implies(And.make(eqs), fp.removeOTQuantifiers()))
}
})
}
// f[newvars/vars]
def parallelRename(f: Formula, vars: List[Var], newvars: List[Var]):Formula = {
val repls = vars zip newvars toMap
parallelRename(f, repls)
}
def parallelRename(f: Formula, repls:Map[Var, Var]):Formula = {
f everywhere {
case v: Var if repls.contains(v) => repls(v)
case Fun(f, ind, params) => Fun(f, ind, params map (p => repls.getOrElse(p, p)))
case Quantifier(make, xs, f) => {
val rep = repls -- (xs)
make(xs, parallelRename(f, rep))
}
}
}
}
\ No newline at end of file
......@@ -23,4 +23,21 @@ class FOLTLTest extends FlatSpec {
Forall(List("x","y"), Implies(And(Neg(Eq("x", "z")), Neg(Eq("y", "z"))), Globally("x")))
)
}
"Parallel rename" should "work on simple functions" in {
val f = And("a", Fun("f", List("b","a")))
val res = f.parallelRename(List("a","b"), List("c","a"))
res should be (And("c", Fun("f", List("a","c"))))
}
it should "work on quantors" in {
val f = And("a", Exists("a", Fun("f", List("b","a"))))
val res = f.parallelRename(List("a","b"), List("c","a"))
res should be (And("c", Exists("a", Fun("f", List("a","a")))))
}
}
\ No newline at end of file
package de.tum.workflows.ltl.tests
import org.scalatest.FlatSpec
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.Implicits._
import de.tum.workflows.blocks._
import de.tum.workflows.Preconditions
import de.tum.workflows.foltl.FormulaFunctions
class PreconditionTest extends FlatSpec {
"Preconditions" should "work on simple blocks" in {
// forall a,b S(a) -> R += (a,b)
val s = Add(Fun("S", List("a")), "R", List("a", "b"))
val b = ForallMayBlock(List("a","b"), "choice1", List(s))
val f = Fun("R", Some("t1"), List("x", "y"))
val pre = Preconditions.weakestPrecondition(f, b)
pre should be (
FormulaFunctions.annotate(
Or(Fun("R", List("x","y")), And(Fun("S", List("x")), Fun("choice1", List("x","y")))),
"t1"
)
)
val f2 = Fun("R", Some("t1"), List("a", "b"))
val pre2 = Preconditions.weakestPrecondition(f2, b)
pre2 should be (
FormulaFunctions.annotate(
Or(Fun("R", List("a","b")), And(Fun("S", List("a")), Fun("choice1", List("a","b")))),
"t1"
)
)
}
it should "work on omitting workflows" in {
// forall a,b S(a,b) -> R += (a)
val s = Add(Fun("S", List("a","b")), "R", List("b"))
val b = ForallMayBlock(List("a","b"), "choice1", List(s))
val f = Fun("R", Some("t1"), List("x"))
val pre = Preconditions.weakestPrecondition(f, b)
pre should be (
FormulaFunctions.annotate(
Or(Fun("R", List("x")), Exists("a", And(Fun("S", List("a", "x")), Fun("choice1", List("a","x"))))),
"t1"
)
)
}
it should "work on blocks with several statements" in {
// forall a,b
// R(a,b) -> S += b
// S(a) -> T -= (a,b)
val s1 = Add(Fun("R", List("a","b")), "S", List("b"))
val s2 = Remove(Fun("S", List("b")), "T", List("a"))
val b = ForallMayBlock(List("a","b"), "choice1", List(s1, s2))
val f = Exists("x", And(Fun("S", Some("t1"), List("x")), Fun("T", Some("t2"), List("y"))))
val pre = Preconditions.weakestPrecondition(f, b)
val res1 = FormulaFunctions.annotate(
Or(Fun("S", List("x")), Exists("a", And(Fun("R", List("a", "x")), Fun("choice1", List("a","x"))))),
"t1").simplify()
val res2 = FormulaFunctions.annotate(
And(Fun("T",List("y")), Forall("b", Neg(And(Fun("S", List("b")), Fun("choice1", List("y","b")))))),
"t2").simplify()
pre should be (
Exists("x", And(res1, res2))
)
}
}
\ 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