MainInvariants.scala 1.72 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
      InvariantGenerator.invariantNoninterStubbornBS _
26
27
    //          InvariantChecker.invariantNoninterStubborn _
    //          InvariantChecker.invariantAllEqual _
Christian Müller's avatar
testing  
Christian Müller committed
28

29
30
31
    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
32
    }
Christian Müller's avatar
Christian Müller committed
33
    val msg = s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n"
Christian Müller's avatar
testing  
Christian Müller committed
34

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

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