MainInvariants.scala 1.74 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
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

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

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

25
26
27
28
    def invariant =
      InvariantChecker.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
    }
34
35
    val worked = res.isDefined
    val msg = s"Invariant was ${if (worked) "" else "not "}proven (took $t ms)\n"
Christian Müller's avatar
testing  
Christian Müller committed
36

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

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