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

interpolation and stuff

parent aa3504e5
......@@ -198,7 +198,7 @@ object Encoding extends LazyLogging {
val MAXINVLENGTH = 1200
def toDot(g: WorkflowGraph)(labels:Map[Encoding.WorkflowGraph#NodeT, String], edges:Set[g.EdgeT]) = {
def toDot(g: WorkflowGraph)(labels:Map[Int, String], edges:Set[g.EdgeT]) = {
val root = DotRootGraph(
directed = true,
id = Some("Invariant Labelling"))
......@@ -225,7 +225,7 @@ object Encoding extends LazyLogging {
}
}
def nodeTransformer(innerNode: WorkflowGraph#NodeT): Option[(DotGraph, DotNodeStmt)] = {
val str = labels(innerNode)
val str = labels(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)))))
}
......
......@@ -57,7 +57,7 @@ object InvariantCLI extends App with LazyLogging {
def generate(name: String, spec: Spec, properties: InvProperties) {
logger.info(s"Encoding Spec:\n$spec")
def invariant = InvariantGenerator.invariantNoninterStubbornSingleBS(spec)
def invariant = InvariantGenerator.invariantNoninterSingleBS(spec)
Utils.check(name, "", invariant, spec, properties)
}
......
......@@ -4,10 +4,7 @@ import foltl.FOLTL._
import blocks.Workflow._
import Implicits._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.ltl.FOTransformers
import de.tum.workflows.Utils._
import de.tum.workflows.foltl.Stubborn
import de.tum.workflows.foltl.Properties
import java.io.PrintWriter
import java.io.File
import de.tum.workflows.blocks.Workflow
......@@ -22,7 +19,7 @@ object MainInvariants extends App with LazyLogging {
logger.info(s"Encoding Spec:\n$spec")
def invariant =
InvariantGenerator.invariantNoninterStubbornSingleBS _
InvariantGenerator.invariantNoninterSingleBS _
// InvariantGenerator.invariantNoninterStubbornBS _
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
......
......@@ -3,43 +3,87 @@ package de.tum.workflows
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils._
import de.tum.workflows.blocks.Spec
import de.tum.workflows.blocks.{SimpleBlock, Spec}
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.FOTransformers
import de.tum.workflows.synth.Model
import de.tum.workflows.toz3._
// Labelled Edge to Block
import Implicits._
object MainInvariantsInference extends App with LazyLogging {
def generate(name: String, spec: Spec) {
logger.info(s"Encoding Spec:\n$spec")
def invariant =
InvariantGenerator.invariantNoninterStubbornSingleBS _
InvariantGenerator.invariantNoninterSingleBS _
// InvariantGenerator.invariantNoninterStubbornBS _
// InvariantChecker.invariantNoninterStubborn _
// InvariantChecker.invariantAllEqual _
val props = InvProperties(stubborn = false, eliminateAux = false)
val inv = invariant(spec)
val (res, graph, labels, t) = InvariantChecker.checkInvariantFPHeadLabel(spec, inv, props)
logger.info(s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n")
logger.info(s"Invariant was ${inv}")
val (res, label, t) = InvariantChecker.checkInvariantFPHeadLabel(spec, invariant(spec), InvProperties(stubborn = false, eliminateAux = false))
val msg = s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n"
logger.info(s"Graph: $graph")
val tar = 0
val headlabel = labels(graph.get(tar))
// Invariant not valid
if (!res) {
// Try to break headlabel invariant
val (status, solver) = InvariantChecker.checkOnZ3(label)
val (status, solver) = Z3QFree.checkUniversal(headlabel)
if (status == Status.SATISFIABLE) {
// Broken, found model
// logger.info(s"Model:\n${Z3.printModel(solver.getModel())}")
logger.info(s"Initial State Invariant: ${label}")
val model = Z3QFree.modelFacts(solver.getModel())
model foreach { f => logger.info(f.toString()) }
logger.info(s"State Invariant: ${headlabel}")
val z3model = Z3QFree.modelFacts(solver.getModel())
// make facts
// filter only workflow rels
// val relfacts = model
// Not constant
val tar = 1
logger.info(s"Z3model: $z3model")
val g = Encoding.toGraph(spec.w)
val facts = for ((f, b) <- z3model) yield {
if (b == True) {
f
} else {
Neg(f)
}
}
logger.info(s"Model Facts: ${facts}")
val vars = z3model.flatMap(_._1.freeVars()).distinct
val groupedvars = vars.groupBy { _.typ }
// These should only contain Choice and Oracle predicates
val state = Model.emptystate(spec, groupedvars, props)
val model = Model(groupedvars, And.make(facts), state)
// get outgoing edge
// FIXME: Don't just take head
val edge = graph.get(tar).outgoing.head
val newmodel = Model.warp(And.make(facts), edge, spec, props, model)
logger.info(s"Warped Model: ${newmodel.prettyprint}")
val inv = labels(edge.to)
val neginv = Neg(inv).toNegNf.simplify
// Instantiate inv for given universe
val instInv = FOTransformers.instantiateExistentials(neginv, vars.toSet)
val itp = Z3QFree.interpolate(model.stateFormula(), instInv)
logger.info(s"Interpolant is $itp")
} else {
logger.error("Invariant not valid, but also not satisfiable.")
......@@ -49,6 +93,7 @@ object MainInvariantsInference extends App with LazyLogging {
}
def generateExample(name: String) {
logger.info(s"Generating $name")
val spec = ExampleWorkflows.parseExample(name)
......
......@@ -2,7 +2,7 @@ package de.tum.workflows
import foltl.FOLTL._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.ltl.FOTransformers
import de.tum.workflows.foltl.FOTransformers
import de.tum.workflows.Utils._
import de.tum.workflows.foltl.Properties
import de.tum.workflows.blocks.Spec
......
package de.tum.workflows
import com.typesafe.scalalogging._
import blocks._
import de.tum.workflows.foltl.FOLTL
import de.tum.workflows.foltl.{FOLTL, FOTransformers, FormulaFunctions}
import de.tum.workflows.foltl.FOLTL._
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 if stmt.tuple.head.typ == s.target.params.head.typ) yield {
private def elaborateSteps(b: SimpleBlock, s: Spec): List[SimpleBlock] = {
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))))
})
}
b :: newsteps
}
// For oracly blocks, remove O from guard and add to ForallMay choice predicate
def elaborateOraclyBlock(b: SimpleBlock, s: Spec) = {
if (b.isoracly) {
val stmt = b.steps.head // can only be one
......@@ -66,14 +63,14 @@ object Preconditions extends LazyLogging {
})
}
def getUpdate(s:Statement, b:SimpleBlock, choice:Option[Fun], isOracly:Boolean, spec:Spec, properties:InvProperties) = {
def getUpdate(s:Statement, b:SimpleBlock, choice:Option[Fun], spec:Spec, properties:InvProperties) = {
// 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 con = if (b.isoracly) {
val decl = spec.declass.getOrElse(b.pred.get, (List(), False))._2
// FIXME: substitutions?
// FIXME: decl in T2?
......@@ -110,29 +107,38 @@ object Preconditions extends LazyLogging {
form
}
def elaborate(block: SimpleBlock, spec:Spec, properties:InvProperties) = {
val stepOne = if (!properties.stubborn) elaborateSteps(block, spec) else List(block)
stepOne map { b => elaborateOraclyBlock(b, spec) }
}
def weakestPrecondition(post: Formula, outerb: SimpleBlock, spec: Spec, properties: InvProperties) = {
val steps = elaborate(outerb, spec, properties)
// elaborate only if non-stubborn
val steps = if (!properties.stubborn) elaborateSteps(outerb, spec) else List(outerb)
// 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)
// val innerb = if (b.isoracly) {
// elaborateOraclyBlock(b, spec)
// } else {
// b
// }
val innerprecond = weakestPreconditionSingle(f, b, spec, properties)
innerprecond
})
precond
}
def weakestPreconditionSingle(f: Formula, b: SimpleBlock, isOracly:Boolean, spec: Spec, properties: InvProperties) = {
private def weakestPreconditionSingle(f: Formula, b: SimpleBlock, 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)
getUpdate(s, b, choice, spec, properties)
})
}
......@@ -145,7 +151,7 @@ object Preconditions extends LazyLogging {
removed
}
def abstractPrecondition(f: Formula, b: SimpleBlock, s: Spec, properties: InvProperties) = {
def abstractedPrecondition(f: Formula, b: SimpleBlock, s: Spec, properties: InvProperties) = {
val precond = weakestPrecondition(f, b, s, properties)
// Stubborn agents -> remove trace variable from choice predicate
......
......@@ -70,7 +70,7 @@ object Utils extends LazyLogging {
val filenames = s"${name}_$model${if (desc.isEmpty()) "" else s"_$desc"}"
// do not blow up the formula with auxilliary elimination
val (res, graph, labelling, provens, dot, time, headlabel) =
val (res, graph, labelling, provens, dot, time) =
InvariantChecker.checkInvariantFPLabelling(spec, inv, properties)
for ((s, i) <- dot.zipWithIndex) {
Utils.write(s"${filenames}_$i.dot", s)
......@@ -80,7 +80,7 @@ object Utils extends LazyLogging {
}
val labels = (for ((node, inv) <- labelling.last) yield {
s"Node ${node.value}:\n${inv.pretty()}\n"
s"Node ${node}:\n${inv.pretty()}\n"
}).mkString("\n")
Utils.write(s"$filenames.invariants", labels)
......
......@@ -40,8 +40,8 @@ case class Spec(w: Workflow, declass: Map[String, (List[Var], Formula)], target:
def saneoraclestmt(stmt:Statement, frees:List[Var]) = {
// Oracle only positive
val f = stmt.guard.toNegNf()
val noneg = !(f hasSubFormula {
val f = stmt.guard.toNegNf
val noneg = !(f.hasSubFormula {
case Neg(f:Fun) if f.isOracle() => true
})
val allvars = !(f hasSubFormula {
......@@ -94,10 +94,17 @@ abstract sealed class SimpleBlock extends Block {
steps.exists(s => agents.exists(a => !s.tuple.contains(a)))
}
def isoracly = {
steps.exists(_.guard.hasSubFormula {
def isoracly: Boolean = {
// before transformation
val before = steps.exists(s => {
s.guard.hasSubFormula {
case f:Fun => f.isOracle()
}
})
// after transformation
val after = pred.exists(name => Fun(name, agents).isOracle())
before || after
}
}
......
......@@ -7,24 +7,25 @@ import scala.annotation.tailrec
object FOLTL {
abstract class Formula {
def simplify() = FormulaFunctions.simplify(this)
def freeVars() = FormulaFunctions.freeVars(this)
def everywhere(trans: PartialFunction[Formula, Formula]) = FormulaFunctions.everywhere(trans, this)
def assumeEmpty(name: String) = FormulaFunctions.assumeEmpty(this, name)
def assumeEmpty(names: List[String]) = FormulaFunctions.assumeAllEmpty(this, names)
def in(name: String) = FormulaFunctions.annotate(this, name)
def in(name: String, ignore: Set[String]) = FormulaFunctions.annotate(this, name, ignore)
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 simplify(): Formula = FormulaFunctions.simplify(this)
def freeVars(): Set[Var] = FormulaFunctions.freeVars(this)
def everywhere(trans: PartialFunction[Formula, Formula]): Formula = FormulaFunctions.everywhere(trans, this)
def assumeEmpty(name: String): Formula = FormulaFunctions.assumeEmpty(this, name)
def assumeEmpty(names: List[String]): Formula = FormulaFunctions.assumeAllEmpty(this, names)
def in(name: String): Formula = FormulaFunctions.annotate(this, name)
def in(name: String, ignore: Set[String]): Formula = FormulaFunctions.annotate(this, name, ignore)
def collect[T](coll: PartialFunction[Formula, List[T]]):List[T] = FormulaFunctions.collect(coll, this)
def hasSubFormula(coll: PartialFunction[Formula, Boolean]):Boolean = FormulaFunctions.hasSubFormula(coll, this)
def opsize(): Int = FormulaFunctions.opsize(this)
def toPrenex: Formula = FormulaFunctions.toPrenex(this)
def toNegNf: Formula = FormulaFunctions.toNegNf(this)
def toCNF: Formula = FormulaFunctions.toCNF(this)
def isBS: Boolean = FormulaFunctions.isBS(this)
def isQFree: Boolean = FormulaFunctions.isQFree(this)
def removeOTQuantifiers(): Formula = FormulaFunctions.removeOTQuantifiers(this)
def parallelRename(vars: List[Var], newvars: List[Var]): Formula = FormulaFunctions.parallelRename(this, vars, newvars)
def bracketed(): String = this match {
case _: BinOp => "(" + this + ")"
......@@ -111,7 +112,7 @@ object FOLTL {
}
trait Quantifier extends Formula {
def qmake: (List[Var], Formula) => Quantifier
def make: (List[Var], Formula) => Formula
def qname: String
def vars: List[Var]
def t: Formula
......@@ -123,20 +124,35 @@ object FOLTL {
}
object Quantifier {
def unapply(q: Quantifier) = Some((q.qmake, q.vars, q.t))
def unapply(q: Quantifier) = Some((q.make, q.vars, q.t))
def make(m: (List[Var], Formula) => Quantifier, l:List[Var], f:Formula) = {
if (l.isEmpty) f else m(l, f)
}
}
object Exists {
def make = Quantifier.make(Exists.apply, _:List[Var], _:Formula)
}
object Forall {
def make = Quantifier.make(Forall.apply, _:List[Var], _:Formula)
}
object ForallOtherThan {
def make(l:List[Var], otherthan:List[Var], f:Formula) = {
if (otherthan.isEmpty || l.isEmpty) { Forall.make(l, f) } else {
ForallOtherThan(l, otherthan, f)
}
}
}
case class Exists(vars: List[Var], t: Formula) extends Quantifier {
val qname = "∃"
val qmake = Exists.apply
val make = Quantifier.make(Exists.apply, _, _)
}
case class Forall(vars: List[Var], t: Formula) extends Quantifier {
val qname = "∀"
val qmake = Forall.apply
val make = Quantifier.make(Forall.apply, _, _)
}
case class ForallOtherThan(vars: List[Var], otherthan: List[Var], t: Formula) extends Quantifier {
val qname = "∀"
val qmake = ForallOtherThan.apply(_: List[Var], otherthan, _: Formula)
val make = ForallOtherThan.apply(_: List[Var], otherthan, _: Formula)
override def toString() = {
s"$qname ${vars.map(_.withType()).mkString(",")} ∉ {${otherthan.map(_.withType()).mkString(",")}}. ${t.bracketed()}"
}
......
package de.tum.workflows.ltl
package de.tum.workflows.foltl
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.FOLTL
import de.tum.workflows.foltl.FormulaFunctions
object FOTransformers extends LazyLogging {
// Computes all possible tuples of size i
// Computes all possible tuples of signature types
def comb[T](types:List[String], universe:Map[String, List[T]]):List[List[T]] = {
types match {
case List() => List(List())
......@@ -50,7 +46,7 @@ object FOTransformers extends LazyLogging {
case Quantifier(make, vars, inner) => make(vars.filterNot(bound.contains).distinct, elimSub(inner, bound ++ vars))
}
}
elimSub(f.toNegNf(), Set())
elimSub(f.toNegNf, Set())
}
def eliminateAuxiliaryPredicate(f:Formula, AUX:String) = {
......@@ -109,6 +105,7 @@ object FOTransformers extends LazyLogging {
(agents, res)
}
// Instantiate all universals in a E*A* formula
def eliminateUniversals(t: Formula, agents: List[Var]):Formula = {
// if (agents.isEmpty) {
......@@ -165,13 +162,14 @@ object FOTransformers extends LazyLogging {
* Resulting formula is in E* with all existentials outermost and in NegNF
*/
def instantiateUniversals(f:Formula) = {
// Check fragment
if (!f.isBS()) {
if (!f.isBS) {
logger.error("Trying to instantiate Universals for wrong fragment")
logger.error(s"Formula was $f")
}
val nf = f.toNegNf()
val nf = f.toNegNf
val (agents, inner) = FOTransformers.eliminateExistentials(nf)
val existbound = Exists(agents, inner)
val constants = existbound.freeVars()
......@@ -184,18 +182,39 @@ object FOTransformers extends LazyLogging {
* Resulting formula is in NegNF
*/
def abstractExistentials(f:Formula) = {
val neg = Neg(f).toNegNf().simplify()
val neg = Neg(f).toNegNf.simplify
// Check fragment
if (!neg.isBS()) {
if (!neg.isBS) {
logger.warn("Trying to instantiate Existentials for wrong fragment -- Termination not guaranteed")
// logger.error(s"Formula was $f")
}
val (agents, inner) = FOTransformers.eliminateExistentials(neg)
val existbound = Exists(agents, inner)
val constants = neg.freeVars()
val constants = neg.freeVars
val res = FOTransformers.eliminateUniversals(existbound, constants.toList)
Neg(res).simplify()
}
/**
* Instantiates existentials in E* formulas for a given universe to a disjunction
* @param f Formula in E*
* @param universe Set of variables
* @return Formula without E
*/
def instantiateExistentials(f:Formula, universe:Set[Var]): Formula = {
if (f.hasSubFormula {
case Forall(_, _) => true
}) {
logger.error("Trying to instantiate existentials for formula containing universals")
}
val neg = Neg(f).simplify()
val constants = neg.freeVars ++ universe
val res = FOTransformers.eliminateUniversals(neg, constants.toList)
Neg(res).simplify()
}
}
\ No newline at end of file
......@@ -4,10 +4,10 @@ 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 {
def freeVars(t: Formula) = {
def free(t: Formula, bound: Set[Var]): Set[Var] = {
t match {
......@@ -226,7 +226,7 @@ object FormulaFunctions extends LazyLogging {
}
}
def hasSubFormula(coll: PartialFunction[Formula, Boolean], t: Formula) = {
def hasSubFormula(coll: PartialFunction[Formula, Boolean], t: Formula):Boolean = {
def or(bs: Boolean*) = { bs.exists(identity) }
collect(or)(coll, t)
}
......@@ -379,10 +379,20 @@ object FormulaFunctions extends LazyLogging {
}
def isBS(f: Formula) = {
val quantprefix = collectQuantifiers(f.toNegNf())
val quantprefix = collectQuantifiers(f.toNegNf)
if (quantprefix.length < 2) true else {
// has no forall exists in quantifier prefix
!quantprefix.sliding(2).exists(list => !list.head._1 && list(1)._1)
}
}
def isQFree(formula: Formula): Boolean = {
!formula.hasSubFormula {
case q:Quantifier => true
}
}
def toNegNf(f: Formula) = {
// val bound = if (hasDuplicateBindings(f)) {
......@@ -436,7 +446,7 @@ object FormulaFunctions extends LazyLogging {
// TODO: make sure no quantifiers in scope of others with same name
def toPrenex(f: Formula):Formula = {
val negnf = f.toNegNf()
val negnf = f.toNegNf
// val (simp, boundVars) = fixBinding(negnf, Set())
// Simplify first to push negation inward
......@@ -459,7 +469,7 @@ object FormulaFunctions extends LazyLogging {
}
// FIXME: can we do it without prenex? may be expensive later on
val normalized = f.toNegNf().toPrenex().simplify()
val normalized = f.toNegNf.toPrenex.simplify()
// normalized is now Quantifiers, then only And/Or with Negation inside
// no simplification here
......@@ -502,7 +512,7 @@ object FormulaFunctions extends LazyLogging {
})
}
val norm = f.toCNF()
val norm = f.toCNF
val removed = norm.everywhere({
// find top-level ORs in CNF
......
package de.tum.workflows.synth
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Preconditions
import de.tum.workflows.blocks.{SimpleBlock, Spec}
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.{FOTransformers, Properties}
import de.tum.workflows.toz3.{InvProperties, InvariantChecker, Z3QFree}
case class Model(universe: Map[String, List[Var]], steering: Formula, state:Map[Fun, List[Formula]]) {
def prettyprint() = {
// ignore negated tuples
val rels = for ((s,l) <- state) yield {
s -> (
for (f <- l; if f.opsize() != 2) yield {
f
})
}
s"Model:\nUniverse${universe.mkString("(",",",")")}\nSteering:${steering}\nState:\n${rels.mkString("(","\n",")")}"
}
def stateFormula(): Formula = {
val formulas = for ((_, list) <- state; form <- list) yield {
form
}
And.make(formulas.toList)
}
}
object Model extends LazyLogging {
def emptystate(spec:Spec, universe:Map[String, List[Var]], props:InvProperties) = {
val preds = if (props.stubborn) {
spec.w.sig.preds.toList
} else {
// FIXME: Is there a better way to find out the type?
// FIXME: Compute informedness?
val inf = Fun(Properties.INFNAME, List(spec.causals.head))
inf :: spec.w.sig.preds.toList
}
val emptystate = for (f <- preds) yield {
f -> (
for (tup <- FOTransformers.comb(f.params.map(_.typ), universe);
t <- List(Properties.T1, Properties.T2)
if !(f.name == Properties.INFNAME && t == Properties.T2) // Exclude informed(t2)(a)
) yield {
Neg(Fun(f.name, Some(t), tup))
}
)
}
emptystate toMap
}
def warp(modelfacts: Formula, b: SimpleBlock, spec: Spec, properties: InvProperties, model: Model): Model = {
logger.info(s"Initial Model: ${model}")
val state = And.make(model.steering, model.stateFormula())
logger.info(s"Current state: ${state.pretty()}")
// FIXME: This does not update the state of "informed"
val updated = for (rel <- spec.w.sig.preds) yield {
logger.info(s"Computing new state of ${rel}")
val tups = FOTransformers.comb(rel.params.map(_.typ), model.universe)
val newstate = for (tup <- tups; trace <- List(Properties.T1, Properties.T2)) yield {
val post = Fun(rel.name, Some(trace), tup)
logger.info(s"Checking tuple $post on trace $trace")
val pre = Preconditions.weakestPrecondition(post, b, spec, properties)
val check = Implies(state, pre)
logger.info(s"Precondition is $check")
val (res, _) = Z3QFree.checkUniversal(check)
if (res == Status.SATISFIABLE) {
// Negation sat, so there are models where it's false
Neg(post)
} else {
post
}
}
rel -> newstate
}
Model(model.universe, model.steering, updated.toMap)
}
}
\ No newline at end of file