MainInvariantsInference.scala 1.97 KB
Newer Older
1
package de.tum.niwo
Christian Müller's avatar
Christian Müller committed
2

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

Christian Müller's avatar
Christian Müller committed
14 15 16
// Labelled Edge to Block
import Implicits._

Christian Müller's avatar
Christian Müller committed
17 18
object MainInvariantsInference extends App with LazyLogging {

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

    def invariant =
Christian Müller's avatar
Christian Müller committed
23
      InvariantGenerator.invariantNoninterSingleBS _
Christian Müller's avatar
Christian Müller committed
24 25 26
    // InvariantGenerator.invariantNoninterStubbornBS _
    // InvariantChecker.invariantNoninterStubborn _
    // InvariantChecker.invariantAllEqual _
Christian Müller's avatar
Christian Müller committed
27
//      (_:Spec) => Forall(List("x","p"), Fun("Assign", List("x", "p")) --> Neg(Fun("Conf", List("x", "p")))).in(Properties.T1)
Christian Müller's avatar
Christian Müller committed
28 29

    // TODO: Add single trace properties
Christian Müller's avatar
Christian Müller committed
30

Christian Müller's avatar
src  
Christian Müller committed
31 32
    val props = InvProperties(
      stubborn = true,
Christian Müller's avatar
Christian Müller committed
33
      eliminateA = true,
Christian Müller's avatar
src  
Christian Müller committed
34 35 36
      eliminateB = true
    )

Christian Müller's avatar
Christian Müller committed
37
    val inv = invariant(spec)
Christian Müller's avatar
Christian Müller committed
38
//    val (res, graph, labels, t) = InvariantChecker.checkInvariantFPHeadLabel(spec, inv, props)
Christian Müller's avatar
withB  
Christian Müller committed
39
    val res = Utils.check(name, "elimB", inv, props)
Christian Müller's avatar
Christian Müller committed
40 41 42

  }

Christian Müller's avatar
Christian Müller committed
43

Christian Müller's avatar
Christian Müller committed
44
  def generateExample(name: String, target: Int) {
Christian Müller's avatar
Christian Müller committed
45 46 47 48 49 50 51
    logger.info(s"Generating $name")
    val spec = ExampleWorkflows.parseExample(name)

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

Christian Müller's avatar
Christian Müller committed
52
    spec.foreach(generate(name, _, target))
Christian Müller's avatar
Christian Müller committed
53 54
  }

Christian Müller's avatar
src  
Christian Müller committed
55 56 57 58 59 60 61
  //  def generateAllExamples() {
  //    clear()
  //    // Fill results alphabetically
  //    for (k <- ExampleWorkflows.examples.keys.toList.sorted) {
  //      generateExample(k)
  //    }
  //  }
Christian Müller's avatar
Christian Müller committed
62

Christian Müller's avatar
src  
Christian Müller committed
63
  //  clear()
Christian Müller's avatar
Christian Müller committed
64
  //  generateExample("nonomitting/conference")
Christian Müller's avatar
withB  
Christian Müller committed
65
  generateExample("tests/conference_linear_small_withB", 1)
Christian Müller's avatar
src  
Christian Müller committed
66 67
  //  generateExample("nonomitting/conference_linear", 2)
  //  generateExample("tests/loopexampleNoOracle")
Christian Müller's avatar
Christian Müller committed
68
  //  generateAllExamples()
Christian Müller's avatar
src  
Christian Müller committed
69
}