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

ts converter

parent bb32d548
......@@ -4,11 +4,10 @@ import scala.io.Source
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.Utils._
import de.tum.niwo.blocks.NISpec
import de.tum.niwo.toz3.InvariantChecker
import de.tum.niwo.toz3.InvariantGenerator
import de.tum.niwo.toz3.InvProperties
import de.tum.niwo.invariants.InvariantChecker
import java.io.File
import de.tum.niwo.invariants.{InvProperties, InvariantGenerator}
import de.tum.niwo.parser.WorkflowParser
object InvariantCLI extends App with LazyLogging {
......@@ -58,7 +57,7 @@ object InvariantCLI extends App with LazyLogging {
def generate(name: String, spec: NISpec, properties: InvProperties) {
logger.info(s"Encoding Spec:\n$spec")
def invariant = InvariantGenerator.invariantNoninterSingleBS(spec)
def invariant = InvariantGenerator.invariantNoninterSingleBS _
Utils.check(name, "", invariant, spec, properties)
}
......
......@@ -10,12 +10,10 @@ import de.tum.niwo.foltl.Stubborn
import de.tum.niwo.foltl.Properties
import java.io.PrintWriter
import java.io.File
import de.tum.niwo.blocks.Workflow
import de.tum.niwo.blocks.NISpec
import de.tum.niwo.blocks.{NISpec, TSConverter, Workflow}
import de.tum.niwo.foltl.FormulaFunctions
import de.tum.niwo.toz3.InvariantChecker
import de.tum.niwo.toz3.InvariantGenerator
import de.tum.niwo.toz3.InvProperties
import de.tum.niwo.invariants.{InvProperties, InvariantChecker, InvariantGenerator}
import de.tum.niwo.toz3.Z3QFree
object InvariantInspector extends App with LazyLogging {
......@@ -36,11 +34,13 @@ object InvariantInspector extends App with LazyLogging {
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
val props = InvProperties(stubborn = false, eliminateA = true)
val invspec = TSConverter.toInvariantSpec(spec, props, invariant)
val (t, (res, dot)) = time {
// InvariantChecker.checkInvariantOnce(spec.w, inv(spec), true)
val props = InvProperties(stubborn = false, eliminateA = true)
val (result, graph, afterlabels, proven, dot, time) =
InvariantChecker.checkInvariantFPLabelling(spec, invariant(spec), props)
val (result, graph, afterlabels, proven, dot, time) =
InvariantChecker.checkInvariantFPLabelling(invspec, props)
// non-omitting conference linear inspection
val lastlabels = afterlabels.last
......
......@@ -7,11 +7,10 @@ import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.Utils._
import java.io.PrintWriter
import java.io.File
import de.tum.niwo.blocks.Workflow
import de.tum.niwo.blocks.NISpec
import de.tum.niwo.blocks.{InvariantSpec, NISpec, TSConverter, Workflow}
import de.tum.niwo.foltl.FormulaFunctions
import de.tum.niwo.toz3.InvariantChecker
import de.tum.niwo.toz3.InvariantGenerator
import de.tum.niwo.invariants.{InvProperties, InvariantChecker, InvariantGenerator}
object MainInvariants extends App with LazyLogging {
......@@ -24,7 +23,10 @@ object MainInvariants extends App with LazyLogging {
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
val (res, dot, t) = InvariantChecker.checkInvariantFPDot(spec, invariant(spec))
val props = InvProperties.DEFAULT
val s = TSConverter.toInvariantSpec(spec, props, invariant)
val (res, dot, t) = InvariantChecker.checkInvariantFPDot(s, props)
val msg = s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n"
write(name, s"$name.inv", msg)
......
......@@ -4,12 +4,13 @@ import com.typesafe.scalalogging.LazyLogging
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.Utils._
import de.tum.niwo.blocks.{SimpleWFBlock, NISpec}
import de.tum.niwo.blocks.{NISpec, SimpleWFBlock}
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.FOTransformers
import de.tum.niwo.synth.Model
import de.tum.niwo.toz3._
import de.tum.niwo.foltl.Properties
import de.tum.niwo.invariants.{InvProperties, InvariantGenerator}
// Labelled Edge to Block
import Implicits._
......@@ -34,9 +35,8 @@ object MainInvariantsInference extends App with LazyLogging {
eliminateB = true
)
val inv = invariant(spec)
// val (res, graph, labels, t) = InvariantChecker.checkInvariantFPHeadLabel(spec, inv, props)
val res = Utils.check(name, "elimB", inv, props)
val res = Utils.check(name, "elimB", invariant, props)
}
......
......@@ -3,12 +3,14 @@ package de.tum.niwo
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.Utils._
import de.tum.niwo.blocks.{SimpleWFBlock, NISpec}
import de.tum.niwo.blocks.{NISpec, SimpleWFBlock, TSConverter}
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.FOTransformers
import de.tum.niwo.synth.Model
import de.tum.niwo.toz3._
import de.tum.niwo.foltl.Properties
import de.tum.niwo.graphs.TSGraphEncoding
import de.tum.niwo.invariants.{InvProperties, InvariantChecker, InvariantGenerator}
// Labelled Edge to Block
import de.tum.niwo.graphs.WFGraphEncoding.EdgeImplicits._
......@@ -25,10 +27,10 @@ object MainInvariantsInterpolation extends App with LazyLogging {
// InvariantChecker.invariantAllEqual _
val props = InvProperties(stubborn = false, eliminateA = true)
val inv = invariant(spec)
val (res, graph, labels, t) = InvariantChecker.checkInvariantFPHeadLabel(spec, inv, props)
val invspec = TSConverter.toInvariantSpec(spec, props, invariant)
val (res, graph, labels, t) = InvariantChecker.checkInvariantFPHeadLabel(invspec, props)
logger.info(s"Invariant was ${inv}")
logger.info(s"Invariant was ${invspec.inv}")
logger.info(s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n")
......@@ -80,7 +82,7 @@ object MainInvariantsInterpolation extends App with LazyLogging {
logger.info(s"Path from source to target: $path")
val newmodel = path.edges.foldLeft(model)((m, e) => m.warp(e, spec, props))
val newmodel = path.edges.foldLeft(model)((m, e) => m.warp(TSGraphEncoding.toBlock(e), invspec, props))
logger.info(s"Warped Model: ${newmodel.prettyprint}")
......
......@@ -5,7 +5,8 @@ import blocks._
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.toz3.{InvProperties, Z3BSFO}
import de.tum.niwo.invariants.InvProperties
import de.tum.niwo.toz3.Z3BSFO
object Preconditions extends LazyLogging {
......@@ -46,7 +47,7 @@ object Preconditions extends LazyLogging {
// precond
// }
private def weakestPrecondition(f: Formula, b:SimpleTSBlock, spec: InvariantSpec, properties: InvProperties) = {
def weakestPrecondition(f: Formula, b:SimpleTSBlock, spec: InvariantSpec, properties: InvProperties) = {
val updates = for (s <- b.steps) yield {
s.fun -> (s.tuple, {
......
......@@ -5,9 +5,10 @@ import de.tum.niwo.foltl.FOLTL._
import java.io.File
import java.io.PrintWriter
import de.tum.niwo.toz3.{InvProperties, InvariantChecker, Z3BSFO}
import de.tum.niwo.toz3.Z3BSFO
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.graphs.WFGraphEncoding
import de.tum.niwo.invariants.{InvProperties, InvariantChecker}
object Utils extends LazyLogging {
......@@ -66,17 +67,22 @@ object Utils extends LazyLogging {
writer.close()
logger.info(s"Written $file")
}
def check(name: String, desc:String, inv:NISpec => Formula, spec:NISpec, properties: InvProperties):Boolean = {
val invspec = TSConverter.toInvariantSpec(spec, properties, inv)
check(name, desc, invspec, properties)
}
def check(name:String, desc:String, inv:Formula, spec:NISpec, properties:InvProperties) = {
def check(name:String, desc:String, spec:InvariantSpec, properties:InvProperties):Boolean = {
val model = if (properties.stubborn) "stubborn" else "causal"
val basename = name.split("/").last
val filenames = s"${basename}_$model${if (desc.isEmpty()) "" else s"_$desc"}"
val (res, graph, labelling, provens, dot, time) =
InvariantChecker.checkInvariantFPLabelling(spec, inv, properties)
InvariantChecker.checkInvariantFPLabelling(spec, properties)
logger.info(s"Invariant was ${inv}")
logger.info(s"Invariant was ${spec.inv}")
logger.info(s"Invariant was ${if (res) "" else "not "}proven (took $time ms)\n")
if (!res) {
......@@ -108,21 +114,22 @@ object Utils extends LazyLogging {
val avgsize = invsizes.sum / invsizes.size
Utils.write(name, s"$filenames.metrics",
s"""Name: $name
Description: $desc
Invariant:
${inv.pretty.lines.map(s => " " + s).mkString("\n")}
Model: $model
Result: ${if (!res) "not " else ""}inductive
WF size: $wfsize
Time: $time ms
Proof steps: ${dot.size}
Strengthenings: ${strengthenings.size}
Largest Inv: $maxsize
Average Inv: $avgsize""")
|Description: $desc
| Invariant:
|${spec.inv.pretty.lines.map(s => " " + s).mkString("\n")}
| Model: $model
| Result: ${if (!res) "not " else ""}inductive
| WF size: $wfsize
| Time: $time ms
| Proof steps: ${dot.size}
| Strengthenings: ${strengthenings.size}
| Largest Inv: $maxsize
| Average Inv: $avgsize""".stripMargin
)
res
}
def check(name:String, desc:String, inv:Formula, properties:InvProperties):Boolean = {
def check(name:String, desc:String, inv:NISpec => Formula, properties:InvProperties):Boolean = {
val spec = Examples.parseExampleWF(name).get
check(name, desc, inv, spec, properties)
}
......
package de.tum.niwo
package de.tum.niwo.blocks
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
import de.tum.niwo.invariants.{InvProperties, InvariantGenerator}
object TSConverter extends LazyLogging {
def toInvariantSpec(spec:NISpec):InvariantSpec = {
// TODO: move stubbornness flag out of properties
def toInvariantSpec(spec:NISpec,
properties:InvProperties,
invgen:NISpec => Formula
):InvariantSpec = {
val w = spec.w
// Elaborate all statements to Hyperproperty updates with informedness depending on stubbornness
// (maybe add causal switch into spec)
val elaboratefun = (b:SimpleWFBlock[_]) => elaborate(b, spec, properties)
val elaborated = everywhere(w.steps, elaboratefun)
// 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 = elaborated.map(s => toTSBlock(s)(w.sig, properties))
val steps = elaborate(outerb, spec, properties)
// Add causals to constants?
val newsig = w.sig.copy(
preds = w.sig.preds + Fun(INFNAME, List(spec.target.params.head)),
constants = spec.causals.toSet ++ w.sig.constants
)
val ts = TransitionSystem(newsig, steps)
InvariantSpec(ts, spec.axioms, invgen(spec))
}
private def everywhere(list: List[WFBlock],
update: SimpleWFBlock[_] => List[SimpleWFBlock[_]]):List[WFBlock] = {
list match {
case (l:WFLoop) :: xs => l.update(everywhere(l.steps, update)) :: everywhere(xs, update)
case (nd:WFNondetChoice) :: xs => nd.update(
everywhere(nd.left, update),
everywhere(nd.right, update)
) :: everywhere(xs, update)
case (s:SimpleWFBlock[_]) :: xs => update(s) ++ everywhere(xs, update)
case Nil => Nil
}
}
private def toTSBlock(b:WFBlock)(implicit sig:Signature, properties:InvProperties):TSBlock = {
b match {
case WFLoop(steps) =>
TSLoop(steps.map(toTSBlock))
case WFNondetChoice(left, right) =>
TSNondetChoice(left.map(toTSBlock), right.map(toTSBlock))
case s:SimpleWFBlock[_] =>
SimpleTSBlock(s.steps.map(s => toSetStmt(s, sig, properties)))
}
}
def getUpdate(s:Statement[_], spec:InvariantSpec, properties:InvProperties): Formula = {
def toSetStmt(s:Statement[_], sig:Signature, properties:InvProperties): SetStmt = {
val frees = s.guard.freeVars -- s.tuple.toSet -- spec.ts.sig.constants
val frees = s.guard.freeVars -- s.tuple.toSet -- sig.constants
val form = s match {
// Quantify free, non-const variables
val guard = 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
}
case st:SetStmt => Exists(frees.toList, s.guard).simplify
}
form
True
SetStmt(guard, s.fun, s.tuple)
}
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) {
......@@ -138,4 +127,42 @@ object TSConverter extends LazyLogging {
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
}
}
......@@ -47,14 +47,14 @@ trait Spec {
case class InvariantSpec(ts:TransitionSystem, axioms:Formula, inv:Formula) extends Spec {
override def toString: String = {
s"InvSpec\nTransition System:\n$ts\n\nAxioms:\n$axioms\n\nInvariant:$inv"
s"InvSpec\nTransition System:\n$ts\n\nAxioms:\n$axioms\n\nInvariant:$inv\n"
}
def addAxiom(k:Formula) = {
InvariantSpec(ts, And.make(axioms, k), inv)
}
def addInv(k:Formula) = {
InvariantSpec(ts, axioms, And.make(inv, k))
copy(axioms = And.make(axioms, k))
}
// def addInv(k:Formula) = {
// InvariantSpec(ts, axioms, And.make(inv, k))
// }
def isSane: Boolean = {
// TODO: add sanity checking for axioms and invariant signatures
ts.isSane()
......
......@@ -21,6 +21,7 @@ object Workflow {
val EMPTY = Workflow(Signature.EMPTY, List())
}
// TODO: make causals a set
case class NISpec(w: Workflow, declass: Map[String, (List[Var], Formula)], axioms: Formula, target: Fun, causals:List[Var]) extends Spec with LazyLogging {
override def toString: String = {
s"NISpec\nWorkflow:\n$w\nDeclass:$declass\nTarget:$target"
......
......@@ -66,8 +66,7 @@ object Causal {
}
object Noninterference extends LazyLogging {
def buildViolations(vars:List[Var], t:Formula, causals:List[Var]) = {
val univ = causals.groupBy(_.typ).withDefault(_ => List())
......
......@@ -5,7 +5,7 @@ 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 de.tum.niwo.invariants.InvProperties
import scalax.collection.Graph
import scalax.collection.GraphTraversal.BreadthFirst
import scalax.collection.edge.LBase.LEdgeImplicits
......
......@@ -5,11 +5,11 @@ import de.tum.niwo.Preconditions
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.Properties
import de.tum.niwo.toz3.InvProperties
import scalax.collection.Graph
import scalax.collection.GraphTraversal.BreadthFirst
import scalax.collection.edge.LDiEdge
import de.tum.niwo.Implicits._
import de.tum.niwo.invariants.InvProperties
import scalax.collection.edge.LBase.LEdgeImplicits
object WFGraphEncoding extends GraphBuilder with LazyLogging {
......
package de.tum.niwo.toz3
package de.tum.niwo.invariants
import scala.annotation.tailrec
import com.microsoft.z3.{Solver, Status}
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.Preconditions
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.FormulaFunctions
import de.tum.niwo.Utils
import de.tum.niwo.graphs.{TSGraphEncoding, WFGraphEncoding}
import de.tum.niwo.graphs.WFGraphEncoding.WorkflowGraph
import de.tum.niwo.graphs.{TSGraphEncoding, WFGraphEncoding}
import de.tum.niwo.toz3.{Z3BSFO, Z3FOEncoding}
import de.tum.niwo.{Preconditions, Utils}
import scala.annotation.tailrec
case class InvProperties(stubborn:Boolean, eliminateA:Boolean, eliminateB:Boolean = false) { }
object InvProperties {
val DEFAULT = InvProperties(stubborn = true, eliminateA = true, eliminateB = true)
val DEFAULT = InvProperties(
stubborn = true,
eliminateA = true,
eliminateB = true
)
}
object InvariantChecker extends LazyLogging {
......@@ -30,7 +35,7 @@ object InvariantChecker extends LazyLogging {
(Z3BSFO.checkAE(f.simplify), precond)
}
def checkInvariantFPLabelling(spec: InvariantSpec, inv: Formula, properties:InvProperties) = {
def checkInvariantFPLabelling(spec: InvariantSpec, properties:InvProperties) = {
val graph = TSGraphEncoding.toGraph(spec.ts)
type Node = graph.NodeT
type Edge = graph.EdgeT
......@@ -59,7 +64,14 @@ object InvariantChecker extends LazyLogging {
// try to prove
val pre = labels(nextEdge.from)
val post = labels(nextEdge.to)
val ((status, solver), strengthened) = checkBlockInvariant(spec, TSGraphEncoding.toBlock(nextEdge), pre, post, properties, untouched(nextEdge.from))
val ((status, solver), strengthened) =
checkBlockInvariant(
spec,
TSGraphEncoding.toBlock(nextEdge),
pre,
post,
properties,
untouched(nextEdge.from))
val from = TSGraphEncoding.toNumber(nextEdge._1)
val to = TSGraphEncoding.toNumber(nextEdge._2)
......@@ -111,7 +123,7 @@ object InvariantChecker extends LazyLogging {
}
// create labelling
val labels = (for (n <- graph.nodes) yield { n.value -> inv }).toMap
val labels = (for (n <- graph.nodes) yield { n.value -> spec.inv }).toMap
// update initial labels with untouched map
val untouchedlabels = for ((n, inv) <- labels) yield {
......@@ -128,24 +140,28 @@ object InvariantChecker extends LazyLogging {
(result, graph, labellings.reverse, proven.reverse, dot2, time)
}
def checkInvariantFPDot(spec: InvariantSpec, inv: Formula, properties:InvProperties = InvProperties.DEFAULT): (Boolean, List[String], Long) = {
val (result, graph, afterlabels, proven, dot, time) = checkInvariantFPLabelling(spec, inv, properties)
def checkInvariantFPDot(spec: InvariantSpec,
properties:InvProperties = InvProperties.DEFAULT
): (Boolean, List[String], Long) = {
val (result, graph, afterlabels, proven, dot, time) = checkInvariantFPLabelling(spec, properties)
(result, dot, time)
}
def checkInvariantFPHeadLabel(spec: InvariantSpec, inv: Formula, properties:InvProperties = InvProperties.DEFAULT): (Boolean, WorkflowGraph, Map[Int, Formula], Long) = {
val (result, graph, afterlabels, proven, dot, time) = checkInvariantFPLabelling(spec, inv, properties)
def checkInvariantFPHeadLabel(spec: InvariantSpec,
properties:InvProperties = InvProperties.DEFAULT
): (Boolean, WorkflowGraph, Map[Int, Formula], Long) = {
val (result, graph, afterlabels, proven, dot, time) = checkInvariantFPLabelling(spec, properties)
(result, graph, afterlabels.last, time)
}
def checkInvariantOnce(spec: InvariantSpec, inv: Formula, properties: InvProperties): (Boolean, StringBuilder) = {
def checkInvariantOnce(spec: InvariantSpec, properties: InvProperties): (Boolean, StringBuilder) = {
// Build graph
val graph = TSGraphEncoding.toGraph(spec.ts)
val untouched = TSGraphEncoding.untouchedMap(graph, spec.ts.sig, properties)
val msg = new StringBuilder()
msg ++= s"Trying to prove safe with invariant:\n\n${inv.pretty}\n\n"
msg ++= s"Trying to prove safe with invariant:\n\n${spec.inv.pretty}\n\n"
// Check all edges
val list = for (e <- graph.edges) yield {
......@@ -153,7 +169,7 @@ object InvariantChecker extends LazyLogging {
// Check I -> WP[w](inv)
val b = TSGraphEncoding.toBlock(e)
val ((res, solver), strengthened) = checkBlockInvariant(spec, b, inv, inv, properties, untouched(e.from))
val ((res, solver), _) = checkBlockInvariant(spec, b, spec.inv, spec.inv, properties, untouched(e.from))
if (res != Status.UNSATISFIABLE) {
msg ++= s"Possibly unsafe: Block may not uphold invariant:\n\n${e.label}\n\n"
......@@ -164,7 +180,7 @@ object InvariantChecker extends LazyLogging {
msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
}
msg ++= "\n"
logger.info(s"Could not prove invariant $inv")
logger.info(s"Could not prove invariant ${spec.inv}")
logger.info(s"Z3 status $res")
logger.info(s"Block ${e.label} may not uphold it")
}
......@@ -174,7 +190,7 @@ object InvariantChecker extends LazyLogging {
val safe = list.reduceLeft(_ && _)
if (safe) {
msg ++= s"Proven safe.\n"
logger.info(s"Workflow ${spec.ts}\n proven safe for invariant:\n${inv.pretty}")
logger.info(s"Workflow ${spec.ts}\n proven safe for invariant:\n${spec.inv.pretty}")
}
(safe, msg)
}
......
package de.tum.niwo.toz3
package de.tum.niwo.invariants
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.FOTransformers
import de.tum.niwo.Implicits._
import de.tum.niwo.foltl.Properties.T1
import de.tum.niwo.foltl.Properties.T2
import de.tum.niwo.foltl.Properties.{T1, T2}
object InvariantGenerator {
def genEq(f: Fun, p: List[Var]) = {
val newf = f.parallelRename(f.params, p)
def genEq(f: String, p: List[Var]) = {
val newf = Fun(f, p)
Equiv(newf.in(T1), newf.in(T2))
}
def genEq(f:Fun) = {
Equiv(f.in(T1), f.in(T2))
}
// def invariantNoninterStubborn(spec: Spec) = {
// val agent = spec.target.params(0)
......@@ -40,7 +39,7 @@ object InvariantGenerator {
// }
// val quants = premise.flatMap(_._1).toSet.toList // eliminate doubles
val conclusion = genEq(spec.target, spec.target.params)
val conclusion = genEq(spec.target)
Forall(spec.target.params, conclusion).simplify
// Constants
// conclusion
......@@ -66,7 +65,7 @@ object InvariantGenerator {
def invariantAllEqual(spec: NISpec) = {
And.make(for (r <- spec.w.sig.preds.toList if r.params.head.typ == spec.target.params.head.typ) yield {
val params = r.params.map(v => Var(v.name + "t", v.typ))
Forall(params, genEq(r, params))
Forall(params, genEq(r.name, params))
})
}
}
\ No newline at end of file
......@@ -3,11 +3,12 @@ package de.tum.niwo.synth
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.Preconditions
import de.tum.niwo.blocks.{SimpleWFBlock, NISpec}
import de.tum.niwo.blocks.{InvariantSpec, NISpec, SimpleTSBlock, SimpleWFBlock}
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.{FOTransformers, Properties}
import de.tum.niwo.invariants.InvProperties
import de.tum.niwo.synth.Model.logger
import de.tum.niwo.toz3.{InvProperties, InvariantChecker, Z3QFree}
import de.tum.niwo.toz3.Z3QFree
case class Model(universe: Map[String, List[Var]], steering: Formula, state:Map[Fun, List[Formula]]) {
def prettyprint() = {
......@@ -30,7 +31,7 @@ case class Model(universe: Map[String, List[Var]], steering: Formula, state:Map[
And.make(formulas.toList)
}
def warp(b: SimpleWFBlock[_], spec: NISpec, properties: InvProperties): Model = {
def warp(b: SimpleTSBlock, spec: InvariantSpec, properties: InvProperties): Model = {