InvariantInspector.scala 1.77 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
2
3
4
5
6
package de.tum.workflows

import foltl.FOLTL._
import blocks.Workflow._
import Implicits._
import com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
7
import de.tum.workflows.foltl.FOTransformers
Christian Müller's avatar
Christian Müller committed
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
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
import de.tum.workflows.toz3.InvariantGenerator
import de.tum.workflows.toz3.InvProperties

object InvariantInspector extends App with LazyLogging {

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

    if (!optspec.isDefined) {
      logger.error(s"Not a valid spec: $name")
    }
    val spec = optspec.get
    logger.info(s"Encoding Spec:\n$spec")

    def invariant =
Christian Müller's avatar
Christian Müller committed
33
      InvariantGenerator.invariantNoninterSingleBS _
Christian Müller's avatar
Christian Müller committed
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
    // InvariantGenerator.invariantNoninterStubbornBS _
    // InvariantChecker.invariantNoninterStubborn _
    // InvariantChecker.invariantAllEqual _

    val (t, (res, dot)) = time {
      //        InvariantChecker.checkInvariantOnce(spec.w, inv(spec), true)
      val (result, graph, afterlabels, proven, dot, time) = 
        InvariantChecker.checkInvariantFPLabelling(spec, invariant(spec), InvProperties.DEFAULT)
      println(graph)  
      println(afterlabels.last)
      (result, dot)
    }
    val msg = s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n"

    write(s"${name}.inv", msg)
    for ((s, i) <- dot.zipWithIndex) {
      write(s"${name}_${i}.dot", s)
    }
  }
  
Christian Müller's avatar
Christian Müller committed
54
55
//  inspect("omitting/conference")
      inspect("tests/loopexampleNoOracle")
Christian Müller's avatar
Christian Müller committed
56
57
  //  generateAllExamples()
}