MainInvariantsInterpolation.scala 5.1 KB
Newer Older
1
package de.tum.niwo
Christian Müller's avatar
src  
Christian Müller committed
2 3 4

import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
5
import de.tum.niwo.Utils._
Christian Müller's avatar
Christian Müller committed
6
import de.tum.niwo.blocks.{NISpec, SimpleWFBlock, TSConverter}
7 8 9 10 11
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
Christian Müller's avatar
Christian Müller committed
12 13
import de.tum.niwo.graphs.TSGraphEncoding
import de.tum.niwo.invariants.{InvProperties, InvariantChecker, InvariantGenerator}
Christian Müller's avatar
src  
Christian Müller committed
14 15

// Labelled Edge to Block
Christian Müller's avatar
Christian Müller committed
16
import de.tum.niwo.graphs.WFGraphEncoding.EdgeImplicits._
Christian Müller's avatar
src  
Christian Müller committed
17 18 19

object MainInvariantsInterpolation extends App with LazyLogging {

Christian Müller's avatar
Christian Müller committed
20
  def generate(name: String, spec: NISpec, tar:Int) {
Christian Müller's avatar
src  
Christian Müller committed
21 22 23 24 25 26 27 28
    logger.info(s"Encoding Spec:\n$spec")

    def invariant =
      InvariantGenerator.invariantNoninterSingleBS _
    // InvariantGenerator.invariantNoninterStubbornBS _
    // InvariantChecker.invariantNoninterStubborn _
    // InvariantChecker.invariantAllEqual _

Christian Müller's avatar
Christian Müller committed
29
    val props = InvProperties(stubborn = false, eliminateA = true)
Christian Müller's avatar
Christian Müller committed
30 31
    val invspec = TSConverter.toInvariantSpec(spec, props, invariant)
    val (res, graph, labels, t) = InvariantChecker.checkInvariantFPHeadLabel(invspec, props)
Christian Müller's avatar
src  
Christian Müller committed
32

Christian Müller's avatar
Christian Müller committed
33
    logger.info(s"Invariant was ${invspec.inv}")
Christian Müller's avatar
src  
Christian Müller committed
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
    logger.info(s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n")


    logger.info(s"Graph: $graph")
    val src = 0

    val headlabel = labels(graph.get(src))

    // Invariant not valid
    if (!res) {
      // Try to break headlabel invariant
      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"State Invariant: ${headlabel}")
        val z3model = Z3QFree.modelFacts(solver.getModel())

        // make facts
        // filter only workflow rels

//        val relfacts = model

        logger.info(s"Z3model:  $z3model")

        val facts = for ((f, b) <- z3model) yield {
          if (b == True) {
            f
          } else {
            Neg(f)
          }
        }
        logger.info(s"Model Facts: ${facts}")

        val vars = z3model.flatMap { case (f:Fun,b:Formula) => f.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)

        logger.info(s"Initial Model: ${model.prettyprint()}")

        // get path
        val source = graph.get(0)
        val target = graph.get(tar)
        val path = source.shortestPathTo(target).get // Has to be connected

        logger.info(s"Path from source to target: $path")

Christian Müller's avatar
Christian Müller committed
85
        val newmodel = path.edges.foldLeft(model)((m, e) => m.warp(TSGraphEncoding.toBlock(e), invspec, props))
Christian Müller's avatar
src  
Christian Müller committed
86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118

        logger.info(s"Warped Model: ${newmodel.prettyprint}")

        val inv = labels(target)
        val neginv = inv.toNegNf.simplify

        logger.info(s"Invariant before: $neginv")

        // Instantiate inv for given universe
        val instinv = FOTransformers.eliminateUniversals(neginv, vars)
        logger.info(s"Invariant instantiated: $instinv")

        // Put steering into instInv
        val z3map = z3model.toMap
        val steeredinv = instinv.everywhere {
          case f:Fun if z3map.contains(f) => z3map(f)
        }
        val steeredInfinv = steeredinv.assumeEmpty(Properties.INFNAME)

        // just for testing
        val tocheck = List("Assign")

        val modelmap = for ((f, vs) <- newmodel.state; v <- vs if !tocheck.contains(f.name)) yield {
          v match {
            case Neg(f) => (f, False)
            case f:Fun => (f, True)
          }
        }

        val modelinv = steeredInfinv.everywhere {
          case f:Fun if modelmap.contains(f) => modelmap(f)
        }

Christian Müller's avatar
Christian Müller committed
119 120
//        val easyinv = modelinv.simplify
        val easyinv = steeredInfinv.simplify
Christian Müller's avatar
src  
Christian Müller committed
121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143
        logger.info(s"inv: $easyinv")


        val itp = Z3QFree.interpolate(newmodel.stateFormula(), easyinv)
        logger.info(s"Interpolant is ${itp.get.toNegNf}")

//        logger.info(s"Model for itp is ${Z3.printModel(Z3QFree.checkSatQFree(itp.get).get)}")

        //        val (s, satisfy) = Z3QFree.checkUniversal(Neg(easyinv))
        //        logger.info(s"Model: ${Z3.printModel(satisfy.getModel)}")


      } else {
        logger.error("Invariant not valid, but also not satisfiable.")
      }
    }


  }


  def generateExample(name: String, target: Int) {
    logger.info(s"Generating $name")
144
    val spec = Examples.parseExampleWF(name)
Christian Müller's avatar
src  
Christian Müller committed
145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167

    if (spec.isEmpty) {
      logger.error(s"Not a valid spec: $name")
    }

    spec.foreach(generate(name, _, target))
  }

//  def generateAllExamples() {
//    clear()
//    // Fill results alphabetically
//    for (k <- ExampleWorkflows.examples.keys.toList.sorted) {
//      generateExample(k)
//    }
//  }

//  clear()
  //  generateExample("nonomitting/conference")
  generateExample("tests/conference_linear_small", 1)
//  generateExample("nonomitting/conference_linear", 2)
//  generateExample("tests/loopexampleNoOracle")
  //  generateAllExamples()
}