MainInvariants.scala 1.62 KB
Newer Older
1
package de.tum.niwo
Christian Müller's avatar
Christian Müller committed
2 3 4 5 6

import foltl.FOLTL._
import blocks.Workflow._
import Implicits._
import com.typesafe.scalalogging.LazyLogging
7
import de.tum.niwo.Utils._
Christian Müller's avatar
Christian Müller committed
8 9
import java.io.PrintWriter
import java.io.File
10 11 12 13 14
import de.tum.niwo.blocks.Workflow
import de.tum.niwo.blocks.NISpec
import de.tum.niwo.foltl.FormulaFunctions
import de.tum.niwo.toz3.InvariantChecker
import de.tum.niwo.toz3.InvariantGenerator
Christian Müller's avatar
Christian Müller committed
15

16
object MainInvariants extends App with LazyLogging {
Christian Müller's avatar
Christian Müller committed
17

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

21
    def invariant =
Christian Müller's avatar
Christian Müller committed
22
      InvariantGenerator.invariantNoninterSingleBS _
Christian Müller's avatar
Christian Müller committed
23 24 25
    // InvariantGenerator.invariantNoninterStubbornBS _
    // InvariantChecker.invariantNoninterStubborn _
    // InvariantChecker.invariantAllEqual _
Christian Müller's avatar
Christian Müller committed
26

Christian Müller's avatar
Christian Müller committed
27
    val (res, dot, t) = InvariantChecker.checkInvariantFPDot(spec, invariant(spec))
Christian Müller's avatar
Christian Müller committed
28
    val msg = s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n"
Christian Müller's avatar
Christian Müller committed
29

30
    write(name, s"$name.inv", msg)
31
    for ((s, i) <- dot.zipWithIndex) {
32
      write(name, s"${name}_$i.dot", s)
33
    }
Christian Müller's avatar
Christian Müller committed
34 35 36 37 38 39
  }

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

Christian Müller's avatar
Christian Müller committed
40
    if (spec.isEmpty) {
Christian Müller's avatar
Christian Müller committed
41 42 43
      logger.error(s"Not a valid spec: $name")
    }

Christian Müller's avatar
Christian Müller committed
44
    spec.foreach(generate(name, _))
Christian Müller's avatar
Christian Müller committed
45 46 47 48 49 50 51 52 53 54 55
  }

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

  clear()
Christian Müller's avatar
Christian Müller committed
56
//  generateExample("nonomitting/conference")
Christian Müller's avatar
Christian Müller committed
57 58
  generateExample("omitting/conference")
//      generateExample("tests/loopexampleNoOracle")
Christian Müller's avatar
Christian Müller committed
59 60
  //  generateAllExamples()
}