InvariantInspector.scala 2.98 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4 5 6
package de.tum.workflows

import foltl.FOLTL._
import blocks.Workflow._
import Implicits._
import com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
7
import de.tum.workflows.foltl.FOTransformers
Christian Müller's avatar
Christian Müller committed
8 9 10 11 12 13
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
Christian Müller's avatar
Christian Müller committed
14
import de.tum.workflows.blocks.NISpec
Christian Müller's avatar
Christian Müller committed
15 16 17 18
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.toz3.InvariantGenerator
import de.tum.workflows.toz3.InvProperties
Christian Müller's avatar
Christian Müller committed
19
import de.tum.workflows.toz3.Z3QFree
Christian Müller's avatar
Christian Müller committed
20 21 22 23 24 25 26 27 28 29 30 31 32 33

object InvariantInspector extends App with LazyLogging {

  def inspect(name: String) {
    logger.info(s"Generating $name")
    val optspec = ExampleWorkflows.parseExample(name)

    if (!optspec.isDefined) {
      logger.error(s"Not a valid spec: $name")
    }
    val spec = optspec.get
    logger.info(s"Encoding Spec:\n$spec")

    def invariant =
Christian Müller's avatar
Christian Müller committed
34
      InvariantGenerator.invariantNoninterSingleBS _
Christian Müller's avatar
Christian Müller committed
35 36 37 38 39 40
    // InvariantGenerator.invariantNoninterStubbornBS _
    // InvariantChecker.invariantNoninterStubborn _
    // InvariantChecker.invariantAllEqual _

    val (t, (res, dot)) = time {
      //        InvariantChecker.checkInvariantOnce(spec.w, inv(spec), true)
Christian Müller's avatar
Christian Müller committed
41
      val props = InvProperties(stubborn = false, eliminateA = true)
Christian Müller's avatar
Christian Müller committed
42
      val (result, graph, afterlabels, proven, dot, time) = 
Christian Müller's avatar
Christian Müller committed
43 44 45 46 47
        InvariantChecker.checkInvariantFPLabelling(spec, invariant(spec), props)
        
      // non-omitting conference linear inspection
      val lastlabels = afterlabels.last
      val inv = lastlabels(2)
Christian Müller's avatar
Christian Müller committed
48
      val emptyinv = inv.assumeEmpty(List("informed", "Read", "Comm")).simplify
Christian Müller's avatar
Christian Müller committed
49
      logger.info(s"empty: ${emptyinv.pretty}")
Christian Müller's avatar
Christian Müller committed
50 51 52 53 54 55 56 57 58 59 60
      
//      val auxes = List("O", "choice2")
      // Different Os
      val diffos = emptyinv everywhere {
        case Fun("O", Some(t), vars) => Fun(s"O$t", vars)
      }
      val auxes = List("Ot1", "Ot2")
//      val auxes = List()
      val auxless = auxes.foldLeft(diffos)((inv, p) =>
          FOTransformers.eliminateAuxiliaryPredicate(inv, p)
          )
Christian Müller's avatar
Christian Müller committed
61
      val simped = auxless.toCNF.simplify
Christian Müller's avatar
Christian Müller committed
62
      logger.info(s"auxless: ${simped.pretty}")
Christian Müller's avatar
Christian Müller committed
63 64 65 66 67 68
      
      logger.info("Computing with B now")
      val withB = simped everywhere {
        case Fun("Assign",t,vars) => And(Fun("Assign",t,vars), Neg(Fun("B",vars)))
//        case Fun("Assign",t,vars) => Fun("B",vars)
      }
Christian Müller's avatar
Christian Müller committed
69 70
      logger.info(s"withB: ${withB.simplify.pretty}")
      logger.info(s"withB CNF: ${withB.toCNF.simplify.pretty}")
Christian Müller's avatar
Christian Müller committed
71 72 73
        
      logger.info(s"Graph: $graph")  
      logger.info(s"Final Invariants:\n${afterlabels.last}")
Christian Müller's avatar
Christian Müller committed
74 75 76 77
      (result, dot)
    }
    val msg = s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n"

Christian Müller's avatar
Christian Müller committed
78
    write(name, s"${name}.inv", msg)
Christian Müller's avatar
Christian Müller committed
79
    for ((s, i) <- dot.zipWithIndex) {
Christian Müller's avatar
Christian Müller committed
80
      write(name, s"${name}_${i}.dot", s)
Christian Müller's avatar
Christian Müller committed
81 82 83
    }
  }
  
Christian Müller's avatar
Christian Müller committed
84 85
  inspect("nonomitting/conference_linear")
//      inspect("tests/loopexampleNoOracle")
Christian Müller's avatar
Christian Müller committed
86 87
  //  generateAllExamples()
}