Commit 5cbd41fb authored by Christian Müller's avatar Christian Müller

add ts graphs

parent d9062f39
......@@ -4,7 +4,7 @@ import de.tum.niwo.foltl.FOLTL._
import scalax.collection.edge.LBase.LEdgeImplicits
import de.tum.niwo.blocks.SimpleWFBlock
object Implicits extends LEdgeImplicits[SimpleWFBlock[_ <: SimpleWFBlock[_]]] {
object Implicits {
implicit def toList[A](v: A): List[A] = List(v)
// Logic
......
......@@ -11,7 +11,7 @@ import de.tum.niwo.toz3._
import de.tum.niwo.foltl.Properties
// Labelled Edge to Block
import Implicits._
import de.tum.niwo.graphs.WFGraphEncoding.EdgeImplicits._
object MainInvariantsInterpolation extends App with LazyLogging {
......
......@@ -9,94 +9,7 @@ import de.tum.niwo.toz3.{InvProperties, Z3BSFO}
object Preconditions extends LazyLogging {
private def elaborateSteps(b: SimpleWFBlock[_], spec: NISpec, properties: InvProperties):List[SimpleWFBlock[_]] = {
val guardfix = if (!b.isoracly && b.pred.isDefined) {
// is "normal" may block
val choice = Fun(b.pred.get, b.agents)
val fixed = for (s <- b.steps) yield {
val first = s.tuple.head
val inner = if (first.typ == spec.target.params.head.typ) {
if (properties.stubborn) {
choice.in(T1)
} else {
val inf = Fun(INFNAME, List(b.agents.head))
Or(And(Neg(inf.in(T1)), choice.in(T1)), And(inf.in(T1), choice))
}
} else {
choice
}
val newguard = And(s.guard, inner)
s.update(guard = newguard)
}
fixed
} else {
b.steps
}
// FIXME: wät? why do I have to cast this? this should be an inference error
val newb:Any = b.update(guardfix)
// for causality, add informedness updates
val list = if (properties.stubborn) {
List(newb)
} else {
val newsteps = for (
stmt <- b.steps
if spec.causals.map(_.typ).contains(stmt.tuple.head.typ) ||
stmt.tuple.head.typ == spec.target.params.head.typ) yield {
val fun = Fun(stmt.fun, stmt.tuple)
// TODO
val guard = Neg(Equiv(fun.in(T1), fun.in(T2)))
ForallWFBlock(stmt.tuple, List(Add(guard, INFNAME, List(stmt.tuple.head))))
}
newb :: newsteps
}
list.asInstanceOf[List[SimpleWFBlock[_]]]
}
// For oracly blocks, remove O from guard and add to ForallMay choice predicate
private def elaborateOraclyBlock(b: SimpleWFBlock[_], spec: NISpec) = {
if (b.isoracly) {
val stmt = b.steps.head // can only be one
def findOracle(f: Formula) = {
f.collect {
case f: Fun if f.isOracle => List(f.name)
}
}
val oracles = findOracle(stmt.guard)
val name = oracles.head
if (oracles.size != 1) {
logger.error(s"Found oracly block $b with more than one oracle")
}
val choice = Fun(name, b.agents)
def fixguard(f: Formula, choice:Fun) = {
val nooracles = f.everywhere {
case f: Fun if f.isOracle => True
}
val decl = spec.declass.getOrElse(name, (List(), False))._2
// FIXME: substitutions?
// FIXME: decl in T2?
And(nooracles, Or(And(decl.in(T1), choice.in(T1)), And(Neg(decl.in(T1)), choice)))
}
val newstmt = stmt match {
case Add(guard, fun, tuple) => Add(fixguard(guard, choice).simplify, fun, tuple)
case Remove(guard, fun, tuple) => Remove(fixguard(guard, choice).simplify, fun, tuple)
}
ForallMayWFBlock(b.agents, name, List(newstmt))
} else b
}
def subst(f: Formula, updates: List[(String, (List[FOLTL.Var], FOLTL.Formula))], b: SimpleWFBlock[_]): Formula = {
def subst(f: Formula, updates: List[(String, (List[FOLTL.Var], FOLTL.Formula))], b: SimpleTSBlock): Formula = {
// TODO: should this contain f.freeVars?
val boundvars = f.boundVars
updates.foldRight(f)((update, f) => {
......@@ -119,40 +32,21 @@ object Preconditions extends LazyLogging {
})
}
def getUpdate(s:Statement[_], spec:NISpec, properties:InvProperties): Formula = {
val frees = s.guard.freeVars -- s.tuple.toSet -- spec.constants
val form = s match {
case Add(_, _, _) => {
Or(Fun(s.fun, s.tuple), Exists(frees.toList, s.guard)).simplify
}
case Remove(_, _, _) => {
And(Fun(s.fun, s.tuple), Forall(frees.toList, Neg(s.guard))).simplify
}
}
form
}
def elaborate(block: SimpleWFBlock[_], spec:NISpec, properties:InvProperties): List[SimpleWFBlock[_]] = {
val stepOne = elaborateSteps(block, spec, properties)
stepOne map { b => elaborateOraclyBlock(b, spec) }
def getUpdate(s:SetStmt, spec:InvariantSpec, properties:InvProperties): Formula = {
val frees = s.guard.freeVars -- s.tuple.toSet -- spec.ts.sig.constants
Exists(frees.toList, s.guard).simplify
}
def weakestPrecondition(post: Formula, outerb: SimpleWFBlock[_], spec: NISpec, properties: InvProperties): Formula = {
// TODO: Make 2-trace elaboration optional
val steps = elaborate(outerb, spec, properties)
// FIXME: is this still needed?
// def weakestPrecondition(post: Formula, outerb: SimpleTSBlock, spec: InvariantSpec, properties: InvProperties): Formula = {
// val precond = outerb.steps.foldRight(post)((b, f) => {
// val innerprecond = weakestPreconditionSingle(f, b, spec, properties)
// innerprecond
// })
// precond
// }
val precond = steps.foldRight(post)((b, f) => {
val innerprecond = weakestPreconditionSingle(f, b, spec, properties)
innerprecond
})
precond
}
private def weakestPreconditionSingle(f: Formula, b:SimpleWFBlock[_], spec: NISpec, properties: InvProperties) = {
private def weakestPrecondition(f: Formula, b:SimpleTSBlock, spec: InvariantSpec, properties: InvProperties) = {
val updates = for (s <- b.steps) yield {
s.fun -> (s.tuple, {
......@@ -173,11 +67,11 @@ object Preconditions extends LazyLogging {
}
}
// replaced
removed
replaced
// removed
}
def abstractedPrecondition(f: Formula, b: SimpleWFBlock[_], spec: NISpec, properties: InvProperties, untouched: Set[String]): Formula = {
def abstractedPrecondition(f: Formula, b: SimpleTSBlock, spec: InvariantSpec, properties: InvProperties, untouched: Set[String]): Formula = {
val precond = weakestPrecondition(f, b, spec, properties)
// Assume untouched predicates empty
......@@ -185,10 +79,10 @@ object Preconditions extends LazyLogging {
val z3simpednewinv = Z3BSFO.simplifyBS(untouchedprecond)
// if informedness untouched T1 and T2 are equal anyway, so remove annotations
// TODO: better recognition for necessarily equal
// if informedness untouched then T1 and T2 are equal anyway, so remove annotations
// TODO: better recognition for necessarily equal, this does not work for general cases (also, this is hyperprop-specific)
val removedannotations = if (untouched.contains(Properties.INFNAME)) {
val rels = spec.w.sig.preds.map(_.name)
val rels = spec.ts.sig.preds.map(_.name)
rels.foldRight(z3simpednewinv)((r, f) => Z3BSFO.simplifyBS(FormulaFunctions.removeAnnotation(f, r)))
} else {
z3simpednewinv
......@@ -203,29 +97,27 @@ object Preconditions extends LazyLogging {
removedannotations
}
// Eliminate Choices
val auxless = if (b.pred.isDefined && properties.eliminateA) {
FOTransformers.eliminateAuxiliaryPredicate(universalinv, b.pred.get)
} else {
universalinv
}
// Eliminate Oracles
// Eliminate As (choices/oracles)
val oless = if (properties.eliminateA) {
val oracles = spec.w.sig.as.map(_.name)
oracles.foldRight(auxless)((b, inv) => FOTransformers.eliminateAuxiliaryPredicate(inv, b))
val oracles = spec.ts.sig.as.map(_.name)
val occuringAs = oracles.filter(AUX =>
universalinv.hasSubFormula { case Fun(AUX, _, _) => true }
)
occuringAs.foldRight(universalinv)((AUX, inv) =>
FOTransformers.eliminateAuxiliaryPredicate(inv, AUX)
)
} else {
auxless
universalinv
}
// Win game
// Eliminate Bs (Win game)
val bless = if (properties.eliminateB) {
val bs = spec.w.sig.bs
val bs = spec.ts.sig.bs
val occuringBs = bs.filter(b =>
oless.hasSubFormula {
case Fun(b.name, _, _) => true
}
oless.hasSubFormula { case Fun(b.name, _, _) => true }
)
if (occuringBs.nonEmpty && !untouched.contains(Properties.INFNAME)) {
......
......@@ -7,6 +7,7 @@ import java.io.PrintWriter
import de.tum.niwo.toz3.{InvProperties, InvariantChecker, Z3BSFO}
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.graphs.WFGraphEncoding
object Utils extends LazyLogging {
......@@ -91,8 +92,9 @@ object Utils extends LazyLogging {
true
}
val elabdot = Encoding.toDot(graph, Some(properties, spec))(Map(), Set())
Utils.write(name, s"${filenames}_elaborated.dot", elabdot)
// FIXME move this
// val elabdot = WFGraphEncoding.toDot(graph)(Map(), Set())
// Utils.write(name, s"${filenames}_elaborated.dot", elabdot)
val labels = (for ((node, inv) <- labelling.last) yield {
s"Node ${node}:\n${inv.pretty}\n"
......
package de.tum.niwo
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.Properties.{INFNAME, T1, T2}
import de.tum.niwo.toz3.InvProperties
object TSConverter extends LazyLogging {
def toInvariantSpec(spec:NISpec):InvariantSpec = {
// Elaborate all statements to Hyperproperty updates with informedness depending on stubbornness
// (maybe add causal switch into spec)
// Map WFLoop/Nondet to TSLoop/TSNondet
// Map Add/Remove statements to SetStmt
val frees = s.guard.freeVars -- s.tuple.toSet -- spec.constants
// TODO: Make 2-trace elaboration optional
val steps = elaborate(outerb, spec, properties)
}
def getUpdate(s:Statement[_], spec:InvariantSpec, properties:InvProperties): Formula = {
val frees = s.guard.freeVars -- s.tuple.toSet -- spec.ts.sig.constants
val form = s match {
case Add(_, _, _) => {
Or(Fun(s.fun, s.tuple), Exists(frees.toList, s.guard)).simplify
}
case Remove(_, _, _) => {
And(Fun(s.fun, s.tuple), Forall(frees.toList, Neg(s.guard))).simplify
}
}
form
True
}
def elaborate(block: SimpleWFBlock[_], spec:NISpec, properties:InvProperties): List[SimpleWFBlock[_]] = {
val stepOne = elaborateSteps(block, spec, properties)
stepOne map { b => elaborateOraclyBlock(b, spec) }
}
// For oracly blocks, remove O from guard and add to ForallMay choice predicate
private def elaborateOraclyBlock(b: SimpleWFBlock[_], spec: NISpec) = {
if (b.isoracly) {
val stmt = b.steps.head // can only be one
def findOracle(f: Formula) = {
f.collect {
case f: Fun if f.isOracle => List(f.name)
}
}
val oracles = findOracle(stmt.guard)
val name = oracles.head
if (oracles.size != 1) {
logger.error(s"Found oracly block $b with more than one oracle")
}
val choice = Fun(name, b.agents)
def fixguard(f: Formula, choice:Fun) = {
val nooracles = f.everywhere {
case f: Fun if f.isOracle => True
}
val decl = spec.declass.getOrElse(name, (List(), False))._2
// FIXME: substitutions?
// FIXME: decl in T2?
And(nooracles, Or(And(decl.in(T1), choice.in(T1)), And(Neg(decl.in(T1)), choice)))
}
val newstmt = stmt match {
case Add(guard, fun, tuple) => Add(fixguard(guard, choice).simplify, fun, tuple)
case Remove(guard, fun, tuple) => Remove(fixguard(guard, choice).simplify, fun, tuple)
}
ForallMayWFBlock(b.agents, name, List(newstmt))
} else b
}
private def elaborateSteps(b: SimpleWFBlock[_], spec: NISpec, properties: InvProperties):List[SimpleWFBlock[_]] = {
val guardfix = if (!b.isoracly && b.pred.isDefined) {
// is "normal" may block
val choice = Fun(b.pred.get, b.agents)
val fixed = for (s <- b.steps) yield {
val first = s.tuple.head
val inner = if (first.typ == spec.target.params.head.typ) {
if (properties.stubborn) {
choice.in(T1)
} else {
val inf = Fun(INFNAME, List(b.agents.head))
Or(And(Neg(inf.in(T1)), choice.in(T1)), And(inf.in(T1), choice))
}
} else {
choice
}
val newguard = And(s.guard, inner)
s.update(guard = newguard)
}
fixed
} else {
b.steps
}
// FIXME: wät? why do I have to cast this? this should be an inference error
val newb:Any = b.update(guardfix)
// for causality, add informedness updates
val list = if (properties.stubborn) {
List(newb)
} else {
val newsteps = for (
stmt <- b.steps
if spec.causals.map(_.typ).contains(stmt.tuple.head.typ) ||
stmt.tuple.head.typ == spec.target.params.head.typ) yield {
val fun = Fun(stmt.fun, stmt.tuple)
// TODO
val guard = Neg(Equiv(fun.in(T1), fun.in(T2)))
ForallWFBlock(stmt.tuple, List(Add(guard, INFNAME, List(stmt.tuple.head))))
}
newb :: newsteps
}
list.asInstanceOf[List[SimpleWFBlock[_]]]
}
}
......@@ -59,8 +59,8 @@ object FOTransformers extends LazyLogging {
logger.debug(s"Eliminating universal second order predicate $AUX")
val cnf = f.toCNF
// TODO: saturate before doing this?
// TODO: saturate before doing this? - also make cnf configurable
val repld = cnf everywhere {
case Neg(Fun(AUX, _, _)) => False
case Fun(AUX, _, _) => False
......@@ -68,11 +68,11 @@ object FOTransformers extends LazyLogging {
repld.simplify
}
def eliminateBPredicate(f:Formula, b:Fun) = {
val NAME = b.name
def eliminateBPredicate(f:Formula, B:Fun) = {
val NAME = B.name
// SOQE: \exists B. f <-> f'
logger.debug(s"Eliminating existential second order predicate $b")
logger.debug(s"Eliminating existential second order predicate $B")
if (!f.isUniversal) {
logger.error("Trying to use SOQE on a non-universal formula")
......@@ -164,7 +164,7 @@ object FOTransformers extends LazyLogging {
// Compute solution
val bounds = gks.flatMap(_.freeVars) ++ gks.flatMap(_.boundVars)
val freeparams = b.params.map(p => FormulaFunctions.generateName(p, bounds.toSet))
val freeparams = B.params.map(p => FormulaFunctions.generateName(p, bounds.toSet))
val gkineq = for ((gk, gargs) <- gks.zip(Gargs); garg <- gargs) yield {
// Or.make(gk, ineq(garg, freeparams))
gk.parallelRename(garg, freeparams)
......@@ -176,7 +176,7 @@ object FOTransformers extends LazyLogging {
val z3fsolq = Z3BSFO.simplifyBS(fsolq)
if (Utils.DEBUG_MODE) {
logger.info(s"BSFO SOQE: strategy for ${b.updatedParams(freeparams)}: $z3fsolq")
logger.info(s"BSFO SOQE: strategy for ${B.updatedParams(freeparams)}: $z3fsolq")
}
(felimq, z3fsolq)
......
package de.tum.niwo.foltl
import de.tum.niwo.Encoding._
import de.tum.niwo.graphs.WFGraphEncoding._
import de.tum.niwo.blocks._
import scalax.collection.Graph
import scalax.collection.edge.LDiEdge
......
package de.tum.niwo.foltl
import de.tum.niwo.Implicits._
import de.tum.niwo.Encoding._
import de.tum.niwo.graphs.WFGraphEncoding._
import de.tum.niwo.foltl.LTLEncoding._
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._
......
package de.tum.niwo
package de.tum.niwo.graphs
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.blocks._
import de.tum.niwo.graphs.WFGraphEncoding.MAXINVLENGTH
import scalax.collection.Graph
import de.tum.niwo.Implicits._
import scalax.collection.edge.LDiEdge
import scalax.collection.edge.Implicits._
import blocks._
import de.tum.niwo.foltl.Properties
import de.tum.niwo.foltl.FOLTL._
import com.typesafe.scalalogging._
import scalax.collection.io.dot._
import implicits._
import Implicits._
import de.tum.niwo.toz3.InvProperties
import scalax.collection.GraphTraversal.BreadthFirst
import scalax.collection.io.dot.implicits._
object Encoding extends LazyLogging {
trait GraphBuilder extends LazyLogging {
type WorkflowGraph = Graph[Int, LDiEdge]
val MAXINVLENGTH = 800
def toGraph[BL <: Block](steps:List[_ <: Block], makeid: () => BL): Graph[Int, LDiEdge] = {
var n1 = 0
def newnode() = {
n1 = n1 + 1
n1
}
val edges = (for ((step, i) <- steps.zipWithIndex) yield {
if (i == 0 && step.isInstanceOf[Loop[_, _]]) {
logger.info("Found loop in the initial step")
val n = n1
val n2 = newnode()
val n3 = newnode()
val edges = makeblock(step, n2, n3, newnode, makeid)
val e2 = edges :+ (n ~+> n2)(makeid())
val e3 = if (i == steps.size - 1) {
e2 :+ (n3 ~+> n3)(makeid())
} else e2
e3
} else if (i == steps.size - 1) {
val n = n1
val n2 = newnode()
val edges = makeblock(step, n, n2, newnode, makeid)
edges :+ (n2 ~+> n2)(makeid())
} else {
makeblock(step, n1, newnode(), newnode, makeid)
}
}).flatten
val nodes = (0 until n1).toList
Graph.from(nodes, edges)
}
// Naming
// TODO: make sure there are no clashes
def nodeVar(n: Any) = Fun("n" + n, List())
def choiceVar(n: Any) = "choice" + n
def toBlock(e:WorkflowGraph#EdgeT):SimpleWFBlock[_] = e
def toNumber(n:WorkflowGraph#NodeT):Int = n.toOuter
def makeblock[BL <: Block](b: BL, n1: Int, n2: Int, makeNode: () => Int, makeId: () => BL): List[LDiEdge[Int]] = {
......@@ -73,65 +101,19 @@ object Encoding extends LazyLogging {
}
}
def toGraph(w: Workflow): WorkflowGraph = {
var n1 = 0
def newnode() = {
n1 = n1 + 1
n1
}
def makeid() = ForallWFBlock(List(), List())
val edges = (for ((step, i) <- w.steps.zipWithIndex) yield {
if (i == 0 && step.isInstanceOf[Loop[_, _]]) {
logger.info("Found loop in the initial step")
val n = n1
val n2 = newnode()
val n3 = newnode()
val edges = makeblock(step, n2, n3, newnode, makeid)
val e2 = edges :+ (n ~+> n2)(makeid())
val e3 = if (i == w.steps.size - 1) {
e2 :+ (n3 ~+> n3)(makeid())
} else e2
e3
} else if (i == w.steps.size - 1) {
val n = n1
val n2 = newnode()
val edges = makeblock(step, n, n2, newnode, makeid)
edges :+ (n2 ~+> n2)(makeid())
} else {
makeblock(step, n1, newnode(), newnode, makeid)
}
}).flatten
val nodes = (0 until n1).toList
Graph.from(nodes, edges)
}
val MAXINVLENGTH = 800
def toDot(g: WorkflowGraph, elaboration:Option[(InvProperties, NISpec)] = None)(labels:Map[Int, String], edges:Set[g.EdgeT]) = {
def toDot(g: Graph[Int, LDiEdge])(labels:Map[Int, String], edges:Set[g.EdgeT]) = {
val root = DotRootGraph(
directed = true,
id = Some("Invariant Labelling")
)
def edgeTransformer(innerEdge: WorkflowGraph#EdgeT): Option[(DotGraph, DotEdgeStmt)] = innerEdge.edge match {
def edgeTransformer(innerEdge: Graph[Int, LDiEdge]#EdgeT): Option[(DotGraph, DotEdgeStmt)] = innerEdge.edge match {
case LDiEdge(source, target, label) => label match {
case label: SimpleWFBlock[_] => {
case label: SimpleBlock[_, _] => {
val green = edges.exists(_ == innerEdge)
val color = List(DotAttr("color", if (green) "green" else "red"))
val elaborated = (elaboration map {
case (prop, spec) => Preconditions.elaborate(label, spec, prop)
}).getOrElse(List(label))
val strlabel = elaborated.mkString("\n")
val labelled = DotAttr("label", strlabel) :: color
val labelled = DotAttr("label", label.toString) :: color
Some((
root,
......@@ -145,7 +127,7 @@ object Encoding extends LazyLogging {
}
}
def nodeTransformer(innerNode: WorkflowGraph#NodeT): Option[(DotGraph, DotNodeStmt)] = {
def nodeTransformer(innerNode: Graph[Int, LDiEdge]#NodeT): Option[(DotGraph, DotNodeStmt)] = {
val str = labels.withDefault(d => s"$d").apply(innerNode.value)
val label = if (str.length() > MAXINVLENGTH) str.substring(0, MAXINVLENGTH) + "..." + s"(${str.length()} characters)" else str
Some((root, DotNodeStmt(innerNode.toString, List(DotAttr("label", "Node " + innerNode + ":\n" + label)))))
......@@ -153,33 +135,4 @@ object Encoding extends LazyLogging {
g.toDot(root, edgeTransformer, None, Some(nodeTransformer))
}
/**
* Get an underapproximation of relation symbols that are sure to be untouched, i.e. empty
*
* @param w the graph
*/
def untouchedMap(g:WorkflowGraph, sig:Signature, props:InvProperties): Map[g.NodeT, Set[String]] = {
val sourceid = 0
val sourcenode = g.get(sourceid)
val nodes = sourcenode.withKind(BreadthFirst).filterNot(_ == sourcenode)
// this could 1. be more functional, 2. not just give up for loops
var map:Map[g.NodeT, Set[String]] = Map().withDefault(_ => Set())
// initially all untouched
// TODO: maybe introduce informedness as sig.pred?
map = map.updated(g.get(sourceid), sig.preds.map(_.name) ++ Some(Properties.INFNAME) )
for (elem <- nodes) {
// If all predecessors are known
if (elem.diPredecessors.forall(map.contains(_))) {
val union = elem.diPredecessors.flatMap(map(_))
val touched = elem.incoming.flatMap(_.updating)
map = map.updated(elem, union -- touched)
}
}
map
}
}
\ No newline at end of file
}
package de.tum.niwo.graphs
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL.Fun
import de.tum.niwo.foltl.Properties
import de.tum.niwo.graphs.WFGraphEncoding.WorkflowGraph
import de.tum.niwo.toz3.InvProperties
import scalax.collection.Graph
import scalax.collection.GraphTraversal.BreadthFirst
import scalax.collection.edge.LBase.LEdgeImplicits
import scalax.collection.edge.LDiEdge
object TSGraphEncoding extends GraphBuilder with LazyLogging {
type TSGraph = Graph[Int, LDiEdge]
object EdgeImplicits extends LEdgeImplicits[SimpleTSBlock]
import EdgeImplicits._
def nodeVar(n: Any) = Fun("n" + n, List())
def toBlock(e:TSGraph#EdgeT):SimpleTSBlock = e.label
def toNumber(n:TSGraph#NodeT):Int = n.toOuter
def toGraph(w:TransitionSystem): TSGraph = {
def makeid() = SimpleTSBlock(List())
toGraph(w.steps, makeid)
}