MainInvariantsInference.scala 2.08 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
import de.tum.niwo.Utils._
Christian Müller's avatar
Christian Müller committed
7
import de.tum.niwo.blocks.{NISpec, SimpleWFBlock}
8 9 10 11 12
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
import de.tum.niwo.invariants.{InvProperties, InvariantGenerator}
Christian Müller's avatar
Christian Müller committed
14

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

Christian Müller's avatar
Christian Müller committed
18 19
object MainInvariantsInference 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
Christian Müller committed
21 22 23
    logger.info(s"Encoding Spec:\n$spec")

    def invariant =
Christian Müller's avatar
Christian Müller committed
24
      InvariantGenerator.invariantNoninterSingleBS _
Christian Müller's avatar
Christian Müller committed
25 26 27
    // InvariantGenerator.invariantNoninterStubbornBS _
    // InvariantChecker.invariantNoninterStubborn _
    // InvariantChecker.invariantAllEqual _
Christian Müller's avatar
Christian Müller committed
28
//      (_: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
29 30

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

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

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

  }

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

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

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

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

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

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