MainInvariants.scala 1.7 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
Christian Müller's avatar
Christian Müller committed
10 11

import de.tum.niwo.blocks.{InvariantSpec, NISpec, TSConverter, Workflow}
12
import de.tum.niwo.foltl.FormulaFunctions
Christian Müller's avatar
Christian Müller committed
13
import de.tum.niwo.invariants.{InvProperties, InvariantChecker, InvariantGenerator}
Christian Müller's avatar
Christian Müller committed
14

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

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

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

Christian Müller's avatar
Christian Müller committed
26 27 28 29
    val props = InvProperties.DEFAULT
    val s = TSConverter.toInvariantSpec(spec, props, invariant)

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

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

  def generateExample(name: String) {
    logger.info(s"Generating $name")
40
    val spec = Examples.parseExampleWF(name)
Christian Müller's avatar
Christian Müller committed
41

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

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

  def generateAllExamples() {
    clear()
    // Fill results alphabetically
52
    for (k <- Examples.wfexamples.keys.toList.sorted) {
Christian Müller's avatar
Christian Müller committed
53 54 55 56 57
      generateExample(k)
    }
  }

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