InvariantInspector.scala 2.98 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
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
Christian Müller's avatar
Christian Müller committed
19
import de.tum.workflows.toz3.Z3QFree
Christian Müller's avatar
Christian Müller committed
20
21
22
23
24
25
26
27
28
29
30
31
32
33

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
34
      InvariantGenerator.invariantNoninterSingleBS _
Christian Müller's avatar
Christian Müller committed
35
36
37
38
39
40
    // InvariantGenerator.invariantNoninterStubbornBS _
    // InvariantChecker.invariantNoninterStubborn _
    // InvariantChecker.invariantAllEqual _

    val (t, (res, dot)) = time {
      //        InvariantChecker.checkInvariantOnce(spec.w, inv(spec), true)
Christian Müller's avatar
Christian Müller committed
41
      val props = InvProperties(stubborn = false, eliminateAux = true)
Christian Müller's avatar
Christian Müller committed
42
      val (result, graph, afterlabels, proven, dot, time) = 
Christian Müller's avatar
Christian Müller committed
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
        InvariantChecker.checkInvariantFPLabelling(spec, invariant(spec), props)
        
      // non-omitting conference linear inspection
      val lastlabels = afterlabels.last
      val inv = lastlabels(2)
      val emptyinv = inv.assumeEmpty(List("informed", "Read", "Comm")).simplify()
      logger.info(s"empty: ${emptyinv.pretty()}")
      
//      val auxes = List("O", "choice2")
      // Different Os
      val diffos = emptyinv everywhere {
        case Fun("O", Some(t), vars) => Fun(s"O$t", vars)
      }
      val auxes = List("Ot1", "Ot2")
//      val auxes = List()
      val auxless = auxes.foldLeft(diffos)((inv, p) =>
          FOTransformers.eliminateAuxiliaryPredicate(inv, p)
          )
      val simped = auxless.toCNF.simplify()
      logger.info(s"auxless: ${simped.pretty()}")
      
      logger.info("Computing with B now")
      val withB = simped everywhere {
        case Fun("Assign",t,vars) => And(Fun("Assign",t,vars), Neg(Fun("B",vars)))
//        case Fun("Assign",t,vars) => Fun("B",vars)
      }
      logger.info(s"withB: ${withB.simplify().pretty()}")
      logger.info(s"withB CNF: ${withB.toCNF.simplify().pretty()}")
        
      logger.info(s"Graph: $graph")  
      logger.info(s"Final Invariants:\n${afterlabels.last}")
Christian Müller's avatar
Christian Müller committed
74
75
76
77
78
79
80
81
82
83
      (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
84
85
  inspect("nonomitting/conference_linear")
//      inspect("tests/loopexampleNoOracle")
Christian Müller's avatar
Christian Müller committed
86
87
  //  generateAllExamples()
}