Skip to content

GitLab

Commit 19d48092 authored by Christian Müller's avatar Christian Müller
Browse files
Options

add metrics

parent c712d7e2
Hide whitespace changes
Inline Side-by-side
Showing with 416 additions and 211 deletions
examples/omitting/conference.spec
View file @ 19d48092
......@@ -8,16 +8,16 @@ forall x:A,p:P,r:R
(Assign(x,p) ∧ O(x,p,r)) → Review += (x,p,r)
loop {
forall xa:A,xb:A,p:P,r:R (Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,p,r)
forallmay x:A,p:P,r:R (Assign(x,p) ∧ O(x,p,r)) → Review += (x,p,r)
forallmay x:A,p:P,r:R (Assign(x,p)) → Review += (x,p,r)
}
Declassify
O(x:A,p:P,r:R): ¬ Conf(at:A,p:P)
O(x:A,p:P,r:R): ¬ Conf(xat:A,p:P)
Target
Read(at:A, bt:A, pt:P, rt:R)
Read(xat:A, pt:P, rt:R)
Causality
......
examples/tests/conference_linear_small.spec 0 → 100644
View file @ 19d48092
Workflow
forallmay x:X,p:P
True -> Conf += (x,p)
forall x:X,p:P,r:R
(¬ Conf(x,p) ∧ O(x,p,r)) -> Read += (x,p,r)
forallmay y:X,x:X,p:P
(¬ Conf(x,p) ∧ ¬ Conf(y,p)) -> Comm += (x,y,p)
Declassify
O(x:X,p:P,r:R): ¬ Conf(xt:X,p:P)
Target
Comm(xt:X, yt:X, pt:P)
Causality
a:X
src/main/scala/de/tum/workflows/MainInvariants.scala
View file @ 19d48092
......@@ -29,7 +29,7 @@ object MainInvariants extends App with LazyLogging {
val (t, (res, dot)) = time {
// InvariantChecker.checkInvariantOnce(spec.w, inv(spec), true)
InvariantChecker.checkInvariantFP(spec, invariant(spec), true)
InvariantChecker.checkInvariantFP(spec, invariant(spec))
}
val msg = s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n"
......
src/main/scala/de/tum/workflows/Preconditions.scala
View file @ 19d48092
......@@ -9,55 +9,52 @@ import de.tum.workflows.foltl.FormulaFunctions._
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.ltl.FOTransformers
import de.tum.workflows.foltl.Properties._
import de.tum.workflows.toz3.InvProperties
object Preconditions extends LazyLogging {
def elaborateSteps(b:SimpleBlock, s:Spec) = {
val newsteps = (for (stmt <- b.steps) yield {
val first = stmt.tuple.head
if (first.typ == s.target.params.head.typ) {
val fun = Fun(stmt.fun, stmt.tuple)
// TODO
val guard = Neg(Eq(fun.in(T1), fun.in(T2)))
List(stmt, Add(guard, INFNAME, List(first)))
} else List(stmt)
def elaborateSteps(b: SimpleBlock, s: Spec) = {
val newsteps = (for (stmt <- b.steps if stmt.tuple.head.typ == s.target.params.head.typ) yield {
val fun = Fun(stmt.fun, stmt.tuple)
// TODO
val guard = Neg(Eq(fun.in(T1), fun.in(T2)))
ForallBlock(stmt.tuple, List(Add(guard, INFNAME, List(stmt.tuple.head))))
})
newsteps.flatten
b :: newsteps
}
def elaborateOraclyBlock(b:SimpleBlock, s:Spec) = {
def elaborateOraclyBlock(b: SimpleBlock, s: Spec) = {
if (b.isoracly) {
val stmt = b.steps.head // can only be one
def fixguard(f:Formula) = {
def fixguard(f: Formula) = {
f.everywhere {
case f:Fun if f.isOracle() => True
case f: Fun if f.isOracle() => True
}
}
def findOracle(f:Formula) = {
def findOracle(f: Formula) = {
f.collect {
case f:Fun if (f.isOracle()) => List(f.name)
case f: Fun if (f.isOracle()) => List(f.name)
}
}
val name = findOracle(stmt.guard).head
val newstmt = stmt match {
case Add(guard, fun, tuple) => Add(fixguard(guard).simplify(), fun, tuple)
case Add(guard, fun, tuple) => Add(fixguard(guard).simplify(), fun, tuple)
case Remove(guard, fun, tuple) => Remove(fixguard(guard).simplify(), fun, tuple)
}
ForallMayBlock(b.agents, name, List(newstmt))
} else b
}
def subst(f:Formula, updates: List[(String, (List[FOLTL.Var], FOLTL.Formula))], b:SimpleBlock) = {
def subst(f: Formula, updates: List[(String, (List[FOLTL.Var], FOLTL.Formula))], b: SimpleBlock) = {
updates.foldRight(f)((update, f) => {
val (repname, (vars, form)) = update
f everywhere {
case Fun(name, ind, params) if name == repname => {
val renamed = form.parallelRename(vars, params)
// Annotate the precondition with the index
if (ind.isDefined) {
FormulaFunctions.annotate(renamed, ind.get)
......@@ -69,93 +66,110 @@ object Preconditions extends LazyLogging {
})
}
def weakestPrecondition(f: Formula, outerb: SimpleBlock, spec:Spec, stubborn:Boolean) = {
val b = elaborateOraclyBlock(outerb, spec)
// elaborate only if non-stubborn
val steps = if (!stubborn) elaborateSteps(b, spec) else b.steps
val choice = b.pred.map(n => Fun(n, b.agents))
val updates = 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)
val first = s.tuple.head
// Trace related substitution for informedness
// TODO: make switch on/off etc
val con = if (outerb.isoracly) {
val decl = spec.declass.getOrElse(b.pred.get, (List(), False))._2
// FIXME: substitutions?
// FIXME: decl in T2?
Or(And(decl.in(T1), choice.get.in(T1)), And(Neg(decl.in(T1)), choice.get))
} else if (choice.isDefined) {
val inner = if (first.typ == spec.target.params.head.typ) {
val inf = Fun(INFNAME, List(s.tuple.head))
if (stubborn) {
choice.get.in(T1)
} else {
Or(And(Neg(inf.in(T1)), choice.get.in(T1)), And(inf.in(T1), choice.get))
}
def getUpdate(s:Statement, b:SimpleBlock, choice:Option[Fun], isOracly:Boolean, spec:Spec, properties:InvProperties) = {
val frees = s.guard.freeVars() -- s.tuple.toSet
// val list = List(s.guard) ++ choice.toList
// val guard = And.make(list)
val first = s.tuple.head
// Trace related substitution for informedness
val con = if (isOracly) {
val decl = spec.declass.getOrElse(b.pred.get, (List(), False))._2
// FIXME: substitutions?
// FIXME: decl in T2?
Or(And(decl.in(T1), choice.get.in(T1)), And(Neg(decl.in(T1)), choice.get))
} else if (choice.isDefined) {
// is "normal" may block
val inner = if (first.typ == spec.target.params.head.typ) {
val inf = Fun(INFNAME, List(b.agents.head))
if (properties.stubborn) {
choice.get.in(T1)
} else {
choice.get
Or(And(Neg(inf.in(T1)), choice.get.in(T1)), And(inf.in(T1), choice.get))
}
inner
} else {
True
choice.get
}
val guard = And(s.guard, con).simplify()
// val guard = True
inner
} else {
True
}
val form = 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()
}
val guard = And(s.guard, con).simplify()
// val guard = True
val form = s match {
case Add(_, _, _) => {
Or(Fun(s.fun, s.tuple), Exists(frees.toList, guard)).simplify()
}
form
})
case Remove(_, _, _) => {
And(Fun(s.fun, s.tuple), Forall(frees.toList, Neg(guard))).simplify()
}
}
form
}
def weakestPrecondition(post: Formula, outerb: SimpleBlock, spec: Spec, properties: InvProperties) = {
// elaborate only if non-stubborn
val steps = if (!properties.stubborn) elaborateSteps(outerb, spec) else List(outerb)
val precond = steps.foldRight(post)((b, f) => {
val innerb = if (b.isoracly) {
elaborateOraclyBlock(b, spec)
} else {
b
}
val innerprecond = weakestPreconditionSingle(f, innerb, b.isoracly, spec, properties)
innerprecond
})
precond
}
def weakestPreconditionSingle(f: Formula, b: SimpleBlock, isOracly:Boolean, spec: Spec, properties: InvProperties) = {
val choice = b.pred.map(n => Fun(n, b.agents))
val updates = for (s <- b.steps) yield {
s.fun -> (s.tuple, {
getUpdate(s, b, choice, isOracly, spec, properties)
})
}
// Replace literals with their precondition
val replaced = subst(f, updates, b)
// TODO: have we proven this correct?
val removed = FOTransformers.eliminateDoubleQuantifiers(replaced)
removed
}
def abstractPrecondition(f:Formula, b:SimpleBlock, stubborn:Boolean, s:Spec) = {
val precond = weakestPrecondition(f, b, s, stubborn)
def abstractPrecondition(f: Formula, b: SimpleBlock, s: Spec, properties: InvProperties) = {
val precond = weakestPrecondition(f, b, s, properties)
// Stubborn agents -> remove trace variable from choice predicate
// Not neccessary anymore
// val stubprecond = if (stubborn) {
// precond.everywhere {
// case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
// }
// } else precond
// Abstract away inner existentials
val universalinv = if (b.isomitting) {
FOTransformers.abstractExistentials(precond).simplify()
// val stubprecond = if (stubborn) {
// precond.everywhere {
// case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
// }
// } else precond
// Abstract away inner existentials - always if causal agents
val universalinv = if (!properties.stubborn || b.isomitting) {
FOTransformers.abstractExistentials(precond)
} else {
precond
}
// Abstract away auxilliaries
val auxless = if (b.pred.isDefined) {
FOTransformers.eliminateAuxiliaryPredicate(universalinv, b.pred.get).simplify()
val auxless = if (b.pred.isDefined && properties.eliminateAux) {
FOTransformers.eliminateAuxiliaryPredicate(universalinv, b.pred.get)
} else {
universalinv
}
auxless
auxless.simplify()
}
}
\ No newline at end of file
src/main/scala/de/tum/workflows/foltl/FOLTL.scala
View file @ 19d48092
......@@ -17,32 +17,31 @@ object FOLTL {
def collect[T](coll: PartialFunction[Formula, List[T]]) = FormulaFunctions.collect(coll, this)
def hasSubFormula(coll: PartialFunction[Formula, Boolean]) = FormulaFunctions.hasSubFormula(coll, this)
def opsize() = FormulaFunctions.opsize(this)
def toPrenex() = FormulaFunctions.toPrenex(this)
def toNegNf() = FormulaFunctions.toNegNf(this)
def toCNF() = FormulaFunctions.toCNF(this)
def isBS() = FormulaFunctions.isBS(this)
def removeOTQuantifiers() = FormulaFunctions.removeOTQuantifiers(this)
def parallelRename(vars:List[Var], newvars:List[Var]) = FormulaFunctions.parallelRename(this, vars, newvars)
def parallelRename(vars: List[Var], newvars: List[Var]) = FormulaFunctions.parallelRename(this, vars, newvars)
def bracketed(): String = this match {
case _: BinOp => "(" + this + ")"
case _ => this.toString()
}
def → (f2:Formula) = Implies(this, f2)
def ∧ (f2:Formula) = And(this, f2)
def ∨ (f2:Formula) = Or(this, f2)
def →(f2: Formula) = Implies(this, f2)
def ∧(f2: Formula) = And(this, f2)
def ∨(f2: Formula) = Or(this, f2)
// TODO: better line breaking
def pretty(): String = {
val remeq = this.everywhere {
case Eq(t1, t2) if FormulaFunctions.annotateOverwrite(t1, Properties.T1, Properties.T2) == t2 =>
case Eq(t1, t2) if FormulaFunctions.annotateOverwrite(t1, Properties.T1, Properties.T2) == t2 =>
Eq(t1, Fun("eq", List()))
}
val s = remeq.toString
val broken = s replace ("∧ ", "∧\n") replace ("∨ ", "∨\n")
......@@ -65,7 +64,7 @@ object FOLTL {
object Var {
val DEFAULT_TYPE = "T"
}
case class Var(name: String, typ:String = Var.DEFAULT_TYPE) extends Formula {
case class Var(name: String, typ: String = Var.DEFAULT_TYPE) extends Formula {
override def toString() = s"$name"
def withType() = s"$name:$typ"
}
......@@ -74,27 +73,40 @@ object FOLTL {
def apply(name: String, params: List[Var]): Fun = Fun(name, None, params)
}
object FunFromVar {
val Predicate = "([a-zA-Z0-9]+)(#([a-zA-Z0-9]+))?((_[a-zA-Z0-9]+)*)".r
def unapply(s:String):Option[Fun] = {
val Predicate = "([a-zA-Z0-9]+)(#([a-zA-Z0-9]+))?((_[a-zA-Z0-9]+#[a-zA-Z0-9]+)*)".r
def getVars(s: String) = {
val split = s split ("_")
if (split.length > 1) {
split.drop(1).map(str => {
val Array(name, typ) = str.split("#")
Var(name, typ)
}) toList
} else {
List()
}
}
def unapply(s: String): Option[Fun] = {
s match {
case Predicate(name, null, _, tup, _*) => Some(Fun(name, None, tup split("_") drop(1) map (Var(_)) toList))
case Predicate(name, _, ind, tup, _*) => Some(Fun(name, Some(ind), tup split("_") drop(1) map (Var(_)) toList))
case _ => None
case Predicate(name, null, _, tup, _*) => Some(Fun(name, None, getVars(tup)))
case Predicate(name, _, ind, tup, _*) => Some(Fun(name, Some(ind), getVars(tup)))
case _ => None
}
}
}
case class Fun(name: String, ind: Option[String], params: List[Var]) extends Formula {
override def toString() = name + Utils.mkString(ind, "(", "", ")") + params.map(_.name).mkString("(", ",", ")")
def updatedParams(index: Int, p:Var) = Fun(name, ind, params.updated(index, p))
def updatedParams(index: Int, p: Var) = Fun(name, ind, params.updated(index, p))
def updatedParams(list: List[Var]) = Fun(name, ind, list)
def isOracle() = name.startsWith("O")
def encodeToVar() = {
val pi = if (ind.isDefined) "#" + ind.get else ""
Var(name + pi + Utils.mkString(params, "_", "_", ""))
val pi = if (ind.isDefined) "#" + ind.get else ""
val tup = params.map(p => p.name + "#" + p.typ)
Var(name + pi + Utils.mkString(tup, "_", "_", ""))
}
}
......@@ -122,11 +134,11 @@ object FOLTL {
val qname = "∀"
val qmake = Forall.apply _
}
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 qmake = ForallOtherThan.apply(_:List[Var], otherthan, _:Formula)
val qmake = ForallOtherThan.apply(_: List[Var], otherthan, _: Formula)
override def toString() = {
s"$qname ${vars.map(_.withType()).mkString(",")} ∉ {${otherthan.map(_.withType()).mkString(",")}}. ${t.bracketed()}"
s"$qname ${vars.map(_.withType()).mkString(",")} ∉ {${otherthan.map(_.withType()).mkString(",")}}. ${t.bracketed()}"
}
}
......@@ -150,9 +162,9 @@ object FOLTL {
val make = Until.apply _
val opname = "U"
}
object WUntil {
def apply(t1: Formula, t2: Formula) = Or(Until(t1, t2), Globally(t1))
def apply(t1: Formula, t2: Formula) = Or(Until(t1, t2), Globally(t1))
}
trait UnOp extends Formula {
......@@ -199,7 +211,7 @@ object FOLTL {
}
}
}
object Or {
def make(terms: List[Formula]) = {
BinOp.makeL(Or.apply _, terms, False)
......@@ -208,12 +220,12 @@ object FOLTL {
BinOp.makeL(Or.apply _, terms, False)
}
}
case class Or(t1: Formula, t2: Formula) extends BinOp {
val opname = "∨"
val make = Or.apply _
}
object And {
def make(terms: List[Formula]) = {
BinOp.makeL(And.apply _, terms, True)
......@@ -222,17 +234,25 @@ object FOLTL {
BinOp.makeL(And.apply _, terms, True)
}
}
case class And(t1: Formula, t2: Formula) extends BinOp {
val opname = "∧"
val make = And.apply _
}
case class Eq(t1: Formula, t2: Formula) extends BinOp {
val opname = "↔"
val make = Eq.apply _
}
object Eq {
def make(terms: List[Formula]) = {
BinOp.makeL(Eq.apply _, terms, True)
}
def make(terms: Formula*) = {
BinOp.makeL(Eq.apply _, terms, True)
}
}
case class Implies(t1: Formula, t2: Formula) extends BinOp {
val opname = "→"
val make = Implies.apply _
......
src/main/scala/de/tum/workflows/foltl/FormulaFunctions.scala
View file @ 19d48092
......@@ -4,6 +4,7 @@ import FOLTL._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.blocks.Workflow
import scala.annotation.tailrec
import de.tum.workflows.ltl.FOTransformers
object FormulaFunctions extends LazyLogging {
......@@ -54,6 +55,10 @@ object FormulaFunctions extends LazyLogging {
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))
......@@ -416,7 +421,7 @@ object FormulaFunctions extends LazyLogging {
}).simplify()
}
def toCNF(f: Formula) = {
def toCNFClauses(f: Formula) = {
@tailrec
def toCNFSub(f: Formula): Formula = {
val (changed, sub) = everywhereFP({
......@@ -431,7 +436,27 @@ object FormulaFunctions extends LazyLogging {
// normalized is now Quantifiers, then only And/Or with Negation inside
// no simplification here
toCNFSub(normalized)
val cnf = toCNFSub(normalized)
val quantifiers = FormulaFunctions.collectQuantifiers(cnf)
// Inspect clauses
val clauses = FOTransformers.collectClauses(cnf)
// TODO improve runtime
val simpedset = clauses.toSet
val simped = simpedset.filterNot(c => simpedset.exists(c2 => {
// check if c is superset of c2
c != c2 && c.startsWith(c2)
}))
(quantifiers, clauses)
}
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))
newform
}
/**
......
src/main/scala/de/tum/workflows/ltl/FOTransformers.scala
View file @ 19d48092
......@@ -49,16 +49,13 @@ object FOTransformers extends LazyLogging {
case Quantifier(make, vars, inner) => make(vars.filterNot(bound.contains).distinct, elimSub(inner, bound ++ vars))
}
}
elimSub(f, Set())
elimSub(f.toNegNf(), Set())
}
def eliminateAuxiliaryPredicate(f:Formula, AUX:String) = {
val cnf = f.toCNF()
val quantifiers = FormulaFunctions.collectQuantifiers(cnf)
val (quantifiers, clauses) = FormulaFunctions.toCNFClauses(f)
// Inspect clauses
val clauses = FOTransformers.collectClauses(cnf)
val simped =
for (c <- clauses;
removeclause = (for (c1 <- c if (c.contains(Neg(c1)))) yield true)
......@@ -67,15 +64,8 @@ object FOTransformers extends LazyLogging {
c
}
// TODO improve runtime
val simp2 = simped.filterNot(c => simped.exists(c2 => {
// check if c is superset of c2
c != c2 && c.startsWith(c2)
}))
val form = And.make(simp2.map(Or.make _))
// TODO: improve
val form = And.make(simped.map(Or.make _))
val newform = quantifiers.foldRight(form)((q, inner) => if