Commit 31eadc9d authored by Christian Müller's avatar Christian Müller

test tsconverter, add untouchedmap

parent 8c862890
...@@ -56,7 +56,7 @@ object InvariantInspector extends App with LazyLogging { ...@@ -56,7 +56,7 @@ object InvariantInspector extends App with LazyLogging {
val auxes = List("Ot1", "Ot2") val auxes = List("Ot1", "Ot2")
// val auxes = List() // val auxes = List()
val auxless = auxes.foldLeft(diffos)((inv, p) => val auxless = auxes.foldLeft(diffos)((inv, p) =>
FOTransformers.eliminateAuxiliaryPredicate(inv, p) FOTransformers.eliminateAuxiliaryPredicate(inv, p, props)
) )
val simped = auxless.toCNF.simplify val simped = auxless.toCNF.simplify
logger.info(s"auxless: ${simped.pretty}") logger.info(s"auxless: ${simped.pretty}")
......
...@@ -32,7 +32,8 @@ object MainInvariantsInference extends App with LazyLogging { ...@@ -32,7 +32,8 @@ object MainInvariantsInference extends App with LazyLogging {
val props = InvProperties( val props = InvProperties(
stubborn = true, stubborn = true,
eliminateA = true, eliminateA = true,
eliminateB = true eliminateB = true,
approxElim = true
) )
// val (res, graph, labels, t) = InvariantChecker.checkInvariantFPHeadLabel(spec, inv, props) // val (res, graph, labels, t) = InvariantChecker.checkInvariantFPHeadLabel(spec, inv, props)
......
...@@ -15,7 +15,7 @@ object Utils extends LazyLogging { ...@@ -15,7 +15,7 @@ object Utils extends LazyLogging {
val RESULTSFOLDER = "results" val RESULTSFOLDER = "results"
val DEBUG_MODE = true val DEBUG_MODE = true
def mkString[T](string: Iterable[T], start: String, mid: String, end: String) = { def mkString[T](string: Iterable[T], start: String, mid: String, end: String): String = {
if (string.isEmpty) "" else string.mkString(start, mid, end) if (string.isEmpty) "" else string.mkString(start, mid, end)
} }
...@@ -28,15 +28,15 @@ object Utils extends LazyLogging { ...@@ -28,15 +28,15 @@ object Utils extends LazyLogging {
} }
} }
def allchoices(w: Workflow) = { def allchoices(w: Workflow): Set[Fun] = {
w.steps.flatMap(collectChoices).toSet w.steps.flatMap(collectChoices).toSet
} }
def indentLines(s: String) = { def indentLines(s: String): String = {
s.lines.map(" " + _).mkString("\n") s.lines.map(" " + _).mkString("\n")
} }
def time[R](block: => R) = { def time[R](block: => R): (Long, R) = {
val t0 = System.nanoTime() val t0 = System.nanoTime()
val result = block // call-by-name val result = block // call-by-name
val t1 = System.nanoTime() val t1 = System.nanoTime()
...@@ -69,6 +69,15 @@ object Utils extends LazyLogging { ...@@ -69,6 +69,15 @@ object Utils extends LazyLogging {
} }
def check(name: String, desc:String, inv:NISpec => Formula, spec:NISpec, properties: InvProperties):Boolean = { def check(name: String, desc:String, inv:NISpec => Formula, spec:NISpec, properties: InvProperties):Boolean = {
val basename = name.split("/").last
val filenames = s"$basename${if (desc.isEmpty) "" else s"_$desc"}"
// initial wf graph
val graph = WFGraphEncoding.toGraph(spec.w)
val elabdot = WFGraphEncoding.toDot(graph)(Map(), Set())
Utils.write(name, s"${filenames}_workflow.dot", elabdot)
val invspec = TSConverter.toInvariantSpec(spec, properties, inv) val invspec = TSConverter.toInvariantSpec(spec, properties, inv)
check(name, desc, invspec, properties) check(name, desc, invspec, properties)
} }
...@@ -77,7 +86,7 @@ object Utils extends LazyLogging { ...@@ -77,7 +86,7 @@ object Utils extends LazyLogging {
val model = if (properties.stubborn) "stubborn" else "causal" val model = if (properties.stubborn) "stubborn" else "causal"
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 (res, graph, labelling, provens, dot, time) = val (res, graph, labelling, provens, dot, time) =
InvariantChecker.checkInvariantFPLabelling(spec, properties) InvariantChecker.checkInvariantFPLabelling(spec, properties)
...@@ -94,13 +103,10 @@ object Utils extends LazyLogging { ...@@ -94,13 +103,10 @@ object Utils extends LazyLogging {
for ((s, i) <- dot.zipWithIndex) { for ((s, i) <- dot.zipWithIndex) {
Utils.write(name,s"${filenames}_$i.dot", s) Utils.write(name,s"${filenames}_$i.dot", s)
} }
val strengthenings = for (List(a, b) <- labelling.sliding(2) if (a != b)) yield { val strengthenings = for (List(a, b) <- labelling.sliding(2) if a != b) yield {
true true
} }
// 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 { val labels = (for ((node, inv) <- labelling.last) yield {
s"Node ${node}:\n${inv.pretty}\n" s"Node ${node}:\n${inv.pretty}\n"
......
...@@ -23,11 +23,15 @@ object TSConverter extends LazyLogging { ...@@ -23,11 +23,15 @@ object TSConverter extends LazyLogging {
// Map Add/Remove statements to SetStmt // Map Add/Remove statements to SetStmt
val steps = elaborated.map(s => toTSBlock(s)(w.sig, properties)) val steps = elaborated.map(s => toTSBlock(s)(w.sig, properties))
// Add causals to constants? // Add causals to constants, add informedness for causal agents
val newsig = w.sig.copy( val newsig = if (!properties.stubborn) {
preds = w.sig.preds + Fun(INFNAME, List(spec.target.params.head)), w.sig.copy(
constants = spec.causals.toSet ++ w.sig.constants preds = w.sig.preds + Fun(INFNAME, List(spec.target.params.head)),
) constants = spec.causals.toSet ++ w.sig.constants
)
} else {
w.sig
}
val ts = TransitionSystem(newsig, steps) val ts = TransitionSystem(newsig, steps)
...@@ -106,7 +110,7 @@ object TSConverter extends LazyLogging { ...@@ -106,7 +110,7 @@ object TSConverter extends LazyLogging {
b.steps b.steps
} }
// FIXME: wät? why do I have to cast this? this should be an inference error // FIXME: wät? why do I have to cast this? this should be correctly inferred by the compiler
val newb:Any = b.update(guardfix) val newb:Any = b.update(guardfix)
// for causality, add informedness updates // for causality, add informedness updates
......
...@@ -10,8 +10,7 @@ case class Signature(as: Set[Fun], constas: Set[Fun], bs: Set[Fun], preds: Set[F ...@@ -10,8 +10,7 @@ case class Signature(as: Set[Fun], constas: Set[Fun], bs: Set[Fun], preds: Set[F
{ {
def mkString(set:Set[Fun]) = set.map(_.toTypedString).mkString(",") def mkString(set:Set[Fun]) = set.map(_.toTypedString).mkString(",")
val inner = val inner =
s""" s"""EmptyPredicates:${mkString(preds)}
|EmptyPredicates:${mkString(preds)}
|AxiomPredicates:${mkString(constas)} |AxiomPredicates:${mkString(constas)}
|As:${mkString(as)} |As:${mkString(as)}
|Bs:${mkString(bs)} |Bs:${mkString(bs)}
...@@ -26,10 +25,9 @@ object Signature { ...@@ -26,10 +25,9 @@ object Signature {
} }
case class TransitionSystem(sig: Signature, steps: List[TSBlock]) { case class TransitionSystem(sig: Signature, steps: List[TSBlock]) {
override def toString: String = steps.mkString("\n") override def toString: String = s"$sig\nTransition System\n${Utils.indentLines(steps.mkString("\n"))}"
def isSane() = {
def isSane: Boolean = {
// check that the steps fit the signature // check that the steps fit the signature
val uses = ParserUtils.allpredicates(steps) val uses = ParserUtils.allpredicates(steps)
val sanesteps = ParserUtils.checkSig(sig, uses) val sanesteps = ParserUtils.checkSig(sig, uses)
...@@ -47,9 +45,9 @@ trait Spec { ...@@ -47,9 +45,9 @@ trait Spec {
case class InvariantSpec(ts:TransitionSystem, axioms:Formula, inv:Formula) extends Spec { case class InvariantSpec(ts:TransitionSystem, axioms:Formula, inv:Formula) extends Spec {
override def toString: String = { override def toString: String = {
s"InvSpec\nTransition System:\n$ts\n\nAxioms:\n$axioms\n\nInvariant:$inv\n" s"InvSpec\n$ts\n\nAxioms\n${Utils.indentLines(axioms.toString)}\n\nInvariant\n${Utils.indentLines(inv.toString)}\n"
} }
def addAxiom(k:Formula) = { def addAxiom(k:Formula): InvariantSpec = {
copy(axioms = And.make(axioms, k)) copy(axioms = And.make(axioms, k))
} }
// def addInv(k:Formula) = { // def addInv(k:Formula) = {
...@@ -57,7 +55,7 @@ case class InvariantSpec(ts:TransitionSystem, axioms:Formula, inv:Formula) exten ...@@ -57,7 +55,7 @@ case class InvariantSpec(ts:TransitionSystem, axioms:Formula, inv:Formula) exten
// } // }
def isSane: Boolean = { def isSane: Boolean = {
// TODO: add sanity checking for axioms and invariant signatures // TODO: add sanity checking for axioms and invariant signatures
ts.isSane() ts.isSane
} }
} }
object InvariantSpec { object InvariantSpec {
...@@ -86,7 +84,7 @@ case class Remove(guard: Formula, fun: String, tuple: List[Var]) extends Stateme ...@@ -86,7 +84,7 @@ case class Remove(guard: Formula, fun: String, tuple: List[Var]) extends Stateme
} }
case class SetStmt(guard:Formula, fun:String, tuple: List[Var]) extends Statement[SetStmt] { case class SetStmt(guard:Formula, fun:String, tuple: List[Var]) extends Statement[SetStmt] {
override def toString: String = guard + " → " + fun + " := " + tuple.mkString("(", ",", ")") + ";" override def toString: String = fun + tuple.mkString("(", ",", ")") + " := " + guard + ";"
def toTypedString: String = guard.toTypedString + " → " + fun + " := " + tuple.map(_.withType).mkString("(", ",", ")") + ";" def toTypedString: String = guard.toTypedString + " → " + fun + " := " + tuple.map(_.withType).mkString("(", ",", ")") + ";"
override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = copy(guard, fun, tuple) override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = copy(guard, fun, tuple)
} }
......
...@@ -104,7 +104,7 @@ object NISpec { ...@@ -104,7 +104,7 @@ object NISpec {
sealed trait WFBlock extends Block sealed trait WFBlock extends Block
trait SimpleWFBlock[T <: SimpleWFBlock[T]] extends SimpleBlock[SimpleWFBlock[T], Statement[_]] with WFBlock { sealed trait SimpleWFBlock[T <: SimpleWFBlock[T]] extends SimpleBlock[SimpleWFBlock[T], Statement[_]] with WFBlock {
def agents: List[Var] def agents: List[Var]
def may: Boolean def may: Boolean
def pred: Option[String] def pred: Option[String]
......
...@@ -3,6 +3,7 @@ package de.tum.niwo.foltl ...@@ -3,6 +3,7 @@ package de.tum.niwo.foltl
import com.typesafe.scalalogging.LazyLogging import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.Utils import de.tum.niwo.Utils
import de.tum.niwo.foltl.FOLTL._ import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.invariants.InvProperties
import de.tum.niwo.toz3.Z3BSFO import de.tum.niwo.toz3.Z3BSFO
object FOTransformers extends LazyLogging { object FOTransformers extends LazyLogging {
...@@ -55,12 +56,11 @@ object FOTransformers extends LazyLogging { ...@@ -55,12 +56,11 @@ object FOTransformers extends LazyLogging {
elimSub(f.toNegNf, Set()) elimSub(f.toNegNf, Set())
} }
def eliminateAuxiliaryPredicate(f:Formula, AUX:String) = { def eliminateAuxiliaryPredicate(f:Formula, AUX:String, props:InvProperties) = {
logger.debug(s"Eliminating universal second order predicate $AUX") logger.debug(s"Eliminating universal second order predicate $AUX")
val cnf = f.toCNF val cnf = if (!props.approxElim) f.toCNF else f.toNegNf
// TODO: saturate before doing this? - also make cnf configurable
val repld = cnf everywhere { val repld = cnf everywhere {
case Neg(Fun(AUX, _, _)) => False case Neg(Fun(AUX, _, _)) => False
case Fun(AUX, _, _) => False case Fun(AUX, _, _) => False
......
...@@ -2,7 +2,7 @@ package de.tum.niwo.graphs ...@@ -2,7 +2,7 @@ package de.tum.niwo.graphs
import com.typesafe.scalalogging.LazyLogging import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.blocks._ import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL.Fun import de.tum.niwo.foltl.FOLTL.{Fun, True}
import de.tum.niwo.foltl.Properties import de.tum.niwo.foltl.Properties
import de.tum.niwo.graphs.WFGraphEncoding.WorkflowGraph import de.tum.niwo.graphs.WFGraphEncoding.WorkflowGraph
import de.tum.niwo.invariants.InvProperties import de.tum.niwo.invariants.InvProperties
...@@ -34,7 +34,7 @@ object TSGraphEncoding extends GraphBuilder with LazyLogging { ...@@ -34,7 +34,7 @@ object TSGraphEncoding extends GraphBuilder with LazyLogging {
* *
* @param w the graph * @param w the graph
*/ */
def untouchedMap(g:WorkflowGraph, sig:Signature, props:InvProperties): Map[g.NodeT, Set[String]] = { def untouchedMap(g:TSGraph, sig:Signature, props:InvProperties): Map[g.NodeT, Set[String]] = {
val sourceid = 0 val sourceid = 0
val sourcenode = g.get(sourceid) val sourcenode = g.get(sourceid)
...@@ -44,7 +44,6 @@ object TSGraphEncoding extends GraphBuilder with LazyLogging { ...@@ -44,7 +44,6 @@ object TSGraphEncoding extends GraphBuilder with LazyLogging {
var map:Map[g.NodeT, Set[String]] = Map().withDefault(_ => Set()) var map:Map[g.NodeT, Set[String]] = Map().withDefault(_ => Set())
// initially all untouched // initially all untouched
// TODO: maybe introduce informedness as sig.pred?
map = map.updated(g.get(sourceid), sig.preds.map(_.name)) map = map.updated(g.get(sourceid), sig.preds.map(_.name))
for (elem <- nodes) { for (elem <- nodes) {
...@@ -57,4 +56,40 @@ object TSGraphEncoding extends GraphBuilder with LazyLogging { ...@@ -57,4 +56,40 @@ object TSGraphEncoding extends GraphBuilder with LazyLogging {
} }
map map
} }
/**
* Get an underapproximation of the nodes where all traces are sure to be equal
*
* @param w the graph
*/
def divergedMap(g:TSGraph, sig:Signature, props:InvProperties): Map[g.NodeT, Boolean] = {
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, Boolean] = Map().withDefault(_ => true)
// initially not diverged
map = map.updated(g.get(sourceid), false)
for (elem <- nodes) {
// If all predecessors are known
if (elem.diPredecessors.forall(map.contains(_))) {
// disjunction over all incoming edges
// if an incoming edge is diverged, this is also
val divergedPredecessor = elem.diPredecessors.exists(map(_))
// if the guard contains an A, also diverging
val anames = sig.as.map(_.name)
val touchedOracle = elem.incoming.exists(stmt =>
stmt.steps.exists(_.guard.hasSubFormula{
case Fun(name, _, _) if anames.contains(name) => true
})
)
map = map.updated(elem, divergedPredecessor || touchedOracle)
}
}
map
}
} }
package de.tum.niwo.graphs package de.tum.niwo.graphs
import com.typesafe.scalalogging._ import com.typesafe.scalalogging._
import de.tum.niwo.Preconditions
import de.tum.niwo.blocks._ import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._ import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.Properties import de.tum.niwo.foltl.Properties
...@@ -9,7 +8,7 @@ import scalax.collection.Graph ...@@ -9,7 +8,7 @@ import scalax.collection.Graph
import scalax.collection.GraphTraversal.BreadthFirst import scalax.collection.GraphTraversal.BreadthFirst
import scalax.collection.edge.LDiEdge import scalax.collection.edge.LDiEdge
import de.tum.niwo.Implicits._ import de.tum.niwo.Implicits._
import de.tum.niwo.invariants.InvProperties import de.tum.niwo.invariants.{InvProperties, Preconditions}
import scalax.collection.edge.LBase.LEdgeImplicits import scalax.collection.edge.LBase.LEdgeImplicits
object WFGraphEncoding extends GraphBuilder with LazyLogging { object WFGraphEncoding extends GraphBuilder with LazyLogging {
......
...@@ -8,24 +8,31 @@ import de.tum.niwo.foltl.FormulaFunctions ...@@ -8,24 +8,31 @@ import de.tum.niwo.foltl.FormulaFunctions
import de.tum.niwo.graphs.WFGraphEncoding.WorkflowGraph import de.tum.niwo.graphs.WFGraphEncoding.WorkflowGraph
import de.tum.niwo.graphs.{TSGraphEncoding, WFGraphEncoding} import de.tum.niwo.graphs.{TSGraphEncoding, WFGraphEncoding}
import de.tum.niwo.toz3.{Z3BSFO, Z3FOEncoding} import de.tum.niwo.toz3.{Z3BSFO, Z3FOEncoding}
import de.tum.niwo.{Preconditions, Utils} import de.tum.niwo.Utils
import scala.annotation.tailrec import scala.annotation.tailrec
case class InvProperties(stubborn:Boolean, eliminateA:Boolean, eliminateB:Boolean = false) { } case class InvProperties(stubborn:Boolean, eliminateA:Boolean = true, eliminateB:Boolean = true, approxElim:Boolean = true) { }
object InvProperties { object InvProperties {
val DEFAULT = InvProperties( val DEFAULT = InvProperties(
stubborn = true, stubborn = true,
eliminateA = true, eliminateA = true,
eliminateB = true eliminateB = true,
approxElim = true
) )
} }
object InvariantChecker extends LazyLogging { object InvariantChecker extends LazyLogging {
def checkBlockInvariant(spec: InvariantSpec, b: SimpleTSBlock, pre: Formula, post: Formula, properties:InvProperties, untouched:Set[String]): ((Status, Solver), Formula) = { def checkBlockInvariant(spec: InvariantSpec,
val precond = Preconditions.abstractedPrecondition(post, b, spec, properties, untouched) b: SimpleTSBlock,
pre: Formula,
post: Formula,
properties:InvProperties,
untouched:Set[String],
diverged:Boolean): ((Status, Solver), Formula) = {
val precond = Preconditions.abstractedPrecondition(post, b, spec, properties, untouched, diverged)
// pre is universal, spec.always is AE // pre is universal, spec.always is AE
val f = Implies(And(pre, spec.axioms), precond) val f = Implies(And(pre, spec.axioms), precond)
...@@ -41,6 +48,7 @@ object InvariantChecker extends LazyLogging { ...@@ -41,6 +48,7 @@ object InvariantChecker extends LazyLogging {
type Edge = graph.EdgeT type Edge = graph.EdgeT
val untouched = TSGraphEncoding.untouchedMap(graph, spec.ts.sig, properties) val untouched = TSGraphEncoding.untouchedMap(graph, spec.ts.sig, properties)
val diverged = TSGraphEncoding.divergedMap(graph, spec.ts.sig, properties)
@tailrec @tailrec
def checkInvariantRec(labellist: List[Map[Int, Formula]], provenlist: List[Set[Edge]]): (Boolean, List[Map[Int, Formula]], List[Set[Edge]]) = { def checkInvariantRec(labellist: List[Map[Int, Formula]], provenlist: List[Set[Edge]]): (Boolean, List[Map[Int, Formula]], List[Set[Edge]]) = {
...@@ -71,7 +79,8 @@ object InvariantChecker extends LazyLogging { ...@@ -71,7 +79,8 @@ object InvariantChecker extends LazyLogging {
pre, pre,
post, post,
properties, properties,
untouched(nextEdge.from)) untouched(nextEdge.from),
diverged(nextEdge.from))
val from = TSGraphEncoding.toNumber(nextEdge._1) val from = TSGraphEncoding.toNumber(nextEdge._1)
val to = TSGraphEncoding.toNumber(nextEdge._2) val to = TSGraphEncoding.toNumber(nextEdge._2)
...@@ -159,6 +168,7 @@ object InvariantChecker extends LazyLogging { ...@@ -159,6 +168,7 @@ object InvariantChecker extends LazyLogging {
// Build graph // Build graph
val graph = TSGraphEncoding.toGraph(spec.ts) val graph = TSGraphEncoding.toGraph(spec.ts)
val untouched = TSGraphEncoding.untouchedMap(graph, spec.ts.sig, properties) val untouched = TSGraphEncoding.untouchedMap(graph, spec.ts.sig, properties)
val diverged = TSGraphEncoding.divergedMap(graph, spec.ts.sig, properties)
val msg = new StringBuilder() val msg = new StringBuilder()
msg ++= s"Trying to prove safe with invariant:\n\n${spec.inv.pretty}\n\n" msg ++= s"Trying to prove safe with invariant:\n\n${spec.inv.pretty}\n\n"
...@@ -169,7 +179,7 @@ object InvariantChecker extends LazyLogging { ...@@ -169,7 +179,7 @@ object InvariantChecker extends LazyLogging {
// Check I -> WP[w](inv) // Check I -> WP[w](inv)
val b = TSGraphEncoding.toBlock(e) val b = TSGraphEncoding.toBlock(e)
val ((res, solver), _) = checkBlockInvariant(spec, b, spec.inv, spec.inv, properties, untouched(e.from)) val ((res, solver), _) = checkBlockInvariant(spec, b, spec.inv, spec.inv, properties, untouched(e.from), diverged(e.from))
if (res != Status.UNSATISFIABLE) { if (res != Status.UNSATISFIABLE) {
msg ++= s"Possibly unsafe: Block may not uphold invariant:\n\n${e.label}\n\n" msg ++= s"Possibly unsafe: Block may not uphold invariant:\n\n${e.label}\n\n"
......
package de.tum.niwo package de.tum.niwo.invariants
import com.typesafe.scalalogging._ import com.typesafe.scalalogging.LazyLogging
import blocks._ import de.tum.niwo.Utils
import de.tum.niwo.blocks.{InvariantSpec, SetStmt, SimpleTSBlock}
import de.tum.niwo.foltl.FOLTL.{Exists, Formula, Fun, Neg}
import de.tum.niwo.foltl.{FOLTL, FOTransformers, FormulaFunctions, Properties} import de.tum.niwo.foltl.{FOLTL, FOTransformers, FormulaFunctions, Properties}
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.Properties._
import de.tum.niwo.invariants.InvProperties
import de.tum.niwo.toz3.Z3BSFO import de.tum.niwo.toz3.Z3BSFO
object Preconditions extends LazyLogging { object Preconditions extends LazyLogging {
...@@ -72,7 +71,7 @@ object Preconditions extends LazyLogging { ...@@ -72,7 +71,7 @@ object Preconditions extends LazyLogging {
// removed // removed
} }
def abstractedPrecondition(f: Formula, b: SimpleTSBlock, spec: InvariantSpec, properties: InvProperties, untouched: Set[String]): Formula = { def abstractedPrecondition(f: Formula, b: SimpleTSBlock, spec: InvariantSpec, properties: InvProperties, untouched: Set[String], diverged:Boolean): Formula = {
val precond = weakestPrecondition(f, b, spec, properties) val precond = weakestPrecondition(f, b, spec, properties)
// Assume untouched predicates empty // Assume untouched predicates empty
...@@ -80,14 +79,13 @@ object Preconditions extends LazyLogging { ...@@ -80,14 +79,13 @@ object Preconditions extends LazyLogging {
val z3simpednewinv = Z3BSFO.simplifyBS(untouchedprecond) val z3simpednewinv = Z3BSFO.simplifyBS(untouchedprecond)
// if informedness untouched then T1 and T2 are equal anyway, so remove annotations // TODO: this is hyperproperty-specific
// TODO: better recognition for necessarily equal, this does not work for general cases (also, this is hyperprop-specific) val removedannotations = if (!diverged) {
val removedannotations = if (untouched.contains(Properties.INFNAME)) { val rels = spec.ts.sig.preds.map(_.name)
val rels = spec.ts.sig.preds.map(_.name) rels.foldRight(z3simpednewinv)((r, f) => Z3BSFO.simplifyBS(FormulaFunctions.removeAnnotation(f, r)))
rels.foldRight(z3simpednewinv)((r, f) => Z3BSFO.simplifyBS(FormulaFunctions.removeAnnotation(f, r))) } else {
} else { z3simpednewinv
z3simpednewinv }
}
// Abstract away inner existentials // Abstract away inner existentials
val universalinv = if (removedannotations.toNegNf.hasSubFormula { val universalinv = if (removedannotations.toNegNf.hasSubFormula {
...@@ -107,7 +105,7 @@ object Preconditions extends LazyLogging { ...@@ -107,7 +105,7 @@ object Preconditions extends LazyLogging {
) )
occuringAs.foldRight(universalinv)((AUX, inv) => occuringAs.foldRight(universalinv)((AUX, inv) =>
FOTransformers.eliminateAuxiliaryPredicate(inv, AUX) FOTransformers.eliminateAuxiliaryPredicate(inv, AUX, properties)
) )
} else { } else {
universalinv universalinv
...@@ -138,4 +136,4 @@ object Preconditions extends LazyLogging { ...@@ -138,4 +136,4 @@ object Preconditions extends LazyLogging {
Z3BSFO.simplifyBS(bless.simplify) Z3BSFO.simplifyBS(bless.simplify)
} }
} }
\ No newline at end of file
...@@ -35,6 +35,7 @@ object ParserUtils extends LazyLogging { ...@@ -35,6 +35,7 @@ object ParserUtils extends LazyLogging {
if (!checkTypes) { if (!checkTypes) {
logger.error(s"Predicate $k appears with conflicting arities or types") logger.error(s"Predicate $k appears with conflicting arities or types")
logger.error(s"Usage: ${list.map(_.toTypedString)}")
} }
val invalidConstants = for ( val invalidConstants = for (
......
...@@ -2,11 +2,10 @@ package de.tum.niwo.synth ...@@ -2,11 +2,10 @@ package de.tum.niwo.synth
import com.microsoft.z3.Status import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.Preconditions
import de.tum.niwo.blocks.{InvariantSpec, NISpec, SimpleTSBlock, SimpleWFBlock} import de.tum.niwo.blocks.{InvariantSpec, NISpec, SimpleTSBlock, SimpleWFBlock}
import de.tum.niwo.foltl.FOLTL._ import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.{FOTransformers, Properties} import de.tum.niwo.foltl.{FOTransformers, Properties}
import de.tum.niwo.invariants.InvProperties import de.tum.niwo.invariants.{InvProperties, Preconditions}
import de.tum.niwo.synth.Model.logger import de.tum.niwo.synth.Model.logger
import de.tum.niwo.toz3.Z3QFree import de.tum.niwo.toz3.Z3QFree
......
...@@ -7,7 +7,6 @@ import org.scalatest.Inspectors._ ...@@ -7,7 +7,6 @@ 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.blocks._ import de.tum.niwo.blocks._
import de.tum.niwo.Preconditions
import de.tum.niwo.foltl.FormulaFunctions import de.tum.niwo.foltl.FormulaFunctions
import de.tum.niwo.Examples import de.tum.niwo.Examples
import de.tum.niwo.graphs.WFGraphEncoding._ import de.tum.niwo.graphs.WFGraphEncoding._
...@@ -15,7 +14,7 @@ import de.tum.niwo.Utils ...@@ -15,7 +14,7 @@ import de.tum.niwo.Utils
import de.tum.niwo.tests.TestUtils._ import de.tum.niwo.tests.TestUtils._
import de.tum.niwo.foltl.Properties import de.tum.niwo.foltl.Properties
import de.tum.niwo.graphs.WFGraphEncoding import de.tum.niwo.graphs.WFGraphEncoding
import de.tum.niwo.invariants.InvariantGenerator import de.tum.niwo.invariants.{InvariantGenerator, Preconditions}
class InferenceTests extends FlatSpec { class InferenceTests extends FlatSpec {
......
...@@ -6,7 +6,6 @@ import org.scalatest.Inspectors._ ...@@ -6,7 +6,6 @@ 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.blocks._ import de.tum.niwo.blocks._
import de.tum.niwo.Preconditions
import de.tum.niwo.foltl.FormulaFunctions import de.tum.niwo.foltl.FormulaFunctions
import de.tum.niwo.Examples import de.tum.niwo.Examples
import de.tum.niwo.graphs.WFGraphEncoding._ import de.tum.niwo.graphs.WFGraphEncoding._
...@@ -14,7 +13,7 @@ import de.tum.niwo.Utils ...@@ -14,7 +13,7 @@ import de.tum.niwo.Utils
import de.tum.niwo.tests.TestUtils._ import de.tum.niwo.tests.TestUtils._
import de.tum.niwo.foltl.Properties import de.tum.niwo.foltl.Properties
import de.tum.niwo.graphs.WFGraphEncoding import de.tum.niwo.graphs.WFGraphEncoding
import de.tum.niwo.invariants.InvariantChecker import de.tum.niwo.invariants.{InvariantChecker, Preconditions}
class InvariantSmallCausalFilesTest extends FlatSpec { class InvariantSmallCausalFilesTest extends FlatSpec {
......
...@@ -6,10 +6,9 @@ import org.scalatest.Inspectors._ ...@@ -6,10 +6,9 @@ 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.blocks._ import de.tum.niwo.blocks._
import de.tum.niwo.Preconditions
import de.tum.niwo.foltl.FormulaFunctions import de.tum.niwo.foltl.FormulaFunctions
import de.tum.niwo.Examples import de.tum.niwo.Examples
import de.tum.niwo.invariants.{InvProperties, InvariantChecker, InvariantGenerator}