MainInvariants.scala 1.65 KB
Newer Older
Christian Müller's avatar
testing  
Christian Müller committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
package de.tum.workflows

import foltl.FOLTL._
import blocks.Workflow._
import Implicits._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.ltl.LTL
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
import de.tum.workflows.blocks.Spec
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.toz3.InvariantChecker

object Main extends App with LazyLogging {

  def generate(name: String, spec: Spec) {
    logger.info(s"Encoding Spec:\n$spec")
    val t1 = "pi1"
    val t2 = "pi2"

    def invariants = List(
      InvariantChecker.invariantNoninterStubbornBS _ 
      //          InvariantChecker.invariantNoninterStubborn _
      //          InvariantChecker.invariantAllEqual _
      )

    def msgs = for (inv <- invariants) yield {
      val (t, (safe, msg)) = time {
        InvariantChecker.checkInvariant(spec.w, inv(spec), true)
      }
      s"Proving Invariant (took $t ms):\n$msg\n"
    }

    write(s"${name}.inv", msgs.mkString("\n"))
  }

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

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

    spec.map(generate(name, _))
  }

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

  clear()
  generateExample("nonomitting/conference")
  //    generateExample("tests/declasstest")
  //  generateAllExamples()
}