Model.scala 2.88 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
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)
  }

}