Model.scala 2.93 KB
Newer Older
1
package de.tum.niwo.synth
Christian Müller's avatar
Christian Müller committed
2 3 4

import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
5
import de.tum.niwo.Preconditions
Christian Müller's avatar
Christian Müller committed
6
import de.tum.niwo.blocks.{InvariantSpec, NISpec, SimpleTSBlock, SimpleWFBlock}
7 8
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.{FOTransformers, Properties}
Christian Müller's avatar
Christian Müller committed
9
import de.tum.niwo.invariants.InvProperties
10
import de.tum.niwo.synth.Model.logger
Christian Müller's avatar
Christian Müller committed
11
import de.tum.niwo.toz3.Z3QFree
Christian Müller's avatar
Christian Müller committed
12 13 14 15 16 17 18

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 -> (
Christian Müller's avatar
Christian Müller committed
19
      for (f <- l; if f.opsize != 2) yield {
Christian Müller's avatar
Christian Müller committed
20 21 22 23 24 25 26 27 28 29 30 31 32
        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)
  }
Christian Müller's avatar
Christian Müller committed
33

Christian Müller's avatar
Christian Müller committed
34
  def warp(b: SimpleTSBlock, spec: InvariantSpec, properties: InvProperties): Model = {
Christian Müller's avatar
Christian Müller committed
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
    val facts = And.make(steering, stateFormula())
    //    logger.info(s"Current state: ${state.pretty()}")

    val updated = for (rel <- state.keys) yield {
      //      logger.info(s"Computing new state of ${rel}")

      val tups = FOTransformers.comb(rel.params.map(_.typ), 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")

        // Is now an E* formula
        val pre = Preconditions.weakestPrecondition(post, b, spec, properties)
        val inst = FOTransformers.instantiateExistentials(pre, universe.values.flatten.toSet)

        val check = Implies(facts, inst)
        //        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(universe, steering, updated.toMap)
  }
Christian Müller's avatar
Christian Müller committed
66 67 68 69
}

object Model extends LazyLogging {

Christian Müller's avatar
Christian Müller committed
70
  def emptystate(spec:NISpec, universe:Map[String, List[Var]], props:InvProperties) = {
Christian Müller's avatar
Christian Müller committed
71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96

    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
  }



}