MainInvariants.scala 1.76 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
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
Christian Müller's avatar
Christian Müller committed
17
import de.tum.workflows.toz3.InvariantGenerator
Christian Müller's avatar
testing  
Christian Müller committed
18

19
object MainInvariants extends App with LazyLogging {
Christian Müller's avatar
testing  
Christian Müller committed
20
21
22
23

  def generate(name: String, spec: Spec) {
    logger.info(s"Encoding Spec:\n$spec")

24
    def invariant =
Christian Müller's avatar
Christian Müller committed
25
26
27
28
      InvariantGenerator.invariantNoninterStubbornSingleBS _
    // InvariantGenerator.invariantNoninterStubbornBS _
    // InvariantChecker.invariantNoninterStubborn _
    // InvariantChecker.invariantAllEqual _
Christian Müller's avatar
testing  
Christian Müller committed
29

30
31
32
    val (t, (res, dot)) = time {
      //        InvariantChecker.checkInvariantOnce(spec.w, inv(spec), true)
      InvariantChecker.checkInvariantFP(spec.w, invariant(spec), true)
Christian Müller's avatar
testing  
Christian Müller committed
33
    }
Christian Müller's avatar
Christian Müller committed
34
    val msg = s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n"
Christian Müller's avatar
testing  
Christian Müller committed
35

36
37
    write(s"${name}.inv", msg)
    write(s"${name}.dot", dot)
Christian Müller's avatar
testing  
Christian Müller committed
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
  }

  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()
}