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
        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()
Christian Müller's avatar
Christian Müller committed
49
      logger.info(s"empty: ${emptyinv.pretty}")
Christian Müller's avatar
Christian Müller committed
50
51
52
53
54
55
56
57
58
59
60
61
      
//      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()
Christian Müller's avatar
Christian Müller committed
62
      logger.info(s"auxless: ${simped.pretty}")
Christian Müller's avatar
Christian Müller committed
63
64
65
66
67
68
      
      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)
      }
Christian Müller's avatar
Christian Müller committed
69
70
      logger.info(s"withB: ${withB.simplify().pretty}")
      logger.info(s"withB CNF: ${withB.toCNF.simplify().pretty}")
Christian Müller's avatar
Christian Müller committed
71
72
73
        
      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
      (result, dot)
    }
    val msg = s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n"

Christian Müller's avatar
Christian Müller committed
78
    write(name, s"${name}.inv", msg)
Christian Müller's avatar
Christian Müller committed
79
    for ((s, i) <- dot.zipWithIndex) {
Christian Müller's avatar
Christian Müller committed
80
      write(name, s"${name}_${i}.dot", s)
Christian Müller's avatar
Christian Müller committed
81
82
83
    }
  }
  
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()
}